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 : ComputableInDegree Prod.fst enc enc₁ 1 1

  The first projection is computable in linear time and space.

• snd : ComputableInDegree Prod.snd enc enc₂ 1 1

  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 : ComputableInDegree Option.some enc₁ enc 1 1

  some is computable in linear time and space.

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

  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 : α) : ComputableInDegree (fun (l : List α) => l.headD d) enc enc₁ 1 1

  List.headD is computable in linear time and space.

• tail : ComputableInDegree List.tail enc enc 1 1

  List.tail is computable in linear time and space.

• isEmpty : ComputableInDegree List.isEmpty enc encBool 1 1

  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.