Finite-state transducers

A finite-state transducer reads its input once from left to right. In state q, on the symbol a, it moves to state (τ.step q a).1 and emits the word (τ.step q a).2; at the end of the input it emits τ.final q. Every emitted word has length at most two.

τ.toTM runs a transducer as a Turing machine without work tapes, so every function computed by a transducer is tidily computable in linear time and zero space.

Main definitions

• Turing.MultiTapeTM.Transducer: finite-state transducers.
• Turing.MultiTapeTM.Transducer.run: the word a transducer emits on a word.
• Turing.MultiTapeTM.Transducer.toTM: the transducer as a machine without work tapes.

Main results

• Turing.MultiTapeTM.Transducer.computesInTimeAndSpace_toTM: τ.toTM emits τ.run τ.q₀ w on w within 2 * w.length + 3 steps and zero space.
• Turing.MultiTapeTM.Transducer.computableTidilyInTimeAndSpace: a function computed by a transducer with finitely many states is tidily computable in linear time and zero space.

structure Turing.MultiTapeTM.Transducer (Symbol : Type u_1) (Q : Type u_2) : Type (max u_1 u_2)

A finite-state transducer with input and output alphabet Symbol and states Q. In state q on the symbol a it moves to (step q a).1 and emits (step q a).2; at the end of the input it emits final q.

• q₀ : Q

  The initial state.

• step : Q → Symbol → Q × List Symbol

  The successor state and the emitted word on reading a symbol.

• final : Q → List Symbol

  The word emitted at the end of the input.

• length_step_le (q : Q) (a : Symbol) : (self.step q a).2.length ≤ 2

  At most two symbols are emitted per input symbol.

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

  At most two symbols are emitted at the end of the input.

def Turing.MultiTapeTM.Transducer.run {Symbol : Type u_1} {Q : Type u_2} (τ : Transducer Symbol Q) : Q → List Symbol → List Symbol

The word τ emits on w, started in state q.

@[simp]

theorem Turing.MultiTapeTM.Transducer.run_nil {Symbol : Type u_1} {Q : Type u_2} (τ : Transducer Symbol Q) (q : Q) : τ.run q [] = τ.final q

@[simp]

theorem Turing.MultiTapeTM.Transducer.run_cons {Symbol : Type u_1} {Q : Type u_2} (τ : Transducer Symbol Q) (q : Q) (a : Symbol) (w : List Symbol) : τ.run q (a :: w) = (τ.step q a).2 ++ τ.run (τ.step q a).1 w

def Turing.MultiTapeTM.Transducer.toTM {Symbol : Type u_1} {Q : Type u_2} (τ : Transducer Symbol Q) : MultiTapeTM 0 Symbol (Q × Option Symbol × Bool)

τ as a machine without work tapes. Its states are the states of τ, a pending output symbol, and whether the end of the input has been reached.

theorem Turing.MultiTapeTM.Transducer.computesInTimeAndSpace_toTM {Symbol : Type u_1} {Q : Type u_2} (τ : Transducer Symbol Q) (input : List Symbol) : τ.toTM.ComputesInTimeAndSpace input (τ.run τ.q₀ input) (2 * input.length + 3) 0

τ.toTM emits τ.run τ.q₀ input on input, in 2 * input.length + 3 steps and zero space.

theorem Turing.MultiTapeTM.Transducer.computesTidily {Symbol : Type u_1} {Q : Type u_2} (τ : Transducer Symbol Q) (input : List Symbol) : (τ.toTM.seq (rewindInput Symbol)).ComputesTidilyInTimeAndSpace input (τ.run τ.q₀ input) (4 * input.length + 8) 0

Followed by a rewind of the input head, τ.toTM emits τ.run τ.q₀ input tidily.

theorem Turing.MultiTapeTM.Transducer.computableTidilyInTimeAndSpace {Q : Type} [Finite Q] (τ : Transducer Bool Q) {α : Type u_3} {β : Type u_4} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (hf : ∀ (a : α), encOut (f a) = τ.run τ.q₀ (encIn a)) : ComputableTidilyInTimeAndSpace f encIn encOut (fun (a : α) => 4 * (encIn a).length + 8) fun (x : α) => 0

A function computed by a transducer with finitely many states is tidily computable in linear time and zero space.