Linear time and space, and encodings of pairs, options and lists

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

This file also states, as classes indexed by the encodings, what is required of encodings of pairs, options and lists: their basic operations are tidily computable in linear time and space, and pairing, which builds a value from a common input, preserves tidy computability. Theorems take these classes as instance arguments, so they hold for every encoding with the required capabilities.

Main definitions

• Turing.MultiTapeTM.encBool: the encoding b ↦ [b] of Bool. Case distinctions (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.ite) accept any encoding of Bool, so the choice matters only up to a constant.
• Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace: tidy computability in linear time and space, up to a constant.
• Turing.MultiTapeTM.PairEncoding enc₁ enc₂ enc: enc encodes pairs compatibly with enc₁ and enc₂.
• Turing.MultiTapeTM.OptionEncoding enc₁ enc: enc encodes options compatibly with enc₁, with none encoded by the empty word.
• Turing.MultiTapeTM.ListEncoding enc₁ enc: enc encodes lists compatibly with enc₁.

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.comp, .ite, .append, .pair: closure properties of linear time and space.

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

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

• Turing.MultiTapeTM.PairEncoding.pair_mono: pairing functions computable within different bounds.

def Turing.MultiTapeTM.encBool : Bool ↪ List Bool

The encoding b ↦ [b] of Bool.

@[simp]

theorem Turing.MultiTapeTM.encBool_apply (b : Bool) : encBool b = [b]

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.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableTidilyInLinearTimeAndSpace f encMid encOut) (hg : ComputableTidilyInLinearTimeAndSpace g encIn encMid) : ComputableTidilyInLinearTimeAndSpace (f ∘ g) encIn encOut

Compositions of functions tidily computable in 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.

Encodings of pairs, options and lists

class Turing.MultiTapeTM.PairEncoding {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) (enc : α × β ↪ List Bool) : Prop

enc encodes pairs compatibly with enc₁ and enc₂.

• pair {γ : Type u} {encIn : γ ↪ List Bool} {f : γ → α} {g : γ → β} {t s : γ → ℕ} : ComputableTidilyInTimeAndSpace f encIn enc₁ t s → ComputableTidilyInTimeAndSpace g encIn enc₂ t s → ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (x : γ) => (f x, g x)) encIn enc (fun (x : γ) => c * (t x + 1)) fun (x : γ) => c * (s x + (enc (f x, g x)).length + 1)

  Pairing is a combinator: functions f and g tidily computable from a common input within common bounds combine into fun x => (f x, g x), within a constant factor of those bounds, plus space for the encoded pair. Different bounds are covered by Turing.MultiTapeTM.PairEncoding.pair_mono.

• fst : ComputableTidilyInLinearTimeAndSpace Prod.fst enc enc₁

  The first projection is tidily computable in linear time and space.

• snd : ComputableTidilyInLinearTimeAndSpace Prod.snd enc enc₂

  The second projection is tidily computable in linear time and space.

class Turing.MultiTapeTM.OptionEncoding {α : Type u} (enc₁ : α ↪ List Bool) (enc : Option α ↪ List Bool) : Prop

enc encodes options compatibly with enc₁: none is encoded by the empty word.

• none_eq : enc none = []

  none is encoded by the empty word.

• some : ComputableTidilyInLinearTimeAndSpace Option.some enc₁ enc

  some is tidily computable in linear time and space.

• getD (d : α) : ComputableTidilyInLinearTimeAndSpace (fun (o : Option α) => o.getD d) enc enc₁

  Option.getD is tidily computable in linear time and space.

class Turing.MultiTapeTM.ListEncoding {α : Type u} (enc₁ : α ↪ List Bool) (enc : List α ↪ List Bool) : Prop

enc encodes lists compatibly with enc₁.

• headD (d : α) : ComputableTidilyInLinearTimeAndSpace (fun (l : List α) => l.headD d) enc enc₁

  List.headD is tidily computable in linear time and space.

• tail : ComputableTidilyInLinearTimeAndSpace List.tail enc enc

  List.tail is tidily computable in linear time and space.

• isEmpty : ComputableTidilyInLinearTimeAndSpace List.isEmpty enc encBool

  Testing a list for emptiness is tidily computable in linear time and space.

theorem Turing.MultiTapeTM.PairEncoding.pair_mono {α β : Type u} {enc₁ : α ↪ List Bool} {enc₂ : β ↪ List Bool} {enc : α × β ↪ List Bool} [h : PairEncoding enc₁ enc₂ enc] {γ : Type u} {encIn : γ ↪ List Bool} {f : γ → α} {g : γ → β} {t₁ s₁ t₂ s₂ : γ → ℕ} (hf : ComputableTidilyInTimeAndSpace f encIn enc₁ t₁ s₁) (hg : ComputableTidilyInTimeAndSpace g encIn enc₂ t₂ s₂) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (x : γ) => (f x, g x)) encIn enc (fun (x : γ) => c * (t₁ x + t₂ x + 1)) fun (x : γ) => c * (s₁ x + s₂ x + (enc (f x, g x)).length + 1)

Pairing functions tidily computable within different bounds.

theorem Turing.MultiTapeTM.ComputableTidilyInLinearTimeAndSpace.pair {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [hP : PairEncoding enc₁ enc₂ enc] {f : α → β₁} {g : α → β₂} (hf : ComputableTidilyInLinearTimeAndSpace f encIn enc₁) (hg : ComputableTidilyInLinearTimeAndSpace g encIn enc₂) : ComputableTidilyInLinearTimeAndSpace (fun (x : α) => (f x, g x)) encIn enc

Pairing functions tidily computable in linear time and space.