Ordered interpretations in logarithmic space

The encoded map of a fixed ordered interpretation with a domain formula is computed by the domain-counting transducer of Cslib.Logic.FO.Interpretation.computableInLogSpace_encodedMapWith, instantiated with the ordered formula compiler: canonical numeric atoms (order, BIT, 0, 1, max) are computed from cardinality and indices, and no numeric tables are supplied. The coordinates are enumerated by Fin.revPerm, so that tuple indices are lexicographic ranks. The transducer checks the source shape and size before emitting output, then writes the unary count of the domain tuples and each target relation table over their ranks.

A full-tuple interpretation is the instance with domain ⊤, through FullTupleInterpretation.encodedMap_toDomainInterpretation; it has no separate program.

Main definitions

• Cslib.Logic.FO.Ordered.ModelChecker.formulaCompiler: the ordered formula compiler.

Main results

• Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap_eq_encodedMapWith: the encoded image is the output of the domain-counting transducer.
• Cslib.Logic.FO.Ordered.DomainInterpretation.computableInLogSpace_encodedMap: ordered interpretations with a domain formula are computed in logarithmic space.
• Cslib.Logic.FO.Ordered.IsDomainMap.exists_computableInLogSpace: domain maps are simulated by logspace maps of encodings, the hypothesis of Cslib.Complexity.ManyOneReducibleBy.lift.
• Cslib.Logic.FO.Ordered.DomainInterpretation.logSpaceReducible: admissible interpretations reducing one ordered query to another induce logspace reductions of their encodings.
• Cslib.Logic.FO.Ordered.Reduces.logSpaceReducible: first-order reductions are logspace reductions; Reduces.encodedLanguage_mem_L and Reduces.encodedLanguage_mem_P give closure of L and P.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.computableInLogSpace_encodedMap: the full-domain instance.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.logSpaceReducible_onSentence: the exact map reduces the pulled-back ordered query to the target query.

References

• N. Immerman, Descriptive Complexity, Theorem 3.1 and Propositions 3.5/3.10. Capture remains open.
• The order-free interpretation writer, shared counter-program simulation and Christian Reitwiessner's native arithmetic are reused with their source authorship retained.

def Cslib.Logic.FO.Ordered.ModelChecker.formulaCompiler {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) : Vocabulary.ModelChecker.FormulaCompiler v (language L)

The ordered formula compiler: canonical numeric atoms are computed natively, input atoms read from the input tables, and inputs of size below two are inadmissible.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap_eq_encodedMapWith {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') : I.encodedMap v v' = I.toFOInterpretation.encodedMapWith (ModelChecker.formulaCompiler v) v' Fin.revPerm

The encoded image is the output of the domain-counting transducer with the ordered formula compiler, numbering coordinates in reverse so that tuple indices are lexicographic ranks.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.computableInLogSpace_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') : Turing.MultiTapeTM.ComputableInLogSpace (I.encodedMap v v') encStructure encStructure

Ordered interpretations with a domain formula are computed in logarithmic space. For a fixed interpretation and fixed vocabularies, the encoded image, numbered by lexicographic rank of the domain tuples, is computed by a native transducer whose work space is logarithmic in the full encoded input length. The domain may have fewer than two tuples.

theorem Cslib.Logic.FO.Ordered.IsDomainMap.exists_computableInLogSpace {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (v : Vocabulary L) (v' : Vocabulary L') {f : Structure L → Structure L'} (hf : IsDomainMap f) : ∃ (F : EncodedStructure → EncodedStructure), Turing.MultiTapeTM.ComputableInLogSpace F encStructure encStructure ∧ ∀ (a : EncodedStructure), decode? v' (F a) = Option.map f (decode? v a)

Domain maps are simulated in logarithmic space. Every image map of an admissible ordered interpretation with a domain formula is simulated, through partial decoding, by a map of encodings computable in logarithmic space: its encoded map.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.logSpaceReducible {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (v : Vocabulary L) (v' : Vocabulary L') {k : ℕ} (I : DomainInterpretation L L' k) (hI : I.Admissible) {K : Query L} {K' : Query L'} (hK : ∀ (M : Structure L), M ∈ K ↔ I.map hI M ∈ K') : Complexity.LogSpaceReducible encStructure encStructure (K.encodedLanguage v) (K'.encodedLanguage v')

Ordered interpretations are logspace reductions. An admissible ordered interpretation with a domain formula whose image map reduces the query K to K' induces a logspace many-one reduction between their encoded query languages.

theorem Cslib.Logic.FO.Ordered.Reduces.logSpaceReducible {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (v : Vocabulary L) (v' : Vocabulary L') {K : Query L} {K' : Query L'} (h : Reduces K K') : Complexity.LogSpaceReducible encStructure encStructure (K.encodedLanguage v) (K'.encodedLanguage v')

First-order reductions are logspace reductions [Immerman1999, Theorem 3.1 and the remark after Definition 2.14]: a first-order reduction of the ordered query K to K' induces a logspace many-one reduction between their encoded query languages. The numeric certificate of the reduction is not used; the transducer computes ranks by counting. The closure of L and P under first-order reductions, encodedLanguage_mem_L and encodedLanguage_mem_P, are the corollaries of [Immerman1999, Proposition 3.10].

theorem Cslib.Logic.FO.Ordered.Reduces.encodedLanguage_mem_L {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (v : Vocabulary L) (v' : Vocabulary L') {K : Query L} {K' : Query L'} (h : Reduces K K') (hL : K'.encodedLanguage v' ∈ Complexity.L encStructure) : K.encodedLanguage v ∈ Complexity.L encStructure

Encoded ordered queries in L are closed under first-order reductions.

theorem Cslib.Logic.FO.Ordered.Reduces.encodedLanguage_mem_P {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (v : Vocabulary L) (v' : Vocabulary L') {K : Query L} {K' : Query L'} (h : Reduces K K') (hP : K'.encodedLanguage v' ∈ Complexity.P encStructure) : K.encodedLanguage v ∈ Complexity.P encStructure

Encoded ordered queries in P are closed under first-order reductions.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.computableInLogSpace_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') : Turing.MultiTapeTM.ComputableInLogSpace (I.encodedMap v v') encStructure encStructure

The actual canonical full-tuple encoded map is computed by a native logspace transducer. The dimension, formulas and vocabularies are fixed. Space is logarithmic in full encoded input length; the unary target size and relation tables are streamed through the write-only output. It is the domain-counting transducer for the full domain.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.mem_queryLanguage_encodedMap_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') (hk : 0 < k) (φ : (language L').Sentence) {a : EncodedStructure} : I.encodedMap v v' a ∈ queryLanguage v' φ ↔ a ∈ queryLanguage v (I.onSentence φ)

For positive tuple dimension, the encoded map belongs to the target ordered query language if and only if the source belongs to the pulled-back ordered query language.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.logSpaceReducible_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') (hk : 0 < k) (φ : (language L').Sentence) : Complexity.LogSpaceReducible encStructure encStructure (queryLanguage v (I.onSentence φ)) (queryLanguage v' φ)

For positive tuple dimension, the canonical full-tuple encoded map is a logspace many-one reduction from the pulled-back ordered query language to the target ordered query language.