Lax765601.MealyEquivalenceBound

Decidable equivalence of Mealy machines

concepts/Lax765601/MealyEquivalenceBound.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.MealyEquivalenceBound

⊢Lax765601Proofs.Results.eval_eq_iff_short

In the paper

page 14 of the paper of lax-157538, Transducers

Theorem

The equivalence problem for Mealy machines — do two given machines compute the same function? — is decidable (Theorem A.1.2 of Transducers). The book reduces it to the equivalence of regular languages: a letter-to-letter function is determined by the languages "the last output letter is $b$ ", one for each output letter $b$ , and each of them is recognised by the automaton underlying the machine. In the form stated here, two Mealy machines with $n_1$ and $n_2$ states are equivalent if and only if they agree on all input strings of length at most $n_1 n_2$ — a finite check, since the alphabet is finite.

Lean source view on GitHub

1	import Mathlib.SetTheory.Cardinal.Finite
2	import Lax765601.MealyMachine
3
4	/-!
5	---
6	title: Decidable equivalence of Mealy machines
7	type: theorem
8	---
9	The equivalence problem for Mealy machines — do two given machines compute the
10	same function? — is decidable (Theorem A.1.2 of Transducers). The book reduces
11	it to the equivalence of regular languages: a letter-to-letter function is
12	determined by the languages "the last output letter is $b$ ", one for each output
13	letter $b$ , and each of them is recognised by the automaton underlying the
14	machine. In the form stated here, two Mealy machines with $n_1$ and $n_2$ states
15	are equivalent if and only if they agree on all input strings of length at most
16	$n_1 n_2$ — a finite check, since the alphabet is finite.
17
18	# Formalization notes
19
20	Decidability is expressed by its mathematical content, the finite check, rather
21	than by a decision procedure on encodings of machines: the product of the numbers
22	of states bounds the length of a shortest input on which two inequivalent
23	machines differ, because a pair of runs that repeats a pair of states can be
24	shortened by cutting out the loop. `Nat.card Q` is the number of states of a
25	finite state space. The statement holds over any input alphabet, finite or not;
26	finiteness of the alphabet is what makes the check a finite one.
27	-/
28
29	namespace Lax765601.MealyEquivalenceBound
30
31	open Lax765601.MealyMachine
32
33	/-- Two Mealy machines are equivalent if and only if they agree on every input
34	string of length at most the product of their numbers of states. -/
35	axiom eval_eq_iff_short {A B Q₁ Q₂ : Type} [Finite Q₁] [Finite Q₂]
36	(M : Mealy A B Q₁) (N : Mealy A B Q₂) :
37	M.eval = N.eval ↔
38	∀ w : List A, w.length ≤ Nat.card Q₁ * Nat.card Q₂ → M.eval w = N.eval w
39
40	end Lax765601.MealyEquivalenceBound
41

Show Proof

Formalization notes

Decidability is expressed by its mathematical content, the finite check, rather than by a decision procedure on encodings of machines: the product of the numbers of states bounds the length of a shortest input on which two inequivalent machines differ, because a pair of runs that repeats a pair of states can be shortened by cutting out the loop. $Nat.card Q$ is the number of states of a finite state space. The statement holds over any input alphabet, finite or not; finiteness of the alphabet is what makes the check a finite one.

Builds on

Lax765601.MealyMachine

Used by

none

From Mathlib

Mathlib.SetTheory.Cardinal.Finite

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