Lax Lean Archive

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

Lax132576.WeightedAutomata

Weighted automata

concepts/Lax132576/WeightedAutomata.lean · lax-132576

definition

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

    In the paper

    Definition

    A weighted automaton over a semiring S\mathbb{S} (Definition B.3.2 of Transducers) is defined like a nondeterministic automaton with output, except that the transitions carry elements of S\mathbb{S} instead of output strings, and that every input string is required to have only finitely many accepting runs. Its semantics is the function A∗→SA^* \to \mathbb{S} mapping an input string ww to

    ∑ρweight of ρ,\sum_{\rho} \text{weight of } \rho,

    the sum over the accepting runs ρ\rho over ww of the product of the weights of the transitions of ρ\rho, taken in the order of the run — which matters when the multiplication of S\mathbb{S} is not commutative. The finiteness requirement is what makes the sum well defined. Over the Boolean semiring weighted automata are nondeterministic automata; over the semiring of regular languages they are the rational relations; over Q\mathbb{Q} they have decidable equivalence (Theorem B.3.3).

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Finprod
    2import Lax132576.LabelledAutomata
    3
    4/-!
    5---
    6title: Weighted automata
    7type: definition
    8---
    9A *weighted automaton* over a semiring S\mathbb{S} (Definition B.3.2 of
    10*Transducers*) is defined like a nondeterministic automaton with output, except
    11that the transitions carry elements of S\mathbb{S} instead of output strings,
    12and that every input string is required to have only finitely many accepting
    13runs. Its semantics is the function A∗→SA^* \to \mathbb{S} mapping an input
    14string ww to
    15∑ρweight of ρ,\sum_{\rho} \text{weight of } \rho,
    16the sum over the accepting runs ρ\rho over ww of the product of the weights
    17of the transitions of ρ\rho, taken in the order of the run — which matters when
    18the multiplication of S\mathbb{S} is not commutative. The finiteness
    19requirement is what makes the sum well defined. Over the Boolean semiring
    20weighted automata are nondeterministic automata; over the semiring of regular
    21languages they are the rational relations; over Q\mathbb{Q} they have
    22decidable equivalence (Theorem B.3.3).
    23
    24# Formalization notes
    25
    26A semiring (Definition B.3.1) is mathlib's `Semiring`. A weighted automaton is
    27a labelled automaton (`LabelledAutomata`) with labels in `S`; `weightOf` is
    28the ordered product of the labels of a path, `FinitelyManyRuns` the
    29requirement of the definition, and `wEval` the sum over the set of accepting
    30runs, written as mathlib's finite sum over a set (`∑ᶠ`), which is the intended
    31sum whenever the set is finite. `IsWeighted f` asks for a finite state space
    32and an automaton satisfying the finiteness requirement.
    33-/
    34
    35namespace Lax132576.WeightedAutomata
    36
    37open Lax132576.LabelledAutomata
    38
    39variable {A S Q : Type} [Semiring S]
    40
    41/-- The weight of a path: the product of the weights of its transitions, in the
    42order in which they are taken. -/
    43def weightOf (ts : List (Q × List A × S × Q)) : S := (LabAut.labelsOf ts).prod
    44
    45/-- The semantics of a weighted automaton: the sum of the weights of the accepting
    46runs over the input. -/
    47noncomputable def wEval (M : LabAut A S Q) (w : List A) : S :=
    48 ∑ᶠ ts ∈ M.acceptingOn w, weightOf ts
    49
    50/-- The requirement of Definition B.3.2: every input string has only finitely
    51many accepting runs. -/
    52def FinitelyManyRuns (M : LabAut A S Q) : Prop := ∀ w : List A, (M.acceptingOn w).Finite
    53
    54/-- A function `A* → S` computed by a weighted automaton over the semiring `S`
    55with a finite state space. -/
    56def IsWeighted {A S : Type} [Semiring S] (f : List A → S) : Prop :=
    57 ∃ (Q : Type) (_ : Finite Q) (M : LabAut A S Q), FinitelyManyRuns M ∧ wEval M = f
    58
    59end Lax132576.WeightedAutomata
    60

    Formalization notes

    A semiring (Definition B.3.1) is mathlib's SemiringSemiring. A weighted automaton is a labelled automaton (LabelledAutomataLabelledAutomata) with labels in SS; weightOfweightOf is the ordered product of the labels of a path, FinitelyManyRunsFinitelyManyRuns the requirement of the definition, and wEvalwEval the sum over the set of accepting runs, written as mathlib's finite sum over a set (∑f∑ᶠ), which is the intended sum whenever the set is finite. IsWeightedfIsWeighted f asks for a finite state space and an automaton satisfying the finiteness requirement.

    Builds on

    Used by

    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…