Version 0 of Halting Problem

Updated 2000-05-03 22:23:35

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} {}}] == 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...

Zygo Blaxell


DKF: Well, if you permit a partial solution, then it is trivial to create a command that provides the willHalt functionality. I do so below...

   proc willHalt {script} {
       switch -exact -- [string trim $script] {
           {}             { return 1 }
           {while {1} {}} { return 0 }
       }
       return -code error "Cannot cope with script \"$script\""
   }

It is possible to extend the above to handle many more cases (including assignment if you are willing to ignore the effects of traces) but you cannot produce a general solution for the reasons outlined towards the top of this page.

More interesting is to ask just how little do we need to restrict the language to make termination a problem that can be answered? It turns out that all you need to do is to provide a proof that every recursion and loop will terminate. Tcl actually forces recursion termination anyway, but loop termination is not guaranteed when using the while and for commands (the willHalt procedure above identifies one of these cases.) The typical way of doing this is to prove that there is a finitely decreasing chain of states that the loop proceeds along (since the chain is finite, the loop must be also.) This chain is then used to reconstruct the loop in terms of a primitive-recursive function, and their termination properties are fairly trivial to prove. (All the classical arithmetic operations on integers are primitive recursive. Even finding the next prime number in a list of all the prime numbers is PR, and that's a sophisticated operation.)

I could write several more paragraphs on this, but it is late and I want to get some shut-eye... :^)