Decidability, Undecidability, and the Halting Problem

Decidability and Undecidability: The Limits of What Computers Can Know

In 1936 — a full decade before the first real electronic computer was switched on — Alan Turing proved that there is something no computer can ever do. Not because computers are too slow. Not because we haven't invented the right algorithm yet. But because it is mathematically impossible. The problem is deceptively simple to state: given any program and any input, does the program eventually stop? Turing called this the Halting Problem, and he proved it is undecidable — no algorithm can solve it correctly for all inputs. This single result drew the boundary of what computation can achieve, and it has profound consequences for software engineering, security, and mathematics itself.

Two Levels of Computability

Before the Halting Problem, we need precise definitions.

Turing-Recognisable (Recursively Enumerable, RE): A language L is Turing-recognisable if there exists a Turing machine M such that: for every w ∈ L, M eventually halts and accepts; for every w ∉ L, M either rejects or loops forever. TM M is called a recogniser or enumerator for L.

Decidable (Recursive): A language L is decidable if there exists a Turing machine M that: for every w ∈ L, halts and accepts; for every w ∉ L, halts and rejects. Crucially, M always halts — it never loops. TM M is called a decider for L.

Every decidable language is Turing-recognisable (a decider is a special recogniser that always halts). But the converse fails: there exist languages that are recognisable but not decidable.

The Halting Problem

Define the language:

HALT = { ⟨M, w⟩ | TM M halts on input w }

where ⟨M, w⟩ denotes a standard encoding of the pair (a TM M, a string w) as a binary string.

The question: is HALT decidable? Can we write a program that takes any program and any input, and correctly answers "halts" or "loops forever" every single time?

Intuition for why this seems possible: modern IDEs warn about infinite loops. Static analysers flag potential hangs. Surely a sophisticated enough tool could solve this? The answer — which Turing proved rigorously — is no.

Turing's Diagonalisation Proof

Formal proof:

1. Assume there exists a TM H that decides HALT: H(⟨M, w⟩) accepts if M halts on w, rejects otherwise.
2. Construct a new TM D:
   • Input: ⟨M⟩ (encoding of a TM M).
   • Run H(⟨M, ⟨M⟩⟩) — ask H whether M halts on its own description.
   • If H accepts (M halts on ⟨M⟩): D loops forever.
   • If H rejects (M loops on ⟨M⟩): D halts and accepts.
3. Ask: what does D do on input ⟨D⟩?
   • If D halts on ⟨D⟩: then H(⟨D, ⟨D⟩⟩) must accept → D was supposed to loop. Contradiction.
   • If D loops on ⟨D⟩: then H(⟨D, ⟨D⟩⟩) must reject → D was supposed to halt. Contradiction.
4. Both cases are contradictions. Therefore H cannot exist. HALT is undecidable. ∎

The technique — building a machine that does the opposite of what a hypothetical oracle predicts — is called diagonalisation, borrowed from Georg Cantor's 1891 proof that real numbers are uncountable.

The Hierarchy of Languages

Decidable problems (TM always halts): membership testing for DFAs, NFAs, CFGs; emptiness of DFAs; equivalence of DFAs; parsing in O(n³) by CYK.

Undecidable but RE (TM recognises but may loop): HALT; A_TM = {⟨M, w⟩ | M accepts w} — you can tell when M accepts, but never confirm a loop.

Practical Consequences

1. Static analysis has inherent limits. Every static analyser — ESLint, Pylint, Coverity, SonarQube — produces false positives and false negatives. This is not a quality failure; it is mathematically inevitable. Rice's Theorem (below) guarantees it.

2. Antivirus has inherent limits. Detecting whether a program behaves maliciously is a semantic property of the program. Rice's Theorem says no algorithm can do this perfectly. Every antivirus uses heuristics and signatures, not perfect decision procedures.

3. Compilers cannot verify all correctness properties. Whether a program satisfies an arbitrary specification is undecidable. Formal verification tools (Coq, Isabelle, TLA+) can verify specific properties for specific programs, but only with human-provided proofs.

Rice's Theorem

Theorem (Rice, 1953): Let P be any non-trivial property of Turing machines — meaning P is true for some TMs and false for others, and P depends only on the language the TM recognises (not on the TM's implementation). Then the language {⟨M⟩ | TM M has property P} is undecidable.

Examples of undecidable semantic properties of programs:

• Does this program ever output 0?
• Does this function return the same value for all inputs?
• Does this program contain a memory leak?
• Does this program implement the correct algorithm?
• Does this malware steal passwords?

All undecidable. The proof reduces from A_TM: if you could decide any of these, you could decide A_TM, which is impossible.

Other Undecidable Problems

Hilbert's 10th Problem asked in 1900: does a given Diophantine equation (polynomial equation with integer coefficients) have integer solutions? For example, does x² + y³ = z⁴ have solutions? Yuri Matiyasevich proved in 1970 that this is undecidable — more than a century after Hilbert posed it.

What IS Decidable?

Despite the dramatic scope of undecidability, many important problems are decidable:

• Membership in a regular language: O(n) by DFA simulation.
• Membership in a CFL: O(n³) by CYK.
• Emptiness of a DFA/NFA: graph reachability from start state.
• Equivalence of two DFAs: complementation and intersection, O(n²).
• Satisfiability of linear arithmetic (Presburger arithmetic): decidable (though expensive).
• Propositional logic satisfiability (SAT): decidable (though NP-complete).

Understanding the boundary between decidable and undecidable is not just theoretical — it tells software engineers exactly where formal tools can and cannot go.

Sources: Turing, A. M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 2(42), 230–265. | Rice, H. G. (1953). Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2), 358–366. | Sipser, M. (2013). Introduction to the Theory of Computation (3rd ed.). Cengage.