FO(TC) model checking in nondeterministic logarithmic space

For each fixed sentence of FO(TC) over a finite relational vocabulary expanded by the canonical numeric symbols, the encoded query language belongs to the native class NL. The input uses encStructure, as for ordered first-order model checking in L; malformed table shapes and cardinalities below two are rejected.

The decider is one nondeterministic counter program, nblockDecider around the compiled sentence at polarity true: it validates the input tables, rejects cardinalities below two, and runs the compiled code. Every branch halts with every register at most (N + 1) ^ (d + w) for input length N, maximal input arity d and closure width w, so the program runs in logarithmic space.

[Imm87], Theorem 3.1, places FO(positive TC) in NL; closures under negation add nothing because NL is closed under complementation ([Imm88], Corollary 3; [Sze87]). Here both polarities are compiled directly. A closure at polarity true is evaluated by a bounded guessed path. A closure at polarity false (under an odd number of negations, counted afresh inside each closure body) is evaluated by an inductive-counting block whose tests run the compiled body at both polarities. The converse inclusion NL ⊆ FO(positive TC), and with it FO(TC) = NL, is in Classes.LogSpace.FirstOrder.TransitiveClosure.Converse.

Main results

• Cslib.Logic.FO.Ordered.TCModelChecker.correct: compiler correctness for every formula.
• Cslib.Logic.FO.Ordered.TCModelChecker.encodedLanguage_mem_NL: a query defined by an FO(TC) sentence is in native NL.
• Cslib.Logic.FO.Ordered.TCDefinable.encodedLanguage_mem_NL: FO(TC) ⊆ NL on canonically ordered structures.
• Cslib.Logic.FO.Ordered.PosTCDefinable.encodedLanguage_mem_NL: the positive fragment.

References

• N. Immerman, Languages That Capture Complexity Classes, Theorem 3.1
• N. Immerman, Nondeterministic Space is Closed Under Complementation, Corollary 3
• R. Szelepcsényi, The Method of Forcing for Nondeterministic Automata

theorem Cslib.Logic.FO.Ordered.TCModelChecker.correct_op {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} (hE : Env v a P B Post R) {Γ : List ℕ} {α : Type} (k : ℕ) (body : (i : Fin (TC.shape k).slots) → Operator.Formula (language L) TC.shape (((TC.shape k).binder i).relations ++ Γ) (α ⊕ Fin ((TC.shape k).binder i).vars)) (args : Fin (TC.shape k).arity → (language L).Term α) (ih : Correct v a P B Post R (body ⟨0, Nat.one_pos⟩)) : Correct v a P B Post R (Operator.Formula.op k body args)

theorem Cslib.Logic.FO.Ordered.TCModelChecker.correct {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} (hE : Env v a P B Post R) {Γ : List ℕ} {α : Type} (φ : Operator.Formula (language L) TC.shape Γ α) : Correct v a P B Post R φ

Compiler correctness for every formula without free relation variables.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.encodedLanguage_mem_NL {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {φ : Operator.Formula (language L) TC.shape [] Empty} {K : Query L} (hφ : ∀ (M : Structure L), M ∈ K ↔ Operator.Formula.Realize TC.interpretation φ (fun {k : ℕ} => Operator.RelEnv.empty) Empty.elim) : K.encodedLanguage v ∈ Complexity.NL encStructure

A query defined by an FO(TC) sentence is in native NL: its source-only encoded language is decided by one nondeterministic machine, nblockDecider around the compiled sentence at polarity true, in logarithmic space.

theorem Cslib.Logic.FO.Ordered.TCDefinable.encodedLanguage_mem_NL {L : FirstOrder.Language} [L.IsRelational] {K : Query L} (hK : TCDefinable K) (v : Vocabulary L) : K.encodedLanguage v ∈ Complexity.NL encStructure

FO(TC) ⊆ NL on canonically ordered structures: a query defined by one FO(TC) sentence is in native nondeterministic logarithmic space, at the source-only structure encoding.

theorem Cslib.Logic.FO.Ordered.PosTCDefinable.encodedLanguage_mem_NL {L : FirstOrder.Language} [L.IsRelational] {K : Query L} (hK : PosTCDefinable K) (v : Vocabulary L) : K.encodedLanguage v ∈ Complexity.NL encStructure

FO(positive TC) ⊆ NL on canonically ordered structures: the positive fragment, as a special case of TCDefinable.encodedLanguage_mem_NL.