Undecidable Problems, in depth: a field guide from Post correspondence to type checking, the decidable islands, and tools that ship anyway

Decidable, semi-decidable and reductions

A decision problem is a set of yes/no instances encoded as strings. It is decidable if one program answers every instance correctly and always halts. It is semi-decidable (recursively enumerable) if some program halts with yes on every yes-instance but may run forever on no-instances; it is co-semi-decidable when the same holds with yes and no swapped. A problem that is both is decidable: run the two programs side by side.

Almost every undecidability result is proved by reduction: a computable translation f such that x is a yes-instance of a known undecidable problem A exactly when f(x) is a yes-instance of B. A decider for B would then decide A, which is impossible. This is the same many-one reduction used for NP-hardness in Karp reductions, without the polynomial-time requirement. The direction matters, and getting it backwards is the classic mistake: to show your problem is hard, reduce the known hard problem to yours.

Two consequences shape practice. First, undecidability is a statement about the general problem: a restricted input class can be perfectly decidable, and much of tool design is finding that class. Second, the program that searches for a yes-certificate usually exists; what is missing is a guarantee of a no answer. Tools therefore give one-sided results plus a budget.

Worked example: the Post correspondence problem

The Post correspondence problem (PCP) is the workhorse for reductions because it involves no machines at all. You get a finite set of dominoes, each with a top string and a bottom string. Is there a non-empty sequence of dominoes, repeats allowed, whose concatenated tops equal the concatenated bottoms?

Take the tiles b/ca, a/ab, ca/a and abc/c, numbered 0 to 3. The sequence 1, 0, 2, 1, 3 gives top a+b+ca+a+abc = abcaaabc and bottom ab+ca+a+ab+c = abcaaabc, a match. Post proved the general problem undecidable in 1946. Neary (STACS 2015) showed it stays undecidable with only five dominoes; with two it is decidable, and the cases between were reported open in that paper.

PCP is semi-decidable: enumerate sequences in order of length and check each. The searcher below is smarter in one useful way. After any partial sequence, all that matters for the future is the overhang, the unmatched suffix on whichever side is longer. Searching breadth-first over overhang states with a visited set gives three honest outcomes:

from collections import deque

def pcp(tiles, budget):
    """tiles: list of (top, bottom). Returns (verdict, sequence, states_seen)."""
    start = ("", 0)                      # (overhang, side); side 0 = top is longer
    queue, seen, truncated = deque([(start, ())]), {start}, False
    while queue:
        (over, side), seq = queue.popleft()
        if len(seq) >= budget:
            truncated = True             # we stopped exploring, not the problem
            continue
        for i, (a, b) in enumerate(tiles):
            t, u = (over + a, b) if side == 0 else (a, over + b)
            k = min(len(t), len(u))
            if t[:k] != u[:k]:
                continue                 # prefixes disagree: dead end
            s = seq + (i,)
            if t == u:
                return "SOLUTION", s, len(seen)
            state = (t[k:], 0) if len(t) > len(u) else (u[k:], 1)
            if state not in seen:
                seen.add(state)
                queue.append((state, s))
    return ("UNKNOWN" if truncated else "NO"), None, len(seen)

Run on four instances, the searcher returned:

The NO is a real proof: the set of reachable overhangs closed up at two states with no match, so no sequence of any length can work. The UNKNOWN is exactly the undecidable part showing through. For a/aa the bottom gains one extra a with every tile, the overhang grows forever, and the state space never closes; this instance is obviously hopeless to a human, but nothing in a general algorithm can see that for every instance. The last row is the warning about budgets: four tiny dominoes whose shortest match, by breadth-first order, uses 66 tiles and spells a 154-character string, found after 81,442 overhang states. With a budget of 65 the same search says UNKNOWN. Small instances can have enormous certificates.

Grammars: where the boundary is sharp

Context-free grammars are where most engineers meet undecidability directly, and the boundary is sharp:

Ambiguity reduces from PCP: build one grammar branch that derives the top strings and one that derives the bottom strings, each tagged with the sequence of tile indices used, and the grammar is ambiguous exactly when some sequence produces the same string both ways. That is why yacc and Bison report conflicts, which are a property of the LALR(1) construction, instead of answering whether the grammar is ambiguous. A grammar with no LR(1) conflicts is guaranteed unambiguous, so staying inside the deterministic class buys a sound answer.

The regular-expression row is the escape hatch to remember. Equivalence of regular languages is decidable because DFAs can be minimised to a canonical form; the Thompson construction gets you from a pattern to an automaton. If a rule set, router table or firewall policy can be expressed as regular languages, you can compare two versions exactly. The moment it needs nesting or counting, that guarantee is gone.

A catalogue of undecidable problems

Beyond grammars, these are the undecidable problems that show up in real systems or in arguments about them:

• Type checking. Grigore (POPL 2017) showed that Java subtype checking is undecidable by reducing Turing machine halting to it, and later work carried the construction to Python's type hints. Type inference for System F, the core of many polymorphic type systems, is undecidable as well. Compilers survive with depth limits: deeply recursive C++ templates hit a configurable instantiation depth, and TypeScript stops with an error that a type instantiation is excessively deep and possibly infinite.
• Diophantine equations. Hilbert's tenth problem asked for an algorithm deciding whether a polynomial equation with integer coefficients has an integer solution. Matiyasevich completed the Davis-Putnam-Robinson programme in 1970 and showed none exists. This is why SMT solvers decide linear integer arithmetic (Presburger arithmetic, decidable since 1929) but are incomplete for nonlinear integer constraints and may answer unknown.
• Matrix mortality. Given a finite set of square integer matrices, can some product equal the zero matrix? Paterson proved it undecidable for 3x3 matrices in 1970 by encoding PCP in matrix products. Questions about whether a linear system or a loop over matrices can ever reach a state sit right next to this.
• Tiling. Can a finite set of square tiles with coloured edges tile the whole plane? Berger proved it undecidable in 1966, in the process finding tile sets that tile only aperiodically.
• The word problem for groups. Novikov and Boone showed in the 1950s that there are finitely presented groups where deciding whether two words name the same element is impossible. Rewriting systems and symbolic algebra inherit this.
• Program equivalence and optimality. Whether two programs compute the same function, or whether an optimiser produced the smallest program, follows from Rice's theorem, which forbids only a decider for arbitrary programs. Verified compilers such as CompCert are proved correct once, and translation validators check each compilation's output.
• Kolmogorov complexity and busy beavers. The length of the shortest program for a string is uncomputable, so perfect compression is impossible to certify. The busy beaver function grows faster than any computable function; its fifth value, 47,176,870, was settled only in 2024 by a collaborative, machine-checked proof.

Engineering with undecidable problems

Undecidable does not mean unusable. Every tool that faces one of these problems picks a strategy and should say which:

The common thread is honesty about which side can be wrong. A sound analyser may say a safe program is unsafe but never the reverse; a bounded checker that finds no bug has only shown no bug within k steps. Interfaces that collapse these states into a plain true or false are where real damage happens: a timeout reported as verified, or an unknown treated as unsatisfiable. The same budget-and-escalate pattern used for NP-hard search in SAT solving applies, with one difference: for an NP problem more time always eventually helps, while for an undecidable one some instances never resolve.

Failure modes

• Reducing in the wrong direction. Showing your problem reduces to halting proves nothing about its hardness; reduce halting, or PCP, to your problem.
• Undecidable confused with intractable. NP-complete problems are decidable and merely expensive; undecidable ones have no algorithm at any cost. The practical responses differ.
• Forgetting the general-versus-instance distinction. A specific program or grammar can be analysed completely; undecidability only forbids one algorithm for all of them.
• UNKNOWN reported as NO. A search that stops at its budget and returns false turns an honest semi-decider into a wrong decider.
• Budgets measured in the wrong unit. Wall-clock limits make results depend on load; count steps, states or tiles so a verdict is reproducible.
• Finite memory used as an excuse. Real machines are finite-state, so their behaviour is decidable in principle, but the state space is astronomically large; this changes nothing in practice.

What to do next

1. Run the PCP searcher on the four instances above, then try budgets of 65 and 66 on the last one to watch the verdict flip from UNKNOWN to SOLUTION.
2. For every analysis tool in your pipeline, write down whether it is sound, complete, bounded or three-valued, and what it reports on a timeout.
3. Find one place where you compare rule sets, routes or filters and check whether they fit in regular languages; if they do, compare them exactly with automata.
4. Audit your code for any path that maps a solver's unknown or a timeout to a definite answer, and make it a separate result.
5. Replace wall-clock budgets in verification jobs with step or state budgets so verdicts are reproducible.
6. Read the halting problem article for the diagonal proof and Rice's theorem that every result here builds on.