fbpx
Wikipedia

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. Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program–input pairs cannot exist.

For any program f that might determine whether programs halt, a "pathological" program g, called with some input, can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. No f can exist that handles this case. A key part of the proof is a mathematical definition of a computer and program, which is known as a Turing machine; the halting problem is undecidable over Turing machines. It is one of the first cases of decision problems proven to be unsolvable. This proof is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.

Jack Copeland attributes the introduction of the term halting problem to the work of Martin Davis in the 1950s.[1]

Background

The halting problem is a decision problem about properties of computer programs on a fixed Turing-complete model of computation, i.e., all programs that can be written in some given programming language that is general enough to be equivalent to a Turing machine. The problem is to determine, given a program and an input to the program, whether the program will eventually halt when run with that input. In this abstract framework, there are no resource limitations on the amount of memory or time required for the program's execution; it can take arbitrarily long and use an arbitrary amount of storage space before halting. The question is simply whether the given program will ever halt on a particular input.

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

print "Hello, world!"

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. But if the program does not halt, it is unknown whether the program 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.[2] However, most subroutines are intended to finish.[3] 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.[4]

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:[5]

...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:[6]

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":[6]

...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

The halting problem is historically important because it was one of the first problems to be proved undecidable. 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.

Timeline

  • 1900 (1900): David 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".[7]
  • 1920 (1920) – 1921 (1921): Emil Post explores the halting problem for tag systems, regarding it as a candidate for unsolvability.[8] Its unsolvability was not established until much later, by Marvin Minsky.[9]
  • 1928 (1928): Hilbert recasts his 'Second Problem' at the Bologna International Congress.[10] He posed three questions: i.e. #1: Was mathematics complete? #2: Was mathematics consistent? #3: Was mathematics decidable?[11] The third question is known as the Entscheidungsproblem (Decision Problem).[12]
  • 1930 (1930): Kurt Gödel announces a proof as an answer to the first two of Hilbert's 1928 questions.[13] "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"[14]
  • 1931 (1931): Gödel publishes "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I"[15]
  • 19 April 1935 (1935-04-19): Alonzo 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.[16]
  • 1936 (1936): Church publishes the first proof that the Entscheidungsproblem is unsolvable.[17]
  • 7 October 1936 (1936-10-07): Emil 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."[18]
  • May 1936 (1936-05) – January 1937 (1937-01): Alan Turing's paper On Computable Numbers With an Application to the Entscheidungsproblem went to press in May 1936 and reached print in January 1937.[19] Turing's proof departs from calculation by recursive functions and introduces the notion of computation by machine. This is one of the "first examples of decision problems proved unsolvable".[20][page needed]
  • 1939 (1939): J. Barkley Rosser observes the essential equivalence of "effective method" defined by Gödel, Church, and Turing[21]
  • 1943 (1943): In a paper, Stephen Kleene 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?'."
  • 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): Martin 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]

Etymology of the phrase "halting problem"

In none of his work did Turing use the word "halting" or "termination". Turing's biographer Hodges does not have the word "halting" or words "halting problem" in his index. The earliest recorded use of the words "halting problem" is in a proof by Davis in 1958:[24]

"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".

Davis adds no attribution for his proof, so one infers that it is original with him. But Davis has said that Kleene stated the proof informally.[22] Copeland states that:[1]

"The halting problem was so named (and it appears, first stated)[23] by Martin Davis... (It is often said that Turing stated and proved the halting theorem in 'On Computable Numbers', but strictly this is not true)."

Formalization

In his original proof Turing formalized the concept of algorithm by introducing Turing machines. However, the result is in no way specific to them; it applies equally to any other model of computation that is equivalent in its computational power to Turing machines, such as Markov algorithms, Lambda calculus, Post systems, register machines, or tag systems.

What is important is that the formalization allows a straightforward mapping of algorithms to some data type that the algorithm can operate upon. For example, if the formalism lets algorithms define functions over strings (such as Turing machines) then there should be a mapping of these algorithms to strings, and if the formalism lets algorithms define functions over natural numbers (such as computable functions) then there should be a mapping of algorithms to natural numbers. The mapping to strings is usually the most straightforward, but strings over an alphabet with n characters can also be mapped to numbers by interpreting them as numbers in an n-ary numeral system.

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 recursively enumerable, which means there is a computable function that lists all of the pairs (ix) it contains. However, the complement of this set is not recursively enumerable.[25]

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

Christopher Strachey outlined a proof by contradiction that the halting problem is not solvable.[26][27] The proof proceeds as follows: Suppose that there exists a total computable function halts(f) that returns true if the subroutine f halts (when run with no inputs) and returns false otherwise. Now consider the following subroutine:

def g(): if halts(g): loop_forever() 

halts(g) must either return true or false, because halts was assumed to be total. If halts(g) returns true, then g will call loop_forever and never halt, which is a contradiction. If halts(g) returns false, then g will halt, because it will not call loop_forever; this is also a contradiction. Overall, g does the opposite of what halts says g should do, so halts(g) can not return a truth value that is consistent with whether g halts. Therefore, the initial assumption that halts is a total computable function must be false.

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 self-referential. A rigorous proof addresses these issues. The overall goal is to show that there is no total computable function that decides whether an arbitrary program i halts on arbitrary input x; that is, the following function h (for "halts") is not computable:[28]

 

Here program i refers to the i th program in an enumeration of all the programs of a fixed Turing-complete model of computation.

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 it to the halting problem. 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.

Gregory Chaitin has defined a halting probability, represented by the symbol Ω, a type of real number that informally is said to represent the probability that a randomly produced program halts. These numbers have the same Turing degree as the halting problem. It is a normal and transcendental number which can be defined but cannot be completely computed. This means one can prove that there is no algorithm 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 Church–Turing thesis limits what can be accomplished by any machine that implements effective methods. However, not all machines conceivable to human imagination are subject to the Church–Turing thesis (e.g. oracle machines). It is an open question whether there can be actual deterministic physical processes that, in the long run, elude simulation by a Turing machine, and in particular whether any such hypothetical process could usefully be harnessed in the form of a calculating machine (a hypercomputer) that could solve the halting problem for a Turing machine amongst other things. It is also an open question whether any such unknown physical processes are involved in the working of the human brain, and whether humans can solve the halting problem.[29]

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.[30]

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 indexes   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.[31] 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.[32] 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.[33]

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:[31][33]

  • For every algorithm  ,  
  • There exists   such that for every algorithm  ,  
  •  . However, this includes 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.[33]

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.[31]

Gödel's incompleteness theorems

The concepts raised by Gödel's incompleteness theorems are very similar to those raised by the halting problem, and the proofs are quite similar. In fact, a weaker form of the First Incompleteness Theorem is an easy consequence of the undecidability of the halting problem. This weaker form differs from the standard statement of the incompleteness theorem by asserting that an axiomatization of the natural numbers that is both complete and sound is impossible. The "sound" part is the weakening: it means that we require the axiomatic system in question to prove only true statements about natural numbers. Since soundness implies consistency, this weaker form can be seen as a corollary of the strong form. It is important to observe that the statement of the standard form of Gödel's First Incompleteness Theorem is completely unconcerned with the truth value of a statement, but only concerns the issue of whether it is possible to find it through a mathematical proof.

The weaker form of the theorem can be proved from the undecidability of the halting problem as follows.[34] Assume that we have a sound (and hence consistent) and complete axiomatization of all true first-order logic statements about natural numbers. Then we can build an algorithm that enumerates all these statements. This means that there is an algorithm N(n) that, given a natural number n, computes a true first-order logic statement about natural numbers, and that for all true statements, there is at least one n such that N(n) yields that statement. Now suppose we want to decide if the algorithm with representation a halts on input i. We know that this statement can be expressed with a first-order logic statement, say H(a, i). Since the axiomatization is complete it follows that either there is an n such that N(n) = H(a, i) or there is an n' such that N(n') = ¬ H(a, i). So if we iterate over all n until we either find H(a, i) or its negation, we will always halt, and furthermore, the answer it gives us will be true (by soundness). This means that this gives us an algorithm to decide the halting problem. Since we know that there cannot be such an algorithm, it follows that the assumption that there is a consistent and complete axiomatization of all true first-order logic statements about natural numbers must be false.

Generalization

Many variants of the halting problem can be found in computability textbooks.[35] Typically, these problems are RE-complete and describe sets of complexity   in the arithmetical hierarchy, the same as the standard halting problem. The variants are thus undecidable, and the standard halting problem reduces to each variant and vice-versa. However, some variants have a higher degree of unsolvability and cannot be reduced to the standard halting problem. The next two examples are common.

Halting on all inputs

The universal halting problem, also known (in recursion theory) as totality, is the problem of determining whether a given computer program will halt for every input (the name totality comes from the equivalent question of whether the computed function is total). This problem is not only undecidable, as the halting problem is, but highly undecidable. In terms of the arithmetical hierarchy, it is  -complete.[36]

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 reduction of the halting problem to PHS recognition, and in the same manner, harder problems such as halting on all inputs can also be reduced, implying that PHS recognition is not only undecidable, but higher in the arithmetical hierarchy, specifically  -complete.

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-primitive recursive.[37]

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

Notes

  1. ^ a b Copeland 2004, p. 40.
  2. ^ McConnell, Steve (2004). Code Complete (2nd ed.). Pearson Education. p. 374. ISBN 9780735636972.
  3. ^ 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.
  4. ^ 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.
  5. ^ Minsky 1967, p. 24. italics in original
  6. ^ a b Minsky 1967, p. 25.
  7. ^ Hodges 1983, p. 83; Davis' commentary in Davis 1965, p. 108
  8. ^ Absolutely unsolvable problems and relatively undecidable propositions – account of an anticipation, reprinted in Davis 1965, pp. 340–433
  9. ^ Minsky 1967.
  10. ^ Reid 1996, pp. 188–189.
  11. ^ Hodges 1983, p. 91.
  12. ^ Hodges 1983, p. 91; Penrose 1989, p. 34.
  13. ^ Reid 1996, p. 198.
  14. ^ Reid 1996, p. 199.
  15. ^ reprinted in Davis 1965, p. 5ff
  16. ^ Church 1936.
  17. ^ A Note on the Entscheidungsproblem, reprinted in Davis 1965, p. 110
  18. ^ Davis 1965, p. 289ff.
  19. ^ reprinted in Davis 1965, p. 115
  20. ^ Kleene 1952.
  21. ^ Rosser, "Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem", reprinted in Davis 1965, p. 223
  22. ^ a b Kleene 1952, p. 382.
  23. ^ a b letter from Davis to Copeland, 12 December 2001, Footnote 61 in Copeland 2004, p. 40
  24. ^ Davis 1958, pp. 70–71.
  25. ^ Moore & Mertens 2011, pp. 236–237.
  26. ^ Strachey, C. (1 January 1965). "An impossible program". The Computer Journal. 7 (4): 313. doi:10.1093/comjnl/7.4.313.
  27. ^ Daylight, Edgar G. (16 April 2021). "The halting problem and security's language-theoretic approach: Praise and criticism from a technical historian" (PDF). Computability. 10 (2): 141–158. doi:10.3233/COM-180217. S2CID 233329507. Retrieved 26 August 2021.
  28. ^ Penrose 1989, pp. 57–63.
  29. ^ Copeland 2004, p. 15.
  30. ^ Hamkins, Joel David; Miasnikov, Alexei (1 October 2006). "The Halting Problem Is Decidable on a Set of Asymptotic Probability One" (PDF). Notre Dame Journal of Formal Logic. 47 (4). doi:10.1305/ndjfl/1168352664. S2CID 15005164. Retrieved 5 November 2022.
  31. ^ a b c Köhler, Sven; Schindelhauer, Christian; Ziegler, Martin (2005). "On Approximating Real-World Halting Problems". Fundamentals of Computation Theory. Lecture Notes in Computer Science. 3623: 454–466. doi:10.1007/11537311_40. ISBN 978-3-540-28193-1.
  32. ^ Lynch, Nancy (October 1974). "Approximations to the halting problem" (PDF). Journal of Computer and System Sciences. 9 (2): 143–150. doi:10.1016/S0022-0000(74)80003-6.
  33. ^ a b c Bienvenu, Laurent; Desfontaines, Damien; Shen, Alexander (5 April 2016). "Generic algorithms for halting problem and optimal machines revisited". Logical Methods in Computer Science. 12 (2): 1. arXiv:1505.00731. doi:10.2168/LMCS-12(2:1)2016. S2CID 14763862.
  34. ^ Aaronson, Scott (21 July 2011). "Rosser's Theorem via Turing machines". Shtetl-Optimized. Retrieved 2 November 2022.
  35. ^ for example, Sipser 2006, Davis 1958, Minsky 1967, Hopcroft & Ullman 1979, Börger 1989
  36. ^ Börger 1989, p. 121.
  37. ^ Abdulla & Jonsson 1996, p. 92.

References

  • Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (2): 345–363. doi:10.2307/2371045. 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..
  • Kleene, Stephen Cole (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.
  • Minsky, Marvin (1967). Computation: finite and infinite machines. Englewood Cliffs, NJ: Prentice-Hall. ISBN 0131655639.. See chapter 8, Section 8.2 "Unsolvability of the Halting Problem."
  • Moore, Cristopher; Mertens, Stephan (2011). The Nature of Computation. Oxford University Press. doi:10.1093/acprof:oso/9780199233212.001.0001. ISBN 978-0-19-923321-2.
  • Reid, Constance (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.
  • Sipser, Michael (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.
  • Turing, A. M. (1937). "On Computable Numbers, with an Application to the Entscheidungsproblem". Proceedings of the London Mathematical Society. Wiley. s2-42 (1): 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. Wiley. s2-43 (1): 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.
  • Penrose, Roger (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.
  • Hopcroft, John E.; 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.
  • Hodges, Andrew (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.
  • 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. doi:10.1006/inco.1996.0053.

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.
  • Martin Davis, "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.
  • Edward Beltrami, 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.
  • Ernest Nagel 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.
  • Daras, Nicholas J.; Rassias, Themistocles M. (2018). Modern discrete mathematics and analysis: with applications in cryptography, information systems and modeling. Cham, Switzerland. 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.
  • Taylor Booth, 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.
  • Busy Beaver 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.
  • 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) ISBN 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.
  • 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

halting, problem, this, article, includes, list, general, references, lacks, sufficient, corresponding, inline, citations, please, help, improve, this, article, introducing, more, precise, citations, september, 2018, learn, when, remove, this, template, messag. This article includes a list of general references but it lacks sufficient corresponding inline citations Please help to improve this article by introducing more precise citations September 2018 Learn how and when to remove this template message 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 Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program input pairs cannot exist For any program f that might determine whether programs halt a pathological program g called with some input can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do No f can exist that handles this case A key part of the proof is a mathematical definition of a computer and program which is known as a Turing machine the halting problem is undecidable over Turing machines It is one of the first cases of decision problems proven to be unsolvable This proof is significant to practical computing efforts defining a class of applications which no programming invention can possibly perform perfectly Jack Copeland attributes the introduction of the term halting problem to the work of Martin Davis in the 1950s 1 Contents 1 Background 1 1 Programming consequences 1 2 Common pitfalls 2 History 2 1 Timeline 2 2 Etymology of the phrase halting problem 3 Formalization 3 1 Representation as a set 3 2 Proof concept 3 3 Sketch of rigorous proof 4 Computability theory 4 1 Approximations 4 2 Godel s incompleteness theorems 5 Generalization 5 1 Halting on all inputs 5 2 Recognizing partial solutions 5 3 Lossy computation 5 4 Oracle machines 6 See also 7 Notes 8 References 9 Further reading 10 External linksBackground EditThe halting problem is a decision problem about properties of computer programs on a fixed Turing complete model of computation i e all programs that can be written in some given programming language that is general enough to be equivalent to a Turing machine The problem is to determine given a program and an input to the program whether the program will eventually halt when run with that input In this abstract framework there are no resource limitations on the amount of memory or time required for the program s execution it can take arbitrarily long and use an arbitrary amount of storage space before halting The question is simply whether the given program will ever halt on a particular input For example in pseudocode the program while true continuedoes not halt rather it goes on forever in an infinite loop On the other hand the program a href Hello world program html class mw redirect title Hello world program print Hello world a 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 But if the program does not halt it is unknown whether the program 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 Edit Some infinite loops can be quite useful For instance event loops are typically coded as infinite loops 2 However most subroutines are intended to finish 3 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 4 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 Edit 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 5 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 6 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 6 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 EditFurther information Algorithm History Development of the notion of algorithm The halting problem is historically important because it was one of the first problems to be proved undecidable 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 Timeline Edit 1900 1900 David 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 7 1920 1920 1921 1921 Emil Post explores the halting problem for tag systems regarding it as a candidate for unsolvability 8 Its unsolvability was not established until much later by Marvin Minsky 9 1928 1928 Hilbert recasts his Second Problem at the Bologna International Congress 10 He posed three questions i e 1 Was mathematics complete 2 Was mathematics consistent 3 Was mathematics decidable 11 The third question is known as the Entscheidungsproblem Decision Problem 12 1930 1930 Kurt Godel announces a proof as an answer to the first two of Hilbert s 1928 questions 13 At first he Hilbert was only angry and frustrated but then he began to try to deal constructively with the problem Godel himself felt and expressed the thought in his paper that his work did not contradict Hilbert s formalistic point of view 14 1931 1931 Godel publishes On Formally Undecidable Propositions of Principia Mathematica and Related Systems I 15 19 April 1935 1935 04 19 Alonzo 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 16 1936 1936 Church publishes the first proof that the Entscheidungsproblem is unsolvable 17 7 October 1936 1936 10 07 Emil 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 18 May 1936 1936 05 January 1937 1937 01 Alan Turing s paper On Computable Numbers With an Application to the Entscheidungsproblem went to press in May 1936 and reached print in January 1937 19 Turing s proof departs from calculation by recursive functions and introduces the notion of computation by machine This is one of the first examples of decision problems proved unsolvable 20 page needed 1939 1939 J Barkley Rosser observes the essential equivalence of effective method defined by Godel Church and Turing 21 1943 1943 In a paper Stephen Kleene 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 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 Martin 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 Etymology of the phrase halting problem Edit In none of his work did Turing use the word halting or termination Turing s biographer Hodges does not have the word halting or words halting problem in his index The earliest recorded use of the words halting problem is in a proof by Davis in 1958 24 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 Davis adds no attribution for his proof so one infers that it is original with him But Davis has said that Kleene stated the proof informally 22 Copeland states that 1 The halting problem was so named and it appears first stated 23 by Martin Davis It is often said that Turing stated and proved the halting theorem in On Computable Numbers but strictly this is not true Formalization EditIn his original proof Turing formalized the concept of algorithm by introducing Turing machines However the result is in no way specific to them it applies equally to any other model of computation that is equivalent in its computational power to Turing machines such as Markov algorithms Lambda calculus Post systems register machines or tag systems What is important is that the formalization allows a straightforward mapping of algorithms to some data type that the algorithm can operate upon For example if the formalism lets algorithms define functions over strings such as Turing machines then there should be a mapping of these algorithms to strings and if the formalism lets algorithms define functions over natural numbers such as computable functions then there should be a mapping of algorithms to natural numbers The mapping to strings is usually the most straightforward but strings over an alphabet with n characters can also be mapped to numbers by interpreting them as numbers in an n ary numeral system Representation as a set Edit Main article Decision problem 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 recursively enumerable which means there is a computable function that lists all of the pairs i x it contains However the complement of this set is not recursively enumerable 25 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 Edit Christopher Strachey outlined a proof by contradiction that the halting problem is not solvable 26 27 The proof proceeds as follows Suppose that there exists a total computable function halts f that returns true if the subroutine f halts when run with no inputs and returns false otherwise Now consider the following subroutine def g if halts g loop forever halts g must either return true or false because halts was assumed to be total If halts g returns true then g will call loop forever and never halt which is a contradiction If halts g returns false then g will halt because it will not call loop forever this is also a contradiction Overall g does the opposite of what halts says g should do so halts g can not return a truth value that is consistent with whether g halts Therefore the initial assumption that halts is a total computable function must be false Sketch of rigorous proof Edit 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 self referential A rigorous proof addresses these issues The overall goal is to show that there is no total computable function that decides whether an arbitrary program i halts on arbitrary input x that is the following function h for halts is not computable 28 h i x 1 if program i halts on input x 0 otherwise displaystyle h i x begin cases 1 amp text if text program i text halts on input x 0 amp text otherwise end cases Here program i refers to the i th program in an enumeration of all the programs of a fixed Turing complete model of computation f i j i1 2 3 4 5 6j 1 1 0 0 1 0 12 0 0 0 1 0 03 0 1 0 1 0 14 1 0 0 1 0 05 0 0 0 1 1 16 1 1 0 0 1 0f i i 1 0 0 1 1 0g i U 0 0 U U 0Possible 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 g i 0 if f i i 0 undefined otherwise displaystyle g i begin cases 0 amp text if f i i 0 text undefined amp text otherwise end cases 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 EditMain article Computability theory A typical method of proving a problem to be undecidable is to reduce it to the halting problem 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 Gregory Chaitin has defined a halting probability represented by the symbol W a type of real number that informally is said to represent the probability that a randomly produced program halts These numbers have the same Turing degree as the halting problem It is a normal and transcendental number which can be defined but cannot be completely computed This means one can prove that there is no algorithm which produces the digits of W 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 Church Turing thesis limits what can be accomplished by any machine that implements effective methods However not all machines conceivable to human imagination are subject to the Church Turing thesis e g oracle machines It is an open question whether there can be actual deterministic physical processes that in the long run elude simulation by a Turing machine and in particular whether any such hypothetical process could usefully be harnessed in the form of a calculating machine a hypercomputer that could solve the halting problem for a Turing machine amongst other things It is also an open question whether any such unknown physical processes are involved in the working of the human brain and whether humans can solve the halting problem 29 Approximations Edit 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 lim n P x halts is decidable x has n states 1 displaystyle lim n to infty P x text halts is decidable mid x text has n text states 1 over programs x displaystyle x 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 30 To avoid these issues several restricted notions of the size of a program have been developed A dense Godel 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 Godelization f is dense iff for all i displaystyle i there exists a c gt 0 displaystyle c gt 0 such that lim inf n j N 0 j lt n ϕ i ϕ j n c displaystyle liminf n to infty j in mathbb N 0 leq j lt n phi i phi j n geq c For example a numbering that assigns indexes 2 n displaystyle 2 n to nontrivial programs and all other indices the error state is not dense but there exists a dense Godel numbering of syntactically correct Brainfuck programs 31 A dense Godel numbering is called optimal if for any other Godel numbering a displaystyle alpha there is a 1 1 total recursive function f displaystyle f and a constant c displaystyle c such that for all i displaystyle i a i ϕ f i displaystyle alpha i phi f i and f i c i displaystyle f i leq ci This condition ensures that all programs have indices not much larger than their indices in any other Godel numbering Optimal Godel numberings are constructed by numbering the inputs of a universal Turing machine 32 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 V x U h x displaystyle V x U h x 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 n c displaystyle n c outputting x 33 We consider partial computable functions algorithms A displaystyle A For each n displaystyle n we consider the fraction ϵ n A displaystyle epsilon n A of errors among all programs of size metric at most n displaystyle n counting each program x displaystyle x for which A displaystyle A fails to terminate produces a don t know answer or produces a wrong answer i e x displaystyle x halts and A x displaystyle A x outputs DOES NOT HALT or x displaystyle x does not halt and A x displaystyle A x outputs HALTS The behavior may be described as follows for dense Godelizations and optimal machines 31 33 For every algorithm A displaystyle A lim inf n ϵ n A gt 0 displaystyle liminf n to infty epsilon n A gt 0 There exists ϵ gt 0 displaystyle epsilon gt 0 such that for every algorithm A displaystyle A lim sup n ϵ n A ϵ displaystyle limsup n to infty epsilon n A geq epsilon inf A lim inf n ϵ n A 0 displaystyle inf A liminf n to infty epsilon n A 0 However this includes 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 inf A honest lim inf n ϵ n A displaystyle inf A textrm honest liminf n to infty epsilon n A 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 33 The complex nature of these bounds is due to the oscillatory behavior of ϵ n A displaystyle epsilon n A 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 ϵ displaystyle epsilon 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 31 Godel s incompleteness theorems Edit This section needs additional citations for verification Please help improve this article by adding citations to reliable sources Unsourced material may be challenged and removed August 2019 Learn how and when to remove this template message The concepts raised by Godel s incompleteness theorems are very similar to those raised by the halting problem and the proofs are quite similar In fact a weaker form of the First Incompleteness Theorem is an easy consequence of the undecidability of the halting problem This weaker form differs from the standard statement of the incompleteness theorem by asserting that an axiomatization of the natural numbers that is both complete and sound is impossible The sound part is the weakening it means that we require the axiomatic system in question to prove only true statements about natural numbers Since soundness implies consistency this weaker form can be seen as a corollary of the strong form It is important to observe that the statement of the standard form of Godel s First Incompleteness Theorem is completely unconcerned with the truth value of a statement but only concerns the issue of whether it is possible to find it through a mathematical proof The weaker form of the theorem can be proved from the undecidability of the halting problem as follows 34 Assume that we have a sound and hence consistent and complete axiomatization of all true first order logic statements about natural numbers Then we can build an algorithm that enumerates all these statements This means that there is an algorithm N n that given a natural number n computes a true first order logic statement about natural numbers and that for all true statements there is at least one n such that N n yields that statement Now suppose we want to decide if the algorithm with representation a halts on input i We know that this statement can be expressed with a first order logic statement say H a i Since the axiomatization is complete it follows that either there is an n such that N n H a i or there is an n such that N n H a i So if we iterate over all n until we either find H a i or its negation we will always halt and furthermore the answer it gives us will be true by soundness This means that this gives us an algorithm to decide the halting problem Since we know that there cannot be such an algorithm it follows that the assumption that there is a consistent and complete axiomatization of all true first order logic statements about natural numbers must be false Generalization EditMany variants of the halting problem can be found in computability textbooks 35 Typically these problems are RE complete and describe sets of complexity S 1 0 displaystyle Sigma 1 0 in the arithmetical hierarchy the same as the standard halting problem The variants are thus undecidable and the standard halting problem reduces to each variant and vice versa However some variants have a higher degree of unsolvability and cannot be reduced to the standard halting problem The next two examples are common Halting on all inputs Edit The universal halting problem also known in recursion theory as totality is the problem of determining whether a given computer program will halt for every input the name totality comes from the equivalent question of whether the computed function is total This problem is not only undecidable as the halting problem is but highly undecidable In terms of the arithmetical hierarchy it is P 2 0 displaystyle Pi 2 0 complete 36 This means in particular that it cannot be decided even with an oracle for the halting problem Recognizing partial solutions Edit 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 reduction of the halting problem to PHS recognition and in the same manner harder problems such as halting on all inputs can also be reduced implying that PHS recognition is not only undecidable but higher in the arithmetical hierarchy specifically P 2 0 displaystyle Pi 2 0 complete Lossy computation Edit 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 primitive recursive 37 Oracle machines Edit See also Turing jump 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 EditBusy beaver Godel s incompleteness theorem Brouwer Hilbert controversy Kolmogorov complexity P versus NP problem Termination analysis Worst case execution timeNotes Edit a b Copeland 2004 p 40 McConnell Steve 2004 Code Complete 2nd ed Pearson Education p 374 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 Kleene 1952 Rosser Informal Exposition of Proofs of Godel 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 Davis 1958 pp 70 71 Moore amp Mertens 2011 pp 236 237 Strachey C 1 January 1965 An impossible program The Computer Journal 7 4 313 doi 10 1093 comjnl 7 4 313 Daylight Edgar G 16 April 2021 The halting problem and security s language theoretic approach Praise and criticism from a technical historian PDF Computability 10 2 141 158 doi 10 3233 COM 180217 S2CID 233329507 Retrieved 26 August 2021 Penrose 1989 pp 57 63 Copeland 2004 p 15 Hamkins Joel David Miasnikov Alexei 1 October 2006 The Halting Problem Is Decidable on a Set of Asymptotic Probability One PDF Notre Dame Journal of Formal Logic 47 4 doi 10 1305 ndjfl 1168352664 S2CID 15005164 Retrieved 5 November 2022 a b c Kohler Sven Schindelhauer Christian Ziegler Martin 2005 On Approximating Real World Halting Problems Fundamentals of Computation Theory Lecture Notes in Computer Science 3623 454 466 doi 10 1007 11537311 40 ISBN 978 3 540 28193 1 Lynch Nancy October 1974 Approximations to the halting problem PDF Journal of Computer and System Sciences 9 2 143 150 doi 10 1016 S0022 0000 74 80003 6 a b c Bienvenu Laurent Desfontaines Damien Shen Alexander 5 April 2016 Generic algorithms for halting problem and optimal machines revisited Logical Methods in Computer Science 12 2 1 arXiv 1505 00731 doi 10 2168 LMCS 12 2 1 2016 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 amp Ullman 1979 Borger 1989 Borger 1989 p 121 Abdulla amp Jonsson 1996 p 92 References EditChurch Alonzo 1936 An Unsolvable Problem of Elementary Number Theory American Journal of Mathematics 58 2 345 363 doi 10 2307 2371045 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 Kleene Stephen Cole 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 Minsky Marvin 1967 Computation finite and infinite machines Englewood Cliffs NJ Prentice Hall ISBN 0131655639 See chapter 8 Section 8 2 Unsolvability of the Halting Problem Moore Cristopher Mertens Stephan 2011 The Nature of Computation Oxford University Press doi 10 1093 acprof oso 9780199233212 001 0001 ISBN 978 0 19 923321 2 Reid Constance 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 Sipser Michael 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 Turing A M 1937 On Computable Numbers with an Application to the Entscheidungsproblem Proceedings of the London Mathematical Society Wiley s2 42 1 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 Wiley s2 43 1 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 Penrose Roger 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 Hopcroft John E 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 Hodges Andrew 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 Borger 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 doi 10 1006 inco 1996 0053 Further reading Editc2 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 Martin Davis 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 Edward Beltrami 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 Ernest Nagel 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 Daras Nicholas J Rassias Themistocles M 2018 Modern discrete mathematics and analysis with applications in cryptography information systems and modeling Cham Switzerland 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 Taylor Booth 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 Busy Beaver 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 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 Kohler Christian Schindelhauer Martin Ziegler On approximating real world halting problems pp 454 466 2005 ISBN 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 Logical Limitations to Machine Ethics with Consequences to Lethal Autonomous Weapons paper discussed in Does the Halting Problem Mean No Moral Robots External links EditScooping 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 Retrieved from https en wikipedia org w index php title Halting problem amp oldid 1134678960, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.