Left folds are tidily computable

If list and init are tidily computable from a common input, and step is tidily computable on pairs, then fun x => (list x).foldl step (init x) is tidily computable, relative to encodings of pairs, options and lists as in Turing.MultiTapeTM.PairEncoding, Turing.MultiTapeTM.OptionEncoding and Turing.MultiTapeTM.ListEncoding.

The fold is computed by Turing.MultiTapeTM.iterateWhile on the state some (l, b), holding the rest l of the list and the accumulator b: one round replaces it by some (l.tail, step b a), where a is the head of l, or by none once l is empty. The case distinction is made by Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.ite.

Main results

• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl: left folds are tidily computable.

Bounds up to a constant factor

One round of the fold

Left folds

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl {γ α β : Type u} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encBA : β × α ↪ List Bool} {encS : List α × β ↪ List Bool} {encO : Option (List α × β) ↪ List Bool} [hLE : ListEncoding encA encL] [hBA : PairEncoding encB encA encBA] [hSE : PairEncoding encL encB encS] [hOE : OptionEncoding encS encO] {list : γ → List α} {init : γ → β} {step : β → α → β} {t s : γ → ℕ} {tStep sStep : β × α → ℕ} {tMax sMax lMax : γ → ℕ} (hlist : ComputableTidilyInTimeAndSpace list encIn encL t s) (hinit : ComputableTidilyInTimeAndSpace init encIn encB t s) (hstep : ComputableTidilyInTimeAndSpace (fun (p : β × α) => step p.1 p.2) encBA encB tStep sStep) (htMax : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), tStep (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ tMax x) (hsMax : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), sStep (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ sMax x) (hlMax : ∀ (x : γ), ∀ i ≤ (list x).length, (encS (List.drop i (list x), List.foldl step (init x) (List.take i (list x)))).length ≤ lMax x) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB (fun (x : γ) => c * (t x + ((list x).length + 1) * (tMax x + lMax x + 1))) fun (x : γ) => c * (s x + sMax x + lMax x + 1)

If list and init are tidily computable from a common input and step is tidily computable on pairs, then fun x => (list x).foldl step (init x) is tidily computable. Each of the (list x).length steps is bounded by tMax x steps and sMax x cells, and the encodings of the intermediate states ((list x).drop i, ((list x).take i).foldl step (init x)) by lMax x.