Resource transfer from multi-tape machines to Mathlib stack machines

Polynomial time transfers from an ordinary binary multi-tape computation, without a tidy normal form or a polynomial source-space hypothesis. Polynomial space transfers independently of runtime when the output length is polynomially bounded. In particular, Boolean computations need only termination and a polynomial work-space bound.

All stack alphabets of the resulting Mathlib certificates are finite. Target stack bounds count the input and output, whereas native space counts only visited work-tape cells. The equivalences preserve the caller's binary encodings and impose no computable-inverse hypothesis on them.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.exists_tm2ComputableInPolyTime.
• Turing.MultiTapeTM.ComputableInPolySpace.exists_tm2Computable.
• Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_tm2Computable_bool.
• Turing.MultiTapeTM.computableInPolyTime_iff_tm2.
• Turing.MultiTapeTM.computableInPolySpace_iff_tm2.
• Cslib.Complexity.mem_PSPACE_iff_tm2.

References

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

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_tm2ComputableInPolyTime {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (ht : PolyBounded (fun (a : α) => (encIn a).length) t) : ∃ (h : TM2ComputableInPolyTime (⇑encIn) (⇑encOut) f), ∀ (stack : h.tm.K), Finite (h.tm.Γ stack)

Polynomial native time gives a Mathlib polynomial-time certificate with finite working alphabets. No polynomial bound on native space is needed.

theorem Turing.MultiTapeTM.ComputableInPolyTime.exists_tm2ComputableInPolyTime {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ComputableInPolyTime f encIn encOut) : ∃ (h : TM2ComputableInPolyTime (⇑encIn) (⇑encOut) f), ∀ (stack : h.tm.K), Finite (h.tm.Γ stack)

Polynomial-time computation has a finite-alphabet Mathlib certificate under the same binary encodings.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_tm2Computable {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (hs : PolyBounded (fun (a : α) => (encIn a).length) s) (hout : PolyBounded (fun (a : α) => (encIn a).length) fun (a : α) => (encOut (f a)).length) : ∃ (h : TM2Computable (⇑encIn) (⇑encOut) f), (∀ (stack : h.tm.K), Finite (h.tm.Γ stack)) ∧ ∃ (space : α → ℕ), PolyBounded (fun (a : α) => (encIn a).length) space ∧ h.StacksBounded space

Polynomial native space and explicitly polynomial output length give a terminating Mathlib certificate with polynomially bounded reachable stacks. Runtime is unrestricted.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_tm2Computable_bool {α : Type} {encIn : α ↪ List Bool} {t s : α → ℕ} {f : α → Bool} (h : ComputableInTimeAndSpace f encIn encBool t s) (hs : PolyBounded (fun (a : α) => (encIn a).length) s) : ∃ (h : TM2Computable (⇑encIn) (⇑encBool) f), (∀ (stack : h.tm.K), Finite (h.tm.Γ stack)) ∧ ∃ (space : α → ℕ), PolyBounded (fun (a : α) => (encIn a).length) space ∧ h.StacksBounded space

For a Boolean computation the output is one bit, so only the native work-space bound needs to be supplied. The native time bound may be arbitrary.

theorem Turing.MultiTapeTM.ComputableInPolySpace.exists_tm2Computable {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ComputableInPolySpace f encIn encOut) : ∃ (h : TM2Computable (⇑encIn) (⇑encOut) f), (∀ (stack : h.tm.K), Finite (h.tm.Γ stack)) ∧ ∃ (space : α → ℕ), PolyBounded (fun (a : α) => (encIn a).length) space ∧ h.StacksBounded space

A polynomial-space computation transfers with all target stacks polynomially bounded. The source notion explicitly bounds the encoded output length.

theorem Turing.MultiTapeTM.computableInPolyTime_iff_tm2 {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} : ComputableInPolyTime f encIn encOut ↔ ∃ (h : TM2ComputableInPolyTime (⇑encIn) (⇑encOut) f), ∀ (stack : h.tm.K), Finite (h.tm.Γ stack)

Polynomial-time computability is the same for native multi-tape machines and Mathlib stack machines with finite working alphabets, under the original binary encodings.

theorem Turing.MultiTapeTM.computableInPolySpace_iff_tm2 {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} : ComputableInPolySpace f encIn encOut ↔ ∃ (h : TM2Computable (⇑encIn) (⇑encOut) f), (∀ (stack : h.tm.K), Finite (h.tm.Γ stack)) ∧ ∃ (space : α → ℕ), PolyBounded (fun (a : α) => (encIn a).length) space ∧ h.StacksBounded space

Polynomial-space computability is equivalent to termination with polynomially bounded reachable Mathlib stacks. This equivalence also applies to functions with non-Boolean outputs: the stack bound already includes the entire output.

theorem Cslib.Complexity.mem_PSPACE_iff_tm2 {α : Type} {encIn : α ↪ List Bool} {A : Set α} : A ∈ PSPACE encIn ↔ ∃ (f : α → Bool) (h : Turing.TM2Computable (⇑encIn) (⇑Turing.MultiTapeTM.encBool) f), (∀ (stack : h.tm.K), Finite (h.tm.Γ stack)) ∧ (∃ (space : α → ℕ), Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) space ∧ h.StacksBounded space) ∧ ∀ (a : α), a ∈ A ↔ f a = true

PSPACE is exactly Boolean Mathlib stack-machine computation with finite alphabets and a polynomial bound on every reachable stack, under the original binary input encoding.