I’ve seen explanations about this, but I don’t see how will the program run in the first place. Example program that will be fed to itself:
define haltOrLoop(P):
if halt(P): loop forever
else: exit
If we run `haltOrLoop(haltOrLoop)` wouldn’t that be incomplete as `haltOrLoop` (the one inside the parenthesis) needs a program to run first?
In: 2
In the traditional definition, the program being tested is always given itself as its input.
In this case, `halt(program, progInput)` is the proper “halting problem” function call, and the program you wrote in your original post should read `halt(P,P)`
The point is we can’t solve the Halting Problem with computers. Computers can’t tell the difference between “a program that is running for a long time” and “a program that cannot ever finish”.
What you did is called “infinite recursion”, and on a real computer it causes a problem called “stack overflow”. But when we’re being computer scientists and talking about Turing Machines, they have infinite memory. You can’t stack overflow with infinite memory, but you will keep using more and more memory forever.
The point of this exercise is to showcase it’s not simple to write `halt(P)` that works for all `P`, because we just wrote a program `P` that cannot be properly evaluated by `halt(P)`.
It’s easy to propose a solution to this case, but real-life infinite recursions are often more subtle and more difficult to detect. Stack overflows don’t really mean that the program can’t finish, they just mean a program has taken so many iterations to complete it’s hit the finite memory bounds of the computer. For example, a recursive AI for a chess program may take what looks like “the same steps” millions of times yet still find a move to make.
Humans can figure this out because we can use intuition and make non-deterministic decisions. Computers (at least not Turing Machines) can’t do this so they cannot reliably distinguish “does the same things very often” from “an infinite loop”. THAT is core of the halting problem.
The details of `haltOrLoop()` are not important. The proof by contradiction is sufficient without any consideration for how it would be implemented.
The only thing the proof must do is propose, “assume `haltOrLoop()` is possible”. *How* it is possible isn’t important. We’re stating as a given that it is possible.
Once it is merely stated that it is possible, we show how that very simple assumption all on its own creates a contradiction. The only logical conclusion, then, is that `haltOrLoop()` is *not* possible. Not for the reason you’re asking about regarding recursion, but in general. There is literally no conceivable way to build `haltOrLoop()`. At all. Recursion or no.
There is another way of thinking about this proof which is equivalent, but I find it a little bit more intuitive.
Instead of assuming we have a halting solver, let’s try to build an actual program maybe_halt(prog). It will analyze the source code of prog in some way. Then our construction is the same: we build
define haltOrLoop(P):
if maybe_halt(P): loop forever
else: exit
It turns out that if maybe_halt(haltOrLoop) says yes, implying that haltOrLoop will halt, the program itself will end up looping. It turns out our maybe_halt is not a full halting solver. It might be right sometimes, but for the program haltOrLoop it makes a mistake.
We can try to build maybe_halt2, which is like maybe_halt, but it also checks if it has been given the original haltOrLoop, and will reverse the original answer. However, now we can create haltOrLoop2:
define haltOrLoop2(P):
if maybe_halt2(P): loop forever
else: exit
Even though maybe_halt2 is a better halting solver, it’s now wrong on this new program haltOrLoop2. And we could do this forever – no matter how good of a halting solver we build, it always makes a mistake somewhere.
Using this framing, we never have to talk about programs that don’t exist. We can build maybe_halt, and in fact we can build it to be very robust and correctly identify many programs that halt. But, there will always be some programs that every prospective halting solver makes mistakes on, no matter how clever we make it, because in the end it is a machine that follows rules rigidly, and we can use those very rules to make it make a mistake.
This proof has the same structure because it’s effectively proving the same statement. Instead of “a perfect halting solver doesn’t exist”, we’re proving “every halting solver is imperfect”. They’re equivalent statements, but the latter means we don’t have to introduce a nonexistent machine and then later prove a contradiction.
Latest Answers