Lax Lean Archive

Prime Mealy machines: reversible and flip-flop

Lax765601.PrimeMealyMachines · concepts/Lax765601/PrimeMealyMachines.lean · lax-765601

definition

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.

    Natural Language Statement

    Definition

    The prime Mealy machines are defined in terms of the state transformations of their letters (Definition A.2.1 of Transducers). There are two kinds.

    • Reversible machines: the state transformation of every letter is a permutation of the state space.
    • Flip-flop machines: the state transformation of every letter is either the identity or a constant, all states being mapped to the same one.

    A one-state machine is both. The machine outputting abab⋯abab\cdots on ana^n is reversible; the delay machine, which shifts the input one position to the right, is a flip-flop. Since composing permutations gives a permutation and composing constants gives a constant, nothing changes if the definition is phrased for the state transformations of input strings rather than of letters.

    The Krohn–Rhodes theorem (Theorem A.2.2) says that every Mealy machine is a composition of prime Mealy machines; Theorem A.2.8 characterises the compositions of flip-flops alone.

    Concept map
    3 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    Lean source view on GitHub

    1import Mathlib.Logic.Function.Defs
    2import Lax765601.MealyMachine
    3import Lax765601.CompositionClosure
    4
    5/-!
    6---
    7title: Prime Mealy machines: reversible and flip-flop
    8type: definition
    9---
    10The *prime Mealy machines* are defined in terms of the state transformations of
    11their letters (Definition A.2.1 of *Transducers*). There are two kinds.
    12
    13* *Reversible* machines: the state transformation of every letter is a
    14 permutation of the state space.
    15* *Flip-flop* machines: the state transformation of every letter is either the
    16 identity or a constant, all states being mapped to the same one.
    17
    18A one-state machine is both. The machine outputting abab⋯abab\cdots on ana^n is
    19reversible; the delay machine, which shifts the input one position to the right,
    20is a flip-flop. Since composing permutations gives a permutation and composing
    21constants gives a constant, nothing changes if the definition is phrased for the
    22state transformations of input strings rather than of letters.
    23
    24The Krohn–Rhodes theorem (Theorem A.2.2) says that every Mealy machine is a
    25composition of prime Mealy machines; Theorem A.2.8 characterises the compositions
    26of flip-flops alone.
    27
    28# Formalization notes
    29
    30`Reversible` and `FlipFlop` are properties of a machine. The families that the
    31composition closure is taken over are families of *functions* (as in
    32`CompositionClosure`), so a function is a prime if it is computed by some prime
    33machine with a finite state space: `PrimeMealyFam` collects the reversible and
    34the flip-flop functions, and `FlipFlopFam` the flip-flop ones alone, for
    35Theorem A.2.8. Bijectivity is mathlib's `Function.Bijective`.
    36-/
    37
    38namespace Lax765601.PrimeMealyMachines
    39
    40open Lax765601.MealyMachine Lax765601.CompositionClosure
    41
    42/-- A Mealy machine is reversible if the state transformation of every letter is a
    43permutation of the state space. -/
    44def Reversible {A B Q : Type} (M : Mealy A B Q) : Prop :=
    45 ∀ a : A, Function.Bijective (M.letterTrans a)
    46
    47/-- A Mealy machine is a flip-flop if the state transformation of every letter is
    48the identity or a constant. -/
    49def FlipFlop {A B Q : Type} (M : Mealy A B Q) : Prop :=
    50 ∀ a : A, M.letterTrans a = id ∨ ∃ q₀ : Q, ∀ q : Q, M.letterTrans a q = q₀
    51
    52/-- A function is computed by a reversible Mealy machine with a finite state
    53space. -/
    54def IsReversibleMealy {A B : Type} (f : List A → List B) : Prop :=
    55 ∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ Reversible M
    56
    57/-- A function is computed by a flip-flop Mealy machine with a finite state
    58space. -/
    59def IsFlipFlopMealy {A B : Type} (f : List A → List B) : Prop :=
    60 ∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ FlipFlop M
    61
    62/-- The family of prime Mealy machines: the functions computed by a reversible or
    63by a flip-flop machine. -/
    64def PrimeMealyFam : Family := fun _ _ f => IsReversibleMealy f ∨ IsFlipFlopMealy f
    65
    66/-- The family of flip-flop Mealy machines. -/
    67def FlipFlopFam : Family := fun _ _ f => IsFlipFlopMealy f
    68
    69end Lax765601.PrimeMealyMachines
    70
    Formalization notes

    ReversibleReversible and FlipFlopFlipFlop are properties of a machine. The families that the composition closure is taken over are families of functions (as in CompositionClosureCompositionClosure), so a function is a prime if it is computed by some prime machine with a finite state space: PrimeMealyFamPrimeMealyFam collects the reversible and the flip-flop functions, and FlipFlopFamFlipFlopFam the flip-flop ones alone, for Theorem A.2.8. Bijectivity is mathlib's Function.BijectiveFunction.Bijective.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…