Binary encodings of finite relational structures

A finite structure is given to a machine as a bit string. Fix a vocabulary (Cslib.Logic.Vocabulary): a relational language L together with an enumeration of its relation symbols, which fixes the order of their truth tables. A finite L-structure M is encoded, along a numbering e : M ≃ Fin n of its elements, as its cardinality n followed by one truth table per relation symbol (Cslib.Logic.Vocabulary.encode): the table of a symbol of arity k lists the truth values of the relation on the n ^ k tuples of Fin n, in the order of their index Cslib.Logic.tupleIndex, the order of finFunctionFinEquiv. The cardinality is written in unary and the tables as raw bit strings, framed as a pair and a list (Cslib.Logic.encStructure), so that the input has polynomial length in the number of tuples and polynomial-time programs can read its components.

Conversely, every input (n, tables) decodes to an L-structure on Fin n (Cslib.Logic.Vocabulary.decode), a missing table entry reading as false. The input is well formed (Cslib.Logic.Vocabulary.WellFormed) when it has exactly one table of the right length per symbol; the well-formed inputs are exactly the encodings of their decoded structures (Cslib.Logic.Vocabulary.wellFormed_iff). The empty structure, n = 0, is included: its tables are empty except for those of nullary symbols, which hold a single truth value.

The query language of a class K of finite structures (Cslib.Logic.Vocabulary.queryLanguage) is the set of well-formed inputs whose decoded structure belongs to K; malformed inputs never belong to it. When K is closed under isomorphism, whether an encoding of M belongs to the query language does not depend on the numbering (Cslib.Logic.Vocabulary.mem_queryLanguage_encode). This is the convention of Immerman, Section 2.1 and Fagin, Section 3, with the order of tuples and the treatment of malformed inputs spelled out.

Main definitions

• Cslib.Logic.Vocabulary: an enumeration of the relation symbols of a language.
• Cslib.Logic.EncodedStructure, Cslib.Logic.encStructure: inputs and their binary encoding.
• Cslib.Logic.Vocabulary.decode, Cslib.Logic.Vocabulary.WellFormed, Cslib.Logic.Vocabulary.checkShape, Cslib.Logic.Vocabulary.encode: decoding, well-formedness and its check, and encoding along a numbering.
• Cslib.Logic.Vocabulary.queryLanguage: the inputs encoding the members of a class.

Main results

• Cslib.Logic.Vocabulary.encode_congr: encodings agree when a size cast preserves every relation.
• Cslib.Logic.Vocabulary.decodeEncodeEquiv: decoding an encoding of M gives a structure isomorphic to M.
• Cslib.Logic.Vocabulary.wellFormed_iff: an input is well formed exactly when it is the encoding of its decoded structure.
• Cslib.Logic.Vocabulary.mem_queryLanguage_encode: for a class closed under isomorphism, an encoding of M belongs to the query language exactly when M belongs to the class.

References

• R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets
• N. Immerman, Descriptive Complexity

Vocabularies and inputs

structure Cslib.Logic.Vocabulary (L : FirstOrder.Language) : Type v

A vocabulary: an enumeration of the relation symbols of a language, with their arities. It fixes the order of the truth tables in encoded structures.

• count : ℕ

  The number of relation symbols.

• symbol : Fin self.count ≃ (n : ℕ) × L.Relations n

  The enumeration of the relation symbols.

@[reducible, inline]

abbrev Cslib.Logic.EncodedStructure : Type

An input over finite structures: a cardinality and a list of truth tables.

@[reducible, inline]

abbrev Cslib.Logic.encStructure : EncodedStructure ↪ List Bool

The binary encoding of inputs: the cardinality in unary, then the framed list of raw truth tables.

theorem Cslib.Logic.card_le_length_encStructure (a : EncodedStructure) : a.1 ≤ (encStructure a).length

The cardinality is at most the length of the encoded input.

def Cslib.Logic.Vocabulary.index {L : FirstOrder.Language} (v : Vocabulary L) (r : (n : ℕ) × L.Relations n) : ℕ

The position of the table of a relation symbol.

theorem Cslib.Logic.Vocabulary.index_lt {L : FirstOrder.Language} (v : Vocabulary L) (r : (n : ℕ) × L.Relations n) : v.index r < v.count

def Cslib.Logic.Vocabulary.arity {L : FirstOrder.Language} (v : Vocabulary L) (i : Fin v.count) : ℕ

The arity of the relation symbol at a position.

def Cslib.Logic.Vocabulary.table {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (r : (n : ℕ) × L.Relations n) : List Bool

The truth table of a relation symbol in an input, empty if the input has none.

Decoding

@[instance_reducible]

def Cslib.Logic.Vocabulary.decode {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] (a : EncodedStructure) : L.Structure (Fin a.1)

The structure decoded from an input: a relation holds of a tuple when its table has true at the index of the tuple; a missing entry reads as false.

theorem Cslib.Logic.Vocabulary.relMap_decode {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] (a : EncodedStructure) {n : ℕ} (r : L.Relations n) (x : Fin n → Fin a.1) : FirstOrder.Language.Structure.RelMap r x ↔ (v.table a ⟨n, r⟩).getD (tupleIndex x) false = true

def Cslib.Logic.Vocabulary.decoded {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] (a : EncodedStructure) : CategoryTheory.Bundled L.Structure

The decoded structure, bundled.

def Cslib.Logic.Vocabulary.WellFormed {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) : Prop

An input is well formed when it has exactly one table per relation symbol, of length the number of tuples of the arity of the symbol.

def Cslib.Logic.Vocabulary.checkShape {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) : Bool

The program checking that an input is well formed.

theorem Cslib.Logic.Vocabulary.checkShape_eq_true_iff {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) : v.checkShape a = true ↔ v.WellFormed a

@[instance_reducible]

instance Cslib.Logic.Vocabulary.instDecidableWellFormed {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) : Decidable (v.WellFormed a)

theorem Cslib.Logic.Vocabulary.WellFormed.length_table {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (h : v.WellFormed a) (r : (n : ℕ) × L.Relations n) : (v.table a r).length = a.1 ^ r.fst

Encoding

noncomputable def Cslib.Logic.Vocabulary.relTable {L : FirstOrder.Language} (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (r : (k : ℕ) × L.Relations k) : List Bool

The truth table of a relation on a numbered finite structure: the truth values on all tuples, in the order of their index.

noncomputable def Cslib.Logic.Vocabulary.encode {L : FirstOrder.Language} (v : Vocabulary L) (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) : EncodedStructure

The encoding of a finite structure along a numbering of its elements: the cardinality and the truth tables of the relation symbols, in the order of the vocabulary.

theorem Cslib.Logic.Vocabulary.length_relTable {L : FirstOrder.Language} (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (r : (k : ℕ) × L.Relations k) : (relTable M e r).length = n ^ r.fst

theorem Cslib.Logic.Vocabulary.getD_relTable_eq_true_iff {L : FirstOrder.Language} (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) {k : ℕ} (r : L.Relations k) (x : Fin k → Fin n) : (relTable M e ⟨k, r⟩).getD (tupleIndex x) false = true ↔ FirstOrder.Language.Structure.RelMap r (⇑e.symm ∘ x)

theorem Cslib.Logic.Vocabulary.table_encode {L : FirstOrder.Language} {v : Vocabulary L} (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (r : (k : ℕ) × L.Relations k) : v.table (v.encode M e) r = relTable M e r

theorem Cslib.Logic.Vocabulary.wellFormed_encode {L : FirstOrder.Language} {v : Vocabulary L} (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) : v.WellFormed (v.encode M e)

Encodings are well formed.

theorem Cslib.Logic.Vocabulary.encode_congr {L : FirstOrder.Language} (v : Vocabulary L) {M N : Type} [L.Structure M] [L.Structure N] {m n : ℕ} (e₁ : M ≃ Fin m) (e₂ : N ≃ Fin n) (h : m = n) (hrel : ∀ {r : ℕ} (R : L.Relations r) (x : Fin r → Fin m), FirstOrder.Language.Structure.RelMap R (⇑e₁.symm ∘ x) ↔ FirstOrder.Language.Structure.RelMap R (⇑e₂.symm ∘ Fin.cast h ∘ x)) : v.encode M e₁ = v.encode N e₂

Encodings agree when the numberings have equal sizes and the size cast preserves every relation.

theorem Cslib.Logic.Vocabulary.relMap_decode_encode {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) {k : ℕ} (r : L.Relations k) (x : Fin k → Fin n) : FirstOrder.Language.Structure.RelMap r x ↔ FirstOrder.Language.Structure.RelMap r (⇑e.symm ∘ x)

The structure decoded from an encoding of M interprets a relation of the tuples numbering the elements related in M.

def Cslib.Logic.Vocabulary.decodeEncodeEquiv {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) : L.Equiv M (Fin (v.encode M e).1)

Decoding an encoding of M along e gives a structure isomorphic to M, by e.

theorem Cslib.Logic.Vocabulary.wellFormed_iff {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] (a : EncodedStructure) : v.WellFormed a ↔ v.encode (Fin a.1) (Equiv.refl (Fin a.1)) = a

An input is well formed exactly when it is the encoding of its decoded structure, numbered by itself.

Query languages

def Cslib.Logic.Vocabulary.queryLanguage {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] (K : Set (CategoryTheory.Bundled L.Structure)) : Set EncodedStructure

The query language of a class K of finite structures: the well-formed inputs whose decoded structure belongs to K. Malformed inputs never belong to it.

theorem Cslib.Logic.Vocabulary.mem_queryLanguage {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {a : EncodedStructure} : a ∈ v.queryLanguage K ↔ v.WellFormed a ∧ v.decoded a ∈ K

theorem Cslib.Logic.Vocabulary.WellFormed.mem_queryLanguage_iff {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {a : EncodedStructure} (h : v.WellFormed a) : a ∈ v.queryLanguage K ↔ v.decoded a ∈ K

theorem Cslib.Logic.Vocabulary.mem_queryLanguage_encode {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} (hK : IsoClosed K) (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) : v.encode M e ∈ v.queryLanguage K ↔ CategoryTheory.Bundled.of M ∈ K

For a class closed under isomorphism, an encoding of M belongs to the query language exactly when M belongs to the class, whatever the numbering.