Tidy computability in polynomial time

ComputableTidilyInPolyTime f encIn encOut: f is tidily computable within time and space bounded by a polynomial in the length of the encoded input. The class is closed under composition, case distinctions and pairing, and contains every function tidily computable in linear time and space.

Main definitions

• Turing.MultiTapeTM.PolyBounded: a function bounded by a polynomial in a size.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime: tidy computability in polynomial time and space.
• Turing.MultiTapeTM.EncodingEquiv: encodings that convert into each other in polynomial time.

Main results

• Turing.MultiTapeTM.PolyBounded.exists_le, .of_forall_le: recover and supply explicit polynomial bounds for the size adapter over Cslib.PolynomiallyBounded.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp, .ite, .pair: closure properties.
• Turing.MultiTapeTM.computableTidilyInPolyTime_succ: the successor in binary.

The closure properties are registered with fun_prop, so polynomial-time computability of a composite function follows from that of its parts.

Polynomial time

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

f is tidily computable within time and space bounded by a polynomial in the length of the encoded input.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.polyBounded_length {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableTidilyInPolyTime f encIn encMid) : PolyBounded (fun (a : α) => (encIn a).length) fun (a : α) => (encMid (f a)).length

The encoded value of a function computable in polynomial time has polynomial length.

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

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableTidilyInPolyTime f encMid encOut) (hg : ComputableTidilyInPolyTime g encIn encMid) : ComputableTidilyInPolyTime (f ∘ g) encIn encOut

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

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

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

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

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.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₁ : ComputableTidilyInPolyTime f₁ encIn encMid) (h₂ : ComputableTidilyInPolyTime f₂ encIn enc₂) (hg : ∀ (x : α), encOut (g x) = encMid (f₁ x) ++ enc₂ (f₂ x)) : ComputableTidilyInPolyTime g encIn encOut

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

Automation

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.id' {α : Type u_1} {encIn : α ↪ List Bool} : ComputableTidilyInPolyTime (fun (a : α) => a) encIn encIn

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableTidilyInPolyTime f encMid encOut) (hg : ComputableTidilyInPolyTime g encIn encMid) : ComputableTidilyInPolyTime (fun (a : α) => f (g a)) encIn encOut

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

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.fst {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableTidilyInPolyTime (fun (p : β₁ × β₂) => p.1) (encPair enc₁ enc₂) enc₁

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.snd {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableTidilyInPolyTime (fun (p : β₁ × β₂) => p.2) (encPair enc₁ enc₂) enc₂

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.ite' {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableTidilyInPolyTime c encIn encC) (hf : ComputableTidilyInPolyTime f encIn encMid) (hg : ComputableTidilyInPolyTime g encIn encMid) : ComputableTidilyInPolyTime (fun (x : α) => if c x = true then f x else g x) encIn encMid

A case distinction between functions computable in polynomial time on all inputs.

Equivalent encodings

def Turing.MultiTapeTM.EncodingEquiv {α : Type u_1} (enc₁ enc₂ : α ↪ List Bool) : Prop

Encodings that convert into each other in polynomial time.

theorem Turing.MultiTapeTM.EncodingEquiv.refl {α : Type u_1} (enc : α ↪ List Bool) : EncodingEquiv enc enc

theorem Turing.MultiTapeTM.EncodingEquiv.symm {α : Type u_1} {enc₁ enc₂ : α ↪ List Bool} (h : EncodingEquiv enc₁ enc₂) : EncodingEquiv enc₂ enc₁

theorem Turing.MultiTapeTM.EncodingEquiv.trans {α : Type u_1} {enc₁ enc₂ enc₃ : α ↪ List Bool} (h₁₂ : EncodingEquiv enc₁ enc₂) (h₂₃ : EncodingEquiv enc₂ enc₃) : EncodingEquiv enc₁ enc₃

theorem Turing.MultiTapeTM.computableTidilyInPolyTime_succ : ComputableTidilyInPolyTime (fun (x : ℕ) => x + 1) encNat encNat

The successor is tidily computable in polynomial time, in the binary encoding encNat, from the transducer certificate computableInTimeAndSpace_succ.