Lax Lean Archive

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

Lax132576.WeightedEquivalenceDecidable

Decidable equivalence of weighted automata over the rationals

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

    Given two weighted automata over the field of rationals, it is decidable whether they compute the same function (Theorem B.3.3 of Transducers, Schützenberger). The book proves it through linear representations: the difference of the two automata is a weighted automaton, and by Schützenberger's rank argument it is zero on all inputs as soon as it is zero on the inputs of length less than its dimension, a finite check. The same proof works for any field whose elements are finitely representable and whose operations are computable.

    Lean source view on GitHub

    1import Lax132576.TransducerCodes
    2import Lax132576.WeightedCodes
    3
    4/-!
    5---
    6title: Decidable equivalence of weighted automata over the rationals
    7type: theorem
    8---
    9Given two weighted automata over the field of rationals, it is decidable
    10whether they compute the same function (Theorem B.3.3 of *Transducers*,
    11Schützenberger). The book proves it through linear representations: the
    12difference of the two automata is a weighted automaton, and by Schützenberger's
    13rank argument it is zero on all inputs as soon as it is zero on the inputs of
    14length less than its dimension, a finite check. The same proof works for any
    15field whose elements are finitely representable and whose operations are
    16computable.
    17
    18# Formalization notes
    19
    20The automata are given by codes (`WeightedCodes`), the promise is that both
    21codes are valid, and the decided property is equality of the two computed
    22functions on all of `ℕ*`; decidability is `DecidableUnderPromise` of
    23`TransducerCodes`. The decision procedure combines the effective form of
    24Schützenberger's bound with a primitive recursive evaluation of a coded
    25automaton on a string, both developed in the proof package.
    26-/
    27
    28namespace Lax132576.WeightedEquivalenceDecidable
    29
    30open Lax132576.TransducerCodes Lax132576.WeightedCodes
    31
    32/-- Equivalence of two valid coded weighted automata over `ℚ` is decidable. -/
    33axiom decidable_wcodeEval_eq :
    34 DecidableUnderPromise (fun p : WCode × WCode => WCodeValid p.1 ∧ WCodeValid p.2)
    35 (fun p => wcodeEval p.1 = wcodeEval p.2)
    36
    37end Lax132576.WeightedEquivalenceDecidable
    38
    Show Proof

    Formalization notes

    The automata are given by codes (WeightedCodesWeightedCodes), the promise is that both codes are valid, and the decided property is equality of the two computed functions on all of N∗ℕ*; decidability is DecidableUnderPromiseDecidableUnderPromise of TransducerCodesTransducerCodes. The decision procedure combines the effective form of Schützenberger's bound with a primitive recursive evaluation of a coded automaton on a string, both developed in the proof package.

    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…