Tidy computability within a space bound

ComputableTidilyInSpace f encIn encOut S says that f is tidily computable within space O(S), with values of length O(S), in some time. For space-bounded algorithms only the work space matters, and this calculus tracks it alone: composition, pairs, conditionals and loops keep the work space explicit and leave the time to be whatever it is. In loops, the time of a round is the largest over the rounds actually run.

Main definitions

• Turing.MultiTapeTM.ComputableTidilyInSpace: tidy computability within a space bound.

Main results

• Turing.MultiTapeTM.ComputableTidilyInSpace.comp, .prod, .ite: closure properties.
• Turing.MultiTapeTM.ComputableTidilyInSpace.iterate, .foldl: loops.

def Turing.MultiTapeTM.ComputableTidilyInSpace {α : Type u_1} {β : Type u_2} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (S : α → ℕ) : Prop

f is tidily computable within space O(S a) on the input a, and its encoded value has length O(S a), in some time.

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

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

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

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

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

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

theorem Turing.MultiTapeTM.ComputableTidilyInSpace.ite {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {S₁ S₂ : α → ℕ} {c : α → Bool} {f g : α → β} {Sc : α → ℕ} (hc : ComputableTidilyInSpace c encIn encBool Sc) (hf : ComputableTidilyInSpace f encIn encB S₁) (hg : ComputableTidilyInSpace g encIn encB S₂) : ComputableTidilyInSpace (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.ComputableTidilyInSpace.const {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} (b : β) : ComputableTidilyInSpace (fun (x : α) => b) encIn encB fun (a : α) => (encIn a).length

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

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

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

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

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

theorem Turing.MultiTapeTM.ComputableTidilyInSpace.iterate {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} [Inhabited β] {n : α → ℕ} {init : α → β} {step : β → β} {Sn Si Q B : α → ℕ} {Ss : β → ℕ} (hn : ComputableTidilyInSpace n encIn encNat Sn) (hinit : ComputableTidilyInSpace init encIn encB Si) (hstep : ComputableTidilyInSpace 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) : ComputableTidilyInSpace (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.ComputableTidilyInSpace.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 : ComputableTidilyInSpace list encIn encL Sl) (hinit : ComputableTidilyInSpace init encIn encB Si) (hstep : ComputableTidilyInSpace (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) : ComputableTidilyInSpace (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.