Halting and every-prefix storage of the complement query machine

Fix a round J₀ whose radix is closed on the input, as a space bound of the source provides. The radix moves to the next round only after a certified overflow, so every reachable state is in a round at most J₀ (Turing.InductiveCounting.round_le). Each round's controller halts within the instruction budget of round J₀, so every branch halts within a common clock (Turing.InductiveCounting.queryMachine_haltsWithin). Every controller register is below a power of two linear in J₀ and the binary length of the input, so every prefix, including rejecting and dishonest ones, has short encoded state (Turing.InductiveCounting.length_run_le).

Main definitions

• Turing.InductiveCounting.roundBudget: the instruction budget of round J₀.
• Turing.InductiveCounting.abstractTime: a clock for every branch.
• Turing.InductiveCounting.storageBound: a bound on every encoded state.

Main results

• Turing.InductiveCounting.queryMachine_haltsWithin: every branch halts within the clock.
• Turing.InductiveCounting.length_run_le: storage on every choice prefix.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6

theorem Turing.InductiveCounting.vertexBound_mono {k B B' : ℕ} (h : B ≤ B') : MultiTapeNTM.ConfigurationGraph.vertexBound B ≤ MultiTapeNTM.ConfigurationGraph.vertexBound B'

Larger radices have larger ambient graphs.

theorem Turing.InductiveCounting.roundRadix_mono {State : Type} [Fintype State] (n : ℕ) {j j' : ℕ} (h : j ≤ j') : roundRadix State n j ≤ roundRadix State n j'

theorem Turing.InductiveCounting.round_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {J₀ j : ℕ} (hJ₀ : Closed ntm (roundRadix State input.length J₀) input) (hj : ∀ i < j, ¬Closed ntm (roundRadix State input.length i) input) : j ≤ J₀

Rounds stop at a closed one: a state's round has only unclosed rounds before it.

noncomputable def Turing.InductiveCounting.roundBudget (k : ℕ) (State : Type) [Fintype State] (J₀ n : ℕ) : ℕ

The instruction budget of the controller on round J₀, which bounds every earlier round.

theorem Turing.InductiveCounting.rank_install_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {J₀ n j : ℕ} (hj : j ≤ J₀) : Cslib.InductiveCounting.rank (MultiTapeNTM.ConfigurationGraph.vertexBound (roundRadix State n j)) (guessWidth k (roundRadix State n j)) (install ntm (roundRadix State n j)) ≤ roundBudget k State J₀ n

theorem Turing.InductiveCounting.halted_replay_checked {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {B : ℕ} {c : Cslib.InductiveCounting.State} (choices : List Bool) (h : Cslib.InductiveCounting.rank (MultiTapeNTM.ConfigurationGraph.vertexBound B) (guessWidth k B) c ≤ choices.length) : (queryMachine ntm).halted ((queryMachine ntm).replay input choices { length := input.length, radix := B, checked := true, counting := some c }) = true

On a checked radix, every branch halts within the controller's progress measure.

noncomputable def Turing.InductiveCounting.abstractTime (k : ℕ) (State : Type) [Fintype State] (J₀ n : ℕ) : ℕ

An explicit clock for every abstract branch, including dishonest guesses, given a closed round J₀.

theorem Turing.InductiveCounting.queryMachine_haltsWithin {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {J₀ : ℕ} (hJ₀ : Closed ntm (roundRadix State input.length J₀) input) : (queryMachine ntm).HaltsWithin input (abstractTime k State J₀ input.length)

Every branch halts within the same input-dependent clock, given a closed round.

Storage

def Turing.InductiveCounting.storageBound (k : ℕ) (State : Type) [Fintype State] (J₀ n : ℕ) : ℕ

A bound on every encoded runtime state reachable on an input of length n, given a closed round J₀: linear in J₀ and the binary length of n.

theorem Turing.InductiveCounting.length_runtime_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {J₀ : ℕ} (hJ₀ : Closed ntm (roundRadix State input.length J₀) input) {s : Runtime} (h : RuntimeInvariant ntm input s) : (encRuntime s).length ≤ storageBound k State J₀ input.length

Every state allowed by the invariant has a short encoding, given a closed round.

theorem Turing.InductiveCounting.length_run_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {input : List Bool} {J₀ : ℕ} (hJ₀ : Closed ntm (roundRadix State input.length J₀) input) (choices : List Bool) : (encRuntime ((queryMachine ntm).run input choices)).length ≤ storageBound k State J₀ input.length

The encoded state bound holds on every computation prefix, including rejecting branches.