Lax Lean Archive

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

Lax132576.UnambiguousOfRational

Rational functions are computed by unambiguous automata

concepts/Lax132576/UnambiguousOfRational.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 rational function is computed by an unambiguous nondeterministic automaton with output, one with exactly one accepting run per input string: the implication (1) ⇒ (2) of Theorem B.2.3 of Transducers (Eilenberg). It is a consequence of the uniformisation lemma (Lemma B.2.5): the graph of a function is a total rational relation, so it contains an unambiguous rational relation, which must be the graph itself.

    Lean source view on GitHub

    1import Lax132576.RationalFunctions
    2
    3/-!
    4---
    5title: Rational functions are computed by unambiguous automata
    6type: theorem
    7---
    8Every rational function is computed by an unambiguous nondeterministic
    9automaton with output, one with exactly one accepting run per input string:
    10the implication (1) ⇒ (2) of Theorem B.2.3 of *Transducers* (Eilenberg). It is
    11a consequence of the uniformisation lemma (Lemma B.2.5): the graph of a
    12function is a total rational relation, so it contains an unambiguous rational
    13relation, which must be the graph itself.
    14
    15# Formalization notes
    16
    17The conclusion is `IsUnambiguousRel` for the graph `fun w v => v = f w`. Both
    18alphabets are assumed finite, as the uniformisation construction needs.
    19-/
    20
    21namespace Lax132576.UnambiguousOfRational
    22
    23open Lax132576.RationalRelations Lax132576.RationalFunctions
    24
    25/-- The graph of a rational function is computed by an unambiguous automaton with
    26output. -/
    27axiom isUnambiguousRel_of_isRationalFun {A B : Type} [Finite A] [Finite B]
    28 {f : List A → List B} (hf : IsRationalFun f) : IsUnambiguousRel (fun w v => v = f w)
    29
    30end Lax132576.UnambiguousOfRational
    31
    Show Proof

    Formalization notes

    The conclusion is IsUnambiguousRelIsUnambiguousRel for the graph funwv=>v=fwfun w v => v = f w. Both alphabets are assumed finite, as the uniformisation construction needs.

    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…