Did Turing prove the undecidability of the halting problem?

Original Article ↗ Hacker News Discussion ↗

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.