Elgot–Mezei composition

Feeding a right-to-left transducer the output of a left-to-right one gives a bimachine: the left automaton is the first machine, and the right automaton carries the map taking a state of the first machine to the state the second reaches over the image of the suffix. We show that a right-subsequential function after a left-subsequential one is bimachine-computable as soon as the composite preserves the empty word — the composition half of [EM65]'s decomposition theorem ([Sak09], Cor. V.2.5). The decomposition half, that every rational function factors this way ([Sak09], Th. V.2.2), is not formalized here.

Main definitions

• SubsequentialTransducer.rightComp: the bimachine running T₂ right-to-left over the output of T₁

Implementation notes

The empty-word hypothesis is not an artifact of the construction: Bimachine.run [] = [], so a composite whose flushes emit anything on the empty input is computed by no bimachine at all.

[UPSTREAM] candidate: Mathlib.Computability.Bimachine.

TODO

• The decomposition half: every bimachine-computable function is a right-subsequential function after a left-subsequential one.
• The letter-to-letter refinement: Mealy after Mealy gives a length-preserving bimachine (IsLengthPreservingBimachineComputable).

def SubsequentialTransducer.rightComp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) : Bimachine (Bool × σ₁) (Bool × (σ₁ → σ₂)) α γ

T₂.rightComp T₁ is the bimachine reading T₁ left to right and T₂ right to left over T₁'s output. Its right state is the map sending the T₁-state entering the suffix to the T₂-state over the image of that suffix, T₁'s flush already consumed; the two flags mark the ends of the input, where T₂'s flush and the image of T₁'s flush are emitted.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SubsequentialTransducer.rightComp_rStep {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (r : Bool × (σ₁ → σ₂)) (a : α) : (T₂.rightComp T₁).rStep r a = (false, fun (s : σ₁) => T₂.stateAfter (r.2 (T₁.step s a)) (T₁.output s a).reverse)

@[simp]

theorem SubsequentialTransducer.rightComp_rInit {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) : (T₂.rightComp T₁).rInit = (true, fun (s : σ₁) => T₂.stateAfter T₂.start (T₁.finalOutput s).reverse)

@[simp]

theorem SubsequentialTransducer.rightComp_output {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (l : Bool × σ₁) (a : α) (r : Bool × (σ₁ → σ₂)) : (T₂.rightComp T₁).output l a r = (if l.1 = true then T₂.runFrom (r.2 (T₁.step l.2 a)) (T₁.output l.2 a).reverse else T₂.emitted (r.2 (T₁.step l.2 a)) (T₁.output l.2 a).reverse).reverse ++ if r.1 = true then (T₂.emitted T₂.start (T₁.finalOutput (T₁.step l.2 a)).reverse).reverse else []

@[simp]

theorem SubsequentialTransducer.rightComp_lInit {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) : (T₂.rightComp T₁).lInit = (true, T₁.start)

@[simp]

theorem SubsequentialTransducer.rightComp_lStep {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (l : Bool × σ₁) (a : α) : (T₂.rightComp T₁).lStep l a = (false, T₁.step l.2 a)

@[simp]

theorem SubsequentialTransducer.rightComp_rState_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (suf : List α) : ((T₂.rightComp T₁).rState suf).1 = suf.isEmpty

@[simp]

theorem SubsequentialTransducer.rightComp_rState_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (suf : List α) (s : σ₁) : ((T₂.rightComp T₁).rState suf).2 s = T₂.stateAfter T₂.start (T₁.runFrom s suf).reverse

theorem SubsequentialTransducer.rightComp_runFrom {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (b : Bool) (s : σ₁) (a : α) (xs : List α) : (T₂.rightComp T₁).runFrom (b, s) (a :: xs) = (if b = true then T₂.runFrom T₂.start (T₁.runFrom s (a :: xs)).reverse else T₂.emitted T₂.start (T₁.runFrom s (a :: xs)).reverse).reverse

Each cell emits the reverse of what T₂ produces over the reversed image of the input: its whole run at the left end, its emission alone — no flush — elsewhere.

theorem SubsequentialTransducer.rightComp_run_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (a : α) (xs : List α) : (T₂.rightComp T₁).run (a :: xs) = T₂.runRight (T₁.run (a :: xs))

The bimachine computes the composite on every nonempty input — the empty word is the only obstruction.

theorem SubsequentialTransducer.rightComp_run {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} (T₂ : SubsequentialTransducer σ₂ β γ) (T₁ : SubsequentialTransducer σ₁ α β) (h : T₂.runRight (T₁.run []) = []) : (T₂.rightComp T₁).run = T₂.runRight ∘ T₁.run

The bimachine computes T₂.runRight ∘ T₁.run, given that the composite preserves the empty word.

theorem IsRightSubsequential.isBimachineComputable_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : List α → List β} {g : List β → List γ} (hg : IsRightSubsequential g) (hf : IsLeftSubsequential f) (hnil : g (f []) = []) : IsBimachineComputable (g ∘ f)

Elgot–Mezei composition: a right-subsequential function after a left-subsequential one is bimachine-computable, as soon as the composite preserves the empty word (as every bimachine-computable function does).

theorem Mealy.isBimachineComputable_runRight_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_4} {σ₂ : Type u_5} [Fintype σ₁] [Fintype σ₂] (T₂ : Mealy σ₂ β γ) (T₁ : Mealy σ₁ α β) : IsBimachineComputable (T₂.runRight ∘ T₁.run)

The synchronous case: a Mealy machine run right to left over the output of another is a bimachine, with no side condition since both passes preserve the empty word.