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 full encoding — the cardinality in unary, the relational truth tables, and one one-hot block per distinguished constant — and computes its length; it is step 5 (structure → bit-string encoding) of the Fagin decomposition.

Main definitions and results

• DescriptiveComplexity.encodeStruct — the full computable encoding of a decidable structure: card in unary (terminated by false), the relational truth tables, then the constant blocks.
• DescriptiveComplexity.encodeStruct_length, encodeStruct_card — its length, and recovery of the cardinality from the unary prefix.
• DescriptiveComplexity.encodeStruct_of_isRelational — for constant-free vocabularies the encoding is the unary cardinality followed by the relations.
• 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.encodeConstC, encodeConstsC, encodeConstC_injective — computable one-hot encodings of the distinguished constants; a block determines its constant.
• 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.encodeConstC {card : ℕ} (c : Fin card) : List Bool

Encode a distinguished constant as the truth table of its singleton unary relation. The resulting one-hot block has exactly card bits.

Equations

• Complexity.DescriptiveComplexity.encodeConstC c = List.map (fun (i : Fin card) => i == c) (List.finRange card)

@[simp]

theorem Complexity.DescriptiveComplexity.encodeConstC_length {card : ℕ} (c : Fin card) : (encodeConstC c).length = card

theorem Complexity.DescriptiveComplexity.encodeConstC_injective {card : ℕ} : Function.Injective encodeConstC

A one-hot constant block determines the distinguished element.

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

Encode all distinguished constants as consecutive one-hot blocks.

Equations

• Complexity.DescriptiveComplexity.encodeConstsC A = List.flatMap (fun (i : Fin V.numConsts) => Complexity.DescriptiveComplexity.encodeConstC (A.const i)) (List.finRange V.numConsts)

@[simp]

theorem Complexity.DescriptiveComplexity.encodeConstsC_length {V : Vocabulary} (A : DecFinStruct V) : (encodeConstsC A).length = V.numConsts * A.card

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 truth tables and one one-hot block per distinguished constant. The unary prefix makes card self-delimiting.

Equations

• Complexity.DescriptiveComplexity.encodeStruct A = List.replicate A.card true ++ false :: (Complexity.DescriptiveComplexity.encodeRelsC A ++ Complexity.DescriptiveComplexity.encodeConstsC 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.

theorem Complexity.DescriptiveComplexity.encodeStruct_of_isRelational {V : Vocabulary} (A : DecFinStruct V) (hV : V.IsRelational) : encodeStruct A = List.replicate A.card true ++ false :: encodeRelsC A

Constant-free vocabularies retain the prior cardinality-plus-relations wire format.

theorem Complexity.DescriptiveComplexity.encodeStruct_length {V : Vocabulary} (A : DecFinStruct V) : (encodeStruct A).length = A.card + 1 + (List.map (fun (i : Fin V.numRels) => A.card ^ V.relArity i) (List.finRange V.numRels)).sum + V.numConsts * A.card

The full encoding has one unary cardinality block, all relation tables, and one card-bit block for each constant symbol.

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).