Halting within the number of reachable views

A nondeterministic machine whose computation paths all halt, and whose computation prefixes all stay within space s, halts within as many steps as it has reachable views: at most 2 ^ (2 * coreLengthBound k State n s + 1) on an input of length n (Turing.MultiTapeNTM.runsInTime_of_runsInSpace). Under a logarithmic space bound this is polynomial in n: halting within Turing.polyClock d n = 2 * (2 * (n + 1)) ^ d steps for an exponent d depending only on the machine and the space constant (Turing.MultiTapeNTM.exists_runsInTime_polynomial_of_runsInSpace_log). So for logarithmic-space machines "every branch halts" already gives a polynomial clock.

The argument is the classical one Sipser, Section 8.4: the views along a computation path form a walk of views (Turing.MultiTapeNTM.ViewRep.step); a running path longer than the number of reachable views repeats a running view, and repeating the cycle gives running walks of every length, which lift back to computation paths of the same length (Turing.MultiTapeNTM.ViewRep), contradicting that every path halts.

Main results

• Turing.MultiTapeNTM.runsInTime_of_runsInSpace: halting on every path within some time implies halting within the number of reachable views.
• Turing.MultiTapeNTM.exists_runsInTime_polynomial_of_runsInSpace_log: under a logarithmic space bound, halting on every path implies halting within a polynomial time bound.

References

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

theorem Turing.MultiTapeNTM.exists_viewChain {k : ℕ} {State : Type} {ntm : MultiTapeNTM k Bool State} {input : List Bool} (p : ntm.RunPath input) (hp : RelSeries.head p = ntm.initCfg input) : ∃ (views : List (FiniteCfg k Bool State)) (x : views.length = p.length + 1), List.IsChain ntm.ViewStep views ∧ views.head? = some (ntm.initView input) ∧ ∀ (i : ℕ) (hi : i < views.length), ViewRep views[i] (p.toFun ⟨i, ⋯⟩)

Views along a computation path. A computation path has a chain of views from the initial view, one view per configuration, each representing its configuration.

theorem Turing.MultiTapeNTM.exists_computationPath_of_relatesInSteps {k : ℕ} {State : Type} {ntm : MultiTapeNTM k Bool State} {input : List Bool} {n : ℕ} {finite : FiniteCfg k Bool State} (h : Relation.RelatesInSteps ntm.ViewStep (ntm.initView input) finite n) : ∃ (p : ntm.ComputationPath input), p.time = n ∧ ViewRep finite p.last

Counted view walks lift to computation paths of the same length.

theorem Turing.MultiTapeNTM.runsInTime_of_runsInSpace {k : ℕ} {State : Type} {ntm : MultiTapeNTM k Bool State} {input : List Bool} [Finite State] {s t : ℕ} (hs : ntm.RunsInSpace input s) (ht : ntm.RunsInTime input t) : ntm.RunsInTime input (2 ^ (2 * coreLengthBound k State input.length s + 1))

Halting within the number of reachable views. If every computation path stays within space s and every computation path halts within some time t, then every computation path halts within 2 ^ (2 * coreLengthBound k State n s + 1) steps, the bound on the number of reachable views.

theorem Turing.MultiTapeNTM.exists_runsInTime_polynomial_of_runsInSpace_log {k : ℕ} {State : Type} [Finite State] (ntm : MultiTapeNTM k Bool State) (c : ℕ) : ∃ (d : ℕ), ∀ {input : List Bool} {t : ℕ}, ntm.RunsInSpace input (c * (input.length.log2 + 1)) → ntm.RunsInTime input t → ntm.RunsInTime input (polyClock d input.length)

Logarithmic space gives a polynomial clock. For every space constant c there is an exponent d such that on every input of length n, if every computation path stays within space c * (log₂ n + 1) and every computation path halts within some time, then every computation path halts within polyClock d n steps.