This is great but (unfortunately) it's not quite right. The author seems to have forgotten the difference between a program without specified inputs -- which can't be said to "halt" or "not halt", because it might halt on some inputs and loop on others -- and a program with specified inputs, which always either halts or loops.
Thus at one point the poem asks whether Q halts without specifying an input to Q. This question is meaningless.
The correct proof is given by BrandonM in a thread somewhere on this page. Check it out. (scott_s restates the incorrect proof above BrandonM, for comparison.)
The bug in my pseudocode is that I did the wrong thing after consulting P inside Q. I'm not convinced that using "program" or "Q" as shorthand for "program(inputs)" and "Q(inputs)" changes the semantics of the pseudocode or the implications of the paradox.
It's a proof, but not a formal one. It doesn't define the notion of "program", for example. It's somewhere between an informal proof and a proof sketch (a correct and valid one, of course).
A formal proof is a sequence of statements where each is either an axiom or derived from previous ones via a set of derivation rules, and wherein assessing the validity of each axiom statement or derivation can be done "typographically" (mechanically and primitive-recursively). It's nigh-impossible to write a human-readable formal proof of anything interesting; the vast majority of mathematical papers published are informal proofs.
(Of course, this diversion doesn't detract from the matter of this proof-poem being very cool.)
Yes I am sorry, I believe I ment "it is in some ways a formal proof." It is indeed a proof sketch. With a preliminary section defining things more rigorously, I do believe that this is publishable in most of the Cryptography conferences I have published in.
Actually, that gives me a sort of unique idea: An online, wikipedia like proof database with understandable informal proofs with click-to-expand (inline) annotated sections, if you click them, they would expand into proof of less formal claims.
The idea would be that we generally share understanding of obvious axioms (and thus, allow them to be request-able assumptions), and so can enhance readability.
I still wonder why the anti-halting-detecting-program + halting-detecting-program aren't viewed as a single program, as they can't be separated from each other in the proof. By wrapping the detector in an external application, aren't you modifying the detector, changing the assumptions of the proof?
An external halting detector (such as one of us) would tell you the hypothetical arrangement would never halt. If we can prove it would never halt, can't a program?
An "external halting detector" couldn't correctly tell if the arrangement would halt. If we decide that the input of the program halts, then the wrapper instance loops infinitely and we were wrong. If we decide that the input of the program doesn't halt, then the wrapper halts and we were also wrong.
That's just it, in that case we are part of the process, because we affect the operation / output. Any halting detector looking the whole thing, which must include us, would show that we always negate what comes out of what we're doing, and would say so.
Just like you did. You've accounted for all output, and demonstrated that it always negates us.
By that, if a halting detector cannot exist, then how do we exist? We can tell if a hypothetically-impossible device (Q calling P and reversing the output) will loop forever or not.
By changing the detector,
you're surely a defector
from the point of the proof.
If what comes out is made moot,
give the whole thing the boot:
look at it from the roof.
edit: previous comment requested my argument in rhyme :)
edit2: second verse!
If the halt-checker is wrapped, isn't it not?
Since we've just solved it, why can't a 'bot?
Just what's going on here?
So if it's internal...
... this damned, infernal...
Lets just go get a beer.
It does look at the wrapper. The problem is that whatever decision P makes about Q, Q then goes and does the opposite. Consider:
def P(program):
if program halts:
true
else:
false
def Q(program):
if P(program):
false
else:
Q(program)
When we call Q(Q), we call P(Q). Let's say P(Q) returns false; P says that Q halts. In that case, the conditional fails, and we then call Q(Q) infinitely. Q has done the opposite of what P said it would do.
Now let's say that P(Q) returns true; P says that Q does not halt. In that case, the conditional succeeds, and Q returns false - it halts. Again, Q has done the opposite of what P said it would do.
Here we have a situation where Q will always do the opposite of what P says it will do. We've constructed a situation where P is always wrong; we've created a paradox. The only way out of it is to say P cannot exist.
Your explanation is good, but your pseudocode doesn't match what you're saying about it. There is a bug. One way to write it would be:
def P (program, input):
if [program on input] halts:
true
else:
false
def Q (input):
if P(Q, input):
Q(input) # P says we halt, so we won't
else:
true # P says we don't halt, so we will
Now, calling P(Q, Q) is what shows the truth of the Halting Problem.
It may be hard to think of conceptually, but when you explicitly state it all, it's pretty easy. P is a program. Q can be a program with P embedded in it. This is not anything unrealistic at all. Furthermore, calling P on (Q, Q) is not all that strange either, until you consider the resulting behavior:
P(Q, Q) -> should return true if Q halts on Q and false otherwise
Q halts on Q:
P -> true
Q loops. P was wrong
Q doesn't halt on Q:
P -> false
Q exits. P was wrong again
As long as programs like Q are allowed in your language, P cannot exist. Now, if you constrain Q such that every loop and recursion includes a proof of completion* , you can write a program P.
* This is generally possible by annotating the loop with a mathematical proof that the looping mechanism is approaching a terminating condition)
While running some errands, I think I realized the core of my trouble accepting this proof. I think it may be the same for a lot of people, but I've never heard it stated, so here it is:
To my mind, it seems logical that if P reaches a paradox, it never returns. It's an infinite logical loop, never finishing, thus never returning true or false. Like evaluating "this statement is false", it's stuck on "if it's true, it's false. If false, true". To that end, the paradox isn't a paradox: it just never finishes.
If this is the case, then P(Q(Q)) does indeed escape the problem entirely: it shows that Q(Q) will never finish. That argument I've made, and I've seen others make, but the realization of the previous paragraph is new. And nobody I've debated this with has really attempted to look outside of "but it's a proof, it proves it", and re-iterating the steps of the proof. Not that many have tried for very long, they usually get upset that I can't see the "obvious". Thanks for sticking it out, I've had longer to think on this than I've had with others, and that may have been what I needed.
This reveals a missing assumption in the proof, or at least one I've never seen stated: that P must finish. If it must finish, then I accept the proof completely. If it's a paradox, I agree, it's a paradox, and it certainly is within that requirement. It must return, but it cannot, therefore it can not exist.
But then I must ask: Why must P finish on all inputs? I can make a program which doesn't (print(num) when passed Pi), why not this one?
I'd be very interested in any input / rebuttals to this. I'm not trying to be difficult, honest! I've understood the proof where P must finish for quite a while, but I don't see that it's a valid assumption if categorically stating that it's inherently un-doable.
Th original P is defined as a program that can decide whether any program halts or not. If your proposed P doesn't terminate for some programs, then it hasn't made a decision, and it's not really the P you set out to find.
In other words: can you make a P that decides correctly for -some- programs, but never gives an answer for others? Sure. (E.g., if the program is "while(true) {}", then it loops, otherwise I don't know.) But unless P works (terminates and gives a decision) for any arbitrary program, it's not generally useful.
Good point. But that doesn't mean it's useless. Check it with an external P: If it's a paradoxical process like is given in the proof, it won't finish, which will be detected, uniquely, as a paradox because it won't halt.
There's a difference between P(Q(Q)) not being able to finish its evaluation and P(Q(Q)) stating that Q(Q) will never finish. If P does not finish, then you have no answer. If you have no answer, then P does not do what we defined it to do.
But I think you're missing the more important point. We defined P to be a certain way, and as a result of that definition, we also demonstrated that it cannot do what we defined it to do. That's the fundamental problem. If you want to think of it in terms of what you're currently hung up on, then consider that implicit in our definition of P is that it will finish.
Also consider that if P does not finish, it's no better than just running the program with its input and observing the behavior.
No, P(Q(Q)) will finish, because P(Q) will not, and Q(Q) will call P(Q), preventing Q(Q) from halting.
As to the definition, I suppose, though it's largely implicit, which is effectively a big no-no in proofs. But that doesn't show that a real-world P must finish. If it doesn't, the failure of it to finish can be detected as detecting a paradox: just detect if the halt-detection halts.
We're doing proof sketches, not formal proofs. In a formal proof, it would be explicit. A proof sketch is to show the big concepts behind the proof. The formal proof grinds through the details to make sure those concepts do, in fact, pan out as we think.
P(Q) will finish because we defined it to do so. It will return either true or false. The problem isn't with the termination (or non-termination) of P(Q), it's with Q(Q). The termination status of Q(Q) is what gives us the paradox: its behavior is the opposite of what P(Q) said it would be. If we can construct a case where P behaves contrary to its definition, then it cannot exist.
In other words, we asked our oracle "Will Q finish?" and our oracle gave us a reply. Then Q went off and did the exact opposite, proving the oracle wrong. But our oracle is, by definition, always right, so we have a Serious Problem. We resolve this Serious Problem by recognizing that we asked our oracle a question that it can never know the answer to.
Remember that Q(Q) is what gives us the paradox in the first place. P(Q(Q)) is nonsense. It's like recognizing that 4/0 is undefined, then trying to define cos(4/0).
I think your discussion about a "real-world P" begs the question. (In the original meaning of the phrase.) The existence of P presents us with a paradox, so how can there be a real-world P?
Because you can re-define the problem by assuming P finishes if and only if it does not encounter a paradox. It's not hard to see it as possible, as we're already assuming P exists and finishes: allowing it more flexibility should only make it more likely to exist.
By allowing it to not finish on paradoxical situations, it can exist in what would normally be a paradox. Thus P(Q(Q)) can indeed exist, because P(Q) does, even though it does not return.
There may still be a way to prove such a paradox-avoiding P cannot exist; I'm not claiming that. Just wondering why we require it to return, when as far as I can tell there's no legitimate, real-world reason to do so. Sure, it makes the proof easier, and allows us to use simple logical grammars... but since when has "simple" always been correct?
The equivalent would be the oracle remaining silent, denying the paradox the possibility of existing. If no statement is made, no paradox can be formed.
P does not encounter a paradox. P is the paradox. We encounter the paradox because we observe that P is incorrect. You can't dance around a paradox at runtime. A paradox means either one of your assumptions is invalid, or your logic is wrong. If it exists, there's no getting around it.
When constructing proofs, we can make assumptions and then run with them. But it's not valid to assume magic - and that's essentially how you want to define P. You want P to be able to detect that it has been used in a paradoxical situation. But it's not reasonable to assume a function knows how it's being used; to do so is basically magic.
We require that P returns because we defined it as a function in the mathematical sense, and mathematical functions have to provide an answer (even if that answer is "undefined"). P is a function that has to return true or false. No other responses, including not giving us an answer, are valid.
We encounter the paradox of P because of the definition.
It doesn't need to detect its own use (though remember: reflection), it just needs to see when a separate use of it will cause a paradoxical situation. The proof wouldn't exist if P(Q) weren't part of Q, because that's what sets up the paradox: it's own return cannot be correct... unless it has another output, maybe?
And when I see a proof that a program cannot detect paradoxes, I'll accept that a modified P cannot. But I've never heard of anything along those lines. Until then, a mis-applied proof simply stifles attempts which may have been fruitful.
Honestly, I think the difficulty you're having is one of form, not content. That is, you understand the mechanics behind the proof, but you don't accept that the form of the proof works. Your objections hinge on the implications of a paradox, and our seemingly arbitrary construction of Q.
Instead of banging your head against this proof more, I think you may want to read up on proofs in general. Your objections would apply to any proof by contradiction.
Example: consider that Q exists even if we don't define it. We discovered it, not invented it. Given P, we can define Q', but the problem with Q is still there. But this really has nothing to do with this specific proof - it's more fundamental than that.
> We encounter the paradox of P because of the definition.
The point of the problem is this: to create a program P that will tell us if f(x) halts or not. Q is simply a function that breaks P so that it cannot give the right answer. Thus making P impossible.
Paradoxes are irrelevant to the issue :)
(You're over thinking this a lot; read one of the formal proofs and it will address pretty much all of your points)
Because you can re-define the problem by assuming P finishes if and only if it does not encounter a paradox. It's not hard to see it as possible, as we're already assuming P exists and finishes: allowing it more flexibility should only make it more likely to exist.
And now P is a nonsolution to the original problem (the halting problem). The original problem was to come up with a program that always decides whether its input program halts. We already can build programs that identify the programs which halt and say nothing about programs that don't -- this is a trivial extension to any working interpreter for the language in question.
P doesn't detect the paradox. We do. We have intelligence; algorithms follow a prescribed set of rules. No one is sure what, exactly, "intelligence" is, but we can say it's not the same as just an algorithm. We're also not guaranteed to be correct.
Remember that P is a program to detect whether any program halts. It's possible to write a program that can detect if some programs will halt. You just have to constrain what the programs can do to the point that the rules the programs can follow will not be Turing-complete. We could also use machine-learning techniques to try to recognize the structure of infinite-loop programs, but that's not the same as an algorithm that is always correct.
To state that requires the assumption that we are qualitatively different than a program. I believe that's been a question since far before Turing's time.
What if we are equivalent to a program? Then a program can be made to detect paradoxes.
I'm comfortable stating that we are qualitatively different than an algorithm. I'm also comfortable stating that we're probably similar to a Bayesian machine-learning process which is only able to make probabilistic determinations.
Same here, just felt it needed to be pointed out. There are plenty of people who do make the claim, in which case experience appears to disprove the proof.
I don't understand your question. Q calls P because it's defined to do so.
I described the runtime behavior because that's easy to grok. Presumably, any P must do some sort of "Oh, this happens, so that must happen." Whether we call that "running" or "inspection" is irrelevant.
The poem got me thinking critically as well. Here is how I rationalized it:
No single program can ever predict the output of another one, because the program doing the predicting could theoretically be embedded in the program being analyzed.
People can theoretically predict outcomes, because they cannot be embedded in programs.
Say halting detectors exist, then you can build a looping detector trivially by merely reversing the outputs from the halting detector. You can then modify the looping detector so that it loops if it doesn't find any loops in the target program.
Then you use the modified looping detector on itself. If you think about it, it can't be used on itself. Because if it says that it will loop then it will itself not loop, and if it says that it won't loop then it will itself loop.
It's a logical paradox, which is also a reductio ad absurbum proof that no such thing as a halting detector can exist.
http://www.muppetlabs.com/~breadbox/txt/al.html