The Halting Problem

Suppose oracle HALT(code, input): it takes a program and an input, and returns True/False, telling you whether the program halts. With such an oracle you could build a perfect debugger, a perfect antivirus, a perfect static analyzer. Turing proved in 1936 that this oracle is mathematically impossible. And that puts a permanent ceiling on what software can do.

• **ThreadSanitizer (TSan):** a Google tool for detecting data races in C++. It runs as a dynamic analyzer (an approximation). Exact detection of every race condition is undecidable under Rice's theorem. TSan catches real races at the cost of a moderate runtime overhead.
• **Rust ownership system:** the borrow checker proves the absence of race conditions and use-after-free for a subclass of programs. This is a decidable task (a concrete algorithm). The cost is that some valid programs are rejected, a deliberate trade-off.
• **TLA+ at Amazon:** Jeff Bezos circulated a memo on using TLA+ in 2014. AWS uses it to verify S3, DynamoDB, and EC2 algorithms. The trick: it checks finite models (not arbitrary programs), a domain restriction.
• **Polymorphic viruses:** viruses that mutate their code on each run. Signature-based antiviruses fail. Sandbox emulation is an approximation, it runs for a bounded number of steps. The halting problem guarantees there is no perfect detector.

Proof by Diagonalization

HALT = {<M, w> : TM M halts on w}. Turing proved in 1936 that no algorithm decides HALT. The proof is a small masterpiece: assume such an algorithm H exists, then build a machine D that, when run on its own description, produces a contradiction. The technique is called **diagonalization**, a reference to Cantor's diagonal method.

Structure of the proof: **reductio ad absurdum** with self-reference. The program D 'looks at' itself through H and does the opposite of what H predicts. This is impossible for any H. Self-reference (D running on D) is what creates the unavoidable contradiction. It is the analogue of the liar paradox: 'this statement is false'.

Diagonalization: Method and Idea

The **diagonalization** method was invented by Georg Cantor in 1891 to prove the uncountability of the reals. The idea: assume a list of all reals in [0, 1]. Construct a number d such that d_i differs from the i-th number in position i. Then d does not match any number on the list, the list is incomplete. Turing applied the same idea to programs.

The same idea underlies **Goedel's incompleteness theorem** (1931): every sufficiently strong consistent formal system contains true statements that cannot be proved inside it. Goedel constructs a sentence 'this statement is not provable' using self-reference through coding of proofs by numbers (Goedel numbering). Diagonalization is a universal tool for proving limits of formal systems.

Consequences and Practical Impact

Undecidability of HALT immediately yields other undecidable problems. **A_TM** = {<M, w> : M accepts w} is undecidable (HALT <=_m A_TM). **E_TM** = {<M> : L(M) = empty} is undecidable. **EQ_TM** = {<M1, M2> : L(M1) = L(M2)} is undecidable. All of them are proved by reduction to HALT or A_TM.

Partial Solutions and Workarounds

Undecidability of HALT is not the end of the story. In practice we use **restricted versions**: halting checks for subclasses of programs (terminating recursive schemes, loop-free programs with bounded indices). Tools include Coq, Agda (termination proofs), Z3 (bounded verification), and CBMC (bounded model checking).

The main practical tool is **restricting the domain**. Coq and Agda require recursion to be **structural**, decreasing the size of the argument. This guarantees termination for a broad class of programs. Rust async/await and Erlang supervisor trees are architectural patterns that sidestep the halting problem by constraining structure.

Key ideas

• **HALT is undecidable:** proof by diagonalization. Assume H, build D, then D(D) contradicts H, so H does not exist.
• **Cantor's diagonalization:** the same technique proves uncountability of R and Goedel's incompleteness theorem. Self-reference creates the contradiction.
• **Consequences:** A_TM, E_TM, EQ_TM are undecidable. There is no perfect antivirus, no perfect static analyzer, no perfect optimizer.
• **Workarounds:** restrict the program class (Coq), approximate (TSan, Coverity), bounded model checking (CBMC). Always a trade-off between completeness and soundness.

Related Topics

The halting problem is the central theorem of computability theory:

• Reductions — HALT is the standard base undecidable problem used to reduce to other problems.
• Rice's Theorem — Generalizes HALT: every non-trivial semantic property is undecidable, proved by reduction from HALT.
• Church-Turing Thesis — HALT is undecidable under any reasonable model of computation, not just TMs.

Вопросы для размышления

• A Python function can call itself (recursion). Is this self-reference in Turing's sense? What is the difference?
• Coq accepts only structurally recursive programs. What class of programs does it reject, and is this a essential restriction of the language?
• If HALT is undecidable, how do tools like Valgrind and AddressSanitizer work? What exactly do they detect, and why not 100%?

Связанные уроки

• comp-18-type-checking