March 18, 2012 2 Comments
Take your favorite programming language and write a program in it. Your compute stores the source code as a string of zeros and ones. We can interpret that code as a number in binary. So to each program, we have a number. We may have many numbers whose programs that do the same thing, but any program I can write down has a number associated with it. Let be the program which is encoded by . This might not do anything. It might have lots of spelling mistakes and syntactical errors, but every program is , for some number .
Programs take in inputs and spit out outputs. Or at least, sometimes they do. Sometimes programs run forever. Suppose I am handed a bunch of programs and told to run them on some inputs, but I’m told I only have an hour to do this. Obviously I can’t run the ones that go one forever, so how do I know which ones those are? How do I tell the difference between a program that runs for an obscenely long time, and one that will never end?
The short of it is that I can’t. There is no algorithmic way to determine which programs halt and which programs run forever.
Theorem: There is no program which takes input (an encoding of a program) and (some input to the program encoded by ), and spits out if halts and otherwise.
Proof: Suppose I had such a program. I’m going to make a slightly different program. What it will do is take in some input , and determine whether or not halts. If never halts, it will return . Otherwise, it will enter an infinite loop and never halt. This program sometimes stops and sometimes goes without stopping, so we’ll call it the “Yielding Program.” Here’s some pseudocode for that program:
To save space, I’m going to write for the “yielding program,” and I’m going to let be the number encoding it. That is, . Ready for the magic? Does halt? That is, does return ? If it did, that would mean that we were in the first case in the if-statement, so . But means that (a.k.a. ) doesn’t halt. That’s a contradiction.
What about the other possibility goes on forever. This means that is not , so it must be . But this too is a problem, for then (a.k.a. ) does halt. That’s another contradiction.
Since we used the existence of a program to construct , which lead to a contradiction, it must be that cannot not really exist.
If you didn’t like this proof, then perhaps this one in a Dr. Seuss style will suit you better: Scooping the Loop Snooper