Lax979537.StructureEncoding
Binary encodings of ordered structures and tuples
concepts/Lax979537/StructureEncoding.lean · lax-979537
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.
1st statement encodeInjective proven
2nd statement encodeLength proven
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.
Lean source view on GitHub
| 1 | import Lax979537.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 Lax979537.StructureEncoding |
| 22 | |
| 23 | open Lax979537.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 Lax979537.StructureEncoding |
| 48 |
Builds on
From Mathlib
none
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments