Lax Lean Archive

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

Lax132576.MealyDecidable

Deciding whether a rational function is a Mealy machine

concepts/Lax132576/MealyDecidable.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

    One can decide whether a given rational function is computed by a Mealy machine (Theorem B.4.2 of Transducers). By Theorem B.4.1 it suffices to check the three properties of a Mealy function: continuity is automatic for a rational function, length preservation is decided by Lemma B.4.3, and after Lemma B.4.5 has put the automaton in a form where every transition reads and writes one letter, prefix preservation fails exactly when two transitions with the same input letter and different output letters start in states reachable by a common input string.

    Lean source view on GitHub

    1import Lax765601.MealyMachine
    2import Lax132576.TransducerCodes
    3
    4/-!
    5---
    6title: Deciding whether a rational function is a Mealy machine
    7type: theorem
    8---
    9One can decide whether a given rational function is computed by a Mealy
    10machine (Theorem B.4.2 of *Transducers*). By Theorem B.4.1 it suffices to check
    11the three properties of a Mealy function: continuity is automatic for a
    12rational function, length preservation is decided by Lemma B.4.3, and after
    13Lemma B.4.5 has put the automaton in a form where every transition reads and
    14writes one letter, prefix preservation fails exactly when two transitions with
    15the same input letter and different output letters start in states reachable
    16by a common input string.
    17
    18# Formalization notes
    19
    20The function is given by a functional code, and the decided property is that
    21some function computed by a Mealy machine agrees with the coded relation on
    22the code words: a code reads only the letters of its alphabet, so the
    23comparison is relativised to `CodeWord c` — without the relativisation the
    24property would be false for every code and the statement empty. The proof
    25reduces prefix preservation to the equality of two rational functions, decided
    26by Theorem B.3.4.
    27-/
    28
    29namespace Lax132576.MealyDecidable
    30
    31open Lax765601.MealyMachine Lax132576.TransducerCodes
    32
    33/-- Whether a coded rational function is computed by a Mealy machine is decidable.
    34-/
    35axiom decidable_isMealy :
    36 DecidableUnderPromise CodeFunctional
    37 (fun c => ∃ f : List ℕ → List ℕ,
    38 (∀ w, CodeWord c w → ∀ v, (codeRel c w v ↔ v = f w)) ∧ IsMealy f)
    39
    40end Lax132576.MealyDecidable
    41
    Show Proof

    Formalization notes

    The function is given by a functional code, and the decided property is that some function computed by a Mealy machine agrees with the coded relation on the code words: a code reads only the letters of its alphabet, so the comparison is relativised to CodeWordcCodeWord c — without the relativisation the property would be false for every code and the statement empty. The proof reduces prefix preservation to the equality of two rational functions, decided by Theorem B.3.4.

    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…