Feeding the compact native graph to inductive counting

The local configuration edge test already rejects vertices beyond the ambient bound of its radix. Consequently restricting the graph to this bound changes no edge. A radix is closed on an input when no vertex reachable in its graph overflows (Turing.InductiveCounting.Closed): then every reachable view of the source fits the radix, and the counting controller's safety property for the accepting vertices is exactly nonacceptance by the source (Turing.InductiveCounting.safe_iff_not_accepts). No space bound of the source is used for this; a space bound only shows that large radices are closed (Turing.InductiveCounting.closed_of_runsInSpace).

Main definitions

• Turing.InductiveCounting.graphEdge, Turing.InductiveCounting.graphOverflow, Turing.InductiveCounting.graphAccepting: the local tests on an actual input.
• Turing.InductiveCounting.startRadix: the first radix tried.
• Turing.InductiveCounting.Closed: no reachable vertex overflows.

Main results

• Turing.InductiveCounting.closed_iff_fits: a closed radix represents every reachable view.
• Turing.InductiveCounting.safe_iff_not_accepts: native nonacceptance as graph safety.
• Turing.InductiveCounting.closed_of_runsInSpace: a space bound closes large radices.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6
• N. Immerman, Nondeterministic Space Is Closed under Complementation

noncomputable def Turing.InductiveCounting.graphEdge {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (input : List Bool) (u v : ℕ) : Bool

The Boolean edge test obtained by supplying the one actual input symbol requested by the compact graph. The operational query machine supplies this symbol without storing input.

noncomputable def Turing.InductiveCounting.graphOverflow {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (input : List Bool) (u : ℕ) : Bool

The overflow test on the actual input.

noncomputable def Turing.InductiveCounting.graphAccepting (k : ℕ) (State : Type) [Fintype State] (B : ℕ) (input : List Bool) (u : ℕ) : Bool

The accepting halted vertices; no input symbol is needed.

theorem Turing.InductiveCounting.graphEdge_bounds {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (input : List Bool) {u v : ℕ} (h : graphEdge ntm B input u v = true) : u < MultiTapeNTM.ConfigurationGraph.vertexBound B ∧ v < MultiTapeNTM.ConfigurationGraph.vertexBound B

Both endpoints of every accepted local edge are below the ambient bound.

theorem Turing.InductiveCounting.boundedGraph_eq {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (input : List Bool) : Cslib.InductiveCounting.Graph (MultiTapeNTM.ConfigurationGraph.vertexBound B) (graphEdge ntm B input) = MultiTapeNTM.ConfigurationGraph.Edge ntm B input

The controller's explicit vertex guards remove no compact configuration edge.

def Turing.InductiveCounting.startRadix (State : Type) [Fintype State] (n : ℕ) : ℕ

The first radix tried: above every input position and every finite tag.

theorem Turing.InductiveCounting.le_startRadix {State : Type} [Fintype State] (n : ℕ) : n + 2 ≤ startRadix State n

theorem Turing.InductiveCounting.card_lt_startRadix {State : Type} [Fintype State] (n : ℕ) : Fintype.card (Option State) + 3 < startRadix State n

theorem Turing.InductiveCounting.fits_init {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {input : List Bool} (hB : Fintype.card (Option State) + 1 < B) : MultiTapeNTM.ConfigurationGraph.Fits B (MultiTapeNTM.ConfigurationGraph.registers (ntm.initView input))

The initial view fits every radix above the finite tags.

theorem Turing.InductiveCounting.startID_lt {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} (hB : Fintype.card (Option State) + 1 < B) : MultiTapeNTM.ConfigurationGraph.startID ntm B < MultiTapeNTM.ConfigurationGraph.vertexBound B

The start vertex lies below the ambient bound of every radix above the finite tags.

def Turing.InductiveCounting.Closed {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (input : List Bool) : Prop

A radix is closed on an input when no vertex reachable in its graph overflows.

theorem Turing.InductiveCounting.closed_iff_fits {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {input : List Bool} (hB : Fintype.card (Option State) + 1 < B) : Closed ntm B input ↔ ∀ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView input) v → MultiTapeNTM.ConfigurationGraph.Fits B (MultiTapeNTM.ConfigurationGraph.registers v)

A closed radix represents every reachable view, and conversely.

theorem Turing.InductiveCounting.safe_iff_not_accepts {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {input : List Bool} (hB : Fintype.card (Option State) + 1 < B) (hc : Closed ntm B input) : Cslib.InductiveCounting.Safe (MultiTapeNTM.ConfigurationGraph.vertexBound B) (MultiTapeNTM.ConfigurationGraph.startID ntm B) (graphEdge ntm B input) (graphAccepting k State B input) ↔ ¬ntm.Accepts input

On a closed radix, the controller's safety property for the accepting vertices is exactly the absence of an accepting native computation path.

theorem Turing.InductiveCounting.Closed.mono {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {input : List Bool} {B' : ℕ} (hB : Fintype.card (Option State) + 1 < B) (hBB : B ≤ B') (hc : Closed ntm B input) : Closed ntm B' input

A larger radix of a closed one is closed.

theorem Turing.InductiveCounting.closed_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {input : List Bool} {S : ℕ} (hs : ntm.RunsInSpace input S) (hn : input.length + 2 ≤ B) (hB : Fintype.card (Option State) + 3 < B) (hstack : 3 ^ (4 * S + 1) ≤ B) : Closed ntm B input

A space bound closes large radices: those above the input positions, the finite tags and the stack codes of the visited cells.