The Post correspondence problem in index form is undecidable
Lax251941.PostCorrespondenceIndexUndecidable · concepts/Lax251941/PostCorrespondenceIndexUndecidable.lean · lax-251941
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
No algorithm decides, given a finite list of pairs of strings over , whether some nonempty sequence of indices makes the two concatenations equal. This is the undecidability of the Post correspondence problem in the index form used by the book Transducers, where it is the source of the undecidability of equivalence of rational relations (Theorem B.1.6). A list of dominos taken from an instance and a list of positions in the instance carry the same information, so the index form is the domino form restated.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Computability.Halting |
| 2 | import Lax251941.PostCorrespondence |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: The Post correspondence problem in index form is undecidable |
| 7 | type: theorem |
| 8 | --- |
| 9 | No algorithm decides, given a finite list of pairs of strings over , |
| 10 | whether some nonempty sequence of indices makes the two concatenations equal. |
| 11 | This is the undecidability of the Post correspondence problem in the index form |
| 12 | used by the book *Transducers*, where it is the source of the undecidability of |
| 13 | equivalence of rational relations (Theorem B.1.6). A list of dominos taken from |
| 14 | an instance and a list of positions in the instance carry the same information, |
| 15 | so the index form is the domino form `PostCorrespondenceUndecidable` restated. |
| 16 | |
| 17 | # Formalization notes |
| 18 | |
| 19 | `Solvable` is the index form of `PostCorrespondence`; decidability is mathlib's |
| 20 | `ComputablePred` on lists of pairs of lists of natural numbers. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax251941.PostCorrespondenceIndexUndecidable |
| 24 | |
| 25 | open Lax251941.PostCorrespondence |
| 26 | |
| 27 | /-- The Post correspondence problem in index form is undecidable. -/ |
| 28 | axiom not_computablePred_solvable : ¬ ComputablePred Solvable |
| 29 | |
| 30 | end Lax251941.PostCorrespondenceIndexUndecidable |
| 31 |
Formalization notes
is the index form of ; decidability is mathlib's on lists of pairs of lists of natural numbers.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments