Multi-pass folds of tidily computable functions

A multi-pass fold reads a list, encoded as the concatenation of the tokens of its elements, several times. Each pass folds next over the elements, emitting emit for each of them, then emits passEmit of the resulting state and moves on to passEnd of it. The passes stop once cont of the state is false, and the fold ends by emitting finish of the final state. Workspace is controlled by initialization, finalization and the peak state, element and callback bounds, without a separate full-input-copy term.

Main definitions

• Turing.MultiTapeTM.passState: the state at the start of a pass.

Main results

• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.multiPassFold: multi-pass folds are tidily computable, charging each pass and bounding workspace by the initialization, finalization and peak state, element and callback bounds.

def Turing.MultiTapeTM.passState {α : Type u_1} {σ : Type u_2} (init : σ) (next : σ × α → σ) (passEnd : σ → σ) (l : List α) : ℕ → σ

The state at the start of pass i of a multi-pass fold over l: a pass folds next over l and then applies passEnd.

def Turing.MultiTapeTM.flagWord (b : Bool) : List Bool

The flag after a pass: [true] if another pass follows, blank otherwise.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.multiPassFold {α σ : Type u} {γ : Type u_3} {ε : Type u_4} {ε' : Type u_5} {φ : Type u_6} {ω : Type u_7} {encA : α ↪ List Bool} {encS : σ ↪ List Bool} {encE : ε ↪ List Bool} {encE' : ε' ↪ List Bool} {encF : φ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} {Q : Type} [Finite Q] (r : InputReader Bool Q) (tok : α → List Bool) (htok : ∀ (a : α), tok a ≠ []) (hread : ∀ (a : α) (rest : List Bool), r.read r.q₀ (tok a ++ rest) = (encA a, (tok a).length)) (elems : γ → List α) (hL : ∀ (x : γ), encIn x = List.flatMap tok (elems x)) {init : γ → σ} {next : σ × α → σ} {emit : σ × α → ε} {passEmit : σ → ε'} {passEnd : σ → σ} {cont : σ → Bool} {finish : σ → φ} {g : γ → ω} {passes tI sI : γ → ℕ} {tN sN tE sE : σ × α → ℕ} {tPE sPE tPN sPN tC sC tF sF : σ → ℕ} (hinit : ComputableTidilyInTimeAndSpace init encIn encS tI sI) (hnext : ComputableTidilyInTimeAndSpace next (encPair encS encA) encS tN sN) (hemit : ComputableTidilyInTimeAndSpace emit (encPair encS encA) encE tE sE) (hpassEmit : ComputableTidilyInTimeAndSpace passEmit encS encE' tPE sPE) (hpassEnd : ComputableTidilyInTimeAndSpace passEnd encS encS tPN sPN) (hcont : ComputableTidilyInTimeAndSpace cont encS encBool tC sC) (hfinish : ComputableTidilyInTimeAndSpace finish encS encF tF sF) (hpasses : ∀ (x : γ), ∀ i ≤ passes x, cont (passState (init x) next passEnd (elems x) (i + 1)) = decide (i < passes x)) (hg : ∀ (x : γ), encOut (g x) = (List.map (fun (i : ℕ) => streamEmit next (fun (p : σ × α) => encE (emit p)) (passState (init x) next passEnd (elems x) i) (elems x) ++ encE' (passEmit (streamState (passState (init x) next passEnd (elems x) i) next (elems x) (elems x).length))) (List.range (passes x + 1))).flatten ++ encF (finish (passState (init x) next passEnd (elems x) (passes x + 1)))) {tMax sMax lMax : γ → ℕ} (htMax : ∀ (x : γ), ∀ i ≤ passes x, ∀ (j : ℕ) (hj : j < (elems x).length), tN (streamState (passState (init x) next passEnd (elems x) i) next (elems x) j, (elems x)[j]) + tE (streamState (passState (init x) next passEnd (elems x) i) next (elems x) j, (elems x)[j]) ≤ tMax x) (hsMax : ∀ (x : γ), ∀ i ≤ passes x, ∀ (j : ℕ) (hj : j < (elems x).length), sN (streamState (passState (init x) next passEnd (elems x) i) next (elems x) j, (elems x)[j]) + sE (streamState (passState (init x) next passEnd (elems x) i) next (elems x) j, (elems x)[j]) ≤ sMax x) (htEnd : ∀ (x : γ), ∀ i ≤ passes x, tPE (streamState (passState (init x) next passEnd (elems x) i) next (elems x) (elems x).length) + tPN (streamState (passState (init x) next passEnd (elems x) i) next (elems x) (elems x).length) + tC (passState (init x) next passEnd (elems x) (i + 1)) ≤ tMax x) (hsEnd : ∀ (x : γ), ∀ i ≤ passes x, sPE (streamState (passState (init x) next passEnd (elems x) i) next (elems x) (elems x).length) + sPN (streamState (passState (init x) next passEnd (elems x) i) next (elems x) (elems x).length) + sC (passState (init x) next passEnd (elems x) (i + 1)) ≤ sMax x) (hS : ∀ (x : γ), ∀ i ≤ passes x, ∀ j ≤ (elems x).length, (encS (streamState (passState (init x) next passEnd (elems x) i) next (elems x) j)).length ≤ lMax x) (hSlast : ∀ (x : γ), (encS (passState (init x) next passEnd (elems x) (passes x + 1))).length ≤ lMax x) (hA : ∀ (x : γ) (j : ℕ) (hj : j < (elems x).length), (encA (elems x)[j]).length ≤ lMax x) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace g encIn encOut (fun (x : γ) => c * (tI x + tF (passState (init x) next passEnd (elems x) (passes x + 1)) + (passes x + 1) * ((encIn x).length + ((elems x).length + 1) * (tMax x + lMax x + 1)))) fun (x : γ) => c * (sI x + sF (passState (init x) next passEnd (elems x) (passes x + 1)) + sMax x + lMax x + 1)

Multi-pass folds are tidily computable. The input x is encoded by concatenating the non-empty tokens tok a of the elements elems x, from each of which the finite-state reader r reads encA a. Pass i starts from passState … i; the fold makes passes x + 1 passes, which cont signals after each of them. If all the parts are tidily computable and g x is encoded by what the passes emit followed by finish of the final state, then g is tidily computable. Its time is that of a streaming fold for every pass. The bounds tMax, sMax and lMax bound the time and space of a round and of the end of a pass, and the lengths of the states and elements. Workspace also accounts for initialization and finalization, without a separate full-input-copy term. All these bounds may depend on the input.