Streaming folds

A streaming fold reads its input once, from left to right, one token at a time. It keeps a state on a work tape; for each token it appends the token's content to the state, computes the next state from the result and emits a word to the output. The input is never copied, so a round costs time and space in the size of the state and the token only.

Main definitions

• Turing.MultiTapeTM.frozenRound: the part of a round that does not use the input.
• Turing.MultiTapeTM.streamTM: initialization, the loop of rounds, finalization and cleanup.

Main results

• Turing.MultiTapeTM.transformsTapes_frozenRound: the specification of frozenRound.
• Turing.MultiTapeTM.transformsTapesAt_streamLoop_after: the loop of rounds, started just past an input prefix; transformsTapesAt_streamLoop is its empty-prefix case.
• Turing.MultiTapeTM.computesTidily_streamTM_after: the tidy assembly of streamTM from an initializer that may move the input head past a prefix; computesTidily_streamTM is the case of an initializer that leaves the input head at the start.

Specifications on selected tapes

theorem Turing.MultiTapeTM.exists_embedding_eq {m K : ℕ} (h : m ≤ K) (i : Fin m) (a : Fin K) : ∃ (e : Fin m ↪ Fin K), e i = a

An embedding of Fin m into a larger Fin K sending i to a.

theorem Turing.MultiTapeTM.exists_embedding_eq₂ {m K : ℕ} (h : m ≤ K) {i o : Fin m} (hio : i ≠ o) {a b : Fin K} (hab : a ≠ b) : ∃ (e : Fin m ↪ Fin K), e i = a ∧ e o = b

An embedding of Fin m into a larger Fin K sending i to a and o to b.

The part of a round that does not use the input

def Turing.MultiTapeTM.threeTapes {K : ℕ} (V N F : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : Fin (0 + 1 + 2) ↪ Fin K

The three tapes V, N, F of copyWord: target, source and flag.

noncomputable def Turing.MultiTapeTM.frozenRound {K : ℕ} {SE : Type u_3} {SN : Type u_4} (E : MultiTapeTM K Bool SE) (Nm : MultiTapeTM K Bool SN) (V N F : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : MultiTapeTM K Bool (SE ⊕ SN ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState)

Emit with E from the word on tape V, write the next state to tape N with Nm, and move it to tape V, using tape F to flag the left end of the word.

theorem Turing.MultiTapeTM.transformsTapes_frozenRound {K : ℕ} {SE : Type u_3} {SN : Type u_4} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {V N F : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) {w emit next : List Bool} {tE sE tN sN : ℕ} (hE : E.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V w) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = emit) tE sE) (hN : Nm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V w) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws N next ∧ em = []) tN sN) : (E.frozenRound Nm V N F hVN hVF hNF).TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V w) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update (fun (x : Fin K) => []) V next ∧ em = emit) (tE + (tN + (3 * (w.length + 1) + (3 * next.length + 10 + 3 * (next.length + 1))))) (sE + (sN + (w.length + 1 + K + (4 * next.length + K + 15 + (next.length + 1 + K)))))

frozenRound takes the word w on tape V and every other tape blank to next on tape V and every other tape blank, emitting emit, if E emits emit from w and Nm writes next to tape N.

Rounds and the whole machine

noncomputable def Turing.MultiTapeTM.streamRound {K : ℕ} {Q : Type u_3} {SE : Type u_5} {SN : Type u_6} (r : InputReader Bool Q) (E : MultiTapeTM K Bool SE) (Nm : MultiTapeTM K Bool SN) (V N F : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : MultiTapeTM K Bool ((Unit ⊕ Q ⊕ RewindWorkState) ⊕ SE ⊕ SN ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState)

One round: append the content of the next token to the state on tape V, then run frozenRound with the input head frozen.

noncomputable def Turing.MultiTapeTM.streamTM {K : ℕ} {Q : Type u_3} {SI : Type u_4} {SE : Type u_5} {SN : Type u_6} {SF : Type u_7} (r : InputReader Bool Q) (I : MultiTapeTM K Bool SI) (E : MultiTapeTM K Bool SE) (Nm : MultiTapeTM K Bool SN) (Fm : MultiTapeTM K Bool SF) (V N F : Fin K) (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) : MultiTapeTM K Bool (SI ⊕ RepeatUntilBlankState ((Unit ⊕ Q ⊕ RewindWorkState) ⊕ SE ⊕ SN ⊕ (Unit ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState) ⊕ (SF ⊕ Unit ⊕ RewindWorkState) ⊕ RewindState)

The streaming fold: write the initial state to tape V with I, run rounds while there is input left, emit from the final state with Fm, clear tape V and rewind the input.

theorem Turing.MultiTapeTM.transformsTapesAt_streamRound {K : ℕ} {Q : Type u_3} {SE : Type u_5} {SN : Type u_6} {r : InputReader Bool Q} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {V N F : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (x : List Bool) (p₀ : Fin (x.length + 2)) (hp₀ : ↑p₀ ≠ 0) (v : List Bool) {emit next : List Bool} {tE sE tN sN : ℕ} (hE : E.TransformsTapes (fun (x_1 : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (v ++ (r.read r.q₀ (List.drop (↑p₀ - 1) x)).1)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = emit) tE sE) (hN : Nm.TransformsTapes (fun (x_1 : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (v ++ (r.read r.q₀ (List.drop (↑p₀ - 1) x)).1)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws N next ∧ em = []) tN sN) : have rd := r.read r.q₀ (List.drop (↑p₀ - 1) x); (streamRound r E Nm V N F hVN hVF hNF).TransformsTapesAt (fun (input : List Bool) (p : Fin (input.length + 2)) (ws : Fin K → List Bool) => input = x ∧ ↑p = ↑p₀ ∧ ws = Function.update (fun (x : Fin K) => []) V v) (fun (x_1 : List Bool) (x_2 : Fin (x_1.length + 2)) (x_3 : Fin K → List Bool) (p' : Fin (x_1.length + 2)) (ws' : Fin K → List Bool) (em : List Bool) => ↑p' = ↑p₀ + rd.2 ∧ ws' = Function.update (fun (x : Fin K) => []) V next ∧ em = emit) (v.length + 1 + (rd.2 + 1 + ((v ++ rd.1).length + 2)) + (tE + (tN + (3 * ((v ++ rd.1).length + 1) + (3 * next.length + 10 + 3 * (next.length + 1)))))) ((v ++ rd.1).length + 2 + (K - 1) + (sE + (sN + ((v ++ rd.1).length + 1 + K + (4 * next.length + K + 15 + (next.length + 1 + K))))))

One round at the input position p₀ of x, on the state v: if E emits emit from the state with the token's content appended and Nm computes next from it, the round leaves next on tape V, emits emit and moves the input head over the token.

theorem Turing.MultiTapeTM.streamPos_lt (toks : List (List Bool)) (j : ℕ) : 1 + (List.take j toks).flatten.length < toks.flatten.length + 2

The input position after the first j tokens.

theorem Turing.MultiTapeTM.drop_flatten_take (toks : List (List Bool)) {j : ℕ} (hj : j < toks.length) : List.drop (List.take j toks).flatten.length toks.flatten = toks[j] ++ (List.drop (j + 1) toks).flatten

theorem Turing.MultiTapeTM.length_flatten_take_succ (toks : List (List Bool)) {j : ℕ} (hj : j < toks.length) : (List.take (j + 1) toks).flatten.length = (List.take j toks).flatten.length + toks[j].length

def Turing.MultiTapeTM.streamRoundTime (toks : List (List Bool)) (cont vs : ℕ → List Bool) (tE tN : ℕ → ℕ) (j : ℕ) : ℕ

The time of round j of the streaming loop.

theorem Turing.MultiTapeTM.transformsTapesAt_streamLoop_after {K : ℕ} {Q : Type u_3} {SE : Type u_5} {SN : Type u_6} {r : InputReader Bool Q} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {V N F : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (pre : List Bool) (toks : List (List Bool)) (htoks : ∀ t ∈ toks, t ≠ []) (cont vs es : ℕ → List Bool) {sR : ℕ} {tE sE tN sN : ℕ → ℕ} (hread : ∀ (j : ℕ) (hj : j < toks.length), r.read r.q₀ (List.drop (List.take j toks).flatten.length toks.flatten) = (cont j, toks[j].length)) (hE : ∀ j < toks.length, E.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (vs j ++ cont j)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = es j) (tE j) (sE j)) (hN : ∀ j < toks.length, Nm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (vs j ++ cont j)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws N (vs (j + 1)) ∧ em = []) (tN j) (sN j)) (hsR : ∀ j < toks.length, (vs j ++ cont j).length + 2 + (K - 1) + (sE j + (sN j + ((vs j ++ cont j).length + 1 + K + (4 * (vs (j + 1)).length + K + 15 + ((vs (j + 1)).length + 1 + K))))) ≤ sR) : (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 = pre ++ toks.flatten ∧ ↑p = 1 + pre.length ∧ ws = Function.update (fun (x : Fin K) => []) V (vs 0)) (fun (input : List Bool) (x : Fin (input.length + 2)) (x_1 : Fin K → List Bool) (p' : Fin (input.length + 2)) (ws' : Fin K → List Bool) (em : List Bool) => input = pre ++ toks.flatten ∧ ↑p' = 1 + (pre ++ toks.flatten).length ∧ ws' = Function.update (fun (x : Fin K) => []) V (vs toks.length) ∧ em = (List.map es (List.range toks.length)).flatten) (∑ j ∈ Finset.range toks.length, (streamRoundTime toks cont vs tE tN j + 1) + 1) (2 * K * sR + K)

The streaming loop after an input prefix. The input is a prefix pre followed by the concatenation of the non-empty tokens toks, from each of which the reader r reads the content cont j. If for every token j the machine E emits es j and Nm computes the next state vs (j + 1) from the state vs j followed by cont j, then the loop of rounds, started on the state vs 0 just past the prefix, leaves the final state on tape V, emits the words es j and stops at the end of the input. The prefix is neither read nor copied.

theorem Turing.MultiTapeTM.transformsTapesAt_streamLoop {K : ℕ} {Q : Type u_3} {SE : Type u_5} {SN : Type u_6} {r : InputReader Bool Q} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {V N F : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (toks : List (List Bool)) (htoks : ∀ t ∈ toks, t ≠ []) (cont vs es : ℕ → List Bool) {sR : ℕ} {tE sE tN sN : ℕ → ℕ} (hread : ∀ (j : ℕ) (hj : j < toks.length), r.read r.q₀ (List.drop (List.take j toks).flatten.length toks.flatten) = (cont j, toks[j].length)) (hE : ∀ j < toks.length, E.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (vs j ++ cont j)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = es j) (tE j) (sE j)) (hN : ∀ j < toks.length, Nm.TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (vs j ++ cont j)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws N (vs (j + 1)) ∧ em = []) (tN j) (sN j)) (hsR : ∀ j < toks.length, (vs j ++ cont j).length + 2 + (K - 1) + (sE j + (sN j + ((vs j ++ cont j).length + 1 + K + (4 * (vs (j + 1)).length + K + 15 + ((vs (j + 1)).length + 1 + K))))) ≤ sR) : (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 = toks.flatten ∧ ↑p = 1 ∧ ws = Function.update (fun (x : Fin K) => []) V (vs 0)) (fun (input : List Bool) (x : Fin (input.length + 2)) (x_1 : Fin K → List Bool) (p' : Fin (input.length + 2)) (ws' : Fin K → List Bool) (em : List Bool) => input = toks.flatten ∧ ↑p' = 1 + toks.flatten.length ∧ ws' = Function.update (fun (x : Fin K) => []) V (vs toks.length) ∧ em = (List.map es (List.range toks.length)).flatten) (∑ j ∈ Finset.range toks.length, (streamRoundTime toks cont vs tE tN j + 1) + 1) (2 * K * sR + K)

The streaming loop. The input x is the concatenation of the non-empty tokens toks, from each of which the reader r reads the content cont j. If for every token j the machine E emits es j and Nm computes the next state vs (j + 1) from the state vs j followed by cont j, then the loop of rounds, started on the state vs 0 at the start of the input, leaves the final state on tape V, emits the words es j and stops at the end of the input.

theorem Turing.MultiTapeTM.computesTidily_streamTM_after {K : ℕ} {Q : Type u_3} {SI : Type u_4} {SE : Type u_5} {SN : Type u_6} {SF : Type u_7} {r : InputReader Bool Q} {I : MultiTapeTM K Bool SI} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {Fm : MultiTapeTM K Bool SF} {V N F : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (x pre v₀ v₁ em ef : List Bool) {tI sI tLoop sLoop tF sF : ℕ} (hI : I.TransformsTapesAt (fun (inp : List Bool) (p : Fin (inp.length + 2)) (ws : Fin K → List Bool) => inp = x ∧ ↑p = 1 ∧ ws = fun (x : Fin K) => []) (fun (x : List Bool) (x_1 : Fin (x.length + 2)) (x_2 : Fin K → List Bool) (p' : Fin (x.length + 2)) (ws' : Fin K → List Bool) (e : List Bool) => ↑p' = 1 + pre.length ∧ ws' = Function.update (fun (x : Fin K) => []) V v₀ ∧ e = []) tI sI) (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 + pre.length ∧ 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) (hF : Fm.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 = ef) tF sF) : (streamTM r I E Nm Fm V N F hVN hVF hNF).ComputesTidilyInTimeAndSpace x (em ++ ef) (tI + tLoop + (tF + 3 * (v₁.length + 1) + (x.length + 2))) (sI + (sLoop + (sF + (v₁.length + 1 + K) + K)))

Initialize with a phase I that may move the input head past a prefix pre, run a streaming phase from there, emit from its final state and clean up. The phase specifications own the token reader, round callbacks and their resource accounting.

theorem Turing.MultiTapeTM.computesTidily_streamTM {K : ℕ} {Q : Type u_3} {SI : Type u_4} {SE : Type u_5} {SN : Type u_6} {SF : Type u_7} {r : InputReader Bool Q} {I : MultiTapeTM K Bool SI} {E : MultiTapeTM K Bool SE} {Nm : MultiTapeTM K Bool SN} {Fm : MultiTapeTM K Bool SF} {V N F : Fin K} (hVN : V ≠ N) (hVF : V ≠ F) (hNF : N ≠ F) (x v₀ v₁ em ef : List Bool) {tI sI tLoop sLoop 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) (e : List Bool) => ws' = Function.update (fun (x : Fin K) => []) V v₀ ∧ e = []) tI sI) (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) (hF : Fm.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 = ef) tF sF) : (streamTM r I E Nm Fm V N F hVN hVF hNF).ComputesTidilyInTimeAndSpace x (em ++ ef) (tI + tLoop + (tF + 3 * (v₁.length + 1) + (x.length + 2))) (sI + (sLoop + (sF + (v₁.length + 1 + K) + K)))

Initialize, run a streaming phase, emit from its final state and clean up. The phase specification owns the token reader, round callbacks and their resource accounting. This is computesTidily_streamTM_after with an initializer that leaves the input head at the start.