Zip transducers and their machine semantics

A zip transducer reads two binary words in lockstep, least significant digit first, padding the shorter one with none. Its machine ZipTransducer.toTM reads frame u ++ v from the input tape: it copies u to its single work tape, rewinds that tape and then reads v on the input tape and u on the work tape simultaneously. It runs in time linear in the input and uses u.length + 2 work-tape cells.

Main definitions

• Turing.MultiTapeTM.ZipTransducer: finite-state transducers on pairs of optional bits.
• Turing.MultiTapeTM.ZipTransducer.run: the word a zip transducer emits on two words.
• Turing.MultiTapeTM.ZipTransducer.toTM: the zip transducer as a machine with one work tape.

Main results

• Turing.MultiTapeTM.ZipTransducer.computesInTimeAndSpace_toTM: on frame u ++ v, τ.toTM emits τ.run τ.q₀ u v within 3 * (frame u ++ v).length + 1 steps and u.length + 2 cells.

structure Turing.MultiTapeTM.ZipTransducer (Q : Type u_1) : Type u_1

A finite-state transducer reading two words in lockstep. In state q, on the pair (x, y) of the next digits of the two words, where none pads the shorter word, it moves to (step q (x, y)).1 and emits (step q (x, y)).2; when both words are exhausted it emits final q. The value of step on (none, none) is never used.

• q₀ : Q

  The initial state.

• step : Q → Option Bool × Option Bool → Q × List Bool

  The successor state and the emitted word on reading a pair of digits.

• final : Q → List Bool

  The word emitted when both words are exhausted.

• length_step_le (q : Q) (x : Option Bool × Option Bool) : (self.step q x).2.length ≤ 2

  At most two symbols are emitted per pair of digits.

• length_final_le (q : Q) : (self.final q).length ≤ 2

  At most two symbols are emitted at the end.

@[irreducible]

def Turing.MultiTapeTM.ZipTransducer.run {Q : Type u_1} (τ : ZipTransducer Q) (q : Q) : List Bool → List Bool → List Bool

The word τ emits on the words u and v, started in state q.

@[simp]

theorem Turing.MultiTapeTM.ZipTransducer.run_nil_nil {Q : Type u_1} (τ : ZipTransducer Q) (q : Q) : τ.run q [] [] = τ.final q

@[simp]

theorem Turing.MultiTapeTM.ZipTransducer.run_cons_nil {Q : Type u_1} (τ : ZipTransducer Q) (q : Q) (a : Bool) (u : List Bool) : τ.run q (a :: u) [] = (τ.step q (some a, none)).2 ++ τ.run (τ.step q (some a, none)).1 u []

@[simp]

theorem Turing.MultiTapeTM.ZipTransducer.run_nil_cons {Q : Type u_1} (τ : ZipTransducer Q) (q : Q) (b : Bool) (v : List Bool) : τ.run q [] (b :: v) = (τ.step q (none, some b)).2 ++ τ.run (τ.step q (none, some b)).1 [] v

@[simp]

theorem Turing.MultiTapeTM.ZipTransducer.run_cons_cons {Q : Type u_1} (τ : ZipTransducer Q) (q : Q) (a b : Bool) (u v : List Bool) : τ.run q (a :: u) (b :: v) = (τ.step q (some a, some b)).2 ++ τ.run (τ.step q (some a, some b)).1 u v

theorem Turing.MultiTapeTM.ZipTransducer.run_of_ne {Q : Type u_1} (τ : ZipTransducer Q) {q : Q} {u v : List Bool} (h : ¬(u = [] ∧ v = [])) : τ.run q u v = (τ.step q (u.head?, v.head?)).2 ++ τ.run (τ.step q (u.head?, v.head?)).1 u.tail v.tail

Unless both words are exhausted, τ reads their first digits and continues on the rest.

inductive Turing.MultiTapeTM.ZipTransducer.State (Q : Type u_2) : Type u_2

The control states of ZipTransducer.toTM.

• copy {Q : Type u_2} : State Q

  Expecting the next frame marker of the first word.

• copyBit {Q : Type u_2} : State Q

  Expecting the next digit of the first word, to be copied to the work tape.

• rewind {Q : Type u_2} : State Q

  Moving the work head back to the start of the copied word.

• zip {Q : Type u_2} (q : Q) (pending : Option Bool) : State Q

  Running τ in state q, with a pending output symbol.

• flush {Q : Type u_2} (b : Bool) : State Q

  Emitting the last output symbol before halting.

instance Turing.MultiTapeTM.ZipTransducer.State.instFinite {Q : Type u_2} [Finite Q] : Finite (State Q)

With finitely many states of the transducer, the machine has finitely many states.

def Turing.MultiTapeTM.ZipTransducer.toTM {Q : Type u_1} (τ : ZipTransducer Q) : MultiTapeTM 1 Bool (State Q)

τ as a machine with one work tape. On frame u ++ v it copies u to the work tape, rewinds the work tape, and then runs τ on u from the work tape and v from the input tape.

Configurations

Runs through a set of work-head positions

The framed input

The phases of the machine

The transitions used outside the copy phase, for arbitrary read symbols.

theorem Turing.MultiTapeTM.ZipTransducer.computesInTimeAndSpace_toTM {Q : Type u_1} {τ : ZipTransducer Q} (u v : List Bool) : τ.toTM.ComputesInTimeAndSpace (frame u ++ v) (τ.run τ.q₀ u v) (3 * (frame u ++ v).length + 1) (u.length + 2)

On frame u ++ v, τ.toTM emits τ.run τ.q₀ u v within 3 * (frame u ++ v).length + 1 steps, visiting the u.length + 2 work-tape cells -1, …, u.length.