Decidability and the halting problem

With Turing machines and the Church–Turing thesis in hand, we can ask the first great question of the course precisely: which problems can be solved by algorithms at all? Many questions about finite automata and grammars turn out to be decidable, and we begin with those, because they are useful and because they show how machines can take other machines as input. Then we prove the central negative result of computability theory: the halting problem, deciding whether a given program halts on a given input, cannot be decided by any algorithm. The proof is a diagonal argument, the same idea as Cantor's proof in lesson 1, applied to machines that run on their own descriptions. The result has a sharp consequence for software: no tool can perfectly decide termination, or indeed any non-trivial behavioural property of programs.

Decidable problems about automata and grammars

Questions about machines become languages once machines are encoded as strings. Consider \(A_{\text{DFA}} = \{\langle B, w \rangle : B \text{ is a DFA that accepts } w\}\). A Turing machine decides it by checking that the input is a valid encoding, simulating B on w, and accepting if the simulation ends in an accepting state. The simulation always terminates because a DFA reads its input once. The same works for NFAs, by converting to a DFA first, and for regular expressions, by converting to an NFA. Emptiness, \(E_{\text{DFA}} = \{\langle A \rangle : L(A) = \emptyset\}\), is decided by graph search for a reachable accepting state. Equivalence, \(EQ_{\text{DFA}} = \{\langle A, B \rangle : L(A) = L(B)\}\), is decided by building a DFA for the symmetric difference with the product construction and testing it for emptiness. The program below implements all three as functions that take machines as data.

# Deciders for questions about automata: A_DFA (membership), E_DFA (emptiness), EQ_DFA (equivalence).
# Each takes an encoded machine as data and always halts.
from collections import deque
def make(k, acc):   # DFA reading binary numbers, tracking value mod k
    return {"Q": list(range(k)), "start": 0, "acc": set(acc), "d": {(r, b): (2 * r + int(b)) % k for r in range(k) for b in "01"}}

def A_DFA(M, w):
    q = M["start"]
    for c in w: q = M["d"][(q, c)]
    return q in M["acc"]

def E_DFA(M):
    seen, todo = {M["start"]}, deque([M["start"]])
    while todo:
        q = todo.popleft()
        if q in M["acc"]: return False          # an accepting state is reachable
        for c in "01":
            r = M["d"][(q, c)]
            if r not in seen: seen.add(r); todo.append(r)
    return True

def EQ_DFA(M1, M2):
    # build the symmetric-difference product and test it for emptiness
    P = {"start": (M1["start"], M2["start"]), "acc": set(), "d": {}}
    for p in M1["Q"]:
        for q in M2["Q"]:
            if (p in M1["acc"]) != (q in M2["acc"]): P["acc"].add((p, q))
            for c in "01": P["d"][((p, q), c)] = (M1["d"][(p, c)], M2["d"][(q, c)])
    return E_DFA(P)

M3 = make(3, [0])
print("A_DFA(div by 3, 1001):", A_DFA(M3, "1001"), "  A_DFA(div by 3, 1000):", A_DFA(M3, "1000"))
print("E_DFA(mod 4 accepts {}):", E_DFA(make(4, [])), "  E_DFA(div by 3):", E_DFA(M3))
print("EQ_DFA(mod 9 in {0,3,6}, mod 3 = 0):", EQ_DFA(make(9, [0, 3, 6]), M3))
print("EQ_DFA(mod 9 = 0,        mod 3 = 0):", EQ_DFA(make(9, [0]), M3))

A_DFA(div by 3, 1001): True   A_DFA(div by 3, 1000): False
E_DFA(mod 4 accepts {}): True   E_DFA(div by 3): False
EQ_DFA(mod 9 in {0,3,6}, mod 3 = 0): True
EQ_DFA(mod 9 = 0,        mod 3 = 0): False

For grammars, \(A_{\text{CFG}} = \{\langle G, w \rangle : G \text{ generates } w\}\) is decidable: convert G to Chomsky normal form and run CYK, or simply try every derivation of exactly \(2|w| - 1\) steps, of which there are finitely many. Emptiness, \(E_{\text{CFG}}\), is decidable by marking variables that can generate terminal strings: first mark every terminal, then repeatedly mark any variable with a rule whose right side is all marked, and accept if the start variable is never marked. A consequence is that every context-free language is decidable: for a fixed grammar G, the decider for \(A_{\text{CFG}}\) with G built in decides L(G). Not every question about grammars is decidable, though. Equivalence of two CFGs, \(EQ_{\text{CFG}}\), and whether a CFG generates every string, \(ALL_{\text{CFG}}\), are undecidable, as lesson 9 shows.

The acceptance problem is undecidable

Define \(A_{\text{TM}} = \{\langle M, w \rangle : M \text{ is a Turing machine that accepts } w\}\). It is Turing-recognizable: the universal machine U simulates M on w and accepts if M accepts. If M rejects, U rejects; if M runs forever, so does U. So U recognizes \(A_{\text{TM}}\) but does not decide it. Theorem (Turing, 1936). \(A_{\text{TM}}\) is undecidable. Suppose, for contradiction, that a decider H exists: on input \(\langle M, w \rangle\), H halts, accepting if M accepts w and rejecting otherwise. Build a new machine D that, on input \(\langle M \rangle\), runs H on \(\langle M, \langle M \rangle \rangle\) and then does the opposite: if H accepts, D rejects; if H rejects, D accepts. D always halts, because H does.

Now run D on its own description. By construction, D accepts \(\langle D \rangle\) exactly when H rejects \(\langle D, \langle D \rangle \rangle\), which by H's correctness happens exactly when D does not accept \(\langle D \rangle\). So D accepts \(\langle D \rangle\) if and only if D does not accept \(\langle D \rangle\), a contradiction. Hence H cannot exist. The figure shows why this is diagonalization. List all Turing machines \(M_1, M_2, \ldots\) as rows and their descriptions \(\langle M_1 \rangle, \langle M_2 \rangle, \ldots\) as columns, and record in each cell whether the machine accepts that input. D is defined to disagree with the diagonal entry in every row, so D cannot be any row; but D is a Turing machine, so it must be some row. The contradiction shows that the assumed decider H, which was needed to build D, does not exist.

The argument is not a trick about one artificial machine. It shows that any proposed decider for halting or acceptance can be defeated by a program built from that decider. The program below makes this concrete in Python. Programs are source strings defining a generator that yields once per step, and two candidate deciders are tried. The first is a syntactic rule of thumb: a program that contains an infinite loop is predicted to loop. The second simulates the program for a budget of steps, and, so that it always halts even when a program asks about itself, nested calls give up and answer 'loops'. From whichever candidate is plugged in, the same diagonal program D asks the candidate about itself and does the opposite. The rule of thumb predicts that D loops, so D halts; the simulator predicts that D halts, so D loops. Note also what happens if the simulator is not given the escape hatch: simulating D requires simulating the candidate simulating D, and so on, and the 'decider' never halts at all. No budget and no cleverer heuristic escapes: any total procedure can be fed its own diagonal program.

# Any proposed halting decider fails on some program. Programs are Python source strings
# defining a generator f(x) that yields once per step; "halting" means the generator finishes.
def make(src):
    env = {"candidate": candidate}
    exec(src, env)
    return env["f"]

def runs_within(src, arg, limit):
    g = make(src)(arg)
    for _ in range(limit):
        try: next(g)
        except StopIteration: return True
    return False

# Candidate 1: a syntactic rule of thumb. Programs containing "while True" loop.
def candidate1(src, arg):
    return "while True" not in src

# Candidate 2: simulate for a budget. To stay total when a program asks about itself,
# nested calls give up and answer "loops".
depth = 0
def candidate2(src, arg):
    global depth
    if depth: return False
    depth += 1
    try: return runs_within(src, arg, 10_000)
    finally: depth -= 1

# The diagonal program: ask the candidate about yourself, then do the opposite.
D = """
def f(x):
    if candidate(x, x):
        while True:
            yield
    for _ in range(100):
        yield
"""
for name, cand in (("candidate1", candidate1), ("candidate2", candidate2)):
    candidate = cand
    predicted = cand(D, D)
    actual = runs_within(D, D, 200_000)
    print(f"{name}: predicts D(D) {'halts' if predicted else 'loops'}; "
          f"D(D) actually {'halts' if actual else 'is still running after 200,000 steps'}")
print("Each candidate is wrong about the diagonal program built from it.")

candidate1: predicts D(D) loops; D(D) actually halts
candidate2: predicts D(D) halts; D(D) actually is still running after 200,000 steps
Each candidate is wrong about the diagonal program built from it.

The halting problem

The halting problem is \(HALT_{\text{TM}} = \{\langle M, w \rangle : M \text{ halts on } w\}\), asking only whether M halts, not whether it accepts. It is also undecidable, and the proof is our first reduction. Suppose a decider R for HALT existed. Then we could decide \(A_{\text{TM}}\): on \(\langle M, w \rangle\), run R; if R says M does not halt on w, reject; if R says it halts, simulate M on w, which is now guaranteed to finish, and accept exactly if M accepts. This would decide \(A_{\text{TM}}\), which is impossible. So R does not exist. The pattern, 'if we could solve B we could solve A, and A is unsolvable, so B is unsolvable', is how almost every undecidability result is proved, and lesson 9 develops it systematically.

Recognizable, co-recognizable and decidable

A language is co-Turing-recognizable if its complement is Turing-recognizable. Theorem. A language is decidable if and only if it is both Turing-recognizable and co-Turing-recognizable. If L is decidable, its decider recognizes L, and swapping accept and reject recognizes the complement. Conversely, if \(M_1\) recognizes L and \(M_2\) recognizes \(\overline{L}\), run both on the input in parallel, alternating steps. Every string is in exactly one of L and \(\overline{L}\), so exactly one machine eventually accepts; accept if it is \(M_1\) and reject if it is \(M_2\). This machine always halts, so it decides L. Running computations in parallel by interleaving their steps is called dovetailing, and it is the basic technique for building recognizers.

The theorem immediately gives a language that is not even recognizable. \(A_{\text{TM}}\) is recognizable but not decidable, so its complement \(\overline{A_{\text{TM}}}\), the set of pairs \(\langle M, w \rangle\) where M does not accept w, cannot be recognizable: if it were, \(A_{\text{TM}}\) would be decidable. Intuitively, we can confirm acceptance by watching it happen, but we can never confirm non-acceptance by watching, because a machine that has not accepted yet may still accept later. The same holds for halting: \(\overline{HALT_{\text{TM}}}\) is not recognizable. The program below shows dovetailing at work on a process whose termination is famously unknown in general, the Collatz iteration: a recognizer can confirm each number that reaches 1, but it has no way to give up on a number that does not.

# Recognizers can be built by dovetailing: interleave many simulations so none blocks the rest.
# Question: does the Collatz-style process "n -> n/2 if even, 3n+1 if odd" reach 1 from n?
# (Every n tested so far does; whether all n do is a famous open problem.)
def collatz_steps(n):
    while n != 1:
        n = n // 2 if n % 2 == 0 else 3 * n + 1
        yield

# Recognizer for S = { n : the process from n reaches 1 within its run }, run on many n at once.
# Round r advances every n <= r by one step, so each n gets unboundedly many steps.
def dovetail(max_round):
    gens, done = {}, {}
    for r in range(1, max_round + 1):
        gens[r] = collatz_steps(r)
        for n, g in list(gens.items()):
            try: next(g)
            except StopIteration:
                done[n] = r; del gens[n]
    return done, gens

done, pending = dovetail(200)
print("confirmed to reach 1 by round 200:", len(done), "numbers")
print("still running at round 200:", sorted(pending)[:12], "...")
print("27 is confirmed at round", done.get(27, "not yet"), " (27 takes 111 steps)")

confirmed to reach 1 by round 200: 149 numbers
still running at round 200: [97, 107, 108, 109, 110, 121, 124, 125, 126, 129, 137, 142] ...
27 is confirmed at round 138  (27 takes 111 steps)

What undecidability means for software

Undecidability is a statement about every algorithm and every input, not about difficulty on typical inputs. It does not say that no program can determine whether a particular program halts; humans and tools routinely prove termination of specific programs. It says that no single program can do so correctly for all programs. Practical tools respond in three ways. They can be sound but incomplete, proving termination for many programs and answering 'unknown' for the rest, as termination provers such as those used in operating-system driver verification do. They can restrict the language, as total functional languages and proof assistants such as Coq and Agda do by allowing only recursion that provably terminates. Or they can be complete but unsound, flagging possible problems that may be false alarms, as many static analysers do. Lesson 9 generalizes the halting result to all non-trivial behavioural properties with Rice's theorem.

There is also a historical point. In 1928 David Hilbert and Wilhelm Ackermann posed the Entscheidungsproblem: find an algorithm that decides whether a statement of first-order logic is universally valid. Church and Turing both answered it negatively in 1936, and Turing's machines and the halting problem were invented for exactly that purpose. The undecidability of first-order validity follows from the undecidability of halting, by encoding a machine's computation as a logical formula. Gödel's incompleteness theorems of 1931, which say that any consistent, effectively axiomatized theory of arithmetic leaves some true statements unprovable, are closely related: if every true statement about halting were provable, we could decide halting by searching for proofs.

Worked examples