UMBC ebiquity
How Dr. Seuss would prove the halting problem undecidable

How Dr. Seuss would prove the halting problem undecidable

Tim Finin, 11:12am 19 January 2008

I just discovered (via del.icio.us/polular) an extraordinary proof of the halting problem by linguist Geoffrey Pullum, now at the University of Edinburgh. What’s unusual about it is that it’s written as a poem in the style of Dr. Seuss.

Geoffrey K. Pullum, Scooping the loop snooper: An elementary proof of the undecidability of the halting problem. Mathematics Magazine 73.4 (October 2000), 319-320.

It’s a marvelous proof, sure to liven up any undergraduate theory of computation class. But I noticed errors in the proof — not logical errors, but a transcriptional ones in the form of a mangled word, perhaps introduced by an OCR system. The third line of the fifth stanza reads “that would take and program and call P (of course!)” which has problems in syntax, semantics, rhythm and meter. I’d guess it should be “that would take any program and call P (of course!)”. Similarly, “the” in the third line in the third stanza should probably be “they”. Most of the online version I found had these errors, but I eventually found what I take to be a correct version on the QED blog. I’ve not been able to get to the original version in Mathematical Magazine to verify the corrected version which I include below.


 

Scooping the Loop Snooper
an elementary proof of the undecidability of the halting problem

Geoffrey K. Pullum, University of Edinburgh

No program can say what another will do.
Now, I won’t just assert that, I’ll prove it to you:
I will prove that although you might work til you drop,
you can’t predict whether a program will stop.

Imagine we have a procedure called P
that will snoop in the source code of programs to see
there aren’t infinite loops that go round and around;
and P prints the word “Fine!” if no looping is found.

You feed in your code, and the input it needs,
and then P takes them both and it studies and reads
and computes whether things will all end as they should
(as opposed to going loopy the way that they could).

Well, the truth is that P cannot possibly be,
because if you wrote it and gave it to me,
I could use it to set up a logical bind
that would shatter your reason and scramble your mind.

Here’s the trick I would use – and it’s simple to do.
I’d define a procedure – we’ll name the thing Q -
that would take any program and call P (of course!)
to tell if it looped, by reading the source;

And if so, Q would simply print “Loop!” and then stop;
but if no, Q would go right back to the top,
and start off again, looping endlessly back,
til the universe dies and is frozen and black.

And this program called Q wouldn’t stay on the shelf;
I would run it, and (fiendishly) feed it itself.
What behaviour results when I do this with Q?
When it reads its own source, just what will it do?

If P warns of loops, Q will print “Loop!” and quit;
yet P is supposed to speak truly of it.
So if Q’s going to quit, then P should say, “Fine!” -
which will make Q go back to its very first line!

No matter what P would have done, Q will scoop it:
Q uses P’s output to make P look stupid.
If P gets things right then it lies in its tooth;
and if it speaks falsely, it’s telling the truth!

I’ve created a paradox, neat as can be -
and simply by using your putative P.
When you assumed P you stepped into a snare;
Your assumptions have led you right into my lair.

So, how to escape from this logical mess?
I don’t have to tell you; I’m sure you can guess.
By reductio, there cannot possibly be
a procedure that acts like the mythical P.

You can never discover mechanical means
for predicting the acts of computing machines.
It’s something that cannot be done. So we users
must find our own bugs; our computers are losers!


14 Responses to “How Dr. Seuss would prove the halting problem undecidable”

  1. Koen Vervloesem Says:

    If you have access to JSTOR, you can find the original Mathematics Magazine article online on http://www.jstor.org/view/0025570x/di021216/02p0030l/0

    That’s the version I present on my blog QED.

  2. Tim Finin Says:

    Thanks. UMBC appears to have access, but I’ve not been able to figure out how to access it from off campus. I had hoped that using a VPN to UMBC would give me access, but that didn’t work.

  3. Sam Says:

    This made my day! Many thanks.

  4. dr seuss the things you can do printable version Says:

    [...] I won??t just assert that, I??ll prove it to you: I will prove that although you might work til …http://ebiquity.umbc.edu/blogger/2008/01/19/how-dr-suess-would-prove-the-halting-problem-undecidable…Dr. Seuss – WikiquoteIf you can see things out of whack, then you can see how things … Los Angeles [...]

  5. yamex5 Says:

    No way to find out? Should we really say never?
    How about apps that are craftilly clever?
    The very best minds might write such a tool
    That tries to avoid becomming a fool

    But no matter how wise and sneaky they’ll be
    When they construct their impervious P
    There’s always a hack with nothing to do
    Who goes on to devise an updated Q!

  6. thefre Says:

    This is a cool poem, which present a well known result.

    Unfortunately, this result is far too often misunderstood on what are its consequences.

    Just because there exist no program that can take ANY program and check some properties on them, does not mean that there exist no program that can take SOME programs (with well-defined characteristics) and check some properties on them.

    Which is good news, because now that I’ve said that, we can forget about this undecidability theorem which indeed means little in the real world, and concentrate on automatic proofs on USEFUL programs, which IMHO is a field with far too few studies, because every student is deterred to enter it when he is first taught about how this is not possible in the general case.

    The general case does not matter AT ALL, because computers just don’t run randomly generated programs.

    So now everybody please go back to work and write some cool programs that can resonate on useful ones.

    Thanks for listening :p

  7. How Dr. Seuss would prove the halting problem undecidable Says:

    [...] full post on Hacker News If you enjoyed this article, please consider sharing it! Tagged with: halting [...]

  8. Owen Corso Says:

    PUMPING LEMMA THEOREM

    long live Dr. William Fleischman

  9. Shawn J. Goff Says:

    To get to UMBC’s journal database from off-campus: http://aok.lib.umbc.edu/services/remoteaccess.php

  10. Sebastian Says:

    Here is a link to a scanned version from the magazine: http://www.cl.cam.ac.uk/teaching/0910/CompTheory/scooping.pdf

  11. EastZoneSoupCube - links for 2010-05-06 Says:

    [...] How Dr. Seuss would prove the halting problem undecidable (tags: computer humor halting problem) [...]

  12. Halting Problem Poem « Eliminando La Bestia Says:

    [...] Tiki « [...]

  13. sdrgderfg Says:

    The version on GKP’s website is slightly different:
    http://www.ling.ed.ac.uk/~gpullum/loopsnoop.html

  14. Ed The Dev .com » Blog Archive » How Dr. Seuss would teach the Halting problem Says:

    [...] In a feat of awesome nerd-ness, Geoffrey K. Pullum has written up the Computer Programming Halting Problem in Dr. Seuss style. [...]