Lax Lean Archive

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

Lax132576.RationalMachineIndependent

Machine-independent characterisation of rational functions

concepts/Lax132576/RationalMachineIndependent.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 rational if and only if it is continuous and the equivalence relation

    w1∼w2⟺sup⁡w∈A∗∥f(ww1),f(ww2)∥<∞w_1 \sim w_2 \quad\Longleftrightarrow\quad \sup_{w \in A^*} \|f(w w_1), f(w w_2)\| < \infty

    on input strings has finite index (Theorem B.4.13 of Transducers, Reutenauer and Schützenberger). For a rational function computed by a bimachine, two strings with the same state of the suffix automaton are equivalent, so the index is finite; conversely the finitely many classes are used as the states of a suffix automaton, and the output after a prefix is computed by a subsequential transducer for each class. String reversal is not rational: all its input strings are pairwise inequivalent.

    Lean source view on GitHub

    1import Mathlib.Data.Set.Finite.Basic
    2import Lax765601.Continuity
    3import Lax132576.RationalFunctions
    4import Lax132576.LeftDistance
    5
    6/-!
    7---
    8title: Machine-independent characterisation of rational functions
    9type: theorem
    10---
    11A function f:A∗→B∗f : A^* \to B^* is rational if and only if it is continuous and
    12the equivalence relation
    13w1∼w2⟺sup⁡w∈A∗∥f(ww1),f(ww2)∥<∞w_1 \sim w_2 \quad\Longleftrightarrow\quad \sup_{w \in A^*} \|f(w w_1), f(w w_2)\| < \infty
    14on input strings has finite index (Theorem B.4.13 of *Transducers*, Reutenauer
    15and Schützenberger). For a rational function computed by a bimachine, two
    16strings with the same state of the suffix automaton are equivalent, so the
    17index is finite; conversely the finitely many classes are used as the states of
    18a suffix automaton, and the output after a prefix is computed by a
    19subsequential transducer for each class. String reversal is not rational: all
    20its input strings are pairwise inequivalent.
    21
    22# Formalization notes
    23
    24The relation is `BoundedVarRel f` of `LeftDistance`; finite index is the
    25finiteness of the set of its classes `{w₂ | w₁ ∼ w₂}`, as a set of sets. Both
    26alphabets are assumed finite.
    27-/
    28
    29namespace Lax132576.RationalMachineIndependent
    30
    31open Lax765601.Continuity Lax132576.RationalFunctions Lax132576.LeftDistance
    32
    33/-- A function is rational if and only if it is continuous and the relation of
    34bounded variation has finitely many classes. -/
    35axiom isRationalFun_iff {A B : Type} [Finite A] [Finite B] (f : List A → List B) :
    36 IsRationalFun f ↔
    37 Continuous f ∧ {C : Set (List A) | ∃ w₁, C = {w₂ | BoundedVarRel f w₁ w₂}}.Finite
    38
    39end Lax132576.RationalMachineIndependent
    40
    Show Proof

    Formalization notes

    The relation is BoundedVarRelfBoundedVarRel f of LeftDistanceLeftDistance; finite index is the finiteness of the set of its classes w2∣w1∼w2{w₂ | w₁ ∼ w₂}, as a set of sets. Both alphabets are assumed finite.

    Builds on

    Used by

    none

    From Mathlib

    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…