Tidy computability with polynomial bounds of a given degree

ComputableTidilyInDegree f encIn encOut d e: f is tidily computable within time and space O(n ^ d), and its encoded values have length O(n ^ e), where n is the length of the encoded input. The constants are existential, the degrees are explicit. The closure properties compute the degrees: composition multiplies the degree of the outer function by the output degree of the inner one, pairing and case distinctions take maxima, and a left fold adds the output degree of the list to the degree of a round.

Results are stated with the degrees the closure properties produce; mono moves to larger degrees, proving the inequalities by decide or omega. Left folds are in Cslib.Computability.Machines.Turing.MultiTape.Complexity.Fold. For sums, DegreeBounded.add_max combines different degrees directly; DegreeBounded.add keeps an already shared degree.

Main definitions

• Turing.MultiTapeTM.DegreeBounded: a function bounded by c * (size + 1) ^ d.
• Turing.MultiTapeTM.ComputableTidilyInDegree: tidy computability with bounds of given degrees.

Main results

• Turing.MultiTapeTM.ComputableTidilyInDegree.computableTidilyInPolyTime: polynomial time.
• Turing.MultiTapeTM.ComputableTidilyInDegree.comp, .ite, .append, .pair, .prod: closure properties.
• Turing.MultiTapeTM.ComputableTidilyInDegree.of_finite: functions on finite types.

Tidy computability with bounds of given degrees

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

f is tidily computable within time and space bounded by polynomials of degree d in the length of the encoded input, and its encoded values have length bounded by a polynomial of degree e.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.mono {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {d e : ℕ} {f : α → β} {d' e' : ℕ} (h : ComputableTidilyInDegree f encIn encMid d e) (hd : d ≤ d' := by first | decide | omega) (he : e ≤ e' := by first | decide | omega) : ComputableTidilyInDegree f encIn encMid d' e'

Moving to larger degrees.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.of_bounds {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {d : ℕ} {f : α → β} {t s : α → ℕ} (ht : DegreeBounded (fun (a : α) => (encIn a).length) t d) (hs : DegreeBounded (fun (a : α) => (encIn a).length) s d) (hf : ComputableTidilyInTimeAndSpace f encIn encMid t s) : ComputableTidilyInDegree f encIn encMid d d

Bounds of degree d give tidy computability of degree d, with output of degree d.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.computableTidilyInPolyTime {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {d e : ℕ} {f : α → β} (h : ComputableTidilyInDegree f encIn encMid d e) : ComputableTidilyInPolyTime f encIn encMid

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.of_linear {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableTidilyInLinearTimeAndSpace f encIn encMid) : ComputableTidilyInDegree f encIn encMid 1 1

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {d₁ e₁ d₂ e₂ : ℕ} {f : β → γ} {g : α → β} (hf : ComputableTidilyInDegree f encMid encOut d₂ e₂) (hg : ComputableTidilyInDegree g encIn encMid d₁ e₁) : ComputableTidilyInDegree (f ∘ g) encIn encOut (max d₁ (e₁ * d₂)) (e₁ * e₂)

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

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

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

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

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

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

A function whose encoded values are those of a function computable with given degrees.

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

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.prod {d₁ e₁ d₂ e₂ : ℕ} {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁} {g : α → β₂} (hf : ComputableTidilyInDegree f encIn enc₁ d₁ e₁) (hg : ComputableTidilyInDegree g encIn enc₂ d₂ e₂) : ComputableTidilyInDegree (fun (x : α) => (f x, g x)) encIn (encPair enc₁ enc₂) (max d₁ d₂) (max e₁ e₂)

Pairing with the framed encoding of pairs.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.fst {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableTidilyInDegree Prod.fst (encPair enc₁ enc₂) enc₁ 1 1

The first projection of the framed encoding of pairs.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.snd {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableTidilyInDegree Prod.snd (encPair enc₁ enc₂) enc₂ 1 1

The second projection of the framed encoding of pairs.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.fst' {d e : ℕ} {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (h : ComputableTidilyInDegree f encIn (encPair enc₁ enc₂) d e) : ComputableTidilyInDegree (fun (x : α) => (f x).1) encIn enc₁ (max d e) e

The first component of a pair computed with given degrees.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.snd' {d e : ℕ} {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (h : ComputableTidilyInDegree f encIn (encPair enc₁ enc₂) d e) : ComputableTidilyInDegree (fun (x : α) => (f x).2) encIn enc₂ (max d e) e

The second component of a pair computed with given degrees.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.of_finite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} [Finite α] (f : α → β) : ComputableTidilyInDegree f encIn encMid 1 0

Functions on finite types, in linear time and zero space, with output of constant length.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.optionSome {β : Type u_2} {enc₁ : β ↪ List Bool} {enc : Option β ↪ List Bool} [OptionEncoding enc₁ enc] : ComputableTidilyInDegree some enc₁ enc 1 1

Option.some.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.getD {β : Type u_2} {enc₁ : β ↪ List Bool} {enc : Option β ↪ List Bool} [OptionEncoding enc₁ enc] (d : β) : ComputableTidilyInDegree (fun (o : Option β) => o.getD d) enc enc₁ 1 1

Option.getD.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.headD {β : Type u_2} {enc₁ : β ↪ List Bool} {enc : List β ↪ List Bool} [ListEncoding enc₁ enc] (d : β) : ComputableTidilyInDegree (fun (l : List β) => l.headD d) enc enc₁ 1 1

List.headD.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.tail {β : Type u_2} {enc₁ : β ↪ List Bool} {enc : List β ↪ List Bool} [ListEncoding enc₁ enc] : ComputableTidilyInDegree List.tail enc enc 1 1

List.tail.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.isEmpty {β : Type u_2} {enc₁ : β ↪ List Bool} {enc : List β ↪ List Bool} [ListEncoding enc₁ enc] : ComputableTidilyInDegree List.isEmpty enc encBool 1 1

List.isEmpty.