Tidy computability in linear time and space

Tidy computability (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace) is relative to encodings of values as words. Tidy computability in linear time and space is closed under case distinctions and concatenation of encoded values, and contains constant functions and the functions computed by finite-state transducers.

Main definitions

• Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace: tidy computability in linear time and space, up to a constant.

Main results

• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.of_enc_eq: reuse identical encoded outputs with the same machine and exact time and space bounds.

• Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.ite, .append: closure properties of linear time and space. Case distinctions accept any encoding of Bool.

• Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.const: constant functions.

• Turing.MultiTapeTM.Transducer.computableTidilyInLinearTimeAndSpace: functions computed by finite-state transducers.

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

f is tidily computable within a constant factor of the length of the encoded input plus one, in time and in space.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.of_enc_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : α → β} {g : α → γ} {t s : α → ℕ} (hf : ComputableTidilyInTimeAndSpace f encIn encMid t s) (h : ∀ (a : α), encOut (g a) = encMid (f a)) : ComputableTidilyInTimeAndSpace g encIn encOut t s

Reuse the same machine when the new function emits the same encoded output word. The time and space bounds are unchanged; no encoding conversion is performed.

Closure properties of linear time and space

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.restrict {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableTidilyInLinearTimeAndSpace f encIn encMid) (p : α → Prop) : ComputableTidilyInLinearTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype p).trans encIn) encMid

A function tidily computable in linear time and space on all inputs is so on the inputs satisfying p.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableTidilyInLinearTimeAndSpace c encIn encC) (hf : ComputableTidilyInLinearTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = true).trans encIn) encMid) (hg : ComputableTidilyInLinearTimeAndSpace (g ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = false).trans encIn) encMid) : ComputableTidilyInLinearTimeAndSpace (fun (x : α) => if c x = true then f x else g x) encIn encMid

Case distinctions of functions tidily computable in linear time and space, each branch on the inputs where it is taken.

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

Constant functions are tidily computable in linear time and space.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.of_eq {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = encIn a) : ComputableTidilyInLinearTimeAndSpace f encIn encMid

Functions whose encoded value is the encoded input.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {δ : Type u_4} {enc₂ : δ ↪ List Bool} {f₁ : α → β} {f₂ : α → δ} {g : α → γ} (h₁ : ComputableTidilyInLinearTimeAndSpace f₁ encIn encMid) (h₂ : ComputableTidilyInLinearTimeAndSpace f₂ encIn enc₂) (hg : ∀ (x : α), encOut (g x) = encMid (f₁ x) ++ enc₂ (f₂ x)) : ComputableTidilyInLinearTimeAndSpace g encIn encOut

A function whose encoded value is the concatenation of the encoded values of two functions tidily computable in linear time and space.

theorem Turing.MultiTapeTM.Transducer.computableTidilyInLinearTimeAndSpace {Q : Type} [Finite Q] (τ : Transducer Bool Q) {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (hf : ∀ (a : α), encOut (f a) = τ.run τ.q₀ (encIn a)) : ComputableTidilyInLinearTimeAndSpace f encIn encOut

A function computed by a transducer with finitely many states is tidily computable in linear time and space.