Lax Lean Archive

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

Lax916827.TwoWayMealyPrecomposition

Two-way transducers are closed under pre-composition with Mealy machines

concepts/Lax916827/TwoWayMealyPrecomposition.lean · lax-916827

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

    Functions computed by two-way transducers are closed under pre-composition with Mealy machines (Lemma C.2.6 of Transducers). By the Krohn–Rhodes theorem it suffices to pre-compose with a reversible and with a flip-flop machine: a reversible machine can be run backwards, so its state at the head can be maintained when the head moves left; a flip-flop machine's state at a position is determined by the last resetting letter before it, which the two-way transducer finds by a detour to the left.

    Lean source view on GitHub

    1import Lax765601.MealyMachine
    2import Lax916827.TwoWayTransducers
    3
    4/-!
    5---
    6title: Two-way transducers are closed under pre-composition with Mealy machines
    7type: theorem
    8---
    9Functions computed by two-way transducers are closed under pre-composition with
    10Mealy machines (Lemma C.2.6 of *Transducers*). By the Krohn–Rhodes theorem it
    11suffices to pre-compose with a reversible and with a flip-flop machine: a
    12reversible machine can be run backwards, so its state at the head can be
    13maintained when the head moves left; a flip-flop machine's state at a position
    14is determined by the last resetting letter before it, which the two-way
    15transducer finds by a detour to the left.
    16
    17# Formalization notes
    18
    19All three alphabets are assumed finite, as in the book.
    20-/
    21
    22namespace Lax916827.TwoWayMealyPrecomposition
    23
    24open Lax765601.MealyMachine Lax916827.TwoWayTransducers
    25
    26/-- Pre-composing a two-way transducer with a Mealy machine gives a two-way
    27transducer. -/
    28axiom isTwoWay_comp_isMealy {A B C : Type} [Finite A] [Finite B] [Finite C]
    29 {f : List A → List B} {g : List B → List C} (hf : IsMealy f) (hg : IsTwoWay g) :
    30 IsTwoWay (g ∘ f)
    31
    32end Lax916827.TwoWayMealyPrecomposition
    33
    Show Proof

    Formalization notes

    All three alphabets are assumed finite, as in the book.

    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…