Encoding finite structures as bit strings

To connect descriptive complexity to the machine model, a finite structure must be presented as an input to a Turing machine — a bit string. The standard encoding (for an ordered universe Fin card) lists, for each relation, its truth table: the values over all tuples in the canonical order. This module builds the relational part of that encoding and computes its length; it is step 5 (structure → bit-string encoding) of the Fagin decomposition on roadmap track L6.

Main definitions and results

• DescriptiveComplexity.encodeRel, encodeRel_length — a relation's truth table (length card ^ arity).
• DescriptiveComplexity.encodeRels, encodeRels_length — the relational part of a structure's encoding, and its total length.
• DescriptiveComplexity.allTuples, encodeRelC — a computable tuple enumeration and a computable truth-table encoding (needed for the machine-side Fagin bridge).

def Complexity.DescriptiveComplexity.allTuples (card k : ℕ) : List (Fin k → Fin card)

A computable enumeration of all k-tuples over Fin card, built by prepending each element to each shorter tuple.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.allTuples card 0 = [Fin.elim0]

theorem Complexity.DescriptiveComplexity.allTuples_length (card k : ℕ) : (allTuples card k).length = card ^ k

The enumeration has length card ^ k.

theorem Complexity.DescriptiveComplexity.mem_allTuples (card k : ℕ) (t : Fin k → Fin card) : t ∈ allTuples card k

Every tuple appears in the enumeration.

def Complexity.DescriptiveComplexity.encodeRelC {card k : ℕ} (r : (Fin k → Fin card) → Bool) : List Bool

A computable truth-table encoding of a relation, using allTuples.

Equations

• Complexity.DescriptiveComplexity.encodeRelC r = List.map r (Complexity.DescriptiveComplexity.allTuples card k)

theorem Complexity.DescriptiveComplexity.encodeRelC_length {card k : ℕ} (r : (Fin k → Fin card) → Bool) : (encodeRelC r).length = card ^ k

The computable encoding also has length card ^ k.

def Complexity.DescriptiveComplexity.encodeRelsC {V : Vocabulary} (A : DecFinStruct V) : List Bool

The computable relational encoding of a decidable structure: the computable truth tables of all its relations, concatenated.

Equations

• Complexity.DescriptiveComplexity.encodeRelsC A = List.flatMap (fun (i : Fin V.numRels) => Complexity.DescriptiveComplexity.encodeRelC (A.rel i)) (List.finRange V.numRels)

theorem Complexity.DescriptiveComplexity.encodeRelsC_length {V : Vocabulary} (A : DecFinStruct V) : (encodeRelsC A).length = (List.map (fun (i : Fin V.numRels) => A.card ^ V.relArity i) (List.finRange V.numRels)).sum

The computable relational encoding has the expected total length.

def Complexity.DescriptiveComplexity.encodeStruct {V : Vocabulary} (A : DecFinStruct V) : List Bool

The full computable encoding of a decidable structure: the cardinality in unary (a block of card trues terminated by a false), followed by the relational encoding. The unary prefix makes card self-delimiting.

Equations

• Complexity.DescriptiveComplexity.encodeStruct A = List.replicate A.card true ++ false :: Complexity.DescriptiveComplexity.encodeRelsC A

theorem Complexity.DescriptiveComplexity.encodeStruct_card {V : Vocabulary} (A : DecFinStruct V) : (List.takeWhile id (encodeStruct A)).length = A.card

The cardinality is recoverable from the encoding as the length of the leading run of trues.

noncomputable def Complexity.DescriptiveComplexity.encodeRel {card k : ℕ} (r : (Fin k → Fin card) → Bool) : List Bool

Encode a Bool-valued arity-k relation on Fin card as its truth table: the list of its values over all k-tuples, in the canonical Fintype order.

Equations

• Complexity.DescriptiveComplexity.encodeRel r = List.map r Finset.univ.toList

theorem Complexity.DescriptiveComplexity.encodeRel_length {card k : ℕ} (r : (Fin k → Fin card) → Bool) : (encodeRel r).length = card ^ k

The truth-table encoding of an arity-k relation has length card ^ k.

noncomputable def Complexity.DescriptiveComplexity.encodeRels {V : Vocabulary} (A : DecFinStruct V) : List Bool

The relational part of a decidable structure's encoding: the truth tables of all its relations, concatenated.

Equations

• Complexity.DescriptiveComplexity.encodeRels A = List.flatMap (fun (i : Fin V.numRels) => Complexity.DescriptiveComplexity.encodeRel (A.rel i)) (List.finRange V.numRels)

theorem Complexity.DescriptiveComplexity.encodeRels_length {V : Vocabulary} (A : DecFinStruct V) : (encodeRels A).length = (List.map (fun (i : Fin V.numRels) => A.card ^ V.relArity i) (List.finRange V.numRels)).sum

The relational encoding's length is the sum of the per-relation truth-table sizes card ^ (arity).