Mathlib stack-machine computations within polynomial space

The simulation stores one encoded source configuration and a binary clock. Its space bound depends on the sizes of the intermediate configurations, independently of the number of rounds. All source stacks count towards space, including the initial input and final output. The terminating-computation theorem derives an exponential clock from the polynomial stack bound; it does not require a runtime certificate. The simulation gives polynomial space overhead, rather than an assertion of a linear space bound.

Main results

• Turing.TM2.run_polySpace: a polynomial-time binary clock and polynomially bounded source stacks give a polynomial-space simulation.
• Turing.TM2Computable.computableTidilyInPolySpace: transfer termination and a polynomial source-stack bound to tidy polynomial-space computation.

References

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

theorem Turing.TM2.run_polySpace (tm : FinTM2) [∀ (k : tm.K), Finite (tm.Γ k)] {α : Type} {encIn : α ↪ List Bool} {input : α → List (tm.Γ tm.k₀)} {clock space : α → ℕ} (hinput : MultiTapeTM.ComputableTidilyInPolyTime input encIn (MultiTapeTM.encList (MultiTapeTM.encFinite (tm.Γ tm.k₀)))) (hclock : MultiTapeTM.ComputableTidilyInPolyTime clock encIn MultiTapeTM.encNat) (hspace : MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) space) (hstacks : ∀ (a : α), ∀ i ≤ clock a, ∀ (k : tm.K), (((stepTotal tm.m)^[i] (initList tm (input a))).stk k).length ≤ space a) : MultiTapeTM.ComputableTidilyInPolySpace (fun (a : α) => (stepTotal tm.m)^[clock a] (initList tm (input a))) encIn encCfg

Iterate a source machine using a binary clock. The source input may be computed from a typed input; only its actual intermediate stacks need to obey the supplied space bound.

theorem Turing.TM2Computable.computableTidilyInPolySpace {α β αΓ βΓ : Type} [Finite αΓ] [Finite βΓ] {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} (h : TM2Computable ea eb f) [∀ (k : h.tm.K), Finite (h.tm.Γ k)] (ha : Function.Injective ea) (hb : Function.Injective eb) {space : α → ℕ} (hspace : MultiTapeTM.PolyBounded (fun (a : α) => (ea a).length) space) (hstacks : ∀ (a : α) (i : ℕ) (k : h.tm.K), (((TM2.stepTotal h.tm.m)^[i] (initList h.tm (List.map (⇑h.inputAlphabet.symm) (ea a)))).stk k).length ≤ space a) : MultiTapeTM.ComputableTidilyInPolySpace f ({ toFun := ea, inj' := ha }.trans (MultiTapeTM.encList (MultiTapeTM.encFinite αΓ))) ({ toFun := eb, inj' := hb }.trans (MultiTapeTM.encList (MultiTapeTM.encFinite βΓ)))

A terminating Mathlib computation with polynomially bounded source stacks is tidily computable within polynomial space. No source runtime bound or computable space bound is needed. The bound includes the input and output stacks at initialization, during execution and at halting.