Exponential clocks for space-bounded Mathlib TM2 computations

A terminating deterministic computation cannot revisit a configuration before its first halted configuration. A bound on every stack bounds the complete binary configuration encoding linearly; there are fewer than exponentially many words of bounded length. Thus exponential padding suffices to reach the output of any terminating computation with the supplied stack bound.

Main results

• Turing.TM2.exists_exponential_clock: every terminating source run with bounded stacks has an exponential clock depending only on the machine and stack bound.

References

The standard configuration-counting argument for deterministic space bounds; see [AB09]. Source configurations and executions are Mathlib's Mathlib.Computability.TuringMachine.Computable.

theorem Turing.TM2.exists_exponential_clock (tm : FinTM2) [∀ (k : tm.K), Finite (tm.Γ k)] : ∃ (C : ℕ), ∀ (input : List (tm.Γ tm.k₀)) (output : List (tm.Γ tm.k₁)) (space : ℕ) (a : TM2Outputs tm input (some output)), (∀ (i : ℕ) (k : tm.K), (((stepTotal tm.m)^[i] (initList tm input)).stk k).length ≤ space) → (stepTotal tm.m)^[2 ^ (C * (space + 1) + 1)] (initList tm input) = haltList tm output

A fixed finite-alphabet TM2 has a uniform exponential clock for all terminating runs whose stacks, including the initial input and final output, satisfy the supplied bound at every step.