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

Zygo Blaxell%

Actually -- if you have a machine where all algorithms are guaranteed to terminate (no recursion, iteration only over ennumerated sets of items, i/o limited to specific spans of time -- maybe 2^40 seconds), then willHalt is trivial: proc willHalt {} {return 1}. Here, instead of willHalt being bogus, notHalt is using the undefined command while.

And, given that all computers are finite, this way of looking at things isn't completely unreasonable. To "fix" this problem, texts on the halting problem usually are phrased along the lines of "halt before consuming a certain amount of resources" and the assumption is that the line is drawn someplace interesting.

In fact: most of the times I see someone using recursion I also see a better way of approaching the problem (usually involving use of the properties of numbers). Something to ponder... actually, it isn't even necessary to prohibit recursion. Instead just do what real computers do: when the stack gets too deep, throw an error.

Note that if you want to play around with this style of programming in tcl you'll want to define yourself a couple commands before you get rid of stuff like while and for. You'll want a command to make n copies of something, and you'll want a command to generate the first n indices of an array. See Playing APL for somewhat fleshed out examples of that kind of stuff.

DKF: You can define a willHalt using a three-valued logic (yes/no/dontknow) easily enough; I'll leave that as an exercise. What you can't do is turn it from that into a function that always returns a boolean, and as the above shows that you can't do it for even reasonably small programs. As soon as the problem becomes self-referential, you lose the ability to construct such a proof. In fact, the way you really approach such a function is to establish proofs of termination, which in turn is usually done by demonstrating a monotonically-decreasing metric for loops/recursions that corresponds to the remaining search space. Of course, this can sometimes mean that the proof requires solving an “interesting” problem (e.g., consider looking for Goldbach violations ) so be aware that the proof-theoretic approach has no more power than any other.

“Terminate within X timesteps” is a different problem that is both easier (you can definitively prove it) and harder (it's a lot more work); you need a very different type of analysis to solve it, but the easiest approach is probably to just run the program for that long and see if it does terminate…

AMG: [willHalt] would be useful for safe interps. :^)

I wonder if we should establish a Theory category to group pages such as this one.