The Halting Program: The Greatest Program Never Writable
The halting problem is a fairly simple idea to describe: given a program and an input, will the program ever terminate when given that input?
Simple to describe, but not simple to solve. In fact, it's literally impossible to implement a program to solve this in general, for any reasonable programming language. Implementing it would, in fact, be a logical contradiction. Yeah, let that sink in for a second. Something so simple and intuitive is literally impossible, even in theory.
It seems even crazier since, intuitively, programmers solve the halting problem all the time. That's because there's plenty of programs that obviously halt, such as a program that just adds two integers (barring how a first-year undergrad would write such a program). Programmers like to write things that obviously do or don't halt (at least, "obviously" to them at that exact moment in time), so that's what they usually do. However, there's plenty of things which you could give the best programmers in the world, and they would have no idea as to whether it halts or not.
This is the real issue of the halting problem: writing a program that works on every program and every input, and itself always halts.
The proof that this can't be done is something any good computer science education should probably cover at one point or another, and it's actually quite nice and simple. Check out section 5.1.5 of Michiel and Anil's awesome (free) book if you haven't seen it before. TL;DR: if you have the halting program, you can write programs that halt if and only if they don't halt.
But we're not interested in that.
We wanna see what awesome stuff someone could build with a halting program. Now, of course, since the existence of the program is itself a contradiction, assuming it exists will let us draw any conclusion we want. But let's skirt past that. Let's assume we have the halting program anyway.
To begin, we assume that someone has written the halting program and exposed it as a simple program called willItHalt. We feed it the source of our program, and it reports "yes" or "no". We don't even need to worry about how inputs are handled, as we can just hardcode them in our source if we have to.
So, here's the first program we're going to write:
doesItExist(generator, test) while(generator.hasNext()) itExists = test(generator.getNext()) if(itExists) return "yes" endif endwhile return "no" end
So, what do we have here? We have a simple program that takes a generator, and a function that tests elements returned by that generator. If ever the test passes, it returns "yes". Otherwise, it returns "no". Hence, it checks if there exists an element in some set that has some property.
Okay, that's no big deal right? We don't need willItHalt for that. It will obviously always halt as long as the generator has a finite number of elements, and all the other functions we call also halt. But maybe the generator is really big, and the test is really slow. Running this would suck, right? Well how about:
doesItExist2(generator, test) while(generator.hasNext()) itExists = test(generator.getNext()) if(itExists) return "yes" endif endwhile loop forever end
That's... pretty stupid. Rather than returning "no", we now just loop forever? But what if we feed that into willItHalt? The program halts if and only if there is an element with the property. So, the output of willItHalt is now the output of our original program, and now we don't need to run our slow program. Now, of course, the only restriction we had on willItHalt is that it eventually halts, so it might be just as slow, or even slower than running doesItExist.
But what if the generator is infinite? Yes, willItHalt still gives the correct answer in finite time even though doesItExist could never halt if the answer was no!
Woah. We now have the greatest program ever.
As long as we can write a test for a property that always terminates, and a way to enumerate all the elements in the set, we can prove whether there exists an element in that set with that property.
We now have a super-powerful theorem prover for any countably infinite set, like: integers, rational numbers, algebraic numbers, and anything that's a finite tuple of these, like points in space and finite matrices. Got a property that you can deterministically test an element for in finite time? Then you can prove if anything at all has that property. Or if everything has this property (just negate the result of the test).
- Goldbach conjecture: solved.
- Collatz conjecture: solved.
- A heck of a lot of other big open problems: totally solved.
Did we mention that the set of all programs and inputs is countably infinite? Wait, forget that. That's how we starting getting contradictions.
And that's with just one trivial program. Clearly, even if the halting program wasn't impossible, it would be the greatest program ever written. It would have to be able to prove theorems that no mathematician has ever been able to. And that's exactly why mathematicians showed it wasn't possible: they like having jobs.