Binary encodings of ordered structures and tuples
Lax751879.StructureEncoding · concepts/Lax751879/StructureEncoding.lean · lax-751879
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition and theorem
Encode a structure of size by one-bits and a zero-bit, followed by the characteristic tables of its relations in vocabulary order. Each table lists tuples in lexicographic order. The distinguished order is determined by and needs no table. Append each coordinate of the query tuple as one-bits and a zero-bit.
The fixed vocabulary and query arity determine all table boundaries. The encoding is injective and has length . In particular, the length is at least and polynomial in for a fixed vocabulary and arity, including empty vocabularies and small universes.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax751879.OrderedStructures |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Binary encodings of ordered structures and tuples |
| 6 | type: definition and theorem |
| 7 | --- |
| 8 | Encode a structure of size by one-bits and a zero-bit, followed by |
| 9 | the characteristic tables of its relations in vocabulary order. Each table |
| 10 | lists tuples in lexicographic order. The distinguished order is determined |
| 11 | by and needs no table. Append each coordinate of the query tuple |
| 12 | as one-bits and a zero-bit. |
| 13 | |
| 14 | The fixed vocabulary and query arity determine all table boundaries. The |
| 15 | encoding is injective and has length |
| 16 | . |
| 17 | In particular, the length is at least and polynomial in for a fixed |
| 18 | vocabulary and arity, including empty vocabularies and small universes. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax751879.StructureEncoding |
| 22 | |
| 23 | open Lax751879.OrderedStructures |
| 24 | |
| 25 | /-- All tuples, with the first coordinate varying slowest. -/ |
| 26 | def tuples (n : Nat) : (k : Nat) → List (Fin k → Fin n) |
| 27 | | 0 => [Fin.elim0] |
| 28 | | k + 1 => (List.finRange n).flatMap fun a => |
| 29 | (tuples n k).map (Fin.cons a) |
| 30 | |
| 31 | def unary (n : Nat) : List Bool := List.replicate n true ++ [false] |
| 32 | |
| 33 | def encode {σ : Vocabulary} {k : Nat} (A : PointedStructure σ k) : List Bool := |
| 34 | unary A.structureValue.size ++ |
| 35 | (List.finRange σ.length).flatMap (fun r => |
| 36 | (tuples A.structureValue.size (σ.get r)).map (A.structureValue.relation r)) ++ |
| 37 | (List.finRange k).flatMap (fun i => unary (A.tuple i).val) |
| 38 | |
| 39 | axiom encodeInjective (σ : Vocabulary) (k : Nat) : |
| 40 | Function.Injective (@encode σ k) |
| 41 | |
| 42 | axiom encodeLength {σ : Vocabulary} {k : Nat} (A : PointedStructure σ k) : |
| 43 | (encode A).length = A.structureValue.size + 1 + |
| 44 | (σ.map (fun r => A.structureValue.size ^ r)).sum + |
| 45 | ((List.finRange k).map (fun i => (A.tuple i).val + 1)).sum |
| 46 | |
| 47 | end Lax751879.StructureEncoding |
| 48 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments