Lax Lean Archive

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

Lax132576.WeightedZeronessDecidable

Decidable zeroness of weighted automata over the rationals

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

    The zeroness problem — does a given weighted automaton over the field of rationals compute the constant function 00? — is decidable (Theorem B.3.7 of Transducers). It is the special case of equivalence (Theorem B.3.3) in which the second automaton is empty, and conversely equivalence reduces to zeroness of the difference; the book proves the zeroness criterion, Schützenberger's bound on the length of a witness, and derives both.

    Lean source view on GitHub

    1import Lax132576.TransducerCodes
    2import Lax132576.WeightedCodes
    3
    4/-!
    5---
    6title: Decidable zeroness of weighted automata over the rationals
    7type: theorem
    8---
    9The zeroness problem — does a given weighted automaton over the field of
    10rationals compute the constant function 00? — is decidable (Theorem B.3.7 of
    11*Transducers*). It is the special case of equivalence (Theorem B.3.3) in which
    12the second automaton is empty, and conversely equivalence reduces to zeroness
    13of the difference; the book proves the zeroness criterion, Schützenberger's
    14bound on the length of a witness, and derives both.
    15
    16# Formalization notes
    17
    18The automaton is given by a valid code, and the decided property is that its
    19function is `0`.
    20-/
    21
    22namespace Lax132576.WeightedZeronessDecidable
    23
    24open Lax132576.TransducerCodes Lax132576.WeightedCodes
    25
    26/-- Zeroness of a valid coded weighted automaton over `ℚ` is decidable. -/
    27axiom decidable_wcodeEval_eq_zero :
    28 DecidableUnderPromise WCodeValid (fun c => wcodeEval c = 0)
    29
    30end Lax132576.WeightedZeronessDecidable
    31
    Show Proof

    Formalization notes

    The automaton is given by a valid code, and the decided property is that its function is 00.

    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…