Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax765601.KrohnRhodes

The Krohn–Rhodes decomposition theorem

concepts/Lax765601/KrohnRhodes.lean · lax-765601

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    Every Mealy machine ff admits a decomposition

    f=f1⋅f2⋯fnf = f_1 \cdot f_2 \cdots f_n

    in which each Mealy machine f1,…,fnf_1, \ldots, f_n is either reversible or flip-flop (Theorem A.2.2 of Transducers, the Krohn–Rhodes theorem). No uniqueness is claimed. Since Mealy machines are closed under composition, the class of functions computed by Mealy machines is exactly the closure under composition of the prime Mealy machines,

    Mealy=(Reversible∪Flip-flop)∗.\mathrm{Mealy} = (\mathrm{Reversible} \cup \mathrm{Flip\text{-}flop})^*.

    The proof of the book has two steps: map lifting is compatible with decompositions into primes (Lemma A.2.4), and the state transformation transducer of every pre-automaton is a composition of primes (Lemma A.2.5), by an induction on the number of states and the number of letters whose state transformation is not a permutation; the output of the machine is then recovered from the state transformations of the prefixes by a delay machine and a letter-to-letter homomorphism.

    Lean source view on GitHub

    1import Lax765601.PrimeMealyMachines
    2
    3/-!
    4---
    5title: The Krohn–Rhodes decomposition theorem
    6type: theorem
    7---
    8Every Mealy machine ff admits a decomposition
    9f=f1⋅f2⋯fnf = f_1 \cdot f_2 \cdots f_n
    10in which each Mealy machine f1,…,fnf_1, \ldots, f_n is either reversible or flip-flop
    11(Theorem A.2.2 of *Transducers*, the Krohn–Rhodes theorem). No uniqueness is
    12claimed. Since Mealy machines are closed under composition, the class of
    13functions computed by Mealy machines is exactly the closure under composition of
    14the prime Mealy machines,
    15Mealy=(Reversible∪Flip-flop)∗.\mathrm{Mealy} = (\mathrm{Reversible} \cup \mathrm{Flip\text{-}flop})^*.
    16
    17The proof of the book has two steps: map lifting is compatible with
    18decompositions into primes (Lemma A.2.4), and the state transformation
    19transducer of every pre-automaton is a composition of primes (Lemma A.2.5), by an
    20induction on the number of states and the number of letters whose state
    21transformation is not a permutation; the output of the machine is then recovered
    22from the state transformations of the prefixes by a delay machine and a
    23letter-to-letter homomorphism.
    24
    25# Formalization notes
    26
    27The conclusion is membership in the composition closure of the family of prime
    28Mealy machines, `CompClosure PrimeMealyFam`, with finite intermediate alphabets
    29built into the closure. Both alphabets are assumed finite, as in the book, where
    30finiteness of the input alphabet is what the induction on the number of letters
    31uses. The converse inclusion, that a composition of primes is computed by a
    32Mealy machine, is closure under composition (Theorem A.1.3) and is not part of
    33this statement.
    34-/
    35
    36namespace Lax765601.KrohnRhodes
    37
    38open Lax765601.MealyMachine Lax765601.CompositionClosure Lax765601.PrimeMealyMachines
    39
    40/-- Every function computed by a Mealy machine is a composition of reversible and
    41flip-flop Mealy machines. -/
    42axiom compClosure_primeMealy_of_isMealy {A B : Type} [Finite A] [Finite B]
    43 {f : List A → List B} (hf : IsMealy f) : CompClosure PrimeMealyFam A B f
    44
    45end Lax765601.KrohnRhodes
    46
    Show Proof

    Formalization notes

    The conclusion is membership in the composition closure of the family of prime Mealy machines, CompClosurePrimeMealyFamCompClosure PrimeMealyFam, with finite intermediate alphabets built into the closure. Both alphabets are assumed finite, as in the book, where finiteness of the input alphabet is what the induction on the number of letters uses. The converse inclusion, that a composition of primes is computed by a Mealy machine, is closure under composition (Theorem A.1.3) and is not part of this statement.

    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…