Halting problem
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. The halting problem is undecidable, meaning that no general algorithm exists that solves the halting problem for all possible program–input pairs. The problem comes up often in discussions of computability since it demonstrates that some functions are mathematically definable but not computable.
A key part of the formal statement of the problem is a mathematical definition of a computer and program, usually via a Turing machine. The proof then shows, for any program f that might determine whether programs halt, that a "pathological" program g exists for which f makes an incorrect determination. Specifically, g is the program that, when called with some input, passes its own source and its input to f and does the opposite of what f predicts g will do. The behavior of f on g shows undecidability as it means no program f will solve the halting problem in every possible case.
1900 (1900): poses his "23 questions" (now known as Hilbert's problems) at the Second International Congress of Mathematicians in Paris. "Of these, the second was that of proving the consistency of the 'Peano axioms' on which, as he had shown, the rigour of mathematics depended".[6]
David Hilbert
1920 (1920) – 1921 (1921): explores the halting problem for tag systems, regarding it as a candidate for unsolvability.[7] Its unsolvability was not established until much later, by Marvin Minsky.[8]
Emil Post
1928 (1928): Hilbert recasts his 'Second Problem' at the Bologna International Congress. He posed three questions: i.e. #1: Was mathematics complete? #2: Was mathematics consistent? #3: Was mathematics decidable?[10] The third question is known as the Entscheidungsproblem (Decision Problem).[11]
[9]
1930 (1930): announces a proof as an answer to the first two of Hilbert's 1928 questions.[12] "At first he [Hilbert] was only angry and frustrated, but then he began to try to deal constructively with the problem... Gödel himself felt—and expressed the thought in his paper—that his work did not contradict Hilbert's formalistic point of view"[13]
Kurt Gödel
1931 (1931): Gödel publishes "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I"
[14]
19 April 1935 (1935-04-19): publishes "An Unsolvable Problem of Elementary Number Theory", which proposes that the intuitive notion of an effectively calculable function can be formalized by the general recursive functions or equivalently by the lambda-definable functions. He proves that the halting problem for lambda calculus (i.e., whether a given lambda-expression has a normal form) is not effectively calculable.[15]
Alonzo Church
1936 (1936): Church publishes the first proof that the Entscheidungsproblem is unsolvable, using a notion of calculation by .[16]
recursive functions
7 October 1936 (1936-10-07): 's paper "Finite Combinatory Processes. Formulation I" is received. Post adds to his "process" an instruction "(C) Stop". He called such a process "type 1 ... if the process it determines terminates for each specific problem."[17]
Emil Post
May 1936 (1936-05) – January 1937 (1937-01): 's paper On Computable Numbers With an Application to the Entscheidungsproblem goes to press in May 1936 and reaches print in January 1937.[18] Turing proves three problems undecidable: the "satisfaction" problem, the "printing" problem, and the Entscheidungsproblem.[19] Turing's proof differs from Church's by introducing the notion of computation by machine. This is one of the "first examples of decision problems proved unsolvable".[20]
Alan Turing
1939 (1939): observes the essential equivalence of "effective method" defined by Gödel, Church, and Turing[21]
J. Barkley Rosser
1943 (1943): In a paper, states that "In setting up a complete algorithmic theory, what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer, 'Yes' or 'No,' to the question, 'Is the predicate value true?'."
Stephen Kleene
1952 (1952): Kleene includes a discussion of the unsolvability of the halting problem for Turing machines and reformulates it in terms of machines that "eventually stop", i.e. halt: "...there is no algorithm for deciding whether any given machine, when started from any given situation, eventually stops."
[22]
1952 (1952): uses the term 'halting problem' in a series of lectures at the Control Systems Laboratory at the University of Illinois in 1952. It is likely that this is the first such use of the term.[23]
Martin Davis
{i | program i eventually halts when run with input 0}
{i | there is an input x such that program i eventually halts when run with input x}.
For every algorithm , . In words, any algorithm has a positive minimum error rate, even as the size of the problem becomes extremely large.
There exists such that for every algorithm , . In words, there is a positive error rate for which any algorithm will do worse than that error rate arbitrarily often, even as the size of the problem grows indefinitely.
. In words, there is a sequence of algorithms such that the error rate gets arbitrarily close to zero for a specific sequence of increasing sizes. However, this result allows sequences of algorithms that produce wrong answers.
If we consider only "honest" algorithms that may be undefined but never produce wrong answers, then depending on the metric, may or may not be 0. In particular it is 0 for left-total universal machines, but for effectively optimal machines it is greater than 0.
[36]
Busy beaver
Gödel's incompleteness theorem
Brouwer–Hilbert controversy
Kolmogorov complexity
P versus NP problem
Termination analysis
Worst-case execution time
Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (2): 345–363. :10.2307/2371045. JSTOR 2371045.
doi
Copeland, B. Jack, ed. (2004). The essential Turing : seminal writings in computing, logic, philosophy, artificial intelligence, and artificial life, plus the secrets of Enigma. Oxford: Clarendon Press. 0-19-825079-7.
ISBN
(1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. New York: Raven Press.. Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.
Davis, Martin
(1958). Computability and Unsolvability. New York: McGraw-Hill..
Davis, Martin
Rogers, Hartley (Jr.) (1957). . Massachusetts Institute of Technology.
Theory of Recursive Functions and Effective Computability
(1952). Introduction to metamathematics. North-Holland. ISBN 0923891579.. Chapter XIII ("Computable Functions") includes a discussion of the unsolvability of the halting problem for Turing machines. In a departure from Turing's terminology of circle-free nonhalting machines, Kleene refers instead to machines that "stop", i.e. halt.
Kleene, Stephen Cole
Lucas, Salvador (June 2021). "The origins of the halting problem". Journal of Logical and Algebraic Methods in Programming. 121: 100687. :10.1016/j.jlamp.2021.100687. hdl:10251/189460. S2CID 235396831.
doi
(1967). Computation: finite and infinite machines. Englewood Cliffs, NJ: Prentice-Hall. ISBN 0131655639.. See chapter 8, Section 8.2 "Unsolvability of the Halting Problem."
Minsky, Marvin
; Mertens, Stephan (2011). The Nature of Computation. Oxford University Press. doi:10.1093/acprof:oso/9780199233212.001.0001. ISBN 978-0-19-923321-2.
Moore, Cristopher
(1996). Hilbert. New York: Copernicus. ISBN 0387946748.. First published in 1970, a fascinating history of German mathematics and physics from 1880s through 1930s. Hundreds of names familiar to mathematicians, physicists and engineers appear in its pages. Perhaps marred by no overt references and few footnotes: Reid states her sources were numerous interviews with those who personally knew Hilbert, and Hilbert's letters and papers.
Reid, Constance
(2006). "Section 4.2: The Halting Problem". Introduction to the Theory of Computation (Second ed.). PWS Publishing. pp. 173–182. ISBN 0-534-94728-X.
Sipser, Michael
(1937). "On Computable Numbers, with an Application to the Entscheidungsproblem". Proceedings of the London Mathematical Society. s2-42 (1). Wiley: 230–265. doi:10.1112/plms/s2-42.1.230. ISSN 0024-6115. S2CID 73712., Turing, A. M. (1938). "On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction". Proceedings of the London Mathematical Society. s2-43 (1). Wiley: 544–546. doi:10.1112/plms/s2-43.6.544. ISSN 0024-6115. This is the epochal paper where Turing defines Turing machines, formulates the halting problem, and shows that it (as well as the Entscheidungsproblem) is unsolvable.
Turing, A. M.
(1989). The emperor's new mind: concerning computers, minds, and the laws of physics (1990 corrected reprint ed.). Oxford: Oxford University Press. ISBN 0192861980.. Cf. Chapter 2, "Algorithms and Turing Machines". An over-complicated presentation (see Davis's paper for a better model), but a thorough presentation of Turing machines and the halting problem, and Church's Lambda Calculus.
Penrose, Roger
; Ullman, Jeffrey D. (1979). Introduction to Automata Theory, Languages, and Computation (1st ed.). Addison-Wesley. ISBN 81-7808-347-7.. See Chapter 7 "Turing Machines." A book centered around the machine-interpretation of "languages", NP-Completeness, etc.
Hopcroft, John E.
(1983). Alan Turing: the enigma. New York: Simon and Schuster. ISBN 0-671-49207-1.. Cf. Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
Hodges, Andrew
Abdulla, Parosh Aziz; Jonsson, Bengt (1996). . Information and Computation. 127 (2): 91–101. doi:10.1006/inco.1996.0053.
"Verifying Programs with Unreliable Channels"
Pure Mathematics
c2:HaltingProblem
and Bertrand Russell, Principia Mathematica to *56, Cambridge at the University Press, 1962. Re: the problem of paradoxes, the authors discuss the problem of a set not be an object in any of its "determining functions", in particular "Introduction, Chap. 1 p. 24 "...difficulties which arise in formal logic", and Chap. 2.I. "The Vicious-Circle Principle" p. 37ff, and Chap. 2.VIII. "The Contradictions" p. 60ff.
Alfred North Whitehead
"What is a computation", in Mathematics Today, Lynn Arthur Steen, Vintage Books (Random House), 1980. A wonderful little paper, perhaps the best ever written about Turing Machines for the non-specialist. Davis reduces the Turing Machine to a far-simpler model based on Post's model of a computation. Discusses Chaitin proof. Includes little biographies of Emil Post, Julia Robinson.
Martin Davis
What is Random? Chance and order in mathematics and life, Copernicus: Springer-Verlag, New York, 1999. Nice, gentle read for the mathematically inclined non-specialist, puts tougher stuff at the end. Has a Turing-machine model in it. Discusses the Chaitin contributions.
Edward Beltrami
and James R. Newman, Godel’s Proof, New York University Press, 1958. Wonderful writing about a very difficult subject. For the mathematically inclined non-specialist. Discusses Gentzen's proof on pages 96–97 and footnotes. Appendices discuss the Peano Axioms briefly, gently introduce readers to formal logic.
Ernest Nagel
Daras, Nicholas J.; (2018). Modern discrete mathematics and analysis: with applications in cryptography, information systems and modeling. Cham, Switzerland. ISBN 978-3319743240.
{{cite book}}
: CS1 maint: location missing publisher (link). Chapter 3 Section 1 contains a quality description of the halting problem, a proof by contradiction, and a helpful graphic representation of the Halting Problem.
Rassias, Themistocles M.
Sequential Machines and Automata Theory, Wiley, New York, 1967. Cf. Chapter 9, Turing Machines. Difficult book, meant for electrical engineers and technical specialists. Discusses recursion, partial-recursion with reference to Turing Machines, halting problem. Has a Turing Machine model in it. References at end of Chapter 9 catch most of the older books (i.e. 1952 until 1967 including authors Martin Davis, F. C. Hennie, H. Hermes, S. C. Kleene, M. Minsky, T. Rado) and various technical papers. See note under Busy-Beaver Programs.
Taylor Booth
Programs are described in Scientific American, August 1984, also March 1985 p. 23. A reference in Booth attributes them to Rado, T.(1962), On non-computable functions, Bell Systems Tech. J. 41. Booth also defines Rado's Busy Beaver Problem in problems 3, 4, 5, 6 of Chapter 9, p. 396.
Busy Beaver
Turing’s Man: Western Culture in the Computer Age, The University of North Carolina Press, Chapel Hill, 1984. For the general reader. May be dated. Has yet another (very simple) Turing Machine model in it.
David Bolter
Sven Köhler, Christian Schindelhauer, Martin Ziegler, On approximating real-world halting problems, pp.454-466 (2005) 3540281932 Springer Lecture Notes in Computer Science volume 3623: Undecidability of the Halting Problem means that not all instances can be answered correctly; but maybe "some", "many" or "most" can? On the one hand the constant answer "yes" will be correct infinitely often, and wrong also infinitely often. To make the question reasonable, consider the density of the instances that can be solved. This turns out to depend significantly on the Programming System under consideration.
ISBN
- paper discussed in: Does the Halting Problem Mean No Moral Robots?
Logical Limitations to Machine Ethics, with Consequences to Lethal Autonomous Weapons
- a poetic proof of undecidability of the halting problem
Scooping the loop snooper
- an animation explaining the proof of the undecidability of the halting problem
animated movie
- a proof in only 13 lines