Lax Lean Archive

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

Lax132576.WeightedPrecomposition

Weighted automata are closed under pre-composition with rational functions

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

    For every semiring S\mathbb{S}, the composition

    A∗→fB∗→hSA^* \xrightarrow{f} B^* \xrightarrow{h} \mathbb{S}

    of a rational function ff with a function hh computed by a weighted automaton is computed by a weighted automaton (Lemma B.3.5 of Transducers). The automaton for ff is first made unambiguous and ε-free (Lemmas B.2.4 and B.2.5), so that its unique run aligns with the runs of the automaton for hh in a product construction whose transitions carry, as weight, the sum of the weights of the runs of hh over the output of one transition of ff.

    Lean source view on GitHub

    1import Lax132576.RationalFunctions
    2import Lax132576.WeightedAutomata
    3
    4/-!
    5---
    6title: Weighted automata are closed under pre-composition with rational functions
    7type: theorem
    8---
    9For every semiring S\mathbb{S}, the composition
    10A∗→fB∗→hSA^* \xrightarrow{f} B^* \xrightarrow{h} \mathbb{S}
    11of a rational function ff with a function hh computed by a weighted automaton
    12is computed by a weighted automaton (Lemma B.3.5 of *Transducers*). The
    13automaton for ff is first made unambiguous and ε-free (Lemmas B.2.4 and
    14B.2.5), so that its unique run aligns with the runs of the automaton for hh
    15in a product construction whose transitions carry, as weight, the sum of the
    16weights of the runs of hh over the output of one transition of ff.
    17
    18# Formalization notes
    19
    20The semiring is arbitrary (mathlib's `Semiring`); both alphabets are assumed
    21finite, as the unambiguous automaton needs.
    22-/
    23
    24namespace Lax132576.WeightedPrecomposition
    25
    26open Lax132576.RationalFunctions Lax132576.WeightedAutomata
    27
    28/-- Pre-composing a weighted function with a rational function gives a weighted
    29function. -/
    30axiom isWeighted_comp_of_isRationalFun {A B S : Type} [Finite A] [Finite B] [Semiring S]
    31 {f : List A → List B} {h : List B → S} (hf : IsRationalFun f) (hh : IsWeighted h) :
    32 IsWeighted (h ∘ f)
    33
    34end Lax132576.WeightedPrecomposition
    35
    Show Proof

    Formalization notes

    The semiring is arbitrary (mathlib's SemiringSemiring); both alphabets are assumed finite, as the unambiguous automaton 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…