Lax Lean Archive

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

Lax132576.MealyMachineIndependent

Machine-independent characterisation of Mealy machines

concepts/Lax132576/MealyMachineIndependent.lean · lax-132576

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

    A function f:A∗→B∗f : A^* \to B^* is computed by a Mealy machine if and only if it is (a) continuous, (b) prefix preserving, and (c) length preserving (Theorem B.4.1 of Transducers). A Mealy machine clearly has the three properties; conversely, for every output letter bb the language of inputs whose output ends with bb is regular by continuity, each input position contributes exactly one output letter by prefix and length preservation, and the product of the automata of these languages is the state space of a Mealy machine computing ff.

    Lean source view on GitHub

    1import Lax765601.Continuity
    2import Lax765601.ElementaryProperties
    3import Lax765601.MealyMachine
    4
    5/-!
    6---
    7title: Machine-independent characterisation of Mealy machines
    8type: theorem
    9---
    10A function f:A∗→B∗f : A^* \to B^* is computed by a Mealy machine if and only if it is
    11(a) continuous, (b) prefix preserving, and (c) length preserving (Theorem
    12B.4.1 of *Transducers*). A Mealy machine clearly has the three properties;
    13conversely, for every output letter bb the language of inputs whose output
    14ends with bb is regular by continuity, each input position contributes exactly
    15one output letter by prefix and length preservation, and the product of the
    16automata of these languages is the state space of a Mealy machine computing
    17ff.
    18
    19# Formalization notes
    20
    21Both alphabets are assumed finite: the product over the output letters is a
    22finite product. The three properties are those of `Lax765601.Continuity` and
    23`Lax765601.ElementaryProperties`.
    24-/
    25
    26namespace Lax132576.MealyMachineIndependent
    27
    28open Lax765601.Continuity Lax765601.ElementaryProperties Lax765601.MealyMachine
    29
    30/-- A function is computed by a Mealy machine if and only if it is continuous,
    31prefix preserving and length preserving. -/
    32axiom isMealy_iff {A B : Type} [Finite A] [Finite B] (f : List A → List B) :
    33 IsMealy f ↔ Continuous f ∧ PrefixPreserving f ∧ LengthPreserving f
    34
    35end Lax132576.MealyMachineIndependent
    36
    Show Proof

    Formalization notes

    Both alphabets are assumed finite: the product over the output letters is a finite product. The three properties are those of Lax765601.ContinuityLax765601.Continuity and Lax765601.ElementaryPropertiesLax765601.ElementaryProperties.

    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…