Lax765601.AperiodicMealy

Aperiodic Mealy machines are exactly the compositions of flip-flops

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

- thm✓Lax765601.AperiodicOfFlipFlops
- thm✓Lax765601.FlipFlopsOfAperiodic
→
thm✓Lax765601.AperiodicMealy
⊢Lax765601Proofs.Results.aperiodic_iff_compClosure_flipFlop

In the paper

page 28 of the paper of lax-157538, Transducers

Theorem

A function computed by a Mealy machine is aperiodic if and only if it is computed by a composition of flip-flop Mealy machines (Theorem A.2.8 of Transducers). This answers the question what the class $(\mathrm{Flip\text{-}flop})^*$ of compositions of one kind of prime is; for the other kind, $(\mathrm{Reversible})^*$ is the class of reversible machines (Lemma A.2.6).

The two implications are separate results, each with its own proof: $AperiodicOfFlipFlops$ (a composition of flip-flops is aperiodic) and $FlipFlopsOfAperiodic$ (an aperiodic Mealy function decomposes into flip-flops); this statement is their conjunction.

Lean source view on GitHub

1	import Lax765601.PrimeMealyMachines
2	import Lax765601.Aperiodicity
3
4	/-!
5	---
6	title: Aperiodic Mealy machines are exactly the compositions of flip-flops
7	type: theorem
8	---
9	A function computed by a Mealy machine is aperiodic if and only if it is
10	computed by a composition of flip-flop Mealy machines (Theorem A.2.8 of
11	Transducers). This answers the question what the class
12	$(\mathrm{Flip\text{-}flop})^*$ of compositions of one kind of prime is; for the
13	other kind, $(\mathrm{Reversible})^*$ is the class of reversible machines
14	(Lemma A.2.6).
15
16	The two implications are separate results, each with its own proof:
17	`AperiodicOfFlipFlops` (a composition of flip-flops is aperiodic) and
18	`FlipFlopsOfAperiodic` (an aperiodic Mealy function decomposes into flip-flops);
19	this statement is their conjunction.
20
21	# Formalization notes
22
23	The theorem in the book ends with the sentence "moreover, this property can be
24	decided, given a Mealy machine that computes $f$ ". That sentence is not
25	formalised: the characterisation the book's decision procedure rests on, Lemma
26	A.2.11, is, but the enumeration of the state transformations arising from input
27	strings that turns it into an algorithm is not written down. Both alphabets are
28	assumed finite.
29	-/
30
31	namespace Lax765601.AperiodicMealy
32
33	open Lax765601.MealyMachine Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax765601.Aperiodicity
34
35	/-- A function computed by a Mealy machine is aperiodic if and only if it is a
36	composition of flip-flop Mealy machines. -/
37	axiom aperiodic_iff_compClosure_flipFlop {A B : Type} [Finite A] [Finite B]
38	{f : List A → List B} (hf : IsMealy f) :
39	Aperiodic f ↔ CompClosure FlipFlopFam A B f
40
41	end Lax765601.AperiodicMealy
42

Show Proof

Formalization notes

The theorem in the book ends with the sentence "moreover, this property can be decided, given a Mealy machine that computes $f$ ". That sentence is not formalised: the characterisation the book's decision procedure rests on, Lemma A.2.11, is, but the enumeration of the state transformations arising from input strings that turns it into an algorithm is not written down. Both alphabets are assumed finite.

Builds on

Used by

none

From Mathlib

none

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