Folds behind a finite-state translator

A translator reads bits and emits, for each bit, at most one event, with a finite state in between. A fold over the events of a word is a fold over its bits, whose state also holds the state of the translator: each bit steps the translator and, if it emits an event, steps the inner fold. This turns a fold over a convenient encoding into a fold over another one, at the cost of a constant amount of state, so it applies to streaming and multi-pass folds alike.

Main definitions

• Turing.MultiTapeTM.Translator: finite-state translators from bits to events.
• Turing.MultiTapeTM.Translator.lift: the step of a fold on bits from one on events.

Main results

• Turing.MultiTapeTM.Translator.foldl_lift: the lifted fold folds over the events.
• Turing.MultiTapeTM.ComputableTidilyInO.lift: the lifted step is tidily computable.

structure Turing.MultiTapeTM.Translator (Q : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A translator from bits to events: from each state, a bit leads to a state and at most one event.

• q₀ : Q

  The initial state.

• step : Q → Bool → Q × Option E

  The next state and the emitted event, if any.

def Turing.MultiTapeTM.Translator.run {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) : Q → List Bool → Q × List E

The state and the events after reading w from the state q.

def Turing.MultiTapeTM.Translator.events {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) (w : List Bool) : List E

The events of w.

def Turing.MultiTapeTM.Translator.lift {Q : Type u_1} {E : Type u_2} {σ : Type u_3} (tr : Translator Q E) (next : σ × E → σ) (p : (Q × σ) × Bool) : Q × σ

The step of a fold on bits from the step next of a fold on events: step the translator and, if it emits an event, the fold.

theorem Turing.MultiTapeTM.Translator.foldl_lift {Q : Type u_1} {E : Type u_2} {σ : Type u_3} (tr : Translator Q E) (next : σ × E → σ) (q : Q) (s : σ) (w : List Bool) : List.foldl (fun (p : Q × σ) (b : Bool) => tr.lift next (p, b)) (q, s) w = ((tr.run q w).1, List.foldl (fun (s : σ) (e : E) => next (s, e)) s (tr.run q w).2)

The lifted fold folds over the events, and ends in the state of the translator.

theorem Turing.MultiTapeTM.Translator.run_append {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) (q : Q) (u v : List Bool) : tr.run q (u ++ v) = ((tr.run (tr.run q u).1 v).1, (tr.run q u).2 ++ (tr.run (tr.run q u).1 v).2)

theorem Turing.MultiTapeTM.Translator.run_take {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) (q : Q) (w : List Bool) (k : ℕ) : List.take (tr.run q (List.take k w)).2.length (tr.run q w).2 = (tr.run q (List.take k w)).2

The events of a prefix are a prefix of the events.

theorem Turing.MultiTapeTM.Translator.run_take_succ {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) (q : Q) (w : List Bool) {k : ℕ} (hk : k < w.length) : tr.run q (List.take (k + 1) w) = ((tr.step (tr.run q (List.take k w)).1 w[k]).1, (tr.run q (List.take k w)).2 ++ (tr.step (tr.run q (List.take k w)).1 w[k]).2.toList)

The bit at position k emits the next event, if any.

theorem Turing.MultiTapeTM.Translator.streamState_lift {Q : Type u_1} {E : Type u_2} {σ : Type u_3} (tr : Translator Q E) (next : σ × E → σ) (q : Q) (s : σ) (w : List Bool) (k : ℕ) : streamState (q, s) (tr.lift next) w k = ((tr.run q (List.take k w)).1, streamState s next (tr.run q w).2 (tr.run q (List.take k w)).2.length)

The lifted fold after k bits: the state of the translator, and the inner fold after the events of the first k bits.

theorem Turing.MultiTapeTM.Translator.passState_lift {Q : Type u_1} {E : Type u_2} {σ : Type u_3} (tr : Translator Q E) (init : σ) (next : σ × E → σ) (passEnd : σ → σ) (w : List Bool) (i : ℕ) : passState (tr.q₀, init) (tr.lift next) (fun (p : Q × σ) => (tr.q₀, passEnd p.2)) w i = (tr.q₀, passState init next passEnd (tr.events w) i)

The passes of the lifted fold, which restart the translator, are those of the inner fold on the events.

theorem Turing.MultiTapeTM.Translator.elim_le {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) (q : Q) (w : List Bool) {k : ℕ} (hk : k < w.length) (F : ℕ → E → ℕ) {m : ℕ} (hF : ∀ (j : ℕ) (hj : j < (tr.run q w).2.length), F j (tr.run q w).2[j] ≤ m) : (tr.step (tr.run q (List.take k w)).1 w[k]).2.elim 0 (F (tr.run q (List.take k w)).2.length) ≤ m

A bound on the events holds for the event of every bit, if any: the event of bit k is the event after those of the first k bits.

theorem Turing.MultiTapeTM.Translator.length_run_take_le {Q : Type u_1} {E : Type u_2} (tr : Translator Q E) (q : Q) (w : List Bool) (k : ℕ) : (tr.run q (List.take k w)).2.length ≤ (tr.run q w).2.length

The length of the events of a prefix.

theorem Turing.MultiTapeTM.ComputableTidilyInO.lift {Q E σ : Type} [Finite Q] [Inhabited E] {encQ : Q ↪ List Bool} {encE : E ↪ List Bool} {encS : σ ↪ List Bool} {next : σ × E → σ} {T S : σ × E → ℕ} (tr : Translator Q E) (h : ComputableTidilyInO next (encPair encS encE) encS T S) : ComputableTidilyInO (tr.lift next) (encPair (encPair encQ encS) encBool) (encPair encQ encS) (fun (p : (Q × σ) × Bool) => ((encPair (encPair encQ encS) encBool) p).length + (tr.step p.1.1 p.2).2.elim 0 fun (e : E) => T (p.1.2, e)) fun (p : (Q × σ) × Bool) => ((encPair (encPair encQ encS) encBool) p).length + (tr.step p.1.1 p.2).2.elim 0 fun (e : E) => S (p.1.2, e)

The lifted step is tidily computable, within the bounds of the inner step on the emitted event, if any, plus the length of its input.

Bounds

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.multiPassFold_translate {Q E σ γ ε' φ ω : Type} [Finite Q] [Inhabited E] {encQ : Q ↪ List Bool} {encE : E ↪ List Bool} {encS : σ ↪ List Bool} {encE' : ε' ↪ List Bool} {encF : φ ↪ List Bool} {encIn : γ ↪ List Bool} {encOut : ω ↪ List Bool} (tr : Translator Q E) {init : γ → σ} {next : σ × E → σ} {passEmit : σ → ε'} {passEnd : σ → σ} {cont : σ → Bool} {finish : σ → φ} {g : γ → ω} {passes TI SI : γ → ℕ} {T S : σ × E → ℕ} {TPE SPE TPN SPN TC SC TF SF : σ → ℕ} (hinit : ComputableTidilyInO init encIn encS TI SI) (hnext : ComputableTidilyInO next (encPair encS encE) encS T S) (hpassEmit : ComputableTidilyInO passEmit encS encE' TPE SPE) (hpassEnd : ComputableTidilyInO passEnd encS encS TPN SPN) (hcont : ComputableTidilyInO cont encS encBool TC SC) (hfinish : ComputableTidilyInO finish encS encF TF SF) (hpasses : ∀ (x : γ), ∀ i ≤ passes x, cont (passState (init x) next passEnd (tr.events (encIn x)) (i + 1)) = decide (i < passes x)) (hg : ∀ (x : γ), encOut (g x) = (List.map (fun (i : ℕ) => encE' (passEmit (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) (tr.events (encIn x)).length))) (List.range (passes x + 1))).flatten ++ encF (finish (passState (init x) next passEnd (tr.events (encIn x)) (passes x + 1)))) {tMax sMax lMax : γ → ℕ} (htMax : ∀ (x : γ), ∀ i ≤ passes x, ∀ (j : ℕ) (hj : j < (tr.events (encIn x)).length), T (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) j, (tr.events (encIn x))[j]) ≤ tMax x) (hsMax : ∀ (x : γ), ∀ i ≤ passes x, ∀ (j : ℕ) (hj : j < (tr.events (encIn x)).length), S (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) j, (tr.events (encIn x))[j]) ≤ sMax x) (htEnd : ∀ (x : γ), ∀ i ≤ passes x, TPE (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) (tr.events (encIn x)).length) + TPN (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) (tr.events (encIn x)).length) + TC (passState (init x) next passEnd (tr.events (encIn x)) (i + 1)) ≤ tMax x) (hsEnd : ∀ (x : γ), ∀ i ≤ passes x, SPE (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) (tr.events (encIn x)).length) + SPN (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) (tr.events (encIn x)).length) + SC (passState (init x) next passEnd (tr.events (encIn x)) (i + 1)) ≤ sMax x) (hS : ∀ (x : γ), ∀ i ≤ passes x, ∀ j ≤ (tr.events (encIn x)).length, (encS (streamState (passState (init x) next passEnd (tr.events (encIn x)) i) next (tr.events (encIn x)) j)).length ≤ lMax x) (hSlast : ∀ (x : γ), (encS (passState (init x) next passEnd (tr.events (encIn x)) (passes x + 1))).length ≤ lMax x) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace g encIn encOut (fun (x : γ) => c * (TI x + TF (passState (init x) next passEnd (tr.events (encIn x)) (passes x + 1)) + (passes x + 1) * ((encIn x).length + ((encIn x).length + 1) * (tMax x + lMax x + 1)))) fun (x : γ) => c * (SI x + SF (passState (init x) next passEnd (tr.events (encIn x)) (passes x + 1)) + sMax x + lMax x + 1)

Multi-pass folds behind a translator. A multi-pass fold over the events that the translator tr emits on the encoded input is tidily computable on the encoded input itself, from parts computable within the given bounds. Each pass reads every bit, so its time is the length of the input times the bounds on a round; the space is that of the fold on the events. 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.