Myhill–Nerode theorems for transducers

This file characterizes the Mealy-computable (sequential) and bimachine-computable functions by their residuals, in the style of Mathlib.Computability.MyhillNerode (which treats the language case).

Given f : List α → List β and a word u, the residual of f by u is the function v ↦ (f (u ++ v)).drop u.length — what f appends after reading u — and the coresidual of f by a suffix y is u ↦ (f (u ++ y)).take u.length — what f emits before reaching y. A function is Mealy-computable if and only if it is length-preserving, prefix-preserving, and has finitely many residuals — the Nerode criterion for sequential functions ([Eil74] [Hol82]). A function is bimachine-computable if and only if it is length-preserving with finitely many residuals and finitely many coresiduals: residual classes are the left states, coresidual classes the right states, and the two-step exchange through representatives makes the cell output well-defined — the length-preserving stratum of the canonical bimachine of [RS91], surveyed in [FR16].

Main definitions

• residual f u: the residual of f by the word u
• coresidual f y: the coresidual of f by the suffix y

Main theorems

• isMealyComputable_of_stateSummary: a finite left-congruent state summary determining the output yields a machine
• isMealyComputable_iff_residual: f is Mealy-computable if and only if it is length-preserving, prefix-preserving, and Set.range (residual f) is finite
• isLengthPreservingBimachineComputable_iff_residual: f is bimachine-computable if and only if it is length-preserving and both Set.range (residual f) and Set.range (coresidual f) are finite

[UPSTREAM] candidate: Mathlib.Computability.MyhillNerode (as transducer sections of the existing file, with residual beside Language.leftQuotient).

def residual {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) : List α → List β

The residual of f by u is what f appends after reading u — the analogue for string functions of Language.leftQuotient.

Equations

• residual f u v = List.drop u.length (f (u ++ v))

@[simp]

theorem residual_nil {α : Type u_1} {β : Type u_2} (f : List α → List β) : residual f [] = f

theorem residual_append {α : Type u_1} {β : Type u_2} (f : List α → List β) (u v : List α) : residual f (u ++ v) = residual (residual f u) v

theorem residual_append_singleton {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) (x : α) : residual f (u ++ [x]) = fun (v : List α) => List.drop 1 (residual f u (x :: v))

theorem Mealy.residual_run {α : Type u_1} {β : Type u_2} {σ : Type u_3} (T : Mealy σ α β) (u : List α) : residual T.run u = T.runFrom (T.stateAfter T.initial u)

Residuals of a machine's run factor through its states.

Necessity

theorem IsMealyComputable.length_eq {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) (xs : List α) : (f xs).length = xs.length

theorem IsMealyComputable.isPrefix {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) (u v : List α) : f u <+: f (u ++ v)

theorem IsMealyComputable.finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) : (Set.range (residual f)).Finite

Sufficiency

theorem isMealyComputable_of_stateSummary {α : Type u_1} {β : Type u_2} {f : List α → List β} {σ : Type u_3} [Fintype σ] (state : List α → σ) (δ : σ → α → σ) (out : σ → α → β) (hδ : ∀ (u : List α) (x : α), state (u ++ [x]) = δ (state u) x) (hout : ∀ (u : List α) (x : α) (w : List α), (f (u ++ x :: w))[u.length]? = some (out (state u) x)) (hlen : ∀ (xs : List α), (f xs).length = xs.length) : IsMealyComputable f

A length-preserving f with a finite state : List α → σ that is left-congruent (hδ) and determines f's output at each position (hout) is Mealy-computable.

theorem isMealyComputable_of_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hlen : ∀ (xs : List α), (f xs).length = xs.length) (hpre : ∀ (u v : List α), f u <+: f (u ++ v)) (hfin : (Set.range (residual f)).Finite) : IsMealyComputable f

A length-preserving, prefix-preserving function with finitely many residuals is Mealy-computable: the residuals themselves are the states.

theorem isMealyComputable_iff_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsMealyComputable f ↔ (∀ (xs : List α), (f xs).length = xs.length) ∧ (∀ (u v : List α), f u <+: f (u ++ v)) ∧ (Set.range (residual f)).Finite

Myhill–Nerode for Mealy machines: a function is Mealy-computable if and only if it is length-preserving, prefix-preserving, and has finitely many residuals.

Coresiduals

def coresidual {α : Type u_1} {β : Type u_2} (f : List α → List β) (y : List α) : List α → List β

The coresidual of f by the suffix y is what f emits before reaching y — the right-context dual of residual.

Equations

• coresidual f y u = List.take u.length (f (u ++ y))

theorem coresidual_cons {α : Type u_1} {β : Type u_2} (f : List α → List β) (x : α) (y : List α) : coresidual f (x :: y) = fun (u : List α) => List.take u.length (coresidual f y (u ++ [x]))

Coresiduals step by prepending a letter — the right-to-left congruence.

theorem getElem?_residual_cons {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) (x : α) (w : List α) : (residual f u (x :: w))[0]? = (f (u ++ x :: w))[u.length]?

The cell at the seam, read through the residual.

theorem getElem?_coresidual_append {α : Type u_1} {β : Type u_2} (f : List α → List β) (u : List α) (x : α) (w : List α) : (coresidual f w (u ++ [x]))[u.length]? = (f (u ++ x :: w))[u.length]?

The cell at the seam, read through the coresidual.

Myhill–Nerode for bimachines

theorem Bimachine.lState_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (u v : List α) : B.lState (u ++ v) = B.lStateAfter (B.lState u) v

Scanning past a prefix reseeds the left state.

theorem Bimachine.rState_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (u y : List α) : B.rState (u ++ y) = { lInit := B.lInit, lStep := B.lStep, rInit := B.rState y, rStep := B.rStep, output := B.output }.rState u

A pending suffix reseeds the right state.

theorem Bimachine.drop_runFrom_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (l : L) (x v : List α) : List.drop x.length (B.runFrom l (x ++ v)) = B.runFrom (B.lStateAfter l x) v

Dropping a scanned prefix of a letter-to-letter bimachine run reseeds the left state.

theorem Bimachine.take_runFrom_append {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (l : L) (u y : List α) : List.take u.length (B.runFrom l (u ++ y)) = { lInit := B.lInit, lStep := B.lStep, rInit := B.rState y, rStep := B.rStep, output := B.output }.runFrom l u

Taking the unscanned prefix of a bimachine run reseeds the right state.

theorem Bimachine.residual_run {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (x : List α) : residual B.run x = B.runFrom (B.lState x)

Residuals of a bimachine's run reseed the left automaton.

theorem Bimachine.coresidual_run {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (w : B.LetterToLetter) (y : List α) : coresidual B.run y = { lInit := B.lInit, lStep := B.lStep, rInit := B.rState y, rStep := B.rStep, output := B.output }.run

Coresiduals of a bimachine's run reseed the right automaton.

Necessity

theorem IsLengthPreservingBimachineComputable.finite_range_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsLengthPreservingBimachineComputable f) : (Set.range (residual f)).Finite

theorem IsLengthPreservingBimachineComputable.finite_range_coresidual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsLengthPreservingBimachineComputable f) : (Set.range (coresidual f)).Finite

Sufficiency

theorem isLengthPreservingBimachineComputable_of_stateSummaries {α : Type u_1} {β : Type u_2} {f : List α → List β} {L : Type u_5} {R : Type u_6} [Fintype L] [Fintype R] (stateL : List α → L) (δL : L → α → L) (stateR : List α → R) (δR : R → α → R) (out : L → α → R → β) (hδL : ∀ (u : List α) (x : α), stateL (u ++ [x]) = δL (stateL u) x) (hδR : ∀ (x : α) (w : List α), stateR (x :: w) = δR (stateR w) x) (hout : ∀ (u : List α) (x : α) (w : List α), (f (u ++ x :: w))[u.length]? = some (out (stateL u) x (stateR w))) (hlen : ∀ (xs : List α), (f xs).length = xs.length) : IsLengthPreservingBimachineComputable f

A length-preserving f with finite left and right summaries, congruent in their respective scan directions and jointly determining each output cell, is bimachine-computable.

theorem isLengthPreservingBimachineComputable_of_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} (hlen : ∀ (xs : List α), (f xs).length = xs.length) (hfinL : (Set.range (residual f)).Finite) (hfinR : (Set.range (coresidual f)).Finite) : IsLengthPreservingBimachineComputable f

A length-preserving function with finitely many residuals and coresiduals is bimachine-computable: residual classes are the left states, coresidual classes the right states, and the cell output is read off representatives — well-defined by exchanging one context at a time.

theorem isLengthPreservingBimachineComputable_iff_residual {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsLengthPreservingBimachineComputable f ↔ (∀ (xs : List α), (f xs).length = xs.length) ∧ (Set.range (residual f)).Finite ∧ (Set.range (coresidual f)).Finite

Myhill–Nerode for bimachines: a function is bimachine-computable if and only if it is length-preserving with finitely many residuals and finitely many coresiduals.