Lax765601.MealyDerivatives

Myhill–Nerode for Mealy machines

concepts/Lax765601/MealyDerivatives.lean · lax-765601

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax765601.MealyDerivatives

⊢Lax765601Proofs.Results.isMealy_iff_derivatives

In the paper

page 29 of the paper of lax-157538, Transducers

Theorem

A string-to-string function is computed by a Mealy machine if and only if (1) it has finitely many derivatives, (2) it is letter-to-letter, and (3) its $n$ -th output letter depends only on the first $n$ input letters (Lemma A.2.10 of Transducers). From a machine, the derivative $f(w\_)$ is determined by the state reached after reading $w$ , so there are finitely many. Conversely, the minimal machine of $f$ has the derivatives as its states, the derivative of the empty string as initial state, and the transitions

f(w\_) \xrightarrow{a\,/\,\text{last letter of } f(wa)} f(wa\_),

which are well defined because the output letter and the target depend only on the derivative $f(w\_)$ and not on $w$ .

Lean source view on GitHub

1	import Mathlib.Data.Set.Finite.Basic
2	import Lax765601.MealyMachine
3	import Lax765601.ElementaryProperties
4	import Lax765601.Derivatives
5
6	/-!
7	---
8	title: Myhill–Nerode for Mealy machines
9	type: theorem
10	---
11	A string-to-string function is computed by a Mealy machine if and only if (1) it
12	has finitely many derivatives, (2) it is letter-to-letter, and (3) its $n$ -th
13	output letter depends only on the first $n$ input letters (Lemma A.2.10 of
14	Transducers). From a machine, the derivative $f(w\_)$ is determined by the
15	state reached after reading $w$ , so there are finitely many. Conversely, the
16	minimal machine of $f$ has the derivatives as its states, the derivative of the
17	empty string as initial state, and the transitions
18	$f(w\_) \xrightarrow{a\,/\,\text{last letter of } f(wa)} f(wa\_),$
19	which are well defined because the output letter and the target depend only on
20	the derivative $f(w\_)$ and not on $w$ .
21
22	# Formalization notes
23
24	Condition (3) is `PrefixDetermined f`, "the first `n` output letters depend only
25	on the first `n` input letters", which for a letter-to-letter function says
26	exactly that the `n`-th output letter depends only on the first `n` input
27	letters. The set of derivatives is the range of `deriv f`, and its finiteness is
28	mathlib's `Set.Finite`. No finiteness of the alphabets is assumed: the states of
29	the minimal machine are the derivatives, whatever the alphabets.
30	-/
31
32	namespace Lax765601.MealyDerivatives
33
34	open Lax765601.MealyMachine Lax765601.ElementaryProperties Lax765601.Derivatives
35
36	/-- A function is computed by a Mealy machine if and only if it has finitely many
37	derivatives, is letter-to-letter, and its first `n` output letters depend only on
38	its first `n` input letters. -/
39	axiom isMealy_iff {A B : Type} (f : List A → List B) :
40	IsMealy f ↔ (Set.range (deriv f)).Finite ∧ LengthPreserving f ∧ PrefixDetermined f
41
42	end Lax765601.MealyDerivatives
43

Show Proof

Formalization notes

Condition (3) is $PrefixDetermined f$ , "the first $n$ output letters depend only on the first $n$ input letters", which for a letter-to-letter function says exactly that the $n$ -th output letter depends only on the first $n$ input letters. The set of derivatives is the range of $deriv f$ , and its finiteness is mathlib's $Set.Finite$ . No finiteness of the alphabets is assumed: the states of the minimal machine are the derivatives, whatever the alphabets.

Builds on

Used by

none

From Mathlib

Mathlib.Data.Set.Finite.Basic

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive