Tidy computability within given bounds, up to constants

ComputableTidilyInO f encIn encOut T S: f is tidily computable within time O(T a) and space O(S a) on the input a, and its encoded value has length O(S a). Unlike Turing.MultiTapeTM.ComputableTidilyInDegree, the bounds are any functions of the input, not of the length of its encoding, so that they can be stated in several measures of the input, such as the length of a description, the length of an input and a number of steps.

The closure properties are exact up to constants: composition adds the bounds of the outer function at the intermediate value, a case distinction adds the bounds of the branch taken, and a left fold adds, for every round, a bound on the round and on the state to the time, but only once to the space. The encoded value counts towards the space since a combinator keeps it on a work tape.

Main definitions

• Turing.MultiTapeTM.ComputableTidilyInO: tidy computability within given bounds.
• Turing.MultiTapeTM.listMax: the largest value of a function on a list, to bound rounds.

Main results

• Turing.MultiTapeTM.ComputableTidilyInO.comp, .ite, .prod: closure properties.
• Turing.MultiTapeTM.ComputableTidilyInO.foldl, .foldlWith: left folds with a parameter.
• Turing.MultiTapeTM.ComputableTidilyInDegree.inO: bounds of a given degree.

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

f is tidily computable within time O(T a) and space O(S a) on the input a, and its encoded value has length O(S a).

theorem Turing.MultiTapeTM.ComputableInO.tidy {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableInO f encIn encOut T S) : ComputableTidilyInO f encIn encOut T S

A function computable within time O(T) and space O(S) is tidily computable within them.

theorem Turing.MultiTapeTM.ComputableInO.of_tidy {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableTidilyInO f encIn encOut T S) : ComputableInO f encIn encOut T S

A function tidily computable within time O(T) and space O(S) is computable within them, by the same machine.

theorem Turing.MultiTapeTM.ComputableTidilyInO.computableInO {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} (h : ComputableTidilyInO f encIn encOut T S) : ComputableInO f encIn encOut T S

Turing.MultiTapeTM.ComputableInO.of_tidy for dot notation on a tidy hypothesis.

def Turing.MultiTapeTM.listMax {α : Type u_1} (f : α → ℕ) (l : List α) : ℕ

The largest value of f on the elements of l, or 0.

theorem Turing.MultiTapeTM.le_listMax {α : Type u_1} {f : α → ℕ} {l : List α} {a : α} (ha : a ∈ l) : f a ≤ listMax f l

theorem Turing.MultiTapeTM.listMax_le {α : Type u_1} {f : α → ℕ} {l : List α} {b : ℕ} (h : ∀ a ∈ l, f a ≤ b) : listMax f l ≤ b

theorem Turing.MultiTapeTM.ComputableTidilyInO.of_bounds {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} {t s : α → ℕ} (hf : ComputableTidilyInTimeAndSpace f encIn encMid t s) (k : ℕ) (ht : ∀ (a : α), t a ≤ k * (T a + 1)) (hs : ∀ (a : α), s a ≤ k * (S a + 1)) (hl : ∀ (a : α), (encMid (f a)).length ≤ k * (S a + 1)) : ComputableTidilyInO f encIn encMid T S

Bounds within a constant factor.

theorem Turing.MultiTapeTM.ComputableTidilyInO.mono {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} {T' S' : α → ℕ} (h : ComputableTidilyInO f encIn encMid T S) (k : ℕ) (hT : ∀ (a : α), T a ≤ k * (T' a + 1)) (hS : ∀ (a : α), S a ≤ k * (S' a + 1)) : ComputableTidilyInO f encIn encMid T' S'

Weakening the bounds, up to a constant factor.

theorem Turing.MultiTapeTM.ComputableTidilyInO.mono_le {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} {T' S' : α → ℕ} (h : ComputableTidilyInO f encIn encMid T S) (hT : ∀ (a : α), T a ≤ T' a) (hS : ∀ (a : α), S a ≤ S' a) : ComputableTidilyInO f encIn encMid T' S'

Weakening the bounds.

theorem Turing.MultiTapeTM.ComputableTidilyInO.weaken {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} {T' S' : α → ℕ} (h : ComputableTidilyInO f encIn encMid T S) (hT : BigOLe T T') (hS : BigOLe S S') : ComputableTidilyInO f encIn encMid T' S'

Weakening the bounds, up to constant factors.

theorem Turing.MultiTapeTM.ComputableTidilyInO.length_le {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} (h : ComputableTidilyInO f encIn encMid T S) : ∃ (c : ℕ), ∀ (a : α), (encMid (f a)).length ≤ c * (S a + 1)

The encoded values are within the space bound.

theorem Turing.MultiTapeTM.ComputableTidilyInO.length_le_time {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} (h : ComputableTidilyInO f encIn encMid T S) : ∃ (c : ℕ), ∀ (a : α), (encMid (f a)).length ≤ c * (T a + 1)

The encoded values are within the time bound.

theorem Turing.MultiTapeTM.ComputableTidilyInO.of_linear {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableTidilyInLinearTimeAndSpace f encIn encMid) : ComputableTidilyInO f encIn encMid (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

theorem Turing.MultiTapeTM.ComputableTidilyInO.comp {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {T₁ S₁ : α → ℕ} {f : β → γ} {g : α → β} {T₂ S₂ : β → ℕ} (hf : ComputableTidilyInO f encMid encOut T₂ S₂) (hg : ComputableTidilyInO g encIn encMid T₁ S₁) : ComputableTidilyInO (f ∘ g) encIn encOut (fun (a : α) => T₁ a + T₂ (g a)) fun (a : α) => S₁ a + S₂ (g a)

theorem Turing.MultiTapeTM.ComputableTidilyInO.ite {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} {Tc Tf Tg Sc Sf Sg : α → ℕ} (hc : ComputableTidilyInO c encIn encC Tc Sc) (hf : ComputableTidilyInO f encIn encMid Tf Sf) (hg : ComputableTidilyInO g encIn encMid Tg Sg) : ComputableTidilyInO (fun (x : α) => if c x = true then f x else g x) encIn encMid (fun (x : α) => Tc x + if c x = true then Tf x else Tg x) fun (x : α) => Sc x + if c x = true then Sf x else Sg x

theorem Turing.MultiTapeTM.ComputableTidilyInO.append {α β γ δ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {T₁ T₂ S₁ S₂ : α → ℕ} {enc₂ : δ ↪ List Bool} {f₁ : α → β} {f₂ : α → δ} {g : α → γ} (h₁ : ComputableTidilyInO f₁ encIn encMid T₁ S₁) (h₂ : ComputableTidilyInO f₂ encIn enc₂ T₂ S₂) (hg : ∀ (x : α), encOut (g x) = encMid (f₁ x) ++ enc₂ (f₂ x)) : ComputableTidilyInO g encIn encOut (fun (x : α) => T₁ x + T₂ x) fun (x : α) => S₁ x + S₂ x

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

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

Pairing with the framed encoding of pairs.

theorem Turing.MultiTapeTM.ComputableTidilyInO.computableTidilyInPolyTime {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} (h : ComputableTidilyInO f encIn encMid T S) (hT : PolyBounded (fun (a : α) => (encIn a).length) T) (hS : PolyBounded (fun (a : α) => (encIn a).length) S) : ComputableTidilyInPolyTime f encIn encMid

Bounds polynomial in the length of the encoded input give polynomial time.

theorem Turing.MultiTapeTM.ComputableTidilyInO.of_enc_eq {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {T S : α → ℕ} {f : α → β} {g : α → γ} (hf : ComputableTidilyInO f encIn encMid T S) (h : ∀ (x : α), encOut (g x) = encMid (f x)) : ComputableTidilyInO g encIn encOut T S

A function whose encoded values are those of a function computable within the bounds.

theorem Turing.MultiTapeTM.ComputableTidilyInO.of_encIn_eq {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {α' : Type} {encIn' : α' ↪ List Bool} {f : α → β} (e : α' → α) (hf : ComputableTidilyInO f encIn encMid T S) (henc : ∀ (a : α'), encIn' a = encIn (e a)) : ComputableTidilyInO (fun (a : α') => f (e a)) encIn' encMid (fun (a : α') => T (e a)) fun (a : α') => S (e a)

A function computed on another encoding of its input, with the same words.

theorem Turing.MultiTapeTM.ComputableTidilyInO.comp_linear {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {T₁ S₁ : α → ℕ} {f : β → γ} {g : α → β} (hf : ComputableTidilyInO f encMid encOut (fun (b : β) => (encMid b).length) fun (b : β) => (encMid b).length) (hg : ComputableTidilyInO g encIn encMid T₁ S₁) : ComputableTidilyInO (f ∘ g) encIn encOut T₁ S₁

A function computed within the length of its encoded value, after one computed within T and S, is computed within T and S.

theorem Turing.MultiTapeTM.ComputableTidilyInO.const {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableTidilyInO (fun (x : α) => b) encIn encMid (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

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

The first projection of the framed encoding of pairs.

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

The second projection of the framed encoding of pairs.

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

The first component of a pair computed within bounds.

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

The second component of a pair computed within bounds.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.inO {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {d e : ℕ} (h : ComputableTidilyInDegree f encIn encOut d e) : ComputableTidilyInO f encIn encOut (fun (a : α) => ((encIn a).length + 1) ^ d) fun (a : α) => ((encIn a).length + 1) ^ d

Bounds of degree d in the length of the encoded input.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.inO_one {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {e : ℕ} (h : ComputableTidilyInDegree f encIn encOut 1 e) : ComputableTidilyInO f encIn encOut (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

Linear bounds in the length of the encoded input.

Left folds

theorem Turing.MultiTapeTM.ComputableTidilyInO.foldl {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [hS : SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} {Tl Ti Sl Si R Q B : γ → ℕ} {Ts Ss : β × α → ℕ} (hlist : ComputableTidilyInO list encIn encL Tl Sl) (hinit : ComputableTidilyInO init encIn encB Ti Si) (hstep : ComputableTidilyInO (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB Ts Ss) (hround : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ts (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ R x) (hspace : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ss (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ Q x) (hstate : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableTidilyInO (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB (fun (x : γ) => Tl x + Ti x + ((list x).length + 1) * (R x + B x + (encL (list x)).length)) fun (x : γ) => Sl x + Si x + Q x + B x + (encL (list x)).length

Left folds within given bounds. If every round is within the time R x and the space Q x, and every state has length at most B x, a fold takes the time of the list and of the initial state, plus R x, B x and the length of the encoded list for every round, and the space of the list and of the initial state, plus Q x, B x and the length of the encoded list once.

theorem Turing.MultiTapeTM.ComputableTidilyInO.foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [hS : SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} {Tp Tl Ti Sp Sl Si R Q B : γ → ℕ} {Ts Ss : (π × β) × α → ℕ} (hpar : ComputableTidilyInO par encIn encP Tp Sp) (hlist : ComputableTidilyInO list encIn encL Tl Sl) (hinit : ComputableTidilyInO init encIn encB Ti Si) (hstep : ComputableTidilyInO (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB Ts Ss) (hround : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ts ((par x, List.foldl (step (par x)) (init x) (List.take i (list x))), (list x)[i]) ≤ R x) (hspace : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), Ss ((par x, List.foldl (step (par x)) (init x) (List.take i (list x))), (list x)[i]) ≤ Q x) (hstate : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableTidilyInO (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB (fun (x : γ) => Tp x + Tl x + Ti x + ((list x).length + 1) * (R x + B x + (encP (par x)).length + (encL (list x)).length)) fun (x : γ) => Sp x + Sl x + Si x + Q x + B x + (encP (par x)).length + (encL (list x)).length

Left folds with a parameter, within given bounds. The step may depend on a parameter par x, which is kept in the state.