Lax Lean Archive

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

Lax314295.RelabellingOfRational

Rational functions are MSO relabellings

concepts/Lax314295/RelabellingOfRational.lean · lax-314295

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 rational function is definable by an mso relabelling (Theorem C.4.4 of Transducers, Bloem–Engelfriet, the implication from rational to relabelling). A rational function is computed by a bimachine; for each pair of a state of the prefix automaton and a state of the suffix automaton there is an mso formula selecting the positions at which the bimachine is in that pair of states (Claim C.4.5, stated for the index of a bimachine), and the output map is the output function of the bimachine.

    Lean source view on GitHub

    1import Lax132576.RationalFunctions
    2import Lax314295.MSORelabellings
    3
    4/-!
    5---
    6title: Rational functions are MSO relabellings
    7type: theorem
    8---
    9Every rational function is definable by an mso relabelling (Theorem C.4.4 of
    10*Transducers*, Bloem–Engelfriet, the implication from rational to relabelling).
    11A rational function is computed by a bimachine; for each pair of a state of the
    12prefix automaton and a state of the suffix automaton there is an mso formula
    13selecting the positions at which the bimachine is in that pair of states
    14(Claim C.4.5, stated for the index of a bimachine), and the output map is the
    15output function of the bimachine.
    16
    17# Formalization notes
    18
    19Both alphabets are assumed finite, as in the book.
    20-/
    21
    22namespace Lax314295.RelabellingOfRational
    23
    24open Lax132576.RationalFunctions Lax314295.MSORelabellings
    25
    26/-- A rational function is definable by an mso relabelling. -/
    27axiom isMSORelabelling_of_isRationalFun {A B : Type} [Finite A] [Finite B]
    28 {f : List A → List B} (hf : IsRationalFun f) : IsMSORelabelling f
    29
    30end Lax314295.RelabellingOfRational
    31
    Show Proof

    Formalization notes

    Both 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…