Lax Lean Archive

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

Lax765601.MealyComposition

Mealy machines are closed under composition

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

    If f:A∗→B∗f : A^* \to B^* and g:B∗→C∗g : B^* \to C^* are computed by Mealy machines, then so is their composition A∗→fB∗→gC∗A^* \xrightarrow{f} B^* \xrightarrow{g} C^* (Theorem A.1.3 of Transducers). The proof is a product construction: the composed machine runs both machines in lockstep, feeding each output letter of the first to the second, so its state space is the product of the two state spaces.

    Lean source view on GitHub

    1import Lax765601.MealyMachine
    2
    3/-!
    4---
    5title: Mealy machines are closed under composition
    6type: theorem
    7---
    8If f:A∗→B∗f : A^* \to B^* and g:B∗→C∗g : B^* \to C^* are computed by Mealy machines, then
    9so is their composition A∗→fB∗→gC∗A^* \xrightarrow{f} B^* \xrightarrow{g} C^* (Theorem
    10A.1.3 of *Transducers*). The proof is a product construction: the composed
    11machine runs both machines in lockstep, feeding each output letter of the first
    12to the second, so its state space is the product of the two state spaces.
    13
    14# Formalization notes
    15
    16The book writes the composition as f⋅gf \cdot g, first ff then gg; in Lean it is
    17`g ∘ f`. The intermediate alphabet is required to be finite, as in the closure
    18under composition of `CompositionClosure`; nothing is assumed of the outer
    19alphabets.
    20-/
    21
    22namespace Lax765601.MealyComposition
    23
    24open Lax765601.MealyMachine
    25
    26/-- The composition of two functions computed by Mealy machines is computed by a
    27Mealy machine. -/
    28axiom isMealy_comp {A B C : Type} [Finite B] {f : List A → List B} {g : List B → List C}
    29 (hf : IsMealy f) (hg : IsMealy g) : IsMealy (g ∘ f)
    30
    31end Lax765601.MealyComposition
    32
    Show Proof

    Formalization notes

    The book writes the composition as f⋅gf \cdot g, first ff then gg; in Lean it is g∘fg ∘ f. The intermediate alphabet is required to be finite, as in the closure under composition of CompositionClosureCompositionClosure; nothing is assumed of the outer alphabets.

    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…