Multi-pass streaming folds

A multi-pass fold reads its input several times, from left to right, keeping a state on a work tape between the passes. A pass is a streaming loop over the tokens of the input, followed by an end round that computes the state for the next pass, and a flag on a separate tape that says whether another pass follows. Like a streaming fold, it never copies the input.

Main definitions

• Turing.MultiTapeTM.passTM: one pass.
• Turing.MultiTapeTM.multiPassTM: the passes, between the initial state and the final emission.

Main results

• Turing.MultiTapeTM.transformsTapes_passTM: the specification of a pass.
• Turing.MultiTapeTM.computesTidily_multiPassTM: the passes compute tidily.

noncomputable def Turing.MultiTapeTM.passTM {K : ℕ} {Q : Type u_1} {SE : Type u_3} {SN : Type u_4} {SEe : Type u_5} {SNe : Type u_6} {SC : Type u_7} (r : InputReader Bool Q) (E : MultiTapeTM K Bool SE) (Nm : MultiTapeTM K Bool SN) (Ee : MultiTapeTM K Bool SEe) (Ne : MultiTapeTM K Bool SNe) (Cm : MultiTapeTM K Bool SC) (V N F C : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : MultiTapeTM K Bool ((Unit ⊕ RewindWorkState) ⊕ RepeatUntilBlankState ((Unit ⊕ Q ⊕ RewindWorkState) ⊕ SE ⊕ SN ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState) ⊕ (SEe ⊕ SNe ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState) ⊕ SC ⊕ RewindState)

One pass: clear the flag tape C, run the streaming loop with the rounds E, Nm, run the end round Ee, Ne with the input head frozen, write the flag with Cm and rewind the input.

noncomputable def Turing.MultiTapeTM.multiPassTM {K : ℕ} {SI : Type u_2} {SF : Type u_8} {SP : Type u_9} (I : MultiTapeTM K Bool SI) (pass : MultiTapeTM K Bool SP) (Fm : MultiTapeTM K Bool SF) (V C : Fin K) : MultiTapeTM K Bool (SI ⊕ RepeatUntilBlankState SP ⊕ SF ⊕ Unit ⊕ RewindWorkState)

The multi-pass fold: write the initial state to tape V with I, run passes until the flag tape C is blank, emit from the final state with Fm and clear tape V.

def Turing.MultiTapeTM.passTapes {K : ℕ} (V C : Fin K) (v c : List Bool) : Fin K → List Bool

The tapes between two passes: the state v on tape V and the flag c on tape C.

theorem Turing.MultiTapeTM.transformsTapes_passTM {K : ℕ} {Q : Type u_1} {SE : Type u_3} {SN : Type u_4} {SEe : Type u_5} {SNe : Type u_6} {SC : Type u_7} {r : InputReader Bool Q} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {Ee : MultiTapeTM K Bool SEe} {Ne : MultiTapeTM K Bool SNe} {Cm : MultiTapeTM K Bool SC} {V N F C : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (hVC : V ≠ C) (x v₀ v₁ em ee v' c c' : List Bool) {tLoop sLoop tEe sEe tNe sNe tC sC : ℕ} (hloop : (streamRound r E Nm V N F hVN hVF hNF).whileInput.TransformsTapesAt (fun (input : List Bool) (p : Fin (input.length + 2)) (ws : Fin K → List Bool) => input = x ∧ ↑p = 1 ∧ ws = Function.update (fun (x : Fin K) => []) V v₀) (fun (input : List Bool) (x_1 : Fin (input.length + 2)) (x_2 : Fin K → List Bool) (p' : Fin (input.length + 2)) (ws' : Fin K → List Bool) (e : List Bool) => input = x ∧ ↑p' = 1 + x.length ∧ ws' = Function.update (fun (x : Fin K) => []) V v₁ ∧ e = em) tLoop sLoop) (hEe : Ee.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V v₁) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (e : List Bool) => ws' = ws ∧ e = ee) tEe sEe) (hNe : Ne.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V v₁) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (e : List Bool) => ws' = Function.update ws N v' ∧ e = []) tNe sNe) (hC : Cm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V v') (fun (x : List Bool) (ws ws' : Fin K → List Bool) (e : List Bool) => ws' = Function.update ws C c' ∧ e = []) tC sC) : (passTM r E Nm Ee Ne Cm V N F C hVN hVF hNF).TransformsTapes (fun (inp : List Bool) (ws : Fin K → List Bool) => inp = x ∧ ws = passTapes V C v₀ c) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (e : List Bool) => ws' = passTapes V C v' c' ∧ e = em ++ ee) (3 * (c.length + 1) + (tLoop + (tEe + (tNe + (3 * (v₁.length + 1) + (3 * v'.length + 10 + 3 * (v'.length + 1)))) + (tC + (x.length + 2))))) (c.length + 1 + K + (sLoop + (sEe + (sNe + (v₁.length + 1 + K + (4 * v'.length + K + 15 + (v'.length + 1 + K)))) + (sC + K))))

Clear the continuation flag, run a streaming phase, then compute the end-of-pass state and flag and rewind the input. The phase owns the token and round specifications.

theorem Turing.MultiTapeTM.computesTidily_multiPassTM {K : ℕ} {SI : Type u_2} {SF : Type u_8} {SP : Type u_9} {I : MultiTapeTM K Bool SI} {Fm : MultiTapeTM K Bool SF} {V C : Fin K} {pass : MultiTapeTM K Bool SP} (hVC : V ≠ C) (x : List Bool) (passes : ℕ) (vs cs es : ℕ → List Bool) (ef : List Bool) {tI sI tP sP tF sF : ℕ} (hI : I.TransformsTapes (fun (inp : List Bool) (ws : Fin K → List Bool) => inp = x ∧ ws = fun (x : Fin K) => []) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update (fun (x : Fin K) => []) V (vs 0) ∧ em = []) tI sI) (hpass : ∀ i ≤ passes, pass.TransformsTapes (fun (inp : List Bool) (ws : Fin K → List Bool) => inp = x ∧ ws = passTapes V C (vs i) (cs i)) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (em : List Bool) => ws' = passTapes V C (vs (i + 1)) (cs (i + 1)) ∧ em = es i) tP sP) (hfirst : cs 0 = []) (hcs : ∀ i < passes, cs (i + 1) ≠ []) (hlast : cs (passes + 1) = []) (hF : Fm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (vs (passes + 1))) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = ef) tF sF) : (I.multiPassTM pass Fm V C).ComputesTidilyInTimeAndSpace x ((List.map es (List.range (passes + 1))).flatten ++ ef) (tI + ((passes + 1) * (tP + 1) + (tF + 3 * ((vs (passes + 1)).length + 1)))) (sI + (2 * K * sP + K + (sF + ((vs (passes + 1)).length + 1 + K))))

The multi-pass fold. If I writes the initial state vs 0 to tape V, each pass i takes the state vs i and the flag cs i to the state vs (i + 1) and the flag cs (i + 1), emitting es i, where the flag is blank at the start and exactly after the last pass passes, and Fm emits ef from the final state, then multiPassTM emits the words es i followed by ef, tidily.