7 ms·
How Dr. Seuss would prove the halting problem undecidable
- ryanjmo 17y agoThis somehow seems easier to follow than a formal proof (even though it is actually a formal proof). Fun times!
- realrbman 17y agoI wish my professor gave us this in my CS Theory course. Would have made it ten times as much fun, and much less dry.
- pw0ncakes 17y agoIt'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.)
- ryanjmo 17y agoYes 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.
- alain94040 17y agoWith a preliminary section defining things more rigorously I do believe that this is publishable in a conference on Cryptography [trying to get the rhyme going for you]
- kaddar 17y agoActually, 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.
- chbarts 17y agohttp://us.metamath.org/ http://us.metamath.org/ Do you know about Metamath yet? It's something similar to what you want, but it's all in a single program as opposed to being web-based.
- pmichaud 17y agoI can't upvote this enough, it's amazing.
- ireadzalot 17y agoI still don't get it.
- InclinedPlane 17y agoSay 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.
- ireadzalot 17y agoThanks.
- jcl 17y agoReminds me of the "Theory of Relativity in words of four letters or less" (which is also quite readable): http://www.muppetlabs.com/~breadbox/txt/al.html http://www.muppetlabs.com/~breadbox/txt/al.html
- lionhearted 17y agoThat was amazing. Thank you.
- patio11 17y agoThis has greatly improved my understanding of relativity. Thank you.
- elbenshira 17y agoI personally found Einstein's own book more intuitive, probably because he (understandably) goes into more detail than this short story: http://books.google.com/books?id=gQ8LAAAAYAAJ&dq=special%20general%20relativity%20einstein&pg=PR3#v=onepage&q&f=false http://books.google.com/books?id=gQ8LAAAAYAAJ&dq=special...
- ErrantX 17y agoExcellent find! I just started a book of basic world history and this inspired me to have a go at my own Seuss-like verse :D
- Groxx 17y agoI 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?
- meastham 17y agoAn "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.
- Groxx 17y agoThat'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.
- deleted 17y ago[deleted]
- Groxx 17y agoBy 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.
- deleted 17y ago[deleted]
- adamc 17y agoOK, that made my day. Although it reminds me of the barber paradox (http://en.wikipedia.org/wiki/Barber_paradox http://en.wikipedia.org/wiki/Barber_paradox) in its self-referentiality.
- InclinedPlane 17y agoThis is also amusing: http://stackoverflow.com/questions/235984/the-halting-problem-in-the-field http://stackoverflow.com/questions/235984/the-halting-proble...
- trominos 17y agoThis 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.)
- scott_s 17y agoThe 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.
- dmoney 17y agoIt’s something that cannot be done. So we users must find our own bugs; our computers are losers! This doesn't prove that users are capable of finding bugs that computers aren't (theoretically) capable of finding. The sets might be the same.