Mealy machines

A Mealy machine [Mea55] is a deterministic transducer which reads its input left to right and emits exactly one output symbol per input symbol, so the function it computes is length-preserving by construction. Output coordinate i of the run is the output at the state reached after the length-i input prefix (Mealy.getElem?_run), so the output is prefix-determined at every coordinate.

Note that this definition allows for machines with infinite states; a Fintype instance must be supplied for the finite-state class IsMealyComputable.

Main definitions

• Mealy σ α β: transducer with states σ, input alphabet α, output alphabet β
• Mealy.run, Mealy.runRight: the left-to-right and right-to-left passes
• Mealy.comp: the cascade connection, computing the composite function
• Mealy.ofFn: the single-state machine applying a fixed symbol map letter-wise
• Mealy.ofFlag: the one-bit machine tracking whether an earlier symbol satisfies p
• Mealy.map: transport along an equivalence on states
• IsMealyComputable f: f is computed by some finite-state Mealy
• DFA.comapMealy: pulls an acceptor back along a transducer

Main theorems

• Mealy.getElem?_run: output coordinate i is the output at the state reached after the length-i input prefix
• Mealy.getElem?_ofFlag_run, Mealy.getElem?_ofFlag_runRight: each coordinate of a flag machine sees the flag over its strict prefix (its strict suffix, for the right-to-left pass)
• isMealyComputable_iff: the universe-polymorphic characterization
• IsMealyComputable.comp: closure under composition
• IsMealyComputable.isRegular_preimage: Mealy-computable maps pull back regular languages

Implementation notes

The functions computed by Mealy machines are the sequential functions of algebraic automata theory [Hol82]. SubsequentialTransducer generalizes to word-block outputs and a state-final output [Moh97]; Mealy.toSubsequentialTransducer exhibits a Mealy machine as the singleton-output, empty-flush case.

[UPSTREAM] candidate: Mathlib.Computability.Mealy.

The Myhill–Nerode characterization of the Mealy-computable functions by their residuals is in Core/Computability/MyhillNerode.lean.

TODO

• Mealy machine homomorphisms [Hol82], with map at an equivalence as the isomorphism case.
• The right-scan mirror via reverse conjugation.
• Moore machines (state-determined output) and the Mealy–Moore equivalence: same states one way, σ × β states the other, so the computable classes coincide.
• The graph view: the zipped graph of a Mealy-computable map is a regular language over α × β (the synchronous rational relations). Residuals of the map correspond to left quotients of the graph, so this would derive isMealyComputable_iff_residual from the language Myhill–Nerode theorem.

structure Mealy (σ : Type u_4) (α : Type u_5) (β : Type u_6) : Type (max (max u_4 u_5) u_6)

A Mealy machine is a set of states (σ), a starting state (initial), a transition function (step) and an output function (output); it is letter-to-letter, emitting exactly one output symbol per input symbol.

• initial : σ

  Starting state.

• step : σ → α → σ

  Transition function.

• output : σ → α → β

  Output function: the symbol emitted on reading an input symbol in a state.

theorem Mealy.ext_iff {σ : Type u_4} {α : Type u_5} {β : Type u_6} {x y : Mealy σ α β} : x = y ↔ x.initial = y.initial ∧ x.step = y.step ∧ x.output = y.output

theorem Mealy.ext {σ : Type u_4} {α : Type u_5} {β : Type u_6} {x y : Mealy σ α β} (initial : x.initial = y.initial) (step : x.step = y.step) (output : x.output = y.output) : x = y

@[instance_reducible]

instance instInhabitedMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} [Inhabited σ] [Inhabited β] : Inhabited (Mealy σ α β)

Equations

• instInhabitedMealy = { default := { initial := default, step := fun (x : σ) (x_1 : α) => default, output := fun (x : σ) (x_1 : α) => default } }

def Mealy.stateAfter {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) : List α → σ

T.stateAfter s x is the state reached from s after consuming the input x.

Equations

• T.stateAfter s = List.foldl T.step s

def Mealy.runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : σ → List α → List β

T.runFrom s x runs T on the input x starting from the state s, emitting one output symbol per input symbol.

Equations

• T.runFrom x✝ [] = []
• T.runFrom x✝ (x_2 :: xs) = T.output x✝ x_2 :: T.runFrom (T.step x✝ x_2) xs

def Mealy.run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : List α → List β

T.run x runs T on the input x starting from the state T.initial.

Equations

• T.run = T.runFrom T.initial

def Mealy.runRight {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (xs : List α) : List β

T.runRight x runs T right-to-left on the input x.

Equations

• T.runRight xs = (T.run xs.reverse).reverse

@[simp]

theorem Mealy.runFrom_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) : T.runFrom s [] = []

@[simp]

theorem Mealy.runFrom_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (x : α) (xs : List α) : T.runFrom s (x :: xs) = T.output s x :: T.runFrom (T.step s x) xs

@[simp]

theorem Mealy.stateAfter_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) : T.stateAfter s [] = s

@[simp]

theorem Mealy.stateAfter_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (x : α) (xs : List α) : T.stateAfter s (x :: xs) = T.stateAfter (T.step s x) xs

theorem Mealy.stateAfter_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs ys : List α) : T.stateAfter s (xs ++ ys) = T.stateAfter (T.stateAfter s xs) ys

theorem Mealy.runFrom_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs ys : List α) : T.runFrom s (xs ++ ys) = T.runFrom s xs ++ T.runFrom (T.stateAfter s xs) ys

@[simp]

theorem Mealy.length_runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs : List α) : (T.runFrom s xs).length = xs.length

The run is length-preserving (one output symbol per input symbol).

@[simp]

theorem Mealy.length_run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (xs : List α) : (T.run xs).length = xs.length

@[simp]

theorem Mealy.length_runRight {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (xs : List α) : (T.runRight xs).length = xs.length

@[simp]

theorem Mealy.runRight_reverse {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (xs : List α) : T.runRight xs.reverse = (T.run xs).reverse

@[simp]

theorem Mealy.runRight_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : T.runRight [] = []

@[simp]

theorem Mealy.runRight_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (x : α) (xs : List α) : T.runRight (x :: xs) = T.output (T.stateAfter T.initial xs.reverse) x :: T.runRight xs

The right-to-left pass emits the head output at the state reached over the entire reversed tail: the right scan reads the future.

theorem Mealy.getElem?_runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs : List α) (i : ℕ) : (T.runFrom s xs)[i]? = Option.map (T.output (T.stateAfter s (List.take i xs))) xs[i]?

Output coordinate i of the run is the output at the state reached after the first i input symbols.

theorem Mealy.getElem?_run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (xs : List α) (i : ℕ) : (T.run xs)[i]? = Option.map (T.output (T.stateAfter T.initial (List.take i xs))) xs[i]?

Output coordinate i of T.run is the output at the state reached after the first i input symbols.

Composition

def Mealy.comp {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {σ' : Type u_5} (T₂ : Mealy σ' β γ) (T₁ : Mealy σ α β) : Mealy (σ' × σ) α γ

T₂.comp T₁ feeds the outputs of T₁ to T₂ — the cascade connection of [Hol82] — computing T₂.run ∘ T₁.run.

Equations

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

@[simp]

theorem Mealy.comp_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {σ' : Type u_5} (T₂ : Mealy σ' β γ) (T₁ : Mealy σ α β) (p : σ' × σ) (a : α) : (T₂.comp T₁).step p a = (T₂.step p.1 (T₁.output p.2 a), T₁.step p.2 a)

@[simp]

theorem Mealy.comp_output {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {σ' : Type u_5} (T₂ : Mealy σ' β γ) (T₁ : Mealy σ α β) (p : σ' × σ) (a : α) : (T₂.comp T₁).output p a = T₂.output p.1 (T₁.output p.2 a)

@[simp]

theorem Mealy.comp_initial {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {σ' : Type u_5} (T₂ : Mealy σ' β γ) (T₁ : Mealy σ α β) : (T₂.comp T₁).initial = (T₂.initial, T₁.initial)

@[simp]

theorem Mealy.runFrom_comp {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {σ' : Type u_5} (T₂ : Mealy σ' β γ) (T₁ : Mealy σ α β) (p : σ' × σ) (xs : List α) : (T₂.comp T₁).runFrom p xs = T₂.runFrom p.1 (T₁.runFrom p.2 xs)

@[simp]

theorem Mealy.run_comp {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {σ' : Type u_5} (T₂ : Mealy σ' β γ) (T₁ : Mealy σ α β) : (T₂.comp T₁).run = T₂.run ∘ T₁.run

Letter-wise machines

def Mealy.ofFn {α : Type u_2} {β : Type u_3} (h : α → β) : Mealy Unit α β

The single-state machine applying h to every symbol.

Equations

• Mealy.ofFn h = { initial := (), step := fun (x : Unit) (x_1 : α) => (), output := fun (x : Unit) => h }

@[simp]

theorem Mealy.ofFn_output {α : Type u_2} {β : Type u_3} (h : α → β) (u : Unit) : (ofFn h).output u = h

@[simp]

theorem Mealy.ofFn_run {α : Type u_2} {β : Type u_3} (h : α → β) (xs : List α) : (ofFn h).run xs = List.map h xs

Flag machines

def Mealy.ofFlag {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) : Mealy Bool α β

The Mealy machine whose state is the monotone flag "a symbol satisfying p has occurred".

Equations

• Mealy.ofFlag p out = { initial := false, step := fun (b : Bool) (a : α) => b || p a, output := out }

@[simp]

theorem Mealy.ofFlag_initial {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) : (ofFlag p out).initial = false

@[simp]

theorem Mealy.ofFlag_step {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (b : Bool) (a : α) : (ofFlag p out).step b a = (b || p a)

@[simp]

theorem Mealy.ofFlag_output {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) : (ofFlag p out).output = out

@[simp]

theorem Mealy.ofFlag_stateAfter {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (b : Bool) (xs : List α) : (ofFlag p out).stateAfter b xs = (b || xs.any p)

theorem Mealy.getElem?_ofFlag_run {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (xs : List α) (i : ℕ) : ((ofFlag p out).run xs)[i]? = Option.map (out ((List.take i xs).any p)) xs[i]?

Each coordinate of a flag machine sees the flag over its strict prefix.

theorem Mealy.getElem?_ofFlag_runRight {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (xs : List α) (i : ℕ) : ((ofFlag p out).runRight xs)[i]? = Option.map (out ((List.drop (i + 1) xs).any p)) xs[i]?

Each coordinate of a flag machine run right-to-left sees the flag over its strict suffix.

Transport along state equivalences

def Mealy.map {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : Mealy σ α β) : Mealy τ α β

Transport a Mealy machine along an equivalence on states.

Equations

• Mealy.map g T = { initial := g T.initial, step := fun (t : τ) (x : α) => g (T.step (g.symm t) x), output := fun (t : τ) (x : α) => T.output (g.symm t) x }

@[simp]

theorem Mealy.map_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : Mealy σ α β) (t : τ) (x : α) : (map g T).step t x = g (T.step (g.symm t) x)

@[simp]

theorem Mealy.map_initial {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : Mealy σ α β) : (map g T).initial = g T.initial

@[simp]

theorem Mealy.map_output {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : Mealy σ α β) (t : τ) (x : α) : (map g T).output t x = T.output (g.symm t) x

@[simp]

theorem Mealy.map_refl {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : map (Equiv.refl σ) T = T

@[simp]

theorem Mealy.map_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) {τ : Type u_4} {υ : Type u_5} (g : σ ≃ τ) (h : τ ≃ υ) : map h (map g T) = map (g.trans h) T

@[simp]

theorem Mealy.stateAfter_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) {τ : Type u_4} (g : σ ≃ τ) (t : τ) (xs : List α) : (map g T).stateAfter t xs = g (T.stateAfter (g.symm t) xs)

@[simp]

theorem Mealy.runFrom_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) {τ : Type u_4} (g : σ ≃ τ) (t : τ) (xs : List α) : (map g T).runFrom t xs = T.runFrom (g.symm t) xs

@[simp]

theorem Mealy.run_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) {τ : Type u_4} (g : σ ≃ τ) : (map g T).run = T.run

def Mealy.reindex {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) : Mealy σ α β ≃ Mealy τ α β

map as an equivalence of machines.

Equations

• Mealy.reindex g = { toFun := Mealy.map g, invFun := Mealy.map g.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Mealy.coe_reindex {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) : ⇑(reindex g) = map g

@[simp]

theorem Mealy.symm_reindex {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) : (reindex g).symm = reindex g.symm

The Mealy-computable class

def IsMealyComputable {α : Type u_2} {β : Type u_3} (f : List α → List β) : Prop

The class of functions computed by a finite-state Mealy machine.

Equations

• IsMealyComputable f = ∃ (σ : Type) (x : Fintype σ) (T : Mealy σ α β), T.run = f

theorem isMealyComputable_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsMealyComputable f ↔ ∃ (σ : Type v) (x : Fintype σ) (T : Mealy σ α β), T.run = f

The universe-polymorphic form of IsMealyComputable.

theorem Mealy.isMealyComputable {α : Type u_2} {β : Type u_3} {σ : Type u_4} [Fintype σ] (T : Mealy σ α β) : IsMealyComputable T.run

Every finite-state Mealy computes a Mealy-computable function, whatever the universe of its state type.

theorem IsMealyComputable.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g : List β → List γ} {f : List α → List β} (hg : IsMealyComputable g) (hf : IsMealyComputable f) : IsMealyComputable (g ∘ f)

Mealy-computable functions are closed under composition (Mealy.comp).

theorem isMealyComputable_map {α : Type u_2} {β : Type u_3} (h : α → β) : IsMealyComputable (List.map h)

theorem isMealyComputable_id {α : Type u_2} : IsMealyComputable id

Pulling back acceptors

def DFA.comapMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (M : DFA β τ) (T : Mealy σ α β) : DFA α (σ × τ)

M.comapMealy T pulls the acceptor M back along the transducer T: the product machine runs T and feeds its output symbols to M, so it accepts x if and only if M accepts T.run x.

Equations

• M.comapMealy T = { step := fun (p : σ × τ) (a : α) => (T.step p.1 a, M.step p.2 (T.output p.1 a)), start := (T.initial, M.start), accept := {p : σ × τ | p.2 ∈ M.accept} }

@[simp]

theorem DFA.comapMealy_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (M : DFA β τ) (T : Mealy σ α β) (p : σ × τ) (a : α) : (M.comapMealy T).step p a = (T.step p.1 a, M.step p.2 (T.output p.1 a))

@[simp]

theorem DFA.comapMealy_start {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (M : DFA β τ) (T : Mealy σ α β) : (M.comapMealy T).start = (T.initial, M.start)

@[simp]

theorem DFA.comapMealy_accept {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (M : DFA β τ) (T : Mealy σ α β) : (M.comapMealy T).accept = {p : σ × τ | p.2 ∈ M.accept}

@[simp]

theorem DFA.evalFrom_comapMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (M : DFA β τ) (T : Mealy σ α β) (p : σ × τ) (xs : List α) : (M.comapMealy T).evalFrom p xs = (T.stateAfter p.1 xs, M.evalFrom p.2 (T.runFrom p.1 xs))

@[simp]

theorem DFA.accepts_comapMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (M : DFA β τ) (T : Mealy σ α β) : (M.comapMealy T).accepts = T.run ⁻¹' M.accepts

theorem IsMealyComputable.isRegular_preimage {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsMealyComputable f) {L : Language β} (hL : L.IsRegular) : Language.IsRegular (f ⁻¹' L)

Mealy-computable maps pull back regular languages (DFA.comapMealy).

Causality

theorem Mealy.dependsOn_run_Iic {α : Type u_2} {β : Type u_3} {σ : Type u_4} (T : Mealy σ α β) (i : ℕ) : List.DependsOn (fun (u : List α) => (T.run u)[i]?) (Set.Iic i)

A sequential machine's output coordinate i depends only on the input prefix Set.Iic i.

theorem IsMealyComputable.dependsOn_Iic {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsMealyComputable f) (i : ℕ) : List.DependsOn (fun (u : List α) => (f u)[i]?) (Set.Iic i)

A Mealy-computable map's output coordinate i depends only on the input prefix Set.Iic i.