The Halting Problem, in depth: the diagonal proof in code, semi-decidability, reductions, Rice's theorem and engineering with budgets

Stating the problem precisely

Fix a programming language that can express any computation, such as Python with unbounded integers and memory, or a Turing machine. Programs are strings, so a program can be given another program as input. Define HALT as the set of pairs (P, w) such that running P on input w eventually stops. A decider for HALT would be a program halts(P, w) that always stops itself and returns True exactly when P stops on w.

Three words carry the weight. Always: the decider must stop on every input, including programs that do not. Exactly: no false positives or negatives. Every: all programs, not the ones you care about. Relax any one and the problem becomes solvable, which is the space engineering tools work in: a checker that may answer "unknown", or only handles loops over finite ranges, is easy to build.

The diagonal proof, in code

Suppose, for contradiction, that someone hands you a correct, always-terminating halts. Write a second program that asks halts about a program run on its own source, and then does the opposite of the prediction:

def halts(program_src: str, inp: str) -> bool:
    """Hypothetical perfect decider. Assumed, not implemented."""
    ...

def contrary(src: str) -> None:
    if halts(src, src):      # predicted to stop on itself?
        while True:          # ...then loop forever
            pass
    else:
        return               # predicted to loop? then stop at once

CONTRARY_SRC = "<the source text of contrary, as a string>"
contrary(CONTRARY_SRC)       # does this call halt?

Ask what happens on the last line. If halts(CONTRARY_SRC, CONTRARY_SRC) returns True, contrary enters the infinite loop, so it does not halt and the decider was wrong. If it returns False, contrary returns immediately, so it halts and the decider was wrong again. Both answers are wrong, so no such halts exists. The argument only needs programs to read program text and call a subroutine, which any general-purpose language can do.

This is diagonalisation, Cantor's move for the reals: build a program that differs from row i of the program-by-input table on input i. It does not say any particular program's halting is unknowable; it says no single algorithm is correct on all of them.

Recognisable is not decidable

Half of the problem is solvable. If P halts on w, you can confirm it: run it and wait. A procedure that answers yes on every yes-instance and may run forever on no-instances is a recogniser, and problems with one are called recursively enumerable or semi-decidable. HALT is semi-decidable; its complement, "P never halts on w", is not, because if both a set and its complement had recognisers you could run them side by side and one would always answer, which would decide HALT.

Running things side by side is called dovetailing: interleave steps of many candidates so one divergent candidate cannot starve the rest, as search-based program synthesis does.

The asymmetry matters operationally. A test can prove that a job terminates on a given input; no amount of waiting proves that a hung job will never finish. Your monitoring can therefore only ever say "has not finished within the budget", and every timeout you set is a policy decision, not a measurement of the truth.

Reductions: spreading undecidability

Once one problem is known to be undecidable, others follow by reduction: show that a decider for the new problem would give you a decider for HALT. The direction is the usual trap, exactly as in NP-completeness proofs: you transform instances of the known-hard problem into instances of the new one.

Take "does function f ever return 0 on some input?", the core of many assertion and dead-code checks. Given any (P, w), build a new program:

def build_q(p_src: str, w: str) -> str:
    """Q ignores its own input, runs P on w, then returns 0.
    Q returns 0 on some input  <=>  P halts on w."""
    return f"""
def q(_ignored):
    env = {{}}
    exec({p_src!r}, env)            # P's source defines main
    env["main"]({w!r})              # may never return
    return 0
"""

If a tool could decide "returns 0 on some input" it could decide halting by calling itself on build_q(P, w), so it cannot exist. The same template gives "halts on the empty input" (bake w into P), "is line L reachable", "does this program ever write to this file", "are these two programs equivalent" (compare Q with a program that always returns 0) and "is this function total". The construction is mechanical, and once you can do it you will recognise undecidable feature requests quickly.

Rice's theorem

Henry Rice generalised the pattern in 1951. Call a property of programs semantic if it depends only on the input-output behaviour (the partial function the program computes), not on how the code is written, and non-trivial if some programs have it and some do not. Rice's theorem: every non-trivial semantic property is undecidable. "Computes a sorting function", "never divides by zero on any input", "returns the same result as the reference implementation", "leaks no secret to the output": all undecidable in general.

Two boundaries matter. Syntactic properties are decidable: "contains a while loop", "calls eval", "is under 500 lines". Bounded behavioural questions are decidable too: "halts within one million steps on this input" is answered by simulating one million steps. The undecidability lives in unbounded quantifiers: some input, every input, eventually. Most practical verification works by replacing one of those with a bound or an approximation.

The finite-memory caveat

Real computers have finite memory, which seems to dissolve the whole problem. It does, in principle. A machine with S bits of state has at most 2**S configurations, so if it runs longer than that it must have repeated one, and a deterministic machine that repeats a configuration loops forever. Halting for finite-state systems is decidable by cycle detection.

In practice the bound is useless: one kilobyte of mutable state has more configurations than there are atoms in the observable universe, and acceptance for linear-bounded automata (memory limited to the input size) is PSPACE-complete. Halting is undecidable for the idealised model, and decidable but intractable for the physical machine unless the relevant state is small. Protocol state machines and small controllers often are that small, which is what model checkers exploit.

The busy beaver function shows how wild small programs get. BB(n) is the longest any halting n-state, two-symbol Turing machine runs from a blank tape; it grows faster than any computable function. BB(5) was proved to be 47,176,870 steps in 2024 by the bbchallenge collaboration, with a machine-checked Coq proof, after decades of effort. Five states were enough to make the question a research project.

How real tools live with it

Since no tool can be sound, complete and always terminating at once, every real analyser chooses which to sacrifice. The table summarises the common choices.

Termination provers rest on one idea: find a ranking function, a quantity that is bounded below and strictly decreases on every loop iteration. In Euclid's algorithm while b: a, b = b, a % b the value b is a natural number and a % b is less than b, so the loop runs at most b times. Nested loops use lexicographic ranks: an outer counter that decreases, paired with an inner one that may reset whenever the outer one drops. Tools search for linear or lexicographic ranks automatically, often with SAT and SMT solvers, and report "unknown" when none is found. For the Collatz map (halve if even, else triple and add one) nobody has found a rank, and termination for every starting value is an open problem.

Worked example: a three-outcome runner

Here is the finite-state escape hatch as a reusable runner. It drives any deterministic step function, returns three outcomes instead of two, and proves non-termination when the state repeats, which is exact for finite-state behaviour and conservative otherwise.

from enum import Enum

class Outcome(Enum):
    HALTED = "halted"
    LOOPS = "loops"          # proven: a state repeated
    UNKNOWN = "unknown"      # budget exhausted, no proof either way

def run_bounded(step, state, budget, key=lambda s: s):
    """step(state) -> next state, or None when the program halts."""
    seen = set()
    for i in range(budget):
        if state is None:
            return Outcome.HALTED, i
        k = key(state)
        if k in seen:
            return Outcome.LOOPS, i
        seen.add(k)
        state = step(state)
    return Outcome.UNKNOWN, budget

# 1. A counter: halts.
print(run_bounded(lambda n: None if n == 0 else n - 1, 10, 1000))
# 2. A modular counter: state repeats, proven loop.
print(run_bounded(lambda n: (n + 3) % 7, 0, 1000))
# 3. Collatz from 27: reaches 1 after 111 steps; reported as (HALTED, 112).
collatz = lambda n: None if n == 1 else (n // 2 if n % 2 == 0 else 3 * n + 1)
print(run_bounded(collatz, 27, 1000))
# 4. Unbounded growth: never repeats, budget says UNKNOWN.
print(run_bounded(lambda n: n + 1, 0, 1000))

Case 4 is the lesson. The counter obviously never halts, but a generic runner cannot prove it; only a program-specific invariant could. For long runs store state hashes, or use Floyd's tortoise-and-hare for constant memory. The same three-way contract is what you want from any job runner: the caller can retry UNKNOWN with a bigger budget, but should treat LOOPS as a bug report.

Designing systems that run untrusted logic

Systems that execute code or plans written by others inherit the halting problem directly. An LLM agent that decides its own next step, a user-defined SQL recursive query, a workflow engine running customer scripts, a smart contract, and a regular expression supplied by a user can all fail to terminate, or terminate only after an astronomically long time, which is operationally the same thing. Backtracking regex engines are the classic case; Thompson-style engines avoid it by restricting the language to something with linear-time matching.

The design rules follow from the theory. Put an explicit budget on every untrusted loop: steps, tokens, tool calls, wall-clock time and memory. Ethereum's gas is the cleanest example: every instruction costs gas, execution stops when it runs out, and non-termination becomes a priced outcome. Make budget expiry distinct from failure in your API, as in the runner above. Where you control the language, prefer a less expressive one, as build and policy systems do. Measure running time in terms of input size, using the vocabulary of asymptotic analysis, for the code you do accept, so budgets are set from data.

Failure modes

• Reversed reduction. Showing your problem reduces to HALT proves nothing about its hardness; you must reduce HALT to it.
• Treating undecidable as unsolvable. Undecidable means no algorithm is correct on all inputs. Sound-but-incomplete tools solve the instances you have every day.
• Misreading the finite caveat. Real programs are not practically decidable, but small state machines can be checked exhaustively.
• Timeouts reported as hangs. A budget expiry is UNKNOWN, not proof of a loop; alerting and retry logic should say so.
• Budgets on only one resource. A step cap does not stop a single step that allocates unbounded memory or blocks on I/O.
• Confusing slow with non-terminating. Exponential backtracking finishes eventually; the fix is the algorithm or the input limit, not a longer timeout.

Trade-offs

Choosing expressiveness is choosing what you can know. A Turing-complete extension language lets users do anything and lets you prove almost nothing; a restricted one enables static checks and caching but frustrates power users. Sound analysis brings false alarms; bug finders bring misses. Tight budgets kill legitimate long jobs; loose ones let runaways eat shared capacity. The wrong process is picking a point without writing down what you gave up.

What to do next

1. Reproduce the diagonal argument on paper for a friend; if you can explain why both answers fail, you own the proof.
2. Practise one reduction: show "does this program ever print 'done'" is undecidable using the build_q template.
3. List every place your systems run user- or model-supplied logic, and record the budget (steps, time, memory) each one enforces; add the missing ones.
4. Make budget expiry a distinct result type in those APIs, separate from errors.
5. For one small protocol or state machine you own, run an exhaustive state exploration and check that every state can reach a terminal one.
6. Before adopting a static analyser, find out whether it is sound or a bug finder, and set expectations about false alarms or misses accordingly.