My Favourite Theorems 1 (Halting Problem) 
[Jul. 30th, 200611:01 pm]
viked

One bug that most programmers would have faced is there program going into an endless loop. A wrongly constructed check condition in the loop, which never becomes false, might lead to such a case. I myslef have spent innumerable hours trying to remove this abhorrence. Therefore it would be great if we can have some way of checking whether our program can go in to an endless loop or not. If we are able to do this automatically, using a program, even better. So the problem we face is:
Write a program Halt(P,x) whose arguments are a Program P(actually Program P's source code which is a string) and a string x. If program P when given the arguement x, that is P(x), does not go in to an endless loop then Halt should output "Yes" else it should output "No". For simiplicity we are just considering programs which take a single string arguement. Here is a homework: Try writing the code for Halt. If you are keen on doing this then please dont read ahead (Devilish Grin ;).
This is the problem that turing considered albeit in the context of Turing Machines. He was one of the greatest minds of last century. So surely he must have found a solution. Well he did find a solution but not one that you would expect. I will simplify what he did using modern programming terminology.
Let us assume that such a program Halt exists. Now let us write another program Achilles_Heel.
Achilles_Heel(f){
while(Halt(f,f)==YES){ ; } }
Now what would be the output of this: Halt(Achilles_Heel, Achilles_Heel). Let us assume it is "Yes". This means that Achilles_Heel(Achilles_Heel) does not go into an endless loop. Let us see what happens when we run
Achilles_Heel(Achilles_Heel).
It will call Halt(Achilles_Heel,Achilles_Heel). That returns "Yes" according to our assumption. Therefore the condition of while loop is always true and and Achilles_Heel goes into an endless loop. But this is a contradiction because Halt told us that it should not go into an endless loop. Therefore we must change our assumption and Halt must return NO. This implies that Achilles_Heel(Achilles_Heel) does not halt. Some thinking shows that this again leads to a contradiction. Therefore in either case we have a contradiction which means that our original assumption that "program Halt exists" is faulty and such a program can never be written.
This is the famous "Turings Halting Problem". When I first read the proof of this I was awestruck. It was as if someone has pulled the rug from under my feet. This is one of the most beautiful things I have ever seen. Liars Paradox, Godels Theorem, Cantors Diagonal Arguement, all transferred into the familiar domain of programming. The implications are as profound as Godels Incompleteness Theorem, yet the proof is so easy to understand and explain. Anyone who has done the first course in programming CS101 can be explained this and revel in the joy. There are many similarities here to Godels Proof. Once i have written about that, I will try to comment on those.
But what would have been the implications if Halt had actually existed. Apart from saving us poor programmers from the curse of "Tautology", it would have shaken the world of mathematics. Andrew Wiles would have been saved all those reams of papers (and reams they were!) trying to prove fermats last theorem. Just write a program which loops over all possible integer values of x,y,z and n and halts whenever x^n+y^n=z^n. Now the best part is you never need to run this program. Just pass it to halt and if halt says "NO" Fermats thorem is proved else it is disproved. Many other unsolved conjectures, which talk about existence of certain integers satisfying a property, would have been solved using this method. Halt would have been a practicing mathemticians swiss knife. Unfortunately it was not to be.
One thing I havent read so far is where does this "beautifully evil" paradox occur in lambda calculus. That has the same power as turing machines, which means the same limitations. I suspect Y combinator must play some role there but am not sure what. Will try to find more about that and comment on that too. 

