Nondeterministic logarithmic space in FO(TC)

On the library's canonically ordered finite structures, every query whose source-only encoded language belongs to native NL is defined by one FO(TC) sentence whose closures all occur positively. With the forward inclusion TCDefinable.encodedLanguage_mem_NL, this gives FO(TC) = FO(positive TC) = NL.

A configuration of the logarithmic-space machine is a tuple of registers (ConfigurationGraph.stepFormula), one universe element per register. On the power universe Fin (n ^ K) with K chosen from the machine's space bound, every reachable configuration fits, so the acceptance sentence ∃ X Y, start X ∧ accept Y ∧ TC[step](X, Y) holds exactly when the machine accepts. Pullback along the canonical full-tuple interpretation gives one sentence over the original input universe.

Main definitions

• Cslib.Complexity.ConfigurationGraph.acceptanceSentence: some start register tuple reaches an accepting one by a single positive closure of stepFormula.

Main results

• Cslib.Complexity.ConfigurationGraph.realize_acceptanceSentence: the acceptance sentence holds exactly when the machine accepts, on every universe containing all reachable registers. realize_acceptanceSentence_closureBy states this for every transported closure semantics whose transform fixes the register step relation.
• Cslib.Logic.Vocabulary.exists_pow_fits: a power universe n ^ K holds every reachable configuration of a logarithmic-space machine.
• Cslib.Logic.FO.Ordered.exists_sentence_of_decidesInSpace: the sentence for a logarithmic-space decider, under every such closure semantics.
• Cslib.Logic.FO.Ordered.PosTCDefinable.of_encodedLanguage_mem_NL: NL ⊆ FO(positive TC).
• Cslib.Logic.FO.Ordered.posTCDefinable_iff_encodedLanguage_mem_NL, Cslib.Logic.FO.Ordered.tcDefinable_iff_encodedLanguage_mem_NL: FO(positive TC) and FO(TC) capture native NL.
• Cslib.Logic.FO.Ordered.tcDefinable_iff_posTCDefinable: negated closures add nothing.

References

• N. Immerman, Languages That Capture Complexity Classes, Theorem 3.1: NL is the class of queries definable in FO(positive TC) on ordered structures. Its proof codes an instantaneous description by a fixed tuple of variables and takes one closure of the first-order successor relation. Here a description is a tuple of registers on a power universe, and the numeric vocabulary is order, BIT, zero, one and maximum rather than successor, zero and maximum.
• N. Immerman, Nondeterministic Space is Closed Under Complementation, Corollary 3: FO(positive TC) = FO(TC).

noncomputable def Cslib.Complexity.ConfigurationGraph.acceptanceSentence (L : FirstOrder.Language) {k : ℕ} {State : Type} [Fintype State] (inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)) (lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)) (ntm : Turing.MultiTapeNTM k Bool State) : Logic.FO.Operator.Formula (Logic.FO.Ordered.language L) Logic.FO.TC.shape [] Empty

Acceptance by reachability: some start register tuple reaches a halted register tuple with output tag 1 along stepFormula. The sentence has one closure, of width the number of registers, at positive polarity.

@[simp]

theorem Cslib.Complexity.ConfigurationGraph.positive_acceptanceSentence {L : FirstOrder.Language} {k : ℕ} {State : Type} [Fintype State] (inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)) (lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)) (ntm : Turing.MultiTapeNTM k Bool State) : Logic.FO.TC.Positive (acceptanceSentence L inputFormula lengthFormula ntm) true

The acceptance sentence uses its closure positively.

theorem Cslib.Complexity.ConfigurationGraph.realize_acceptanceSentence_closureBy {L : FirstOrder.Language} {k : ℕ} {State : Type} [Fintype State] {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] {T : {β : Type} → (β → β → Prop) → β → β → Prop} (hT : Logic.FO.TC.Tuple.Transports fun {β : Type} => T) {inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)} {lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)} {w : List Bool} (hinput : ∀ (s : Option Bool) (a : Fin N), (inputFormula s).Realize ![a] ↔ Turing.inputAt w ↑a = s) (hlen : ∀ (a : Fin N), lengthFormula.Realize ![a] ↔ w.length = ↑a) (hn : w.length < N) (ntm : Turing.MultiTapeNTM k Bool State) (hstep : (T fun (x y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → Fin N) => Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep ntm w (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(x i)) fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(y i)) = fun (x y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → Fin N) => Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep ntm w (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(x i)) fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(y i)) (hfit : ∀ (v : Turing.FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v → Turing.MultiTapeNTM.ConfigurationGraph.Fits N (Turing.MultiTapeNTM.ConfigurationGraph.registers v)) : Logic.FO.Operator.Formula.Realize (Logic.FO.TC.Tuple.closureBy fun {β : Type} => T) (acceptanceSentence L inputFormula lengthFormula ntm) (fun {k : ℕ} => Logic.FO.Operator.RelEnv.empty) Empty.elim ↔ ntm.Accepts w

The acceptance sentence decides acceptance under every transported closure semantics TC.Tuple.closureBy T whose transform fixes the register step relation on Fin N: on a universe Fin N that contains the input length and every register of every reachable configuration, the sentence holds exactly when the machine accepts. Ordinary closure is T = id (realize_acceptanceSentence); deterministic closure is the deterministic reduct, which fixes the step relation of a deterministic machine.

theorem Cslib.Complexity.ConfigurationGraph.realize_acceptanceSentence {L : FirstOrder.Language} {k : ℕ} {State : Type} [Fintype State] {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] {inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)} {lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)} {w : List Bool} (hinput : ∀ (s : Option Bool) (a : Fin N), (inputFormula s).Realize ![a] ↔ Turing.inputAt w ↑a = s) (hlen : ∀ (a : Fin N), lengthFormula.Realize ![a] ↔ w.length = ↑a) (hn : w.length < N) (ntm : Turing.MultiTapeNTM k Bool State) (hfit : ∀ (v : Turing.FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v → Turing.MultiTapeNTM.ConfigurationGraph.Fits N (Turing.MultiTapeNTM.ConfigurationGraph.registers v)) : Logic.FO.Operator.Formula.Realize Logic.FO.TC.interpretation (acceptanceSentence L inputFormula lengthFormula ntm) (fun {k : ℕ} => Logic.FO.Operator.RelEnv.empty) Empty.elim ↔ ntm.Accepts w

The acceptance sentence decides acceptance: on a universe Fin N that contains the input length and every register of every reachable configuration, the acceptance sentence holds exactly when the machine accepts.

theorem Cslib.Logic.Vocabulary.exists_pow_fits {L : FirstOrder.Language} (v : Vocabulary L) (State : Type) [Fintype State] (c : ℕ) : ∃ (K : ℕ), 1 ≤ K ∧ (∀ (i : Fin v.count), v.arity i ≤ K) ∧ ∀ (a : EncodedStructure), v.WellFormed a → 2 ≤ a.1 → ∀ {k : ℕ} {ntm : Turing.MultiTapeNTM k Bool State}, ntm.RunsInSpace (encStructure a) (c * ((encStructure a).length.log2 + 1)) → (encStructure a).length < a.1 ^ K ∧ ∀ (u : Turing.FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView (encStructure a)) u → Turing.MultiTapeNTM.ConfigurationGraph.Fits (a.1 ^ K) (Turing.MultiTapeNTM.ConfigurationGraph.registers u)

Logarithmic-space configurations fit a power universe: for a vocabulary and a space constant there is a power K ≥ 1 bounding all relation arities such that on every well-formed input of cardinality at least two, the power universe a.1 ^ K is longer than the encoding and contains every register of every view reachable by a machine with states State that runs within space c * (log₂ n + 1).

theorem Cslib.Logic.FO.Ordered.exists_sentence_of_decidesInSpace {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {K : Query L} {T : {β : Type} → (β → β → Prop) → β → β → Prop} (hT : TC.Tuple.Transports fun {β : Type} => T) {k : ℕ} {State : Type} [Fintype State] {ntm : Turing.MultiTapeNTM k Bool State} {c : ℕ} (hdec : ntm.DecidesInSpace encStructure (K.encodedLanguage v) fun (a : EncodedStructure) => c * ((encStructure a).length.log2 + 1)) (hstep : ∀ (w : List Bool) (N : ℕ), (T fun (x y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → Fin N) => Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep ntm w (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(x i)) fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(y i)) = fun (x y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → Fin N) => Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep ntm w (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(x i)) fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(y i)) : ∃ (φ : Operator.Formula (language L) TC.shape [] Empty), TC.Positive φ true ∧ ∀ (M : Structure L), M ∈ K ↔ Operator.Formula.Realize (TC.Tuple.closureBy fun {β : Type} => T) φ (fun {k : ℕ} => Operator.RelEnv.empty) Empty.elim

A machine sentence for every logarithmic-space decider: a query whose source-only encoded language is decided by a native machine within logarithmic space is defined by one sentence with a single positive closure, read under every transported closure semantics TC.Tuple.closureBy T whose transform fixes the machine's register step relation on every Fin N. Ordinary closure gives NL ⊆ FO(positive TC); deterministic closure and a deterministic machine give L ⊆ FO(DTC).

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

NL ⊆ FO(positive TC) on canonically ordered structures: a query whose source-only encoded language is decided by a native nondeterministic logarithmic-space machine is defined by one FO(TC) sentence with a single, positive closure.

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

FO(positive TC) captures NL: a single FO(TC) sentence with positive closures defines an ordered query exactly when its source-only language is in native nondeterministic logarithmic space.

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

FO(TC) captures NL ([Imm88], Corollary 3): a single FO(TC) sentence defines an ordered query exactly when its source-only language is in native nondeterministic logarithmic space.

theorem Cslib.Logic.FO.Ordered.tcDefinable_iff_posTCDefinable {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (K : Query L) : TCDefinable K ↔ PosTCDefinable K

Negated closures add nothing on canonically ordered structures: every FO(TC) query has a sentence whose closures all occur positively.