Finite-state transducers and their machine semantics

Machine declarations are moved from their original module without changing programs or resource formulas. Higher computability-calculus theorems remain in the original facade.

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.