Lax Lean Archive

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

Lax132576.RationalEquivalenceDecidable

Decidable equivalence of rational functions

concepts/Lax132576/RationalEquivalenceDecidable.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 equivalence problem f=gf = g is decidable for rational functions (Theorem B.3.4 of Transducers). The book reduces it to equivalence of weighted automata over the rationals (Theorem B.3.3): output strings are represented injectively by rational numbers through a weighted automaton ι\iota, weighted automata are closed under pre-composition with rational functions (Lemma B.3.5), and f=gf = g exactly when f⋅ι=g⋅ιf \cdot \iota = g \cdot \iota.

    Lean source view on GitHub

    1import Lax132576.TransducerCodes
    2
    3/-!
    4---
    5title: Decidable equivalence of rational functions
    6type: theorem
    7---
    8The equivalence problem f=gf = g is decidable for rational functions (Theorem
    9B.3.4 of *Transducers*). The book reduces it to equivalence of weighted
    10automata over the rationals (Theorem B.3.3): output strings are represented
    11injectively by rational numbers through a weighted automaton ι\iota, weighted
    12automata are closed under pre-composition with rational functions (Lemma
    13B.3.5), and f=gf = g exactly when f⋅ι=g⋅ιf \cdot \iota = g \cdot \iota.
    14
    15# Formalization notes
    16
    17The two functions are given by codes, under the promise that both codes are
    18functional (`TransducerCodes`); the decided property is equality of the coded
    19relations. The proof turns the two codes into codes of weighted automata whose
    20values are the numerical encodings of the outputs, multiplied by the numbers
    21of accepting runs, which are the same for both, and applies the decision
    22procedure of Theorem B.3.3.
    23-/
    24
    25namespace Lax132576.RationalEquivalenceDecidable
    26
    27open Lax132576.TransducerCodes
    28
    29/-- Equivalence of two coded rational functions is decidable. -/
    30axiom decidable_codeRel_eq :
    31 DecidableUnderPromise (fun p : RelCode × RelCode => CodeFunctional p.1 ∧ CodeFunctional p.2)
    32 (fun p => codeRel p.1 = codeRel p.2)
    33
    34end Lax132576.RationalEquivalenceDecidable
    35
    Show Proof

    Formalization notes

    The two functions are given by codes, under the promise that both codes are functional (TransducerCodesTransducerCodes); the decided property is equality of the coded relations. The proof turns the two codes into codes of weighted automata whose values are the numerical encodings of the outputs, multiplied by the numbers of accepting runs, which are the same for both, and applies the decision procedure of Theorem B.3.3.

    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…