Left folds with bounds of given degrees

Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl asks for bounds on the arguments of the step function and on the intermediate states paired with the rest of the list. For list encodings whose elements, suffixes and lengths are bounded by the encoded list (SizedListEncoding), and the framed encodings of pairs and options, only a bound on the intermediate states is left.

A fold whose step also needs a fixed parameter, such as a key to look up, keeps the parameter in its state (Turing.MultiTapeTM.ComputableTidilyInDegree.foldlWith).

Main definitions

• Turing.MultiTapeTM.SizedListEncoding: list encodings that bound their elements, suffixes and lengths.

Main results

• Turing.MultiTapeTM.ComputableTidilyInDegree.foldl': left folds, with the degree of a round plus the degree of the number of rounds.
• Turing.MultiTapeTM.ComputableTidilyInDegree.foldlWith: the same, with a parameter.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.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 : β → α → β} {dL eL dI eI dS eS b : ℕ} (hlist : ComputableTidilyInDegree list encIn encL dL eL) (hinit : ComputableTidilyInDegree init encIn encB dI eI) (hstep : ComputableTidilyInDegree (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB dS eS) {B : γ → ℕ} (hB : DegreeBounded (fun (x : γ) => (encIn x).length) B b) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableTidilyInDegree (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB (max (max dL dI) (eL + max 1 dS * max b eL)) b

Left folds with bounds of given degrees. If the list has output degree eL, the states have length of degree b, and a round has degree dS, a fold takes time of degree eL + max 1 dS * max b eL: at most O(n ^ eL) rounds, on arguments of length O(n ^ max b eL).

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} {dP eP dL eL dI eI dS eS b : ℕ} (hpar : ComputableTidilyInDegree par encIn encP dP eP) (hlist : ComputableTidilyInDegree list encIn encL dL eL) (hinit : ComputableTidilyInDegree init encIn encB dI eI) (hstep : ComputableTidilyInDegree (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB dS eS) {B : γ → ℕ} (hB : DegreeBounded (fun (x : γ) => (encIn x).length) B b) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableTidilyInDegree (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB (max (max dL (max dP dI)) (eL + max 1 dS * max (max eP b) eL)) b

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