Halting problem
This article includes a list of general references, but it lacks sufficient corresponding inline citations. (September 2018) |
In
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.
Background
The halting problem is a decision problem about properties of computer programs on a fixed
For example, in pseudocode, the program
while (true) continue
does not halt; rather, it goes on forever in an infinite loop. On the other hand, the program
does halt.
While deciding whether these programs halt is simple, more complex programs prove problematic. One approach to the problem might be to run the program for some number of steps and check if it halts. However, as long as the program is running, it is unknown whether it will eventually halt or run forever. Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct.
Programming consequences
Some infinite loops can be quite useful. For instance, event loops are typically coded as infinite loops.[1] However, most subroutines are intended to finish.[2] In particular, in hard real-time computing, programmers attempt to write subroutines that are not only guaranteed to finish, but are also guaranteed to finish before a given deadline.[3]
Sometimes these programmers use some general-purpose (Turing-complete) programming language, but attempt to write in a restricted style—such as MISRA C or SPARK—that makes it easy to prove that the resulting subroutines finish before the given deadline.[citation needed]
Other times these programmers apply the rule of least power—they deliberately use a computer language that is not quite fully Turing-complete. Frequently, these are languages that guarantee all subroutines finish, such as Coq.[citation needed]
Common pitfalls
The difficulty in the halting problem lies in the requirement that the decision procedure must work for all programs and inputs. A particular program either halts on a given input or does not halt. Consider one algorithm that always answers "halts" and another that always answers "does not halt". For any specific program and input, one of these two algorithms answers correctly, even though nobody may know which one. Yet neither algorithm solves the halting problem generally.
There are programs (interpreters) that simulate the execution of whatever source code they are given. Such programs can demonstrate that a program does halt if this is the case: the interpreter itself will eventually halt its simulation, which shows that the original program halted. However, an interpreter will not halt if its input program does not halt, so this approach cannot solve the halting problem as stated; it does not successfully answer "does not halt" for programs that do not halt.
The halting problem is theoretically decidable for linear bounded automata (LBAs) or deterministic machines with finite memory. A machine with finite memory has a finite number of configurations, and thus any deterministic program on it must eventually either halt or repeat a previous configuration:[4]
...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine...
However, a computer with a million small parts, each with two states, would have at least 21,000,000 possible states:[5]
This is a 1 followed by about three hundred thousand zeroes ... Even if such a machine were to operate at the frequencies of cosmic rays, the aeons of galactic evolution would be as nothing compared to the time of a journey through such a cycle:
Although a machine may be finite, and finite automata "have a number of theoretical limitations":[5]
...the magnitudes involved should lead one to suspect that theorems and arguments based chiefly on the mere finiteness [of] the state diagram may not carry a great deal of significance.
It can also be decided automatically whether a nondeterministic machine with finite memory halts on none, some, or all of the possible sequences of nondeterministic decisions, by enumerating states after each possible decision.
History
In April 1936, Alonzo Church published his proof of the undecidability of a problem in the lambda calculus. Turing's proof was published later, in January 1937. Since then, many other undecidable problems have been described, including the halting problem which emerged in the 1950s.
Timeline
- 1900David Hilbert 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]
- 1920Emil Post 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]– 1921 :
- 1928Hilbert recasts his 'Second Problem' at the Bologna International Congress.[9] 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] :
- 1930Kurt Gödel 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]
- 1931Gödel publishes "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I" : [14]
- 19 April 1935Alonzo Church 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]
- 1936Church publishes the first proof that the Entscheidungsproblem is unsolvable, using a notion of calculation by recursive functions. : [16]
- 7 October 1936Emil Post'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]:
- May 1936Alan Turing'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][page needed] – January 1937 :
- 1939J. Barkley Rosser observes the essential equivalence of "effective method" defined by Gödel, Church, and Turing : [21]
- 1943In a paper, Stephen Kleenestates 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?'." :
- 1952Kleene 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]
- 1952Martin Davis 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]
Origin of the halting problem
Many papers and textbooks refer the definition and proof of undecidability of the halting problem to Turing's 1936 paper. However, this is not correct.[19][24] Turing did not use the terms "halt" or "halting" in any of his published works, including his 1936 paper.[25] A search of the academic literature from 1936 to 1958 showed that the first published material using the term “halting problem” was Rogers (1957). However, Rogers says he had a draft of Davis (1958) available to him,[19] and Martin Davis states in the introduction that "the expert will perhaps find some novelty in the arrangement and treatment of topics",[26] so the terminology must be attributed to Davis.[19][24] Davis stated in a letter that he had been referring to the halting problem since 1952.[23] The usage in Davis's book is as follows:[27]
"[...] we wish to determine whether or not [a Turing machine] Z, if placed in a given initial state, will eventually halt. We call this problem the halting problem for Z. [...]
Theorem 2.2 There exists a Turing machine whose halting problem is recursively unsolvable.
A related problem is the printing problem for a simple Turing machine Z with respect to a symbol Si".
A possible precursor to Davis's formulation is Kleene's 1952 statement, which differs only in wording:[19][22]
there is no algorithm for deciding whether any given machine, when started from any given situation, eventually stops.
The halting problem is Turing equivalent to both Davis's printing problem ("does a Turing machine starting from a given state ever print a given symbol?") and to the printing problem considered in Turing's 1936 paper ("does a Turing machine starting from a blank tape ever print a given symbol?"). However, Turing equivalence is rather loose and does not mean that the two problems are the same. There are machines which print but do not halt, and halt but not print. The printing and halting problems address different issues and exhibit important conceptual and technical differences. Thus, Davis was simply being modest when he said:[19]
It might also be mentioned that the unsolvability of essentially these problems was first obtained by Turing.
Formalization
In his original proof Turing formalized the concept of
What is important is that the formalization allows a straightforward mapping of algorithms to some
Representation as a set
The conventional representation of decision problems is the set of objects possessing the property in question. The halting set
- K = {(i, x) | program i halts when run on input x}
represents the halting problem.
This set is
There are many equivalent formulations of the halting problem; any set whose Turing degree equals that of the halting problem is such a formulation. Examples of such sets include:
- {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}.
Proof concept
def g():
if halts(g):
loop_forever()
halts(g) must either return true or false, because halts was assumed to be
Sketch of rigorous proof
The concept above shows the general method of the proof, but the computable function halts does not directly take a subroutine as an argument; instead it takes the source code of a program. Moreover, the definition of g is
Here program i refers to the i th program in an
f(i,j) | i | ||||||
1 | 2 | 3 | 4 | 5 | 6 | ||
j | 1 | 1 | 0 | 0 | 1 | 0 | 1 |
2 | 0 | 0 | 0 | 1 | 0 | 0 | |
3 | 0 | 1 | 0 | 1 | 0 | 1 | |
4 | 1 | 0 | 0 | 1 | 0 | 0 | |
5 | 0 | 0 | 0 | 1 | 1 | 1 | |
6 | 1 | 1 | 0 | 0 | 1 | 0 | |
f(i,i) | 1 | 0 | 0 | 1 | 1 | 0 | |
g(i) | U | 0 | 0 | U | U | 0 |
Possible values for a total computable function f arranged in a 2D array. The orange cells are the diagonal. The values of f(i,i) and g(i) are shown at the bottom; U indicates that the function g is undefined for a particular input value.
The proof proceeds by directly establishing that no total computable function with two arguments can be the required function h. As in the sketch of the concept, given any total computable binary function f, the following partial function g is also computable by some program e:
The verification that g is computable relies on the following constructs (or their equivalents):
- computable subprograms (the program that computes f is a subprogram in program e),
- duplication of values (program e computes the inputs i,i for f from the input i for g),
- conditional branching (program e selects between two results depending on the value it computes for f(i,i)),
- not producing a defined result (for example, by looping forever),
- returning a value of 0.
The following pseudocode for e illustrates a straightforward way to compute g:
procedure e(i):
if f(i, i) == 0 then
return 0
else
loop forever
Because g is partial computable, there must be a program e that computes g, by the assumption that the model of computation is Turing-complete. This program is one of all the programs on which the halting function h is defined. The next step of the proof shows that h(e,e) will not have the same value as f(e,e).
It follows from the definition of g that exactly one of the following two cases must hold:
- f(e,e) = 0 and so g(e) = 0. In this case program e halts on input e, so h(e,e) = 1.
- f(e,e) ≠ 0 and so g(e) is undefined. In this case program e does not halt on input e, so h(e,e) = 0.
In either case, f cannot be the same function as h. Because f was an arbitrary total computable function with two arguments, all such functions must differ from h.
This proof is analogous to Cantor's diagonal argument. One may visualize a two-dimensional array with one column and one row for each natural number, as indicated in the table above. The value of f(i,j) is placed at column i, row j. Because f is assumed to be a total computable function, any element of the array can be calculated using f. The construction of the function g can be visualized using the main diagonal of this array. If the array has a 0 at position (i,i), then g(i) is 0. Otherwise, g(i) is undefined. The contradiction comes from the fact that there is some column e of the array corresponding to g itself. Now assume f was the halting function h, if g(e) is defined (g(e) = 0 in this case), g(e) halts so f(e,e) = 1. But g(e) = 0 only when f(e,e) = 0, contradicting f(e,e) = 1. Similarly, if g(e) is not defined, then halting function f(e,e) = 0, which leads to g(e) = 0 under g's construction. This contradicts the assumption of g(e) not being defined. In both cases contradiction arises. Therefore any arbitrary computable function f cannot be the halting function h.
Computability theory
A typical method of proving a problem to be undecidable is to reduce the halting problem to . For example, there cannot be a general algorithm that decides whether a given statement about natural numbers is true or false. The reason for this is that the proposition stating that a certain program will halt given a certain input can be converted into an equivalent statement about natural numbers. If an algorithm could find the truth value of every statement about natural numbers, it could certainly find the truth value of this one; but that would determine whether the original program halts.
Rice's theorem generalizes the theorem that the halting problem is unsolvable. It states that for any non-trivial property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property "halt for the input 0" is undecidable. Here, "non-trivial" means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions. For example, "halts or fails to halt on input 0" is clearly true of all partial functions, so it is a trivial property, and can be decided by an algorithm that simply reports "true." Also, this theorem holds only for properties of the partial function implemented by the program; Rice's Theorem does not apply to properties of the program itself. For example, "halt on input 0 within 100 steps" is not a property of the partial function that is implemented by the program—it is a property of the program implementing the partial function and is very much decidable.
which produces the digits of Ω, although its first few digits can be calculated in simple cases.Since the negative answer to the halting problem shows that there are problems that cannot be solved by a Turing machine, the
Approximations
Turing's proof shows that there can be no mechanical, general method (i.e., a Turing machine or a program in some equivalent model of computation) to determine whether algorithms halt. However, each individual instance of the halting problem has a definitive answer, which may or may not be practically computable. Given a specific algorithm and input, one can often show that it halts or does not halt, and in fact computer scientists often do just that as part of a correctness proof. There are some heuristics that can be used in an automated fashion to attempt to construct a proof, which frequently succeed on typical programs. This field of research is known as automated termination analysis.
Some results have been established on the theoretical performance of halting problem heuristics, in particular the fraction of programs of a given size that may be correctly classified by a recursive algorithm. These results do not give precise numbers because the fractions are uncomputable and also highly dependent on the choice of program encoding used to determine "size". For example, consider classifying programs by their number of states and using a specific "Turing semi-infinite tape" model of computation that errors (without halting) if the program runs off the left side of the tape. Then , over programs chosen uniformly by number of states. But this result is in some sense "trivial" because these decidable programs are simply the ones that fall off the tape, and the heuristic is simply to predict not halting due to error. Thus a seemingly irrelevant detail, namely the treatment of programs with errors, can turn out to be the deciding factor in determining the fraction of programs.[33]
To avoid these issues, several restricted notions of the "size" of a program have been developed. A dense Gödel numbering assigns numbers to programs such that each computable function occurs a positive fraction in each sequence of indices from 1 to n, i.e. a Gödelization φ is dense iff for all , there exists a such that . For example, a numbering that assigns indices to nontrivial programs and all other indices the error state is not dense, but there exists a dense Gödel numbering of syntactically correct Brainfuck programs.[34] A dense Gödel numbering is called optimal if, for any other Gödel numbering , there is a 1-1 total recursive function and a constant such that for all , and . This condition ensures that all programs have indices not much larger than their indices in any other Gödel numbering. Optimal Gödel numberings are constructed by numbering the inputs of a universal Turing machine.[35] A third notion of size uses universal machines operating on binary strings and measures the length of the string needed to describe the input program. A universal machine U is a machine for which every other machine V there exists a total computable function h such that . An optimal machine is a universal machine that achieves the Kolmogorov complexity invariance bound, i.e. for every machine V, there exists c such that for all outputs x, if a V-program of length n outputs x, then there exists a U-program of at most length outputting x.[36]
We consider partial computable functions (algorithms) . For each we consider the fraction of errors among all programs of size metric at most , counting each program for which fails to terminate, produces a "don't know" answer, or produces a wrong answer, i.e. halts and outputs DOES_NOT_HALT
, or does not halt and outputs HALTS
. The behavior may be described as follows, for dense Gödelizations and optimal machines:[34][36]
- 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]
The complex nature of these bounds is due to the oscillatory behavior of . There are infrequently occurring new varieties of programs that come in arbitrarily large "blocks", and a constantly growing fraction of repeats. If the blocks of new varieties are fully included, the error rate is at least , but between blocks the fraction of correctly categorized repeats can be arbitrarily high. In particular a "tally" heuristic that simply remembers the first N inputs and recognizes their equivalents allows reaching an arbitrarily low error rate infinitely often.[34]
Gödel's incompleteness theorems
This section needs additional citations for verification. (August 2019) |
The concepts raised by
The weaker form of the theorem can be proved from the undecidability of the halting problem as follows.
Generalization
Many variants of the halting problem can be found in computability textbooks.
Halting on all inputs
The universal halting problem, also known (in
This means, in particular, that it cannot be decided even with an oracle for the halting problem.
Recognizing partial solutions
There are many programs that, for some inputs, return a correct answer to the halting problem, while for other inputs they do not return an answer at all. However the problem "given program p, is it a partial halting solver" (in the sense described) is at least as hard as the halting problem. To see this, assume that there is an algorithm PHSR ("partial halting solver recognizer") to do that. Then it can be used to solve the halting problem, as follows: To test whether input program x halts on y, construct a program p that on input (x,y) reports true and diverges on all other inputs. Then test p with PHSR.
The above argument is a
Lossy computation
A lossy Turing machine is a Turing machine in which part of the tape may non-deterministically disappear. The halting problem is decidable for a lossy Turing machine but non-
Oracle machines
A machine with an oracle for the halting problem can determine whether particular Turing machines will halt on particular inputs, but they cannot determine, in general, whether machines equivalent to themselves will halt.
See also
- Busy beaver
- Gödel's incompleteness theorem
- Brouwer–Hilbert controversy
- Kolmogorov complexity
- P versus NP problem
- Termination analysis
- Worst-case execution time
Notes
- ISBN 9780735636972.
- ^ Huang, Han-Way (2009). The HCS12 / 9S12: An Introduction to Software and Hardware Interfacing. p. 197.
... if the program gets stuck in a certain loop, ... figure out what's wrong.
- ^ Simon, David E. (1999). An Embedded Software Primer. p. 253.
For hard real-time systems, therefore, it is important to write subroutines that always execute in the same amount of time or that have a clearly identifiable worst case.
- ^ Minsky 1967, p. 24. italics in original
- ^ a b Minsky 1967, p. 25.
- ^ Hodges 1983, p. 83; Davis' commentary in Davis 1965, p. 108
- ^ Absolutely unsolvable problems and relatively undecidable propositions – account of an anticipation, reprinted in Davis 1965, pp. 340–433
- ^ Minsky 1967.
- ^ Reid 1996, pp. 188–189.
- ^ Hodges 1983, p. 91.
- ^ Hodges 1983, p. 91; Penrose 1989, p. 34.
- ^ Reid 1996, p. 198.
- ^ Reid 1996, p. 199.
- ^ reprinted in Davis 1965, p. 5ff
- ^ Church 1936.
- ^ A Note on the Entscheidungsproblem, reprinted in Davis 1965, p. 110
- ^ Davis 1965, p. 289ff.
- ^ reprinted in Davis 1965, p. 115
- ^ a b c d e f Lucas 2021.
- ^ Kleene 1952.
- ^ Rosser, "Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem", reprinted in Davis 1965, p. 223
- ^ a b Kleene 1952, p. 382.
- ^ a b letter from Davis to Copeland, 12 December 2001, Footnote 61 in Copeland 2004, p. 40
- ^ a b Copeland 2004, p. 40.
- ^ Textual search of Turing's collected works: Good (1992), Gandy & Yates (2001), Ince (1992), Saunders (1992). Similarly Hodges (1983) does not have the word "halting" or words "halting problem" in his index.
- ^ Davis 1958, pp. vii–viii.
- ^ Davis 1958, pp. 70–71.
- ^ Moore & Mertens 2011, pp. 236–237.
- .
- S2CID 233329507. Retrieved 26 August 2021.
- ^ Penrose 1989, pp. 57–63.
- ^ Copeland 2004, p. 15.
- S2CID 15005164. Retrieved 5 November 2022.
- ^ ISBN 978-3-540-28193-1.
- .
- ^ S2CID 14763862.
- ^ Aaronson, Scott (21 July 2011). "Rosser's Theorem via Turing machines". Shtetl-Optimized. Retrieved 2 November 2022.
- ^ for example, Sipser 2006, Davis 1958, Minsky 1967, Hopcroft & Ullman 1979, Börger 1989
- ^ Börger 1989, p. 121.
- ^ Abdulla & Jonsson 1996, p. 92.
References
- Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (2): 345–363. JSTOR 2371045.
- 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. ISBN 0-19-825079-7.
- Davis, Martin (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..
- Rogers, Hartley (Jr.) (1957). Theory of Recursive Functions and Effective Computability. Massachusetts Institute of Technology.
- 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.
- Lucas, Salvador (June 2021). "The origins of the halting problem". Journal of Logical and Algebraic Methods in Programming. 121: 100687. S2CID 235396831.
- ISBN 0131655639.. See chapter 8, Section 8.2 "Unsolvability of the Halting Problem."
- ISBN 978-0-19-923321-2.
- 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.
- ISBN 0-534-94728-X.
- ISSN 0024-6115.[permanent dead link ] 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.
- 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.
- ISBN 81-7808-347-7.. See Chapter 7 "Turing Machines." A book centered around the machine-interpretation of "languages", NP-Completeness, etc.
- ISBN 0-671-49207-1.. Cf. Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
- Börger, Egon (1989). Computability, complexity, logic. Amsterdam: North-Holland. ISBN 008088704X.
- Abdulla, Parosh Aziz; Jonsson, Bengt (1996). "Verifying Programs with Unreliable Channels". Information and Computation. 127 (2): 91–101. .
- Collected works of A.M. Turing
- Good, Irving John, ed. (1992). Pure Mathematics. North-Holland. ISBN 978-0-444-88059-8.
- Gandy, R. O.; Yates, C. E. M., eds. (5 December 2001). Mathematical Logic. Elsevier. ISBN 978-0-08-053592-0.
- Ince, D.C., ed. (1992). Mechanical Intelligence. North-Holland. ISBN 978-0-444-88058-1.
- Saunders, P. T., ed. (26 November 1992). Morphogenesis. Elsevier. ISBN 978-0-08-093405-1.
- Good, Irving John, ed. (1992). Pure Mathematics. North-Holland.
Further reading
- c2:HaltingProblem
- Alfred North Whitehead 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.
- Emil Post, Julia Robinson.
- Chaitincontributions.
- Peano Axiomsbriefly, gently introduce readers to formal logic.
- Daras, Nicholas J.; ISBN 978-3319743240.). 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.
{{cite book}}
: CS1 maint: location missing publisher (link - Turing Machinemodel 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.
- Busy BeaverPrograms 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.
- David Bolter, 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.
- Sven Köhler, Christian Schindelhauer, Martin Ziegler, On approximating real-world halting problems, pp.454-466 (2005) Programming Systemunder consideration.
- Logical Limitations to Machine Ethics, with Consequences to Lethal Autonomous Weapons - paper discussed in: Does the Halting Problem Mean No Moral Robots?
External links
- Scooping the loop snooper - a poetic proof of undecidability of the halting problem
- animated movie - an animation explaining the proof of the undecidability of the halting problem
- A 2-Minute Proof of the 2nd-Most Important Theorem of the 2nd Millennium - a proof in only 13 lines
- haltingproblem.org - popular videos and documents explaining the Halting Problem.