Did Turing prove the undecidability of the halting problem?

Original Article ↗ Hacker News Discussion ↗

Whether Alan Turing truly “proved the halting problem” is contested once you look closely at his 1936 paper, which talks instead about “circular” and “circle‑free” machines and an undecidable “symbol‑printing problem.” Commenters explain how these original formulations are technically different yet effectively equivalent to the modern halting problem, credit later authors with coining today’s terminology, and stress that undecidability results (like Rice’s theorem) limit only fully general algorithms—not targeted proofs, formal verification of specific systems, or practical program analysis.

Scope of Turing’s 1936 Result

  • Thread agrees Turing did not use “halt” or “halting problem” terminology.
  • His paper focused on “computable numbers” and notions like “circular” vs “circle‑free” machines and a “symbol‑printing problem.”
  • Later authors introduced the modern “halting problem” name; the thread cites mid‑20th‑century textbooks and earlier work (e.g., on self‑reference) as historical precursors.
  • Several commenters say the symbol‑printing problem is computably equivalent to the halting problem, so substantively Turing proved an equivalent result even if the framing differed.

Symbol‑Printing, Circularity, and Halting

  • Circular: prints only finitely many “symbols of the first kind” (0/1); circle‑free: prints infinitely many.
  • It’s noted this is not exactly the same as “halts/doesn’t halt,” and the mapping between circularity and halting is subtle.
  • One commenter initially claims equivalence is “elementary,” then walks that back after realizing tape contents complicate converting a non‑circular machine into a halting one.
  • Others highlight that Turing also proved undecidability of “will the machine ever print symbol X?”, which is easily turned into a modern halting formulation.

Rice’s Theorem and Practical Verification

  • Rice’s theorem is invoked: undecidability of halting is essentially equivalent to undecidability of any non‑trivial semantic property.
  • Pushback: undecidability is about general algorithms over all programs; many real programs or restricted languages can be proven to halt or satisfy properties.
  • Discussion of total languages and proof assistants: they enforce termination or totality (often via structural recursion or well‑founded measures), at the cost of expressiveness.
  • Debate over whether such subsets are “non–Turing complete” and whether “subset of instances” vs “subset of language” are conceptually distinct.

Quantum Computing and Computability

  • One commenter claims “theoretical quantum computers” could decide halting; multiple replies say this is false.
  • Others state quantum computers are not more powerful than classical ones in what they can compute; they mainly offer speedups for some problems.
  • Several insist: undecidability of halting is about computability, not complexity, so quantum speedups don’t change it.

Decidability for Individual Programs and Gödel Connections

  • Some argue “figuring out whether a single given program halts is decidable” in principle; others counter that “decidable” is defined for sets/languages, not single instances.
  • Clarified distinction:
    • For any specific program, it either halts or not, but we may lack an effective decision procedure within a fixed formal system.
    • There exist programs whose non‑termination is true but unprovable in systems like PA or ZFC (via Gödel‑style constructions).
  • Examples: Turing machines encoding Goldbach conjecture, Collatz, or proof‑search for contradictions in ZFC.
  • Some emphasize that “knowing the answer” to one specific case (even by a trivial constant function) is different from having a generally useful decision algorithm.

Busy Beaver and Complexity of Simple Machines

  • Busy Beaver work is used to show how tiny Turing machines can have extremely complex, hard‑to‑analyze behavior.
  • References to:
    • Many 5‑state binary machines historically undecided.
    • Recent breakthroughs on the 5‑state Busy Beaver and appearance of machines emulating Collatz‑like dynamics.
  • This is presented as practical evidence that even very small systems can be beyond current analytic techniques.

Constructivism and the Reality of Reals

  • Side discussion questions the ontological status of real numbers:
    • Some favor constructivist/computable views: only numbers definable or computable “exist” in a meaningful sense.
    • Others defend standard reals, arguing that mathematics lets us reason about unnameable or uncomputable objects.
  • Debate touches on least upper bounds for sets of rationals, countability arguments, and the role of decision procedures in defining sets.
  • No consensus; it’s acknowledged this is a long‑standing philosophical divide in foundations.

Understanding and Teaching the Halting Problem

  • Several note confusion when first encountering Turing’s terminology (“circle‑free” vs “halts”) and appreciate the linked paper’s clarification.
  • Some express frustration with oversimplified pedagogy that states “you can’t tell if a program halts” without emphasizing “for all arbitrary programs with one general algorithm.”
  • Others remark on the broader significance: the halting problem exemplifies inherently unsolvable computational questions, yet still coexists with extensive, useful formal verification in practice.

Broader Analogies and Reflections

  • One commenter draws an analogy to moral philosophy: just as no algorithm decides halting for all programs, no finite moral rule set can perfectly handle all situations.
  • Another points to Turing’s original paper also containing early notions of universality and “bugs,” suggesting the modern focus on “halting” misses other historical gems.
  • The thread contains both praise for the paper’s nuanced historical analysis and dismissive reactions calling it “click‑bait,” with some later softening after closer reading.