Computational capabilities of pair, option and list encodings

The classes contain proofs of plain computational capabilities, not selected machines or clocks. Pairing retains independent time and workspace bounds and explicitly charges the output pair.

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 : γ → ℕ} : ComputableInTimeAndSpace f encIn enc₁ t s → ComputableInTimeAndSpace g encIn enc₂ t s → ∃ (c : ℕ), ComputableInTimeAndSpace (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 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 : ComputableInLinearTimeAndSpace Prod.fst enc enc₁

  The first projection is computable in linear time and space.

• snd : ComputableInLinearTimeAndSpace Prod.snd enc enc₂

  The second projection is 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 : ComputableInLinearTimeAndSpace Option.some enc₁ enc

  some is computable in linear time and space.

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

  Option.getD is 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 : α) : ComputableInLinearTimeAndSpace (fun (l : List α) => l.headD d) enc enc₁

  List.headD is computable in linear time and space.

• tail : ComputableInLinearTimeAndSpace List.tail enc enc

  List.tail is computable in linear time and space.

• isEmpty : ComputableInLinearTimeAndSpace List.isEmpty enc encBool

  Testing a list for emptiness is 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 : ComputableInTimeAndSpace f encIn enc₁ t₁ s₁) (hg : ComputableInTimeAndSpace g encIn enc₂ t₂ s₂) : ∃ (c : ℕ), ComputableInTimeAndSpace (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 computable within different bounds.