The Halting Problem

Kurt Godel, who first proved that some truths are unprovable, made logic seem more "illogical" for all subsequent students of mathematics. But this concept has important implications for computer science because there are problems that no algorithm can solve. One of these is Alan Turing's Halting Problem, the first problem that was proved to be uncomputable. Computer programs either halt (return an output, raise an error, or change a mutable variable) or they never halt (get caught in an infinite loop) and it would be very useful for programmers to have a program that says whether any function given any input will halt or not halt. Unfortunately, the algorithm for such a program cannot be written.

def halt(f, i):
   '''Iff f(i) halts, return True.'''
   *some algorithm here*

The proof for this is simple (but still confusing too wrap your head around) and uses program, which we'll call bang, that halts for some inputs and not for others.

def bang(f):
   '''Return 0 if halt(f, f) is False, else don't halt.'''
   # if halt(f, f) is True, go into an infinite loop.
   while halt(f, f):
      pass
   # if halt(f, f) is False, then stop.
   return 0

So what happens if we run bang(bang)? There are two possibilities:

1.  bang halts, meaning halt(bang, bang) was false. BUT that means halt identified bang as a program that did not halt!
2. bang does not halt, meaning halt(bang, bang) was true. BUT then halt identified bang as a program that does halt!

Thus, we have a proof by contradiction: bang halts if, and only if, it doesn't halt.

So, if at this point you are completely confused that's okay! I had to work through the explanation several times after class before it started to click. Then I sat my room mate down and took him through the proof. After explaining it to him several times, I felt like an expert.