Polynomial-space certificates

Turing.MultiTapeTM.ComputableInPolySpace packages one machine together with a polynomially bounded space bound. This module converts between that predicate and its explicit certificates: a polynomially bounded Turing.MultiTapeTM.ComputableInSpace bound, in both directions, and plain polynomial time. It registers ComputableInPolySpace with fun_prop, with polynomial time as its first rule. The closure rules (composition, pairing, conditionals and iteration) are in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain; clients that need only these constructors import this module instead and avoid that module's build closure.

Main results

• Turing.MultiTapeTM.ComputableInPolySpace.of_inSpace, Turing.MultiTapeTM.ComputableInPolySpace.exists_inSpace: polynomial space is a polynomially bounded ComputableInSpace bound.
• Turing.MultiTapeTM.ComputableInPolySpace.of_polyTime: plain polynomial time is within polynomial space.

theorem Turing.MultiTapeTM.ComputableInPolySpace.of_inSpace {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {S : α → ℕ} (hS : PolyBounded (fun (a : α) => (encIn a).length) S) (h : ComputableInSpace f encIn encOut S) : ComputableInPolySpace f encIn encOut

Build ComputableInPolySpace from a polynomially bounded ComputableInSpace certificate, retaining the same realizing machine.

theorem Turing.MultiTapeTM.ComputableInPolySpace.exists_inSpace {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableInPolySpace f encIn encOut) : ∃ (S : α → ℕ), PolyBounded (fun (a : α) => (encIn a).length) S ∧ ComputableInSpace f encIn encOut S

Unpack ComputableInPolySpace into a polynomially bounded ComputableInSpace certificate, retaining the same realizing machine.

theorem Turing.MultiTapeTM.ComputableInPolySpace.of_polyTime {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableInPolyTime f encIn encOut) : ComputableInPolySpace f encIn encOut

Polynomial time is within polynomial space.