The Halting Problem and the Shape of the Proof

Here is a service anyone would pay for. Given a program P and an input w, report whether P eventually stops on w, or runs forever. Call it halts(P, w).

The requirements are strict and worth naming, because every one of them is load bearing. The answer must be correct on every pair. It must be produced for every pair, including programs designed to be awkward. And halts must itself always terminate, otherwise it has not answered anything.

No such program exists. This is not a statement about current techniques or available compute. It is a proof that the specification is contradictory, in the same sense that no integer is both even and odd.

Turing proved it in the 1936 paper that introduced the machine, as a step toward answering Hilbert's Entscheidungsproblem in the negative.

Assume halts exists. Then this program can be written, because everything in it is ordinary code:

def halts(program, arg):
    """Assumed: always returns, always correct."""
    ...

def paradox():
    if halts(paradox, None):   # ask about myself
        while True:            # ...then do the opposite
            pass
    return "done"

Now ask what halts(paradox, None) returns.

If it returns True, then paradox enters the infinite loop and never halts. The answer was wrong.

If it returns False, then paradox skips the loop and returns immediately. The answer was wrong again.

Both branches contradict the assumption that halts is correct. The only step that can be rejected is the assumption itself. Therefore halts does not exist.

It is worth isolating what made that work, because the same two ingredients drive every result in this lesson.

The first is universality, established in the previous lesson: a program is data, so paradox can be passed a description of itself without any special mechanism. Self-reference is not a trick here, it is a consequence of stored-program computing.

The second is the ability to negate the answer. paradox does not merely consult halts, it consults it and then behaves in the opposite way. Any purported decider can be wrapped in this way.

Notice what the argument never uses: the size of the program, the speed of the machine, the amount of memory, or any detail of how halts works internally. That is why no better algorithm and no larger computer changes the conclusion.

The halting problem is not entirely beyond reach, and the exact sense in which it is not is the most useful distinction in the subject.

A language is decidable if some machine always halts and answers correctly, yes or no. It is recognisable if some machine halts and says yes on every member, but is permitted to run forever on non-members.

Halting is recognisable. Simulate P on w and say yes the moment it stops. If P halts, this reports yes eventually. If P never halts, the simulation never halts either, so no answer is ever produced. That is allowed by recognisability and forbidden by decidability.

So the failure is precise. The problem is not that nothing can be learned about halting. It is that a program cannot distinguish not yet from never.

The tiers are not a vague ordering, they interlock exactly. A question is decidable precisely when both it and its opposite are recognisable: run the two searches side by side, one step each in turn, and whichever reports first gives the answer, so the combined procedure always terminates.

That criterion settles the last box immediately. Halting is recognisable and not decidable, so its complement cannot be recognisable, or the pairing above would decide it.

So "this program runs forever" is worse off than "this program halts". There is no procedure that reliably confirms an infinite loop even given unlimited time, whereas termination at least announces itself when it happens.

Nobody proves undecidability from scratch twice. The standard move is reduction: show that a decider for your problem X could be used to build a decider for halting. Since halting has none, X has none either.

Take X = "does this program ever print anything?" Suppose ever_prints(Q) existed. Then, given P and w, build:

def make_probe(P, w):
    def probe():
        run(P, w)          # no output of its own
        print("reached")   # only if run(P, w) returned
    return probe

def halts(P, w):
    return ever_prints(make_probe(P, w))

probe prints if and only if P halts on w. So ever_prints would decide halting. It cannot, so ever_prints does not exist.

The direction is the part people invert. To prove X hard, reduce the known-hard problem to X, not the other way around.

Doing reductions one property at a time would be endless. H. G. Rice proved the general case in "Classes of Recursively Enumerable Sets and Their Decision Problems", Transactions of the American Mathematical Society, volume 74, issue 2, 1953, pages 358 to 366.

Rice's theorem: every non-trivial semantic property of programs is undecidable. Two words carry the weight. Semantic means the property depends only on what the program computes, not on how it is written. Non-trivial means at least one program has it and at least one does not.

The reach is total. Does this program compute the identity function? Does it ever dereference null? Is it equivalent to that other program? Does it always terminate? All semantic, all non-trivial, all undecidable.

Syntactic questions escape, because they are not about behaviour: line count, whether an identifier appears, whether the code parses.

The result is quoted far more often than it is stated correctly, and the misreadings all share a shape: they turn a claim about all programs into a claim about each program.

• It does not say any particular program is undecidable. while True: pass obviously loops. print(1) obviously halts. Countless individual cases are settled trivially.
• It does not say the question is hard for restricted languages. Remove unbounded loops and recursion and termination becomes decidable outright. The undecidability is a property of Turing-complete languages, not of programming.
• It does not say approximation is impossible. A tool may answer halts, loops, or do not know. Only the third option is being outlawed as unnecessary.
• It does not depend on resources. Bounded memory makes the state space finite and the question decidable in principle, at a cost so far beyond feasible that it buys nothing.

The top two rows are the ones tools rely on, and both are syntactic or finite-state. Everything below is semantic, and Rice's theorem closes the whole region at once.

This is not an academic boundary. Every type checker, linter, optimiser and verifier is trying to answer a question in the lower half of that table. Since none of them can, each has to choose which way to be wrong. The next lesson is about that choice, and about how much can still be delivered under it.