Polynomial space on plain machines

Turing.MultiTapeTM.ComputableInPolySpace, computability within polynomial space by any machine, has direct plain closure rules — identity, composition, pairing, conditionals and binary-counted iteration — proved directly via Turing.MultiTapeTM.ComputableInSpace without routing through tidy computability. The certificates and the inclusion of polynomial time (Turing.MultiTapeTM.ComputableInPolySpace.of_polyTime) are in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Basic.

The closure rules are registered with fun_prop.

Main results

• Turing.MultiTapeTM.ComputableInPolySpace.polyBounded_length: encoded outputs have polynomially bounded length.
• Turing.MultiTapeTM.ComputableInPolySpace.comp, .prod, .ite, .congr: closure properties.
• Turing.MultiTapeTM.ComputableInPolySpace.iterate: iteration within polynomial space.
• Turing.MultiTapeTM.ComputableInPolyTime.increment: the binary counter in polynomial time.

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

Encoded outputs of a polynomial-space function have polynomially bounded length.

Closure and automation

theorem Turing.MultiTapeTM.ComputableInPolySpace.id' {α : Type} {encIn : α ↪ List Bool} : ComputableInPolySpace (fun (a : α) => a) encIn encIn

The identity.

theorem Turing.MultiTapeTM.ComputableInPolySpace.comp {α β : Type} {encIn : α ↪ List Bool} {γ : Type} {encMid : β ↪ List Bool} {f : β → γ} {g : α → β} {encOut : γ ↪ List Bool} (hf : ComputableInPolySpace f encMid encOut) (hg : ComputableInPolySpace g encIn encMid) : ComputableInPolySpace (fun (a : α) => f (g a)) encIn encOut

Composition.

theorem Turing.MultiTapeTM.ComputableInPolySpace.prod {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {δ : Type} {encD : δ ↪ List Bool} {g : α → δ} (hf : ComputableInPolySpace f encIn encOut) (hg : ComputableInPolySpace g encIn encD) : ComputableInPolySpace (fun (a : α) => (f a, g a)) encIn (encPair encOut encD)

Pairing.

theorem Turing.MultiTapeTM.ComputableInPolySpace.ite {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {c : α → Bool} {g : α → β} (hc : ComputableInPolySpace c encIn encBool) (hf : ComputableInPolySpace f encIn encOut) (hg : ComputableInPolySpace g encIn encOut) : ComputableInPolySpace (fun (a : α) => if c a = true then f a else g a) encIn encOut

Case distinction.

theorem Turing.MultiTapeTM.ComputableInPolySpace.congr {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {g : α → β} (h : ComputableInPolySpace f encIn encOut) (hfg : ∀ (a : α), f a = g a) : ComputableInPolySpace g encIn encOut

Agreement with a function computable within polynomial space.

theorem Turing.MultiTapeTM.ComputableInPolySpace.iterate {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} [Inhabited β] {n : α → ℕ} {init : α → β} {step : β → β} (hn : ComputableInPolyTime n encIn encNat) (hinit : ComputableInPolySpace init encIn encOut) (hstep : ComputableInPolySpace step encOut encOut) {B : α → ℕ} (hB : PolyBounded (fun (a : α) => (encIn a).length) B) (hstate : ∀ (a : α), ∀ k ≤ n a, (encOut (step^[k] (init a))).length ≤ B a) : ComputableInPolySpace (fun (a : α) => step^[n a] (init a)) encIn encOut

Iteration within polynomial space: iterating a step computable within polynomial space a number of times computed in polynomial time in binary, from a start computable within polynomial space, is within polynomial space when all the states along the way have polynomial length.

theorem Turing.MultiTapeTM.ComputableInPolySpace.comp' {α β : Type} {encIn : α ↪ List Bool} {γ : Type} {encMid : β ↪ List Bool} {f : β → γ} {g : α → β} {encOut : γ ↪ List Bool} (hf : ComputableInPolySpace f encMid encOut) (hg : ComputableInPolySpace g encIn encMid) : ComputableInPolySpace (fun (a : α) => f (g a)) encIn encOut

Composition, in the form used by fun_prop.

theorem Turing.MultiTapeTM.ComputableInPolyTime.increment : ComputableInPolyTime Cslib.BitString.increment encBits encBits

The binary counter in polynomial time.