First-order configuration graphs

A configuration of a nondeterministic machine with k binary work tapes is a fixed tuple of registers (Turing.MultiTapeNTM.ConfigurationGraph.Register k): the input head position, the control tag, the output tag and, for each work tape, the head symbol and the ternary codes of the two stacks beside it. This file defines that graph by first-order formulas over the canonical numeric vocabulary (order, BIT, zero, one and maximum, with exact addition) on a universe Fin N: one universe element per register.

The input is read through two caller-supplied formulas: inputFormula s holds of a position exactly when the input symbol there is s (including both endmarkers), and lengthFormula holds exactly of the input length. Every formula has its exact semantics on every universe Fin N with w.length < N. A step whose successor registers would exceed the universe is not defined: no universe element denotes the successor, which is exactly the behaviour of RegisterStep restricted to tuples of Fin N.

Main definitions

• Cslib.Complexity.ConfigurationGraph.stepFormula: one step on register tuples.
• Cslib.Complexity.ConfigurationGraph.startFormula: the start registers.
• Cslib.Complexity.ConfigurationGraph.acceptFormula: halted registers with output tag 1.

Main results

• Cslib.Complexity.ConfigurationGraph.realize_stepFormula: the step formula defines RegisterStep exactly.
• Cslib.Complexity.ConfigurationGraph.realize_startFormula, Cslib.Complexity.ConfigurationGraph.realize_acceptFormula: start and acceptance.

References

• N. Immerman, Languages That Capture Complexity Classes, proof of Theorem 3.1: an instantaneous description of a logarithmic-space machine is coded by a fixed tuple of variables, and its successor relation is first-order. Here each register is one universe element and the arithmetic is the exact addition of the canonical numeric vocabulary; the formulas are original.
• M. Sipser, Introduction to the Theory of Computation, Section 8.4

noncomputable def Cslib.Complexity.ConfigurationGraph.inputMoveFormula (L : FirstOrder.Language) {α : Type u_1} (lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)) (d : SignType) (x y : (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The input head position after a move by d from x, clamped to the endmarkers 0 and n + 1, where lengthFormula holds exactly of the input length n.

noncomputable def Cslib.Complexity.ConfigurationGraph.writeFormula (L : FirstOrder.Language) {α : Type u_1} (o : Option (Option Bool)) (h h' : (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The head symbol after an optional write: unchanged by none, the written symbol's code otherwise.

noncomputable def Cslib.Complexity.ConfigurationGraph.tapeFormula (L : FirstOrder.Language) {α : Type u_1} (a : Option (Option Bool) × SignType) (h l r h' l' r' : (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The three registers of one work tape after the action a: head h, left stack l and right stack r become h', l' and r'. The written head symbol is bound to a fresh variable.

noncomputable def Cslib.Complexity.ConfigurationGraph.outputFormula (L : FirstOrder.Language) {α : Type u_1} (b : Option Bool) (o o' : (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The output tag after an optional emission (outputStep).

noncomputable def Cslib.Complexity.ConfigurationGraph.nextFormula (L : FirstOrder.Language) {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] (lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)) (a : Turing.Action k Bool State) (X Y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The registers Y are the successor registers nextRegisters of X under the action a.

noncomputable def Cslib.Complexity.ConfigurationGraph.matchFormula (L : FirstOrder.Language) {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] (inputFormula : Option Bool → (Logic.FO.Ordered.language L).Formula (Fin 1)) (t : Turing.MultiTapeNTM.ConfigurationGraph.Instruction k State) (X : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The registers X have the observations of the transition table entry t: its control state, the input symbol under the input head and the work-tape head symbols.

noncomputable def Cslib.Complexity.ConfigurationGraph.stepFormula (L : FirstOrder.Language) {α : Type u_1} {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) (X Y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

One step of the configuration graph on register tuples: either X is halted and Y = X, or X has the observations of some transition table entry and Y is its successor.

noncomputable def Cslib.Complexity.ConfigurationGraph.startFormula (L : FirstOrder.Language) {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (X : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The registers X are the start registers of ntm.

noncomputable def Cslib.Complexity.ConfigurationGraph.acceptFormula (L : FirstOrder.Language) {α : Type u_1} {k : ℕ} (State : Type) [Fintype State] (X : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) : (Logic.FO.Ordered.language L).Formula α

The registers X are halted with output tag 1.

theorem Cslib.Complexity.ConfigurationGraph.realize_inputMoveFormula {L : FirstOrder.Language} {α : Type u_1} {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] {lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)} {n : ℕ} (hlen : ∀ (a : Fin N), lengthFormula.Realize ![a] ↔ n = ↑a) (hn : n < N) (d : SignType) (x y : (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (inputMoveFormula L lengthFormula d x y).Realize v ↔ ↑(FirstOrder.Language.Term.realize v y) = Turing.MultiTapeNTM.ConfigurationGraph.inputMove n (↑(FirstOrder.Language.Term.realize v x)) d

The input-move formula has the exact semantics of inputMove, given a length formula that holds exactly of the input length n.

theorem Cslib.Complexity.ConfigurationGraph.realize_tapeFormula {L : FirstOrder.Language} {α : Type u_1} {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] (a : Option (Option Bool) × SignType) (h l r h' l' r' : (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (tapeFormula L a h l r h' l' r').Realize v ↔ Turing.MultiTapeNTM.ConfigurationGraph.tapeStep a (↑(FirstOrder.Language.Term.realize v h), ↑(FirstOrder.Language.Term.realize v l), ↑(FirstOrder.Language.Term.realize v r)) = (↑(FirstOrder.Language.Term.realize v h'), ↑(FirstOrder.Language.Term.realize v l'), ↑(FirstOrder.Language.Term.realize v r'))

The tape formula has the exact semantics of tapeStep.

theorem Cslib.Complexity.ConfigurationGraph.realize_outputFormula {L : FirstOrder.Language} {α : Type u_1} {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] (b : Option Bool) (o o' : (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (outputFormula L b o o').Realize v ↔ ↑(FirstOrder.Language.Term.realize v o') = Turing.MultiTapeNTM.ConfigurationGraph.outputStep (↑(FirstOrder.Language.Term.realize v o)) b

The output formula has the exact semantics of outputStep.

theorem Cslib.Complexity.ConfigurationGraph.realize_nextFormula {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] {lengthFormula : (Logic.FO.Ordered.language L).Formula (Fin 1)} {n : ℕ} (hlen : ∀ (a : Fin N), lengthFormula.Realize ![a] ↔ n = ↑a) (hn : n < N) (a : Turing.Action k Bool State) (X Y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (nextFormula L lengthFormula a X Y).Realize v ↔ (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(FirstOrder.Language.Term.realize v (Y i))) = Turing.MultiTapeNTM.ConfigurationGraph.nextRegisters n (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(FirstOrder.Language.Term.realize v (X i))) a

The successor formula has the exact semantics of nextRegisters.

theorem Cslib.Complexity.ConfigurationGraph.realize_matchFormula {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] {inputFormula : Option Bool → (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) (t : Turing.MultiTapeNTM.ConfigurationGraph.Instruction k State) (X : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (matchFormula L inputFormula t X).Realize v ↔ ↑(FirstOrder.Language.Term.realize v (X Turing.MultiTapeNTM.ConfigurationGraph.Register.control)) = Turing.MultiTapeNTM.ConfigurationGraph.stateCode (some t.1) ∧ Turing.inputAt w ↑(FirstOrder.Language.Term.realize v (X Turing.MultiTapeNTM.ConfigurationGraph.Register.inputPos)) = t.2.1 ∧ ∀ (i : Fin k), ↑(FirstOrder.Language.Term.realize v (X (Turing.MultiTapeNTM.ConfigurationGraph.Register.head i))) = Turing.MultiTapeNTM.ConfigurationGraph.symbolCode (t.2.2.1 i)

The matching formula has the exact semantics of a transition table lookup.

theorem Cslib.Complexity.ConfigurationGraph.realize_stepFormula {L : FirstOrder.Language} {α : Type u_1} {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) (X Y : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (stepFormula L inputFormula lengthFormula ntm X Y).Realize v ↔ Turing.MultiTapeNTM.ConfigurationGraph.RegisterStep ntm w (fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(FirstOrder.Language.Term.realize v (X i))) fun (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k) => ↑(FirstOrder.Language.Term.realize v (Y i))

The step formula defines the configuration graph on register tuples: on every universe Fin N with w.length < N, it holds exactly of RegisterStep between the values of its tuples.

theorem Cslib.Complexity.ConfigurationGraph.realize_startFormula {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] (ntm : Turing.MultiTapeNTM k Bool State) (X : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (startFormula L ntm X).Realize v ↔ ∀ (i : Turing.MultiTapeNTM.ConfigurationGraph.Register k), ↑(FirstOrder.Language.Term.realize v (X i)) = Turing.MultiTapeNTM.ConfigurationGraph.startRegisters ntm i

The start formula holds exactly of the start registers.

theorem Cslib.Complexity.ConfigurationGraph.realize_acceptFormula {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} {State : Type} [Fintype State] {N : ℕ} [Fact (2 ≤ N)] [L.Structure (Fin N)] (X : Turing.MultiTapeNTM.ConfigurationGraph.Register k → (Logic.FO.Ordered.language L).Term α) (v : α → Fin N) : (acceptFormula L State X).Realize v ↔ ↑(FirstOrder.Language.Term.realize v (X Turing.MultiTapeNTM.ConfigurationGraph.Register.control)) = Turing.MultiTapeNTM.ConfigurationGraph.stateCode none ∧ ↑(FirstOrder.Language.Term.realize v (X Turing.MultiTapeNTM.ConfigurationGraph.Register.output)) = 1

The acceptance formula holds exactly of halted registers with output tag 1.