Space bounds on plain machines

Turing.MultiTapeTM.ComputableInSpace tracks work space (with encoded output charged to the bound) while leaving running time existentially quantified. This file provides its direct plain combinator calculus — weakening, encoding transport, composition, pairs, concatenation, conditionals, finite lookup, binary-counted iteration and list folds — built directly from Turing.MultiTapeTM.ComputableInO without routing through tidy computability.

It also records the equivalence with Turing.MultiTapeTM.ComputableTidilyInSpace via Turing.MultiTapeTM.ComputableInSpace.tidy and Turing.MultiTapeTM.ComputableInSpace.of_tidy.

Main results

• Turing.MultiTapeTM.ComputableInSpace.of_inO, .exists_inO: conversion with ComputableInO retaining the realizing machine.
• Turing.MultiTapeTM.ComputableInSpace.comp, .prod, .append, .ite, .constZero: plain closure rules.
• Turing.MultiTapeTM.ComputableInSpace.iterate, .foldl, .foldlWith: plain space-bounded loops.

theorem Turing.MultiTapeTM.ComputableInSpace.tidy {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {S : α → ℕ} (h : ComputableInSpace f encIn encOut S) : ComputableTidilyInSpace f encIn encOut S

A function computable within space O(S) is tidily computable within it.

theorem Turing.MultiTapeTM.ComputableInSpace.of_tidy {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {S : α → ℕ} (h : ComputableTidilyInSpace f encIn encOut S) : ComputableInSpace f encIn encOut S

A function tidily computable within space O(S) is computable within it, by the same machine.

theorem Turing.MultiTapeTM.ComputableTidilyInSpace.computableInSpace {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {S : α → ℕ} (h : ComputableTidilyInSpace f encIn encOut S) : ComputableInSpace f encIn encOut S

Turing.MultiTapeTM.ComputableInSpace.of_tidy for dot notation on a tidy hypothesis.

theorem Turing.MultiTapeTM.ComputableInSpace.of_inO {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S : α → ℕ} {f : α → β} {T : α → ℕ} (h : ComputableInO f encIn encB T S) : ComputableInSpace f encIn encB S

Forget the explicit time bound of a ComputableInO certificate, retaining its machine.

theorem Turing.MultiTapeTM.ComputableInSpace.exists_inO {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S : α → ℕ} {f : α → β} (h : ComputableInSpace f encIn encB S) : ∃ (T : α → ℕ), ComputableInO f encIn encB T S

Recover an existentially quantified ComputableInO certificate from ComputableInSpace, retaining the same realizing machine.

theorem Turing.MultiTapeTM.ComputableInSpace.weaken {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S S₁ : α → ℕ} {f : α → β} (h : ComputableInSpace f encIn encB S) (hS : BigOLe S S₁) : ComputableInSpace f encIn encB S₁

theorem Turing.MultiTapeTM.ComputableInSpace.mono_le {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S S₁ : α → ℕ} {f : α → β} (h : ComputableInSpace f encIn encB S) (hS : ∀ (a : α), S a ≤ S₁ a) : ComputableInSpace f encIn encB S₁

theorem Turing.MultiTapeTM.ComputableInSpace.length_le {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S : α → ℕ} {f : α → β} (h : ComputableInSpace f encIn encB S) : BigOLe (fun (a : α) => (encB (f a)).length) S

theorem Turing.MultiTapeTM.ComputableInSpace.of_enc_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {S : α → ℕ} {f : α → β} {g : α → γ} (h : ComputableInSpace f encIn encB S) (he : ∀ (a : α), encC (g a) = encB (f a)) : ComputableInSpace g encIn encC S

theorem Turing.MultiTapeTM.ComputableInSpace.of_encIn_eq {α : Type u_1} {α' : Type u_2} {β : Type u_3} {encIn : α ↪ List Bool} {encIn' : α' ↪ List Bool} {encB : β ↪ List Bool} {S : α → ℕ} {f : α → β} (e : α' → α) (h : ComputableInSpace f encIn encB S) (he : ∀ (a : α'), encIn' a = encIn (e a)) : ComputableInSpace (fun (a : α') => f (e a)) encIn' encB fun (a : α') => S (e a)

theorem Turing.MultiTapeTM.ComputableInSpace.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {S₁ : α → ℕ} {f : α → β} {g : β → γ} {S₂ : β → ℕ} (hg : ComputableInSpace g encB encC S₂) (hf : ComputableInSpace f encIn encB S₁) : ComputableInSpace (fun (a : α) => g (f a)) encIn encC fun (a : α) => S₁ a + S₂ (f a)

theorem Turing.MultiTapeTM.ComputableInSpace.prod {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {S₁ S₂ : α → ℕ} {f : α → β} {g : α → γ} (hf : ComputableInSpace f encIn encB S₁) (hg : ComputableInSpace g encIn encC S₂) : ComputableInSpace (fun (a : α) => (f a, g a)) encIn (encPair encB encC) fun (a : α) => S₁ a + S₂ a

theorem Turing.MultiTapeTM.ComputableInSpace.append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {encD : δ ↪ List Bool} {S₁ S₂ : α → ℕ} {f₁ : α → β} {f₂ : α → γ} {g : α → δ} (h₁ : ComputableInSpace f₁ encIn encB S₁) (h₂ : ComputableInSpace f₂ encIn encC S₂) (hg : ∀ (x : α), encD (g x) = encB (f₁ x) ++ encC (f₂ x)) : ComputableInSpace g encIn encD fun (x : α) => S₁ x + S₂ x

theorem Turing.MultiTapeTM.ComputableInSpace.ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S₁ S₂ : α → ℕ} {c : α → Bool} {f g : α → β} {Sc : α → ℕ} (hc : ComputableInSpace c encIn encBool Sc) (hf : ComputableInSpace f encIn encB S₁) (hg : ComputableInSpace g encIn encB S₂) : ComputableInSpace (fun (a : α) => if c a = true then f a else g a) encIn encB fun (a : α) => Sc a + if c a = true then S₁ a else S₂ a

theorem Turing.MultiTapeTM.ComputableInSpace.constZero {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} (b : β) : ComputableInSpace (fun (x : α) => b) encIn encB fun (x : α) => 0

A fixed output is computed within constant workspace, even when its input is unbounded: the zero envelope is realized within c * (0 + 1) cells, as in ComputableInO.constZero, and weakens to any other bound by mono_le.

theorem Turing.MultiTapeTM.ComputableInSpace.const {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} (b : β) : ComputableInSpace (fun (x : α) => b) encIn encB fun (a : α) => (encIn a).length

theorem Turing.MultiTapeTM.ComputableInSpace.fst {β γ : Type} (enc₁ : β ↪ List Bool) (enc₂ : γ ↪ List Bool) : ComputableInSpace Prod.fst (encPair enc₁ enc₂) enc₁ fun (p : β × γ) => ((encPair enc₁ enc₂) p).length

theorem Turing.MultiTapeTM.ComputableInSpace.snd {β γ : Type} (enc₁ : β ↪ List Bool) (enc₂ : γ ↪ List Bool) : ComputableInSpace Prod.snd (encPair enc₁ enc₂) enc₂ fun (p : β × γ) => ((encPair enc₁ enc₂) p).length

theorem Turing.MultiTapeTM.ComputableInSpace.fst' {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {S : α → ℕ} {f : α → β × γ} (h : ComputableInSpace f encIn (encPair encB encC) S) : ComputableInSpace (fun (a : α) => (f a).1) encIn encB S

theorem Turing.MultiTapeTM.ComputableInSpace.snd' {α β γ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {S : α → ℕ} {f : α → β × γ} (h : ComputableInSpace f encIn (encPair encB encC) S) : ComputableInSpace (fun (a : α) => (f a).2) encIn encC S

theorem Turing.MultiTapeTM.ComputableInSpace.of_finite {α : Type u_1} {β : Type u_2} [Finite α] {encIn : α ↪ List Bool} {encB : β ↪ List Bool} (f : α → β) : ComputableInSpace f encIn encB fun (a : α) => (encIn a).length

theorem Turing.MultiTapeTM.ComputableInSpace.iterate {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} [Inhabited β] {n : α → ℕ} {init : α → β} {step : β → β} {Sn Si Q B : α → ℕ} {Ss : β → ℕ} (hn : ComputableInSpace n encIn encNat Sn) (hinit : ComputableInSpace init encIn encB Si) (hstep : ComputableInSpace step encB encB Ss) (hspace : ∀ (x : α), ∀ k ≤ n x, Ss (step^[k] (init x)) ≤ Q x) (hstate : ∀ (x : α), ∀ k ≤ n x, (encB (step^[k] (init x))).length ≤ B x) : ComputableInSpace (fun (x : α) => step^[n x] (init x)) encIn encB fun (x : α) => Sn x + Si x + Q x + B x + (encNat (n x)).length

Iterating a step a computed number of times, within the space of the counter, of the initial state, of a round and of the states.

theorem Turing.MultiTapeTM.ComputableInSpace.foldl {α β δ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encA : δ ↪ List Bool} {encL : List δ ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {list : α → List δ} {init : α → β} {step : β → δ → β} {Sl Si Q B : α → ℕ} {Ss : β × δ → ℕ} (hlist : ComputableInSpace list encIn encL Sl) (hinit : ComputableInSpace init encIn encB Si) (hstep : ComputableInSpace (fun (p : β × δ) => step p.1 p.2) (encPair encB encA) encB Ss) (hspace : ∀ (x : α) (i : ℕ) (hi : i < (list x).length), Ss (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ Q x) (hstate : ∀ (x : α), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableInSpace (fun (x : α) => List.foldl step (init x) (list x)) encIn encB fun (x : α) => Sl x + Si x + Q x + B x + (encL (list x)).length

Left folds, within the space of the list, of the initial state, of a round and of the states.

theorem Turing.MultiTapeTM.ComputableInSpace.foldlWith {α β δ : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {π : Type} {encP : π ↪ List Bool} {encA : δ ↪ List Bool} {encL : List δ ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : α → π} {list : α → List δ} {init : α → β} {step : π → β → δ → β} {Sp Sl Si Q B : α → ℕ} {Ss : (π × β) × δ → ℕ} (hpar : ComputableInSpace par encIn encP Sp) (hlist : ComputableInSpace list encIn encL Sl) (hinit : ComputableInSpace init encIn encB Si) (hstep : ComputableInSpace (fun (p : (π × β) × δ) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB Ss) (hspace : ∀ (x : α) (i : ℕ) (hi : i < (list x).length), Ss ((par x, List.foldl (step (par x)) (init x) (List.take i (list x))), (list x)[i]) ≤ Q x) (hstate : ∀ (x : α), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableInSpace (fun (x : α) => List.foldl (step (par x)) (init x) (list x)) encIn encB fun (x : α) => Sp x + Sl x + Si x + Q x + B x + (encP (par x)).length + (encL (list x)).length

Left folds with a parameter, within the space of the parameter, the list, the initial state, a round and the states.