Proof of `Equivalence of rational relations is undecidable`
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 40 of the paper of lax-157538, Transducers
Description
Equivalence of rational relations is undecidable (Theorem B.1.6).
Proof strategy
The source reduces the Post correspondence problem in index form to the equality of two coded rational relations (, : the two codes describe the complements of the two homomorphisms of an instance, and are equal exactly when the instance has no solution). The undecidability of the Post correspondence problem is the archive statement , an assumption of this proof. The concept's codes are named structures; the bridge moves the decision procedure across.
Attribution
Theorem B.1.6 of Transducers (Griffiths); Lean proof by Aristotle.