But if it’s true that there doesn’t exist a proof that it halts, then it will run forever searching for one.
Not remotely! There’s no proof that it halts, and there’s no proof that it doesn’t halt. It will run until it halts or the universe ends—there is no forever. The key is that there can be programs for which nobody can tell which one they are without actually trying them until they halt or the universe ends.
“It’s the halting problem all the way down”, doesn’t resolve the paradox, but does express the issue nicely.
Do you not agree with the sentence you quoted? That if a proof of haltiness doesn’t exist, it will search forever for one? And not halt? Because that trivially follows from the definition of the program. It searches proofs forever, until it finds one.
Nope, it also can’t be proven that it’ll search forever: it might halt a few billion years (or a few hundred ms) in. There’s no period of time of searching after which you can say “it’ll continue to run forever”,as it might halt while you’re saying it, which is embarrassing.
I am referring to the program H which I formally specified in the link I posted. H is a specific program which tries to determine if another program will halt.
I then show how to create a counter example for H. And show that if H returns either true or false, it creates a contradiction. Therefore it can’t ever return true or false.
Therefore I’ve proved it will run forever. And this is just the standard proof of the halting problem. The weird part is that proving this also creates a contradiction.
No, it’s the halting problem all the way down.
Not remotely! There’s no proof that it halts, and there’s no proof that it doesn’t halt. It will run until it halts or the universe ends—there is no forever. The key is that there can be programs for which nobody can tell which one they are without actually trying them until they halt or the universe ends.
The halting problem doesn’t actually imply this.
“It’s the halting problem all the way down”, doesn’t resolve the paradox, but does express the issue nicely.
Do you not agree with the sentence you quoted? That if a proof of haltiness doesn’t exist, it will search forever for one? And not halt? Because that trivially follows from the definition of the program. It searches proofs forever, until it finds one.
Nope, it also can’t be proven that it’ll search forever: it might halt a few billion years (or a few hundred ms) in. There’s no period of time of searching after which you can say “it’ll continue to run forever”,as it might halt while you’re saying it, which is embarrassing.
I am referring to the program
Hwhich I formally specified in the link I posted. H is a specific program which tries to determine if another program will halt.I then show how to create a counter example for
H. And show that ifHreturns eithertrueorfalse, it creates a contradiction. Therefore it can’t ever returntrueorfalse.Therefore I’ve proved it will run forever. And this is just the standard proof of the halting problem. The weird part is that proving this also creates a contradiction.