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. TM2.Reverse.Transfer supplies the converse comparison and PSPACE decision equivalence under the original binary encodings. Its target counts input and output storage, so it does not preserve sublinear native work-space bounds.

Main definitions

• Turing.TM2Computable.StacksBounded: a uniform bound on all reachable stack lengths.

Main results

• Turing.TM2.run_polySpace: a polynomial-time binary clock and polynomially bounded source stacks give a polynomial-space simulation.
• Turing.TM2Computable.computableInPolySpace_encList: transfer termination and a polynomial source-stack bound to 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.ComputableInPolyTime input encIn (MultiTapeTM.encList (MultiTapeTM.encFinite (tm.Γ tm.k₀)))) (hclock : MultiTapeTM.ComputableInPolyTime 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.ComputableInPolySpace (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.

def Turing.TM2Computable.StacksBounded {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} (h : TM2Computable ea eb f) (space : α → ℕ) : Prop

Every stack of every configuration reached from the encoded input a has length at most space a. Since Turing.TM2.stepTotal fixes halted configurations, this bounds the initial, intermediate and final stacks of the computation.

theorem Turing.TM2Computable.computableInPolySpace_encList {α β αΓ βΓ : Type} [Finite αΓ] {encA : αΓ ↪ List Bool} {encB : βΓ ↪ List Bool} {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 : h.StacksBounded space) : MultiTapeTM.ComputableInPolySpace f ({ toFun := ea, inj' := ha }.trans (MultiTapeTM.encList encA)) ({ toFun := eb, inj' := hb }.trans (MultiTapeTM.encList encB))

A terminating Mathlib computation with polynomially bounded source stacks is 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.