I’m Very Confused About The Halting Problem

I’m very confused about the halting problem.

Lets say you want to know whether or not a computer program will get stuck in an infinite loop, or eventually halt. It would be really cool if there was a computer program that could determine if another program would halt or not.

Let’s create one using a naive approach. It won’t be very efficient, but it should eventually find a proof that the program halts or not, if such a proof exists. It will search through the space of all possible proofs. By brute force.

It goes through every possible set of symbols, and feeds them into a proof verifier. If the symbols create a valid proof that the program halts, it returns true. If they create a valid proof that it won’t ever halt, it returns false. Otherwise it keeps searching.

Let me make this a bit more formal. We will call this program H. H takes two arguments: x and i. x is a program that we want to determine halts, and i is an input to that program. If it can prove x(i) halts, then it returns true. If it can prove it doesn’t halt, it returns false.

function H(x, i)
    while true do
        proof = create_next_proof()
        if check_if_proof_proves_x_halts(proof, x, i) then
            return true
        end
        if check_if_proof_proves_x_doesnt_halt(proof, x, i) then
            return false
        end
    end
end

So H(count, 5) will see if the program count halts on the input 5.

Now we are going to trick H. We are going to make another program called “Filthy-Liar” or FL. FL is going to make H’s job hard, by creating a situation where it can’t prove whether it halts or not.

FL takes one input, x. FL runs H(x, x). That is, it asks H if x(x) halts. x is a program and given itself as it’s input.

Now if H returns true, FL enters an infinite loop. If H returns false, FL halts immediately.

FL(x)
    if H(x, x) then
        --infinite loop
        while true do
        end
    else
        --halt
        return
    end
end

Now what happens when I do this:

H(FL, FL)

H will try to determine whether FL(FL) halts. FL(FL)’s halting behaviour is determined by H(FL, FL). If H(FL, FL) returns true - that FL(FL) does halt - then FL(FL) loops forever. If H(FL, FL) returns false - that FL(FL) gets stuck in an infinite loop - then FL(FL) halts immediately.

Therefore, whatever H returns, it must be wrong. Or H doesn’t return anything, and simply gets stuck an infinite loop.

Everything I’ve presented so far is the standard proof that the Halting problem is impossible.

But the standard halting problem only asks if H can exist. A program which determines whether another program halts or not, in a finite amount of time.

I’ve already specified an algorithm for H: searching through all possible proofs.

Therefore, if H can’t ever find a proof that FL(FL) halts, it means that no such proof exists. Otherwise it would eventually find it.

Therefore, no proof that FL(FL) halts, or does not halt, exists.

Therefore, H(FL, FL) will run forever, and never halt.

Now, I’ve just proved that H(FL, FL) doesn’t halt. If H(FL, FL) doesn’t halt, then FL(FL) can’t halt either, since it contains H(FL, FL).

Therefore we’ve also proved that FL(FL) can’t halt.

Now here is the weird and confusing part. If the above is a valid proof, then H will eventually find it. It searches all proofs, remember?

And if H finds that proof, it will return false. And then FL will halt immediately.

And therefore FL(FL) does halt! And H(FL, FL) was wrong!

But if we assume that H can’t be wrong, and that all proofs are checked to be valid, then we are stuck in a terrible paradox. This is where I’m very confused.

Anything we can prove about this system, H should also be able to prove. Even if we prove that there doesn’t exist a proof of something, H can also prove it, and then find the consequences of that.

That means that we can’t actually prove that a proof doesn’t exist, or it creates a paradox. But we did prove it! And the reasoning is sound! Either H returns true, or false, or loops forever. The first two options can’t be true, on pain of paradox. Leaving only the last possibility. But if we can prove that, so can H. And that itself creates a paradox.

I am just very confused about this.

I think the problem was we assumed we were “outside of the system”. Looking in on the weird paradoxes that logical systems can create. But we are also using logical reasoning and inference rules. We are not really outside the system. The same paradoxes apply to us.

If there is no way for H to prove whether it halts or not, then we can’t prove it either. If H is truly “undecidable”, then proving it’s undecidable is also undecidable.

Still very confused.

One possible resolution might be to reject infinity. Infinity is the source of a lot of mathematical paradoxes.

If you ask whether a program will halt in n steps, it’s easily decidable. Even for absurdly large values of n. Does FL(FL) halt in 3↑↑↑3 steps?

At worst, you can create a proof by simply running it n steps and showing that it still hasn’t halted. In theory there might be a way of finding a shorter proof in many cases.

Tags: halting problem undecidability CS math

A Place For Houshalter

I’m Very Confused About The Halting Problem