Decidability & the Halting Problem

In the theory of computation, we model every decision problem as a language: a set L of strings over some alphabet Σ. A decider for L is a Turing machine (equivalently, a program) that halts on every input and accepts exactly the strings in L. A recognizer for L is a TM that accepts every string in L but is allowed to loop forever on strings not in L.

Why encode problems as languages? Because any instance of any decision problem can be encoded as a string. "Does graph G have a Hamiltonian cycle?" becomes "Is ⟨G⟩ ∈ HAMPATH?" where ⟨G⟩ is an encoding of G. This uniform setup lets us reason about all decision problems at once.

A Turing machine has an infinite tape, a finite set of states, and a transition function. At each step it reads a tape symbol, writes a new symbol, moves left or right, and transitions to a new state. It halts by entering an accept or reject state. We use TMs not because we program in them (we do not) but because they precisely capture the notion of effective procedure — everything a real computer can compute, a TM can compute.

The key hierarchy:

• Decidable (recursive): TM halts on every input, accepting iff the string is in L.
• Turing-recognizable (recursively enumerable, r.e.): TM accepts every string in L; may loop on non-members.
• Co-recognizable: the complement of L is recognizable.
• Undecidable: no TM decides L. May still be recognizable or neither.

Every decidable language is recognizable (just ignore the loop case — the decider already halts). But the converse is false, and proving that gap exists is the heart of this module.

# A Python program IS a Turing machine (informally).
# A decider always returns True or False.
# A recognizer may loop forever on some inputs.

def decider_for_even_length(s: str) -> bool:
    """Decides whether len(s) is even. Always terminates."""
    return len(s) % 2 == 0

def recognizer_for_strings_with_aa(s: str) -> bool:
    """Recognizes strings containing 'aa'.
    This one always halts too, but we COULD write one that loops on non-members."""
    return 'aa' in s

# A recognizer that loops on 'no' instances:
def bad_recognizer(s: str) -> bool:
    """Accepts if s encodes a halting computation.
    On non-halting encodings, this function itself never returns."""
    # ... simulate the encoded TM; return True only if it halts
    pass  # demonstration only

Before we prove the Halting Problem is undecidable, we need to understand why there must be undecidable problems at all. The argument is a stunning counting argument.

Fact 1: The set of all Turing machines (equivalently, all programs) is countably infinite. A TM is a finite description — a finite set of transitions — and every finite string over a finite alphabet is countable. We can enumerate all TMs: M₁, M₂, M₃, …

Fact 2: The set of all languages over {0,1} is uncountably infinite. Each language is a subset of {0,1}*, the set of all binary strings. The set of all binary strings is countable (enumerate by length: ε, 0, 1, 00, 01, …), so a language is an infinite binary sequence (does string sᵢ belong?). By Cantor's diagonal argument (the same one showing |P(ℕ)| > |ℕ|), the set of all such sequences is uncountable.

Conclusion by cardinality: We have countably many TMs and uncountably many languages. Therefore most languages have no TM at all — most problems are undecidable. Undecidability is not the exception; computability is the exception. We happen to care mostly about languages that do have TMs, but the landscape is dominated by undecidable territory.

This does not tell us which specific problems are undecidable. For that we need diagonalization applied concretely.

# Cantor's diagonal argument in miniature.
# Suppose we had a list of ALL infinite binary sequences.
# We can construct a new sequence not on the list by flipping the diagonal.

def flip(bit: int) -> int:
    return 1 - bit

def diagonal_escape(sequences: list[list[int]]) -> list[int]:
    """Given a list of binary sequences, produces one NOT in the list."""
    # sequences[i][i] is the i-th bit of the i-th sequence.
    # Flip each: the result differs from sequence i at position i.
    return [flip(sequences[i][i]) for i in range(len(sequences))]

# Example:
seqs = [
    [0, 1, 0, 1, ...],   # s0: differs from diagonal_escape at index 0
    [1, 1, 0, 0, ...],   # s1: differs at index 1
    [0, 0, 0, 1, ...],   # s2: differs at index 2
    # ... infinitely many more
]
# diagonal_escape(seqs)[i] != seqs[i][i] for every i
# => diagonal_escape(seqs) is not equal to any sequence in seqs
# => the list was incomplete — no complete list exists

Cantor showed no list of infinite binary sequences can be complete. Turing applied the same idea to programs. Here is a clean version before we get to the Halting Problem:

The Diagonal Language. Enumerate all TMs: M₁, M₂, M₃, … Enumerate all strings: s₁, s₂, s₃, … Build an infinite table where entry (i, j) = 1 if Mᵢ accepts sⱼ, and 0 otherwise.

Define the diagonal language D = { sᵢ | Mᵢ does NOT accept sᵢ }. D is defined by flipping the diagonal of the table.

Claim: D is not Turing-recognizable. Proof: Suppose some TM Mₖ recognizes D. Consider the string sₖ (the k-th string in the enumeration).

• If sₖ ∈ D, then by definition Mₖ does not accept sₖ — contradiction.
• If sₖ ∉ D, then by definition Mₖ accepts sₖ — contradiction.

So no such Mₖ exists. D is not recognizable (not even by a looping recognizer).

This is the philosophical core of all undecidability: a language defined by a diagonal flip over all possible TM behaviors cannot be captured by any one of those TMs. The self-reference bites.

# Pseudo-Python: the diagonal language
# (We CANNOT actually implement this — the undecidability is the point.)

# Enumerate all TMs as M[1], M[2], ...
# Enumerate all strings as s[1], s[2], ...

# The acceptance table: table[i][j] = 1 if M[i] accepts s[j]
# (conceptually infinite)

# Diagonal language:
# D = { s[i] | M[i] does NOT accept s[i] }
#   = { s[i] | table[i][i] == 0 }

# If some M[k] recognizes D:
#   Does M[k] accept s[k]?
#   Case 1: Yes -> s[k] in L(M[k]) = D -> M[k] does NOT accept s[k]. Contradiction.
#   Case 2: No  -> s[k] not in L(M[k]) = D -> M[k] DOES accept s[k]. Contradiction.
# => No such M[k] exists. D is not recognizable.

The Halting Problem is the language:

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

Here ⟨M, w⟩ is a string encoding of the pair (M, w) — we are asking: "given the source code M and the input w, does M halt?"

Theorem (Turing 1936): HALT is undecidable.

Proof by contradiction. Assume for contradiction that H is a TM that decides HALT:

• H(⟨M, w⟩) = ACCEPT if M halts on w
• H(⟨M, w⟩) = REJECT if M loops on w
• H always halts.

Using H as a subroutine, build a new TM D:

D(⟨M⟩):   // D takes a single TM description as input
  run H(⟨M, ⟨M⟩⟩)   // ask: does M halt when given its OWN description?
  if H accepted (M halts on ⟨M⟩):
    loop forever
  if H rejected (M loops on ⟨M⟩):
    halt and accept

Now ask: what does D do when run on ⟨D⟩ (its own description)?

• If D halts on ⟨D⟩: then H accepted ⟨D, ⟨D⟩⟩, meaning M=D halts on ⟨D⟩ — so D's code says "loop forever" — so D loops. Contradiction.
• If D loops on ⟨D⟩: then H rejected ⟨D, ⟨D⟩⟩, meaning M=D loops on ⟨D⟩ — so D's code says "halt and accept" — so D halts. Contradiction.

Both cases give a contradiction. The assumption that H exists must be false. HALT is undecidable.

Note: HALT is still recognizable: just simulate M on w and accept if it halts. We can never confirm "loops forever," so HALT is r.e. but not decidable. Its complement co-HALT (the set of (M,w) where M loops) is not even recognizable (if it were, we could decide HALT by running both in parallel).

# The impossible halting decider — written as a thought experiment.
# This code CANNOT be made to work correctly for all inputs.

def H(M_source: str, w: str) -> bool:
    """Hypothetical halting decider.
    Returns True if program M_source halts on input w.
    Returns False if it loops forever.
    CLAIM: This function always terminates.
    (Turing proved no such function can exist.)
    """
    raise NotImplementedError("Proven impossible by Turing (1936)")

# Using H, construct the contradicting program D:
import inspect

def D(M_source: str) -> None:
    """Runs M on its own source code.
    Loops if M would halt on its own source.
    Halts  if M would loop  on its own source.
    """
    if H(M_source, M_source):   # M halts on itself?
        while True: pass        # -> D loops
    else:                       # M loops on itself?
        return                  # -> D halts

# Now evaluate D on D's own source code:
D_source = inspect.getsource(D)
# D(D_source):
#   H(D_source, D_source) must return True or False.
#   Either answer leads to a contradiction.
#   Therefore H cannot exist.

The proof above puts HALT in a very specific position in the hierarchy. Let us nail down the landscape precisely.

Definition. A language L is:

• Decidable (recursive) if there is a TM that always halts and accepts L.
• Turing-recognizable (r.e.) if there is a TM that accepts every string in L (may loop on non-members).
• Co-Turing-recognizable (co-r.e.) if the complement L̄ is recognizable.

Key theorem: L is decidable iff L is both recognizable and co-recognizable.

Proof sketch: If L is decidable, both L and L̄ are decidable, hence recognizable. Conversely, if TMs A recognizes L and B recognizes L̄, run A and B in parallel (dovetailing). Every string is in L or L̄, so one of them will eventually accept — we then know the answer and halt.

Corollary: HALT is recognizable but not co-recognizable (and not decidable). This means: we can confirm a program halts (by watching it), but we can never confirm it loops (no finite observation suffices).

The landscape:

[All Languages]
  [Recognizable (r.e.)]
    [Decidable (recursive)]  <- PRIMES, CFG membership
    HALT, A_TM              <- recognizable but not decidable
  co-HALT                   <- co-recognizable but not recognizable
  D (diagonal language)     <- neither recognizable nor co-recognizable

This layered structure is beautiful: each inclusion is strict, and we have explicit examples at each level.

# Dovetailing: run two recognizers in parallel to build a decider.
# This only works when we KNOW L is both r.e. and co-r.e.

def dovetail_decide(s: str, recognize_L, recognize_complement_L) -> bool:
    """
    Decide membership in L by running two recognizers in parallel.
    recognize_L(s)            -> True if s in L  (may diverge if s not in L)
    recognize_complement_L(s) -> True if s not in L (may diverge if s in L)
    Exactly one will terminate — we return appropriately.
    """
    import threading, queue
    result = queue.Queue()

    def run_L():
        recognize_L(s)
        result.put(True)   # s is in L

    def run_comp():
        recognize_complement_L(s)
        result.put(False)  # s is NOT in L

    threading.Thread(target=run_L,    daemon=True).start()
    threading.Thread(target=run_comp, daemon=True).start()

    return result.get()   # whichever answers first

Once we know HALT is undecidable, we can prove many other problems undecidable using reductions. A mapping reduction from A to B (written A ≤ₘ B) is a computable function f such that: x ∈ A ⟺ f(x) ∈ B.

Key lemma: if A ≤ₘ B and B is decidable, then A is decidable. Contrapositive: if A is undecidable and A ≤ₘ B, then B is undecidable.

The strategy: to show problem P is undecidable, assume for contradiction it has a decider D_P. Show how to use D_P to decide HALT — contradiction.

Example: The Acceptance Problem. A_TM = { ⟨M, w⟩ | M accepts w }. Reduction from HALT:

• Given ⟨M, w⟩ (HALT instance), build M': on any input x, simulate M on w; if M accepts, accept; if M rejects, reject.
• Then: M halts on w ⟺ M' accepts some string ⟺ M' does something non-trivial.

Actually the cleanest reduction goes the other way: HALT ≤ₘ A_TM (or we reduce A_TM directly). The key insight is that A_TM is also undecidable (proven independently by a similar diagonal argument) and that HALT ≤ₘ A_TM.

Rice's Theorem (the ultimate generalization): Any non-trivial property of the language recognized by a TM is undecidable. A property P is trivial if it holds for all TMs or no TMs. This kills every interesting semantic question: "does M output 'hello'?", "does M ever access memory location 42?", "does M run in polynomial time?" — all undecidable in general.

# Reduction: proving HALTS_ON_EMPTY is undecidable
# using a reduction FROM HALT.
#
# HALTS_ON_EMPTY = { <M> | M halts on the empty string }
#
# Assume D_HOE decides HALTS_ON_EMPTY.
# We build a decider for HALT:

def decide_HALT_using_D_HOE(M_source: str, w: str) -> bool:
    """
    Reduction: given (M, w), build a new machine M_w that,
    on empty input, simulates M on w.
    Then ask D_HOE whether M_w halts on empty input.
    """
    # Construct M_w's source code: ignores its input, runs M on w
    M_w_source = f"""
def M_w(ignored_input):
    M = {M_source!r}
    simulate(M, {w!r})   # halts iff M halts on w
"""
    return D_HOE(M_w_source)   # True iff M_w halts on empty = iff M halts on w

# If D_HOE existed, decide_HALT_using_D_HOE would decide HALT.
# But HALT is undecidable. So D_HOE cannot exist.

Rice's Theorem is perhaps the most practically important result in this module. It says:

Let P be any non-trivial property of Turing-recognizable languages. Then the problem { ⟨M⟩ | L(M) has property P } is undecidable.

Here "non-trivial" means: there exists some TM with the property and some TM without it.

What this rules out (all undecidable in general):

• Does M halt on all inputs? (emptiness vs. full language)
• Does M accept any string at all?
• Does M accept the string "hello"?
• Does M run in polynomial time?
• Is L(M) regular? context-free? finite?
• Is L(M) = L(some other machine M')?

Proof sketch. Suppose P is a non-trivial property of languages. WLOG assume the empty TM T_∅ (which rejects everything) does NOT have property P (otherwise work with the complement). Let T_yes be a TM whose language does have property P.

For any TM M and string w, construct M_{M,w}: on input x, first simulate M on w (ignoring x); if M halts, then run T_yes on x and accept/reject as T_yes does.

Key: L(M_{M,w}) = L(T_yes) if M halts on w; L(M_{M,w}) = ∅ if M loops on w.

So ⟨M_{M,w}⟩ has property P iff M halts on w. A decider for P gives a decider for HALT. Contradiction.

Practical moral: You cannot write a program that correctly decides any interesting behavioral property of arbitrary programs. Linters, static analyzers, and type systems are always either incomplete (miss some bugs) or unsound (flag false positives), by mathematical necessity.

# Illustration of what Rice's Theorem kills.
# None of these can be implemented correctly for all inputs.

# UNDECIDABLE: Does program P halt on ALL inputs?
def halts_on_all(P_source: str) -> bool:
    raise NotImplementedError("Rice's Theorem: undecidable")

# UNDECIDABLE: Does program P ever print "hello"?
def ever_prints_hello(P_source: str) -> bool:
    raise NotImplementedError("Rice's Theorem: undecidable")

# UNDECIDABLE: Are programs P and Q equivalent?
def programs_equivalent(P_source: str, Q_source: str) -> bool:
    raise NotImplementedError("Rice's Theorem: undecidable")

# DECIDABLE: Does the source code of P contain the string 'for'?
def source_contains_for(P_source: str) -> bool:
    return 'for' in P_source  # syntactic property, not semantic — fine!

# Rice's Theorem only kills SEMANTIC (language/behavior) properties.
# Syntactic properties (does the source look like X?) can be decidable.

Not all undecidability proofs come directly from HALT. The Post Correspondence Problem (PCP), introduced by Emil Post in 1946, is a combinatorial puzzle that is also undecidable, and it is a useful intermediate step for proving other problems (like context-free grammar ambiguity) undecidable.

Problem. Given a finite set of domino-like tiles, each tile being a pair of strings (top, bottom) over some alphabet, can you select a sequence of tiles (with repetition) so that the concatenation of all top strings equals the concatenation of all bottom strings?

For example, tiles [(a, ab), (b, a), (ca, c)] — can you pick a sequence whose tops and bottoms match? Answer: (ca, c), (a, ab), (ca, c) gives tops="caaca" and bottoms="cabca" — no. But (b, a), (ca, c), (b, a) gives "bcab" on top and "acab" on bottom — no. PCP asks if any arrangement works.

Undecidability: PCP is proven undecidable by reducing A_TM to it: given ⟨M, w⟩, construct a tile set that has a solution iff M accepts w. The tiles encode the sequence of configurations in a valid accepting computation.

Why it matters: PCP shows undecidability is not just about programs self-referencing. Purely combinatorial problems over strings can also be undecidable. This is used to prove undecidability of CFG ambiguity, certain matrix problems, and problems in formal language theory.

# Post Correspondence Problem — decidable instance search (brute force, may not terminate)
# This is NOT a general solver (that would be impossible by PCP undecidability).

from itertools import product

def pcp_search(tiles: list[tuple[str, str]], max_len: int) -> list[int] | None:
    """
    Search for a PCP solution of length up to max_len.
    tiles: list of (top, bottom) string pairs (1-indexed: use index+1)
    Returns list of 1-based indices if found, None if no solution of this length.
    WARNING: If no solution exists, the general problem is UNDECIDABLE.
             This function is incomplete — it may return None even when a
             solution exists (just longer than max_len).
    """
    n = len(tiles)
    for length in range(1, max_len + 1):
        for seq in product(range(n), repeat=length):
            tops    = ''.join(tiles[i][0] for i in seq)
            bottoms = ''.join(tiles[i][1] for i in seq)
            if tops == bottoms:
                return [i + 1 for i in seq]  # 1-based indices
    return None

# Example tiles where a solution EXISTS:
tiles = [("a", "ab"), ("b", "a"), ("ca", "c")]
result = pcp_search(tiles, max_len=6)
print(result)  # May find a solution or return None for this small bound

HALT is recognizable but not decidable. This distinction is deeply important and worth dwelling on.

HALT is recognizable. Build a TM U (the universal Turing machine) that, on input ⟨M, w⟩, simulates M on w step by step. If M ever halts and accepts, U accepts. If M ever halts and rejects, U rejects. If M runs forever, U runs forever. U is a recognizer for HALT — it accepts every ⟨M, w⟩ where M does halt, and loops on the rest.

HALT is not decidable. Proven above. No TM can always give a yes/no answer in finite time.

co-HALT is not recognizable. co-HALT = { ⟨M, w⟩ | M does NOT halt on w }. If it were recognizable, we could run the recognizer for HALT and the recognizer for co-HALT in parallel (dovetailing), and one would always accept — making HALT decidable. Contradiction.

Practical meaning: There is a fundamental asymmetry in our ability to verify properties:

• We can ALWAYS verify a program HALTS (just watch it halt).
• We can NEVER verify a program LOOPS FOREVER (how long do you wait?).

This asymmetry appears throughout CS: type checking verifies safety (halting properties); liveness properties ("something good eventually happens") are harder to check. In model checking, safety properties are co-recursively enumerable while liveness properties require more care.

# Universal TM in Python: a recognizer for HALT
# This is precisely what the Python interpreter IS.

def universal_recognizer(M_source: str, w: str) -> bool:
    """
    Simulates TM M on input w.
    Returns True if M halts (and accepts).
    May loop forever if M does not halt.
    This is a RECOGNIZER for HALT, not a DECIDER.
    """
    # In Python, this is just eval/exec — the interpreter IS the universal TM.
    # We cannot add a timeout and still be correct for all inputs.
    import subprocess, sys
    result = subprocess.run(
        [sys.executable, '-c', M_source, w],
        capture_output=True,
        # timeout=10  # a timeout makes this INCORRECT (may reject a slow-halting program)
    )
    return result.returncode == 0

# The insight: any real programming language interpreter IS a universal TM.
# The halting problem is exactly the question: "Will this interpreter run forever?"

Turing's 1936 paper and Gödel's 1931 incompleteness theorems are two faces of the same mathematical coin. Understanding the connection deepens both.

Gödel's First Incompleteness Theorem: Any consistent formal system F (strong enough to express arithmetic) contains a sentence G_F such that G_F is true but not provable in F. Moreover, G_F essentially says "This sentence is not provable in F" — a formal analog of the Liar Paradox.

The connection to Halting. Consider the set of all true statements of arithmetic. This set is not recursively enumerable — there is no program that lists all truths of arithmetic. Why? Because if such a program existed, we could use it to decide HALT: to check if M halts on w, just search through all truths for the statement "M halts on w." But HALT is undecidable.

Turing's proof of Gödel's theorem (informally). Suppose we have a complete and consistent proof system PS. Then we can decide HALT: to test if M halts on w, search for a proof of "M halts on w" or a proof of "M does not halt on w." Completeness guarantees one of these proofs exists; finding it decides HALT. But HALT is undecidable, so PS cannot be both complete and consistent.

Chaitin's perspective. For any formal system F, there is a constant L such that F cannot prove that any specific string has Kolmogorov complexity > L. This connects undecidability to incompressibility — "most" strings are incompressible, but we cannot prove it for any specific string.

The moral: the limits of computation and the limits of formal proof are not separate phenomena. They are the same phenomenon seen from two angles.

# Godel sentence in pseudocode — the self-referential construction

# A Godel sentence G for formal system F is (informally):
#   G = "There is no proof of G in F"
#
# If F is consistent and G is false, then there IS a proof of G,
#   but G says there isn't — F proves a falsehood. Inconsistent.
# If F is consistent and G is true, then there is NO proof of G in F.
#   G is true but unprovable — F is incomplete.
#
# The computational analog:
#   HALT = { <M,w> | M halts on w }
#   Suppose TRUTH = { phi | phi is a true arithmetic statement }
#   If TRUTH were r.e., HALT would be decidable.
#   HALT is undecidable => TRUTH is not r.e. => arithmetic is incomplete.

# def provable_in_F(statement: str) -> bool:
#     for each proof p in F (in lexicographic order):
#         if p proves statement:
#             return True
#     # loops forever if no proof exists
#
# If F were complete: provable_in_F OR provable_in_F(negate(s)) would always halt
# => we could dovetail and decide anything => contradiction with undecidability

Undecidability is not binary — there is a rich hierarchy of "degrees of undecidability" called the Arithmetical Hierarchy, which classifies problems by how many alternating quantifiers over natural numbers are needed to express them.

The hierarchy (Σ and Π notation):

• Σ⁰₁ (r.e.): Problems expressible as ∃x φ(x) for decidable φ. Equivalently: recognizable by a TM. Example: HALT ("there exists a computation that terminates").
• Π⁰₁ (co-r.e.): Complements of Σ⁰₁ problems. co-HALT. "For all computations, they don't terminate" — co-HALT.
• Σ⁰₂: ∃x ∀y φ(x,y). Example: "M halts on infinitely many inputs" = ∃N ∀n>N ∃input_n of size n [M halts on input_n].
• Π⁰₂: ∀x ∃y φ(x,y). Example: "M halts on all inputs" (totality of TMs).
• Δ⁰₁: Both Σ⁰₁ and Π⁰₁ = decidable problems.

Each level is strictly larger than the one below. Problems in Σ⁰₂ \ (Σ⁰₁ ∪ Π⁰₁) are "more undecidable" than HALT in the sense that HALT cannot be reduced to them without an oracle.

Oracle Turing Machines. An oracle TM has access to a black box that solves some fixed problem L in one step. The Turing degree of a problem measures its difficulty relative to oracles. HALT is Turing-complete for Σ⁰₁: any r.e. problem can be solved with a HALT oracle. Problems at higher levels require iterated oracle access.

For practical CS, the key takeaway is that the problems we encounter in verification, analysis, and AI planning are often in Π⁰₂ or higher — and require sophisticated approximation strategies.

# Arithmetical hierarchy — examples classified

# DELTA_0_1 (Decidable):
# - Is w in the language of a given DFA?     Sigma_0_1 ∩ Pi_0_1
# - Is this number prime?                    Decidable
# - Does this CFG generate a given string?   Decidable

# SIGMA_0_1 (Recognizable, r.e.):
# - Does TM M halt on w?            (HALT)
# - Does TM M accept w?             (A_TM)
# - Is L(M) non-empty?              (E_TM complement)
# Expressible as: exists a halting computation on (M, w)

# PI_0_1 (Co-recognizable, co-r.e.):
# - Does TM M NOT halt on w?        (co-HALT)
# - Does TM M reject w on all runs? 
# Expressible as: for all computation prefixes, none halt

# SIGMA_0_2:
# - Does M halt on infinitely many inputs?
# Expressible as: exists N, for all n>N, exists input_n of size n where M halts

# PI_0_2:
# - Does M halt on ALL inputs? (TOTAL_TM)  <- Turing showed this is Pi_0_2-complete
# Expressible as: for all inputs w, exists a halting computation on (M,w)

# Neither (outside arithmetical hierarchy):
# - Does M halt on exactly the inputs that are prime?  (requires describing L(M) exactly)
# - The diagonal language D (not even recognizable)