The compact configuration graph as counter-program expressions

The local functions of the compact configuration graph (Turing.MultiTapeNTM.ConfigurationGraph) are arithmetic in the input length, the vertex identifiers and the one requested input symbol: radix digits are quotients and remainders, the tape registers are ternary stacks, and the transition table is a fixed finite list. So each of them is an expression of a counter program (Turing.CounterProgram.Expr), with Boolean values represented by 0 and 1 and the input symbol by its ternary code symbolCode. This is how a counter program computes the configuration graph of a fixed machine on its input, as the logarithmic-space reduction to directed connectivity requires Sipser, Theorem 8.25. The radix is itself an expression, such as Turing.MultiTapeNTM.ConfigurationGraph.radixExpr.

Main definitions

• Turing.MultiTapeNTM.ConfigurationGraph.vertexBoundExpr, Turing.MultiTapeNTM.ConfigurationGraph.startIDExpr, Turing.MultiTapeNTM.ConfigurationGraph.queryIndexExpr, Turing.MultiTapeNTM.ConfigurationGraph.edgeExpr, Turing.MultiTapeNTM.ConfigurationGraph.badExpr: the expressions.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.eval_vertexBoundExpr, Turing.MultiTapeNTM.ConfigurationGraph.eval_startIDExpr, Turing.MultiTapeNTM.ConfigurationGraph.eval_queryIndexExpr, Turing.MultiTapeNTM.ConfigurationGraph.eval_edgeExpr, Turing.MultiTapeNTM.ConfigurationGraph.eval_badExpr: their values.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.25

def Turing.MultiTapeNTM.ConfigurationGraph.radixExpr (D : ℕ) (n : CounterProgram.Expr) : CounterProgram.Expr

The radix (n + 2) ^ D.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_radixExpr {regs : List ℕ} {D : ℕ} {n : CounterProgram.Expr} : CounterProgram.Expr.eval regs (radixExpr D n) = radix D (CounterProgram.Expr.eval regs n)

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.vertexBoundExpr (k : ℕ) (B : CounterProgram.Expr) : CounterProgram.Expr

The number of vertices of the ambient graph.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_vertexBoundExpr {k : ℕ} {regs : List ℕ} {B : CounterProgram.Expr} : CounterProgram.Expr.eval regs (vertexBoundExpr k B) = vertexBound (CounterProgram.Expr.eval regs B)

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.readRegistersExpr {k : ℕ} (B u : CounterProgram.Expr) (i : Register k) : CounterProgram.Expr

A register of a vertex.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_readRegistersExpr {k : ℕ} {regs : List ℕ} {B u : CounterProgram.Expr} (i : Register k) : CounterProgram.Expr.eval regs (readRegistersExpr B u i) = readRegisters (CounterProgram.Expr.eval regs B) (CounterProgram.Expr.eval regs u) i

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.packExpr {k : ℕ} (B : CounterProgram.Expr) (f : Register k → CounterProgram.Expr) : CounterProgram.Expr

Pack registers in the radix B.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_packExpr {k : ℕ} {regs : List ℕ} {B : CounterProgram.Expr} {f : Register k → CounterProgram.Expr} {g : Register k → ℕ} (hf : ∀ (i : Register k), CounterProgram.Expr.eval regs (f i) = g i) : CounterProgram.Expr.eval regs (packExpr B f) = Cslib.Radix.pack (CounterProgram.Expr.eval regs B) g

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.validExpr (k : ℕ) (State : Type) [Fintype State] (B n u : CounterProgram.Expr) : CounterProgram.Expr

Syntactic validity of a vertex.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_validExpr {k : ℕ} {State : Type} [Fintype State] {regs : List ℕ} {B n u : CounterProgram.Expr} : CounterProgram.Expr.eval regs (validExpr k State B n u) = (valid (CounterProgram.Expr.eval regs B) (CounterProgram.Expr.eval regs n) (CounterProgram.Expr.eval regs u)).toNat

def Turing.MultiTapeNTM.ConfigurationGraph.inputSymbolExpr (n p sym : CounterProgram.Expr) : CounterProgram.Expr

The code of the input symbol seen at the input position p, blank at the boundaries.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_inputSymbolExpr {regs : List ℕ} {n sym p : CounterProgram.Expr} {symbol : Option Bool} (hs : CounterProgram.Expr.eval regs sym = symbolCode symbol) : CounterProgram.Expr.eval regs (inputSymbolExpr n p sym) = symbolCode (inputSymbol (CounterProgram.Expr.eval regs n) (CounterProgram.Expr.eval regs p) symbol)

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.matchesExpr {k : ℕ} {State : Type} [Fintype State] (n : CounterProgram.Expr) (r : Register k → CounterProgram.Expr) (sym : CounterProgram.Expr) (t : Instruction k State) : CounterProgram.Expr

The test that a vertex observes a fixed entry of the transition table.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_matchesExpr {k : ℕ} {State : Type} [Fintype State] {regs : List ℕ} {n sym : CounterProgram.Expr} {r : Register k → CounterProgram.Expr} {g : Register k → ℕ} {symbol : Option Bool} (hr : ∀ (i : Register k), CounterProgram.Expr.eval regs (r i) = g i) (hs : CounterProgram.Expr.eval regs sym = symbolCode symbol) (t : Instruction k State) : CounterProgram.Expr.eval regs (matchesExpr n r sym t) = (matchesEntry (CounterProgram.Expr.eval regs n) g symbol t).toNat

def Turing.MultiTapeNTM.ConfigurationGraph.tapeStepExpr (a : Option (Option Bool) × SignType) (h l r : CounterProgram.Expr) : CounterProgram.Expr × CounterProgram.Expr × CounterProgram.Expr

The registers after a tape action, as expressions in the head, left and right registers.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_tapeStepExpr {regs : List ℕ} (a : Option (Option Bool) × SignType) (h l r : CounterProgram.Expr) : (CounterProgram.Expr.eval regs (tapeStepExpr a h l r).1, CounterProgram.Expr.eval regs (tapeStepExpr a h l r).2.1, CounterProgram.Expr.eval regs (tapeStepExpr a h l r).2.2) = tapeStep a (CounterProgram.Expr.eval regs h, CounterProgram.Expr.eval regs l, CounterProgram.Expr.eval regs r)

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.nextExpr {k : ℕ} {State : Type} [Fintype State] (n : CounterProgram.Expr) (r : Register k → CounterProgram.Expr) (a : Action k Bool State) : Register k → CounterProgram.Expr

The registers after a fixed action.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_nextExpr {k : ℕ} {State : Type} [Fintype State] {regs : List ℕ} {n : CounterProgram.Expr} {r : Register k → CounterProgram.Expr} {g : Register k → ℕ} (hr : ∀ (i : Register k), CounterProgram.Expr.eval regs (r i) = g i) (a : Action k Bool State) (i : Register k) : CounterProgram.Expr.eval regs (nextExpr n r a i) = nextRegisters (CounterProgram.Expr.eval regs n) g a i

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.fitsExpr {k : ℕ} (B : CounterProgram.Expr) (r : Register k → CounterProgram.Expr) : CounterProgram.Expr

The test that all registers fit below the radix.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_fitsExpr {k : ℕ} {regs : List ℕ} {B : CounterProgram.Expr} {r : Register k → CounterProgram.Expr} {g : Register k → ℕ} (hr : ∀ (i : Register k), CounterProgram.Expr.eval regs (r i) = g i) : CounterProgram.Expr.eval regs (fitsExpr B r) = (fitsB (CounterProgram.Expr.eval regs B) g).toNat

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.edgeExpr {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B n u v sym : CounterProgram.Expr) : CounterProgram.Expr

The guarded local edge test, with the input symbol given by its code.

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_edgeExpr {k : ℕ} {State : Type} [Fintype State] {regs : List ℕ} {B n u v sym : CounterProgram.Expr} (ntm : MultiTapeNTM k Bool State) {symbol : Option Bool} (hs : CounterProgram.Expr.eval regs sym = symbolCode symbol) : CounterProgram.Expr.eval regs (edgeExpr ntm B n u v sym) = (edgeWithSymbol ntm (CounterProgram.Expr.eval regs B) (CounterProgram.Expr.eval regs n) (CounterProgram.Expr.eval regs u) (CounterProgram.Expr.eval regs v) symbol).toNat

The edge expression computes the local edge test.

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.badExpr (k : ℕ) (State : Type) [Fintype State] (B n u : CounterProgram.Expr) : CounterProgram.Expr

The test for accepting halted vertices.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_badExpr {k : ℕ} {State : Type} [Fintype State] {regs : List ℕ} {B n u : CounterProgram.Expr} : CounterProgram.Expr.eval regs (badExpr k State B n u) = (bad (CounterProgram.Expr.eval regs B) (CounterProgram.Expr.eval regs n) (CounterProgram.Expr.eval regs u)).toNat

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.startIDExpr {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : CounterProgram.Expr) : CounterProgram.Expr

The start vertex.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_startIDExpr {k : ℕ} {State : Type} [Fintype State] {regs : List ℕ} {B : CounterProgram.Expr} (ntm : MultiTapeNTM k Bool State) : CounterProgram.Expr.eval regs (startIDExpr ntm B) = startID ntm (CounterProgram.Expr.eval regs B)

noncomputable def Turing.MultiTapeNTM.ConfigurationGraph.queryIndexExpr (k : ℕ) (B u : CounterProgram.Expr) : CounterProgram.Expr

The requested input position.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.eval_queryIndexExpr {k : ℕ} {regs : List ℕ} {B u : CounterProgram.Expr} : CounterProgram.Expr.eval regs (queryIndexExpr k B u) = queryIndex (CounterProgram.Expr.eval regs B) (CounterProgram.Expr.eval regs u)