How does the Halting Problem have a contradiction?

Question

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

Answer 1

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.