The domain-counting interpretation transducer

A first-order interpretation whose formulas are written in a language Ls is computed, on encoded finite relational structures, by one logarithmic-space transducer. The language Ls is the input vocabulary itself for order-free interpretations, or its canonical numeric expansion for ordered ones; a FormulaCompiler supplies the atomic handlers for Ls, the least admissible input cardinality, and the semantics of Ls on admissible inputs.

The transducer checks the input shape and cardinality, counts the tuples satisfying the domain formula to emit the unary output cardinality, and emits each relation table by repeatedly reconstructing the tuples of the requested ranks. Tuples are numbered through a fixed enumeration e : ι ≃ Fin d of the coordinates (tupleEquiv e); lexicographic order is the instance e = Fin.revPerm. Each loop counter is polynomially bounded in the input length; the counter-program simulation therefore supplies a total ComputableInLogSpace machine. Neither the output structure nor its tables are stored.

Inputs with invalid table shapes or a cardinality below the compiler's bound map to a fixed malformed target instance. Raw bit strings outside the image of encStructure are outside the encoded-input contract. Empty domains, nullary relations and zero-dimensional interpretations are included.

Main definitions

• Cslib.Logic.Vocabulary.ModelChecker.FormulaCompiler: atomic handlers with their semantics and admissibility bound.
• Cslib.Logic.FO.Interpretation.encodedMapWith: the encoded interpreted structure, numbered by domain rank, with inadmissible inputs sent to a malformed target encoding.

Main results

• Cslib.Logic.FO.Interpretation.computableInLogSpace_encodedMapWith: the encoded map has a total logarithmic-space transducer.

References

• N. Immerman, Descriptive Complexity, Theorem 3.1
• M. Sipser, Introduction to the Theory of Computation, Section 8.5

structure Cslib.Logic.Vocabulary.ModelChecker.FormulaCompiler {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (Ls : FirstOrder.Language) : Type (max (max (max (max 1 u) u') v) v')

A formula compiler for the domain-counting transducer, over input vocabulary v and formula language Ls: the least admissible cardinality minCard, the structure on Ls built from the decoded input on admissible cardinalities, and atomic handlers that realize it on every well-formed admissible input.

• minCard : ℕ

  The least admissible input cardinality.

• expand {n : ℕ} : self.minCard ≤ n → L.Structure (Fin n) → Ls.Structure (Fin n)

  The Ls-structure on an admissible universe, from its input relations.

• atomic {α : Type} : (α → ℕ) → ℕ → AtomicCompiler Ls α

  The atomic handlers, for free variables in registers fv and bound variables from base.

• atomic_correct {a : EncodedStructure} : v.WellFormed a → ∀ (hn : self.minCard ≤ a.1) {α : Type} (fv : α → ℕ) (base : ℕ) (val : α → Fin a.1), (self.atomic fv base).Correct (encStructure a) fv base val

  The handlers realize the expanded structure on well-formed admissible inputs.

noncomputable def Cslib.Logic.FO.Interpretation.encodedMapWith {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {Ls : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation Ls L' ι) (C : Vocabulary.ModelChecker.FormulaCompiler v Ls) (v' : Vocabulary L') (e : ι ≃ Fin d) (a : EncodedStructure) : EncodedStructure

Encode the structure interpreted by I in an admissible input, with the formula semantics of C, numbering its elements by the ranks of their tuple indices under e. Malformed inputs and cardinalities below C.minCard map to a fixed malformed structure encoding.

theorem Cslib.Logic.FO.Interpretation.encodedMapWith_of_admissible {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {Ls : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation Ls L' ι) (C : Vocabulary.ModelChecker.FormulaCompiler v Ls) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} (ha : v.WellFormed a) (hn : C.minCard ≤ a.1) : I.encodedMapWith C v' e a = v'.encode (I.Model (Fin a.1)) (I.rankEquiv e a.1)

theorem Cslib.Logic.FO.Interpretation.encodedMapWith_of_not_admissible {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {Ls : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation Ls L' ι) (C : Vocabulary.ModelChecker.FormulaCompiler v Ls) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} (ha : ¬(v.WellFormed a ∧ C.minCard ≤ a.1)) : I.encodedMapWith C v' e a = (0, List.replicate (v'.count + 1) [])

theorem Cslib.Logic.FO.Interpretation.card_encodedMapWith {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {Ls : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation Ls L' ι) (C : Vocabulary.ModelChecker.FormulaCompiler v Ls) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} (ha : v.WellFormed a) (hn : C.minCard ≤ a.1) : (I.encodedMapWith C v' e a).1 = I.modelCard e a.1

The output cardinality is the number of domain tuples.

@[simp]

theorem Cslib.Logic.FO.Interpretation.wellFormed_encodedMapWith_iff {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {Ls : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation Ls L' ι) (C : Vocabulary.ModelChecker.FormulaCompiler v Ls) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} : v'.WellFormed (I.encodedMapWith C v' e a) ↔ v.WellFormed a ∧ C.minCard ≤ a.1

Shape validity of the output is exactly admissibility of the input.

Registers and code

Frames of counted bits

The complete transducer

theorem Cslib.Logic.FO.Interpretation.computableInLogSpace_encodedMapWith {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {Ls : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation Ls L' ι) (C : Vocabulary.ModelChecker.FormulaCompiler v Ls) (v' : Vocabulary L') (e : ι ≃ Fin d) : Turing.MultiTapeTM.ComputableInLogSpace (I.encodedMapWith C v' e) encStructure encStructure

The domain-counting transducer: computing a first-order interpretation, with the formula semantics of a compiler C, on encoded finite relational structures uses logarithmic work space. The output is streamed, including its unary cardinality frame; inadmissible inputs map to a fixed malformed output.