The Halting Problem is to work out, given an arbitrary program, whether that program terminates. It is known to be completely insoluble.
Nota: no somos hermanos ni familia.
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} {}}] == 0
Now 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...