Lax Lean Archive

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

Lax132576.RationalOfBimachine

Bimachines compute rational functions

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

    Every function computed by a bimachine is rational: the implication (3) ⇒ (1) of Theorem B.2.3 of Transducers, the easiest one. The nondeterministic automaton guesses the runs of both the prefix and the suffix automaton, its states being pairs of their states plus one extra final state; a transition on the letter aa from (p,q)(p, q) to (p′,q′)(p', q') requires p→ap′p \xrightarrow{a} p' in the prefix automaton and q′→aqq' \xrightarrow{a} q in the suffix automaton and outputs the piece of the gap to the left of aa, and an empty transition into the final state outputs the piece of the last gap.

    Lean source view on GitHub

    1import Lax132576.RationalFunctions
    2import Lax132576.Bimachines
    3
    4/-!
    5---
    6title: Bimachines compute rational functions
    7type: theorem
    8---
    9Every function computed by a bimachine is rational: the implication (3) ⇒ (1)
    10of Theorem B.2.3 of *Transducers*, the easiest one. The nondeterministic
    11automaton guesses the runs of both the prefix and the suffix automaton, its
    12states being pairs of their states plus one extra final state; a transition on
    13the letter aa from (p,q)(p, q) to (p′,q′)(p', q') requires p→ap′p \xrightarrow{a} p' in
    14the prefix automaton and q′→aqq' \xrightarrow{a} q in the suffix automaton and
    15outputs the piece of the gap to the left of aa, and an empty transition into
    16the final state outputs the piece of the last gap.
    17
    18# Formalization notes
    19
    20Both alphabets are assumed finite, as in the book's global convention; the
    21transition relation of the constructed automaton is indexed by the letters.
    22-/
    23
    24namespace Lax132576.RationalOfBimachine
    25
    26open Lax132576.RationalFunctions Lax132576.Bimachines
    27
    28/-- A function computed by a bimachine is rational. -/
    29axiom isRationalFun_of_isBimachine {A B : Type} [Finite A] [Finite B]
    30 {f : List A → List B} (hf : IsBimachine f) : IsRationalFun f
    31
    32end Lax132576.RationalOfBimachine
    33
    Show Proof

    Formalization notes

    Both alphabets are assumed finite, as in the book's global convention; the transition relation of the constructed automaton is indexed by the letters.

    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…