The Halting Problem is to work out, given an arbitrary program, whether that program terminates. It is known to be completely insoluble.
To understand why, assume you've got some Tcl command willHalt which takes a single argument (a script) and returns a boolean which says whether that script terminates.
The following are obviously true:
[willHalt {}] == 1
[willHalt {while {1} {}}] == 0Now we build the following procedure:
proc nothalt {script} {
if {[willHalt $script]} {
while {1} {}
}
}Thus, [nothalt $script] will halt exactly when $script does not.
proc foobar {} {
nothalt foobar
}Now, we can say that [nothalt foobar] will terminate when [foobar] does not terminate, but we know that [foobar] is defined as [nothalt foobar]. So [foobar] only terminates when it does not terminate!?! Which is complete rot...
The only assumption we've made that is not completely grounded in a script that we can trivially build is the existance of the [willHalt] test. Consequently, there cannot exist any such test (or at least, not one that is guaranteed to complete with the right answer.) QED.
DKF
JC: Gorgeous. With some luck, we could end up with enough gems in here to interest Tim O'Reilly one day!
I'm not sure I agree with the phrase "completely insoluble". Obviously, if you can write a willHalt function, you have it at least partially solved.
You can prove in special cases whether a program will or will not halt, and you can even do so automatically if you can enumerate all of the program's possible states, and if it does no I/O (or you enumerate all possible I/O as part of your enumeration of the program's states). If a program ever returns to exactly the same state during execution, then it will execute forever (remember: no I/O allowed, unless you count all possible I/O as states in your state machine); conversely, if your program ever hits a terminal state, then you know it terminates.
Perhaps it should read "insoluble completely", which is more accurate (although the set of cases where it can be solved is pretty uninteresting).
I think it's provable that any machine which is capable of solving the halting problem in a specific case is not capable of analyzing itself. That's pretty much the same result, I guess...