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 (i.e., halt) 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. A key part of the proof was a mathematical definition of a computer and program, which became known as a Turing machine; the halting problem is undecidable over Turing machines. It is one of the first examples of a decision problem.
Informally, for any program f that might determine if programs halt, a "pathological" program g called with an 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.
Jack Copeland (2004) attributes the term halting problem to Martin Davis.
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
does not halt; rather, it goes on forever in an infinite loop. On the other hand, the program
does halt.
While deciding whether these programs halt is simple, more complex programs prove problematic.
One approach to the problem might be to run the program for some number of steps and check if it halts. 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 contradict itself and therefore cannot be correct.
Programming
consequences
Some infinite loops can be quite useful. For instance, event loops are typically coded as infinite loops. However, most subroutines are intended to finish (halt). In particular, in hard real-time computing, programmers attempt to write subroutines that are not only guaranteed to finish (halt), but are also guaranteed to finish before a given deadline.
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.
Other times these programmers apply the rule of least power—they deliberately use a computer language that is not quite fully Turing-complete, often a language that guarantees that all subroutines are guaranteed to finish, such as Coq.
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 "doesn't 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 "doesn't 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 states, and thus any deterministic program on it must eventually either halt or repeat a previous state:
Minsky warns us, however, that machines such as computers with e.g., a million small parts, each with two states, will have at least 21,000,000 possible states:
Minsky exhorts the reader to be suspicious—although a machine may be finite, and finite automata "have a number of theoretical limitations":
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.
Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. A key part of the proof was a mathematical definition of a computer and program, which became known as a Turing machine; the halting problem is undecidable over Turing machines. It is one of the first examples of a decision problem.
Informally, for any program f that might determine if programs halt, a "pathological" program g called with an 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.
Jack Copeland (2004) attributes the term halting problem to Martin Davis.
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 contradict itself and therefore cannot be correct.
Programming
consequences
Some infinite loops can be quite useful. For instance, event loops are typically coded as infinite loops. However, most subroutines are intended to finish (halt). In particular, in hard real-time computing, programmers attempt to write subroutines that are not only guaranteed to finish (halt), but are also guaranteed to finish before a given deadline.
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.
Other times these programmers apply the rule of least power—they deliberately use a computer language that is not quite fully Turing-complete, often a language that guarantees that all subroutines are guaranteed to finish, such as Coq.
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 "doesn't 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 "doesn't 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 states, and thus any deterministic program on it must eventually either halt or repeat a previous state:
...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... (italics in original, Minsky 1967, p. 24)
Minsky warns us, however, that machines such as computers with e.g., a million small parts, each with two states, will have at least 21,000,000 possible states:
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 (Minsky 1967 p. 25):
Minsky exhorts the reader to be suspicious—although a machine may be finite, and finite automata "have a number of theoretical limitations":
...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. (Minsky p. 25)
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.
See Also
- Busy beaver
- Gödel's incompleteness theorem
- Kolmogorov complexity
- P versus NP problem
- Termination analysis
- Worst-case execution time
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
Why Is Turing’s Halting
Problem Unsolvable?
No comments:
Post a Comment