In computability theory, the halting problem is the decision problem of, given an arbitrary computer program and an input, determining whether said program will eventually finish running and halt, or will continue to run forever. Alan Turing proved in 1937 that the halting problem is undecidable, meaning that no general algorithm exists that can correctly solve the problem for all possible program–input pairs. The problem comes up often in discussions of computability since it demonstrates that some functions are mathematically definable but not computable.
A key part of the formal statement of the problem is a mathematical definition of a computer and program, usually via a Turing machine. The proof then shows, for any program that might determine whether programs halt, that a "pathological" program exists for which makes an incorrect determination. Specifically, is the program that, when called with some input, passes its own source and its input to f and does the opposite of what predicts will do. The behavior of on shows undecidability as it means no program 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 Turing-complete model of computation. This model of computation includes all programs in Turing-equivalent programming languages. Given a program and an input, the question is whether the program will eventually halt when run with that particular input. In this abstract framework, there are no limitations on the memory or time required for the program's execution; the program may run arbitrarily long and consume arbitrarily large amounts of storage before halting.
For example, in pseudocode, the program
while (true) continue
never halts; rather, it goes on forever in an infinite loop. By contrast,
print "Hello, world!"
halts immediately after printing.
Simple cases like these are easy to decide, but more complex programs are not. 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
Most subroutines are intended to finish. The fact that the halting problem is undecidable is often naively taken to mean that establishing whether a program halts is impossible. However, programs such as the T2 Temporal Prover could automatically establish that certain Windows device-driver dispatch routines will always eventually return. It appears feasible that "future program-termination proof tools [may] work 99.9% of the time on programs written by humans."
Some infinite loops can be quite useful. For instance, event loops are typically coded as infinite loops. In total functional programming languages these are often encoded using corecursion, as functions that process and produce infinite coinductive data types such as streams. This formalism allows proving a dual termination property known as productivity.
In hard real-time computing, subroutines must not only finish, but finish before a given deadline. In order to meet these requirements, programmers apply the rule of least power and use restricted styles, not quite fully Turing-complete, that make it easy to prove that the resulting subroutines finish before the given deadline. These include languages such as MISRA C, SPARK, and Rocq.
Common pitfalls
The halting problem requires a decision procedure that works for all programs and inputs. But for any specific program and input, the answer is simply "halts" or "does not halt". Consider two simple decision procedures, one that always answers "halts" and another that always answers "does not halt". For any given case, one of these two algorithms answers correctly, yet neither algorithm solves the halting problem.
Interpreters are programs that simulate the execution of programs whatever source code they are given. Such programs can demonstrate that a program does halt, by running the program for some number of steps. 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, or determine whether a program will eventually halt or run forever.
The halting problem is decidable for linear bounded automata (LBAs) or deterministic machines with finite memory. Such a machine has finitely many possible configurations, so any deterministic program on it must eventually either halt or repeat a previous configuration:. italics in original
However, Minsky notes:
For example, a computer with a million two-state components would have at least 21,000,000 possible states:
For nondeterministic finite automata (restricted to finite memory), it is also decidable whether the machine 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
; Davis' commentary in
reprinted in
A Note on the Entscheidungsproblem, reprinted in
Rosser, "Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem", reprinted in
letter from Davis to Copeland, 12 December 2001, Footnote 61 in
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. Turing did not use the terms "halt" or "halting" in any of his published works, including his 1936 paper.Textual search of Turing's collected works: , , , . Similarly does not have the word "halting" or words "halting problem" in his index. A search of the academic literature from 1936 to 1958 showed that the first published material using the term "halting problem" was . However, Rogers says he had a draft of available to him, and Martin Davis states in the introduction that "the expert will perhaps find some novelty in the arrangement and treatment of topics", so the terminology must be attributed to Davis. Davis stated in a letter that he had been referring to the halting problem since 1952. The usage in Davis's book is as follows:
A possible precursor to Davis's formulation is Kleene's 1952 statement, which differs only in wording:
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:
Formalization
In theoretical computer science, a decision problem is any problem that can be phrased as a yes–no question about a mathematical object. Formally, the halting problem is the decision problem:
Given the description of a program (P) and an input (x), does (P(x)) eventually halt?
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.
Undecidability
A decision problem is said to be decidable if there exists an algorithm that always halts with the correct answer, and an undecidable problem if no such algorithm exists. 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.
There are many undecidable problems; any set whose Turing degree equals that of the halting problem is such a formulation. Examples of such sets include, besides the halting problem: {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. 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() -> None: 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:
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):