Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax979537.StructureEncoding

Binary encodings of ordered structures and tuples

concepts/Lax979537/StructureEncoding.lean · lax-979537

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    Definition and theorem

    Encode a structure of size nn by nn 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 nn and needs no table. Append each coordinate aia_i of the query tuple as aia_i one-bits and a zero-bit.

    The fixed vocabulary and query arity determine all table boundaries. The encoding is injective and has length n+1+Rσnarity(R)+i<k(ai+1)n+1+\sum_{R\in\sigma}n^{\operatorname{arity}(R)}+\sum_{i<k}(a_i+1). In particular, the length is at least nn and polynomial in nn for a fixed vocabulary and arity, including empty vocabularies and small universes.

    Lean source view on GitHub

    1import Lax979537.OrderedStructures
    2
    3/-!
    4---
    5title: Binary encodings of ordered structures and tuples
    6type: definition and theorem
    7---
    8Encode a structure of size nn by nn one-bits and a zero-bit, followed by
    9the characteristic tables of its relations in vocabulary order. Each table
    10lists tuples in lexicographic order. The distinguished order is determined
    11by nn and needs no table. Append each coordinate aia_i of the query tuple
    12as aia_i one-bits and a zero-bit.
    13
    14The fixed vocabulary and query arity determine all table boundaries. The
    15encoding is injective and has length
    16n+1+Rσnarity(R)+i<k(ai+1)n+1+\sum_{R\in\sigma}n^{\operatorname{arity}(R)}+\sum_{i<k}(a_i+1).
    17In particular, the length is at least nn and polynomial in nn for a fixed
    18vocabulary and arity, including empty vocabularies and small universes.
    19-/
    20
    21namespace Lax979537.StructureEncoding
    22
    23open Lax979537.OrderedStructures
    24
    25/-- All tuples, with the first coordinate varying slowest. -/
    26def 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
    31def unary (n : Nat) : List Bool := List.replicate n true ++ [false]
    32
    33def 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
    39axiom encodeInjective (σ : Vocabulary) (k : Nat) :
    40 Function.Injective (@encode σ k)
    41
    42axiom 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
    47end Lax979537.StructureEncoding
    48
    Show ProofShow Proof

    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

    Loading discussion…