Mathematical logic and foundations Problem
Post correspondence problem
Builds on StringDecidable language
Problem
Let be an alphabet with at least two symbols. An instance is a finite list of pairs of strings over . A match is a finite nonempty sequence of indices such that Is there an algorithm that decides, for every instance, whether it has a match?
Remarks
Post proved in the paper that introduced the problem that no such algorithm exists: the set of instances with a match is not decidable. The set is recursively enumerable, since one can try all index sequences in order of length and stop when a match appears. The standard proof reduces the halting problem to it: the pairs are built so that a match spells out a halting computation of a given Turing machine. Example: the instance has the match , since . The instance alone has no match, since every concatenation of 's is longer than the corresponding concatenation of 's. Over a one-letter alphabet the problem is decidable, because only the lengths of the strings matter. The problem is also decidable for instances with pairs. Because the problem is purely about strings, it is a convenient source of undecidability for questions about grammars, for example whether two context-free grammars generate languages with a common string.
Reading path
To understand this page from the ground up, read these 29 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Element definition
- Function concept
- Monoid concept
- Proposition concept
- Set concept
- Set definition
- Turing machine definition
- Implication definition
- Predicate definition
- Ordered pair definition
- Existential quantifier definition
- Universal quantifier definition
- Cartesian product definition
- Subset definition
- Uniqueness quantifier definition
- Binary relation definition
- Function definition
- Codomain definition
- Injective function definition
- Free monoid definition
- Surjective function definition
- Bijective function definition
- Equinumerous sets definition
- Finite set definition
- Alphabet definition
- String definition
- Formal language definition
- Decidable language definition
- Post correspondence problem problem
Further reading
About this page
| Tag | 4ARVVS526T |
|---|---|
| URI | m2://4ARVVS526T |
| Kind | problem |
| Writing | W0 stub |
| MSC | 03D35, 68Q45, 68R15 |
| Status | This copy of the site has no build data. Run m2 status 4ARVVS526T. |
| About | Decision problem |
| Uses | String, Decidable language |
| Same as | |
| Changed | 3 November 2026 |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
- a source with a locator (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.
What links here
No page links to this page yet.