Lax Lean Archive

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

Lax132576.RationalEquivalenceUndecidable

Equivalence of rational relations is undecidable

concepts/Lax132576/RationalEquivalenceUndecidable.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 R=SR = S is undecidable for rational relations (Theorem B.1.6 of Transducers, Griffiths). The book reduces the Post correspondence problem to the universality problem: for two homomorphisms g,hg, h, the instance has no solution exactly when the union of the complements of gg and hh — a rational relation by Claim B.1.7 and closure under union — is the full relation A∗×B∗A^* \times B^*.

    Lean source view on GitHub

    1import Lax132576.TransducerCodes
    2
    3/-!
    4---
    5title: Equivalence of rational relations is undecidable
    6type: theorem
    7---
    8The equivalence problem R=SR = S is undecidable for rational relations (Theorem
    9B.1.6 of *Transducers*, Griffiths). The book reduces the Post correspondence
    10problem to the universality problem: for two homomorphisms g,hg, h, the instance
    11has no solution exactly when the union of the complements of gg and hh — a
    12rational relation by Claim B.1.7 and closure under union — is the full relation
    13A∗×B∗A^* \times B^*.
    14
    15# Formalization notes
    16
    17The two relations are given by codes (`TransducerCodes`), and undecidability is
    18the negation of mathlib's `ComputablePred` for the equality of the two coded
    19relations. The proof assumes the undecidability of the Post correspondence
    20problem in index form, which the archive states separately
    21(`PostCorrespondenceIndexUndecidable` of the submission on the Post
    22correspondence problem).
    23-/
    24
    25namespace Lax132576.RationalEquivalenceUndecidable
    26
    27open Lax132576.TransducerCodes
    28
    29/-- No algorithm decides whether two coded rational relations are equal. -/
    30axiom not_computablePred_codeRel_eq :
    31 ¬ ComputablePred (fun p : RelCode × RelCode => codeRel p.1 = codeRel p.2)
    32
    33end Lax132576.RationalEquivalenceUndecidable
    34
    Show Proof

    Formalization notes

    The two relations are given by codes (TransducerCodesTransducerCodes), and undecidability is the negation of mathlib's ComputablePredComputablePred for the equality of the two coded relations. The proof assumes the undecidability of the Post correspondence problem in index form, which the archive states separately (PostCorrespondenceIndexUndecidablePostCorrespondenceIndexUndecidable of the submission on the Post correspondence problem).

    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…