222 lines
10 KiB
Markdown
222 lines
10 KiB
Markdown
---
|
||
created_at: '2015-12-25T12:57:10.000Z'
|
||
title: How Dr. Seuss would prove the halting problem undecidable (2008)
|
||
url: http://ebiquity.umbc.edu/blogger/2008/01/19/how-dr-suess-would-prove-the-halting-problem-undecidable/
|
||
author: amelius
|
||
points: 99
|
||
story_text:
|
||
comment_text:
|
||
num_comments: 8
|
||
story_id:
|
||
story_title:
|
||
story_url:
|
||
parent_id:
|
||
created_at_i: 1451048230
|
||
_tags:
|
||
- story
|
||
- author_amelius
|
||
- story_10791113
|
||
objectID: '10791113'
|
||
year: 2008
|
||
|
||
---
|
||
[Source](http://ebiquity.umbc.edu/blogger/2008/01/19/how-dr-suess-would-prove-the-halting-problem-undecidable/ "Permalink to How Dr. Seuss would prove the halting problem undecidable")
|
||
|
||
# How Dr. Seuss would prove the halting problem undecidable
|
||
|
||
|
||
| ----- |
|
||
| ![][1] | ![][1] | ![][1] | ![][1] | ![][1] |
|
||
| ![][1] | [UMBC_ e_biquity][2] | | ![][3] ![][4] ![][5] ![][6] | ![][1] |
|
||
|
||
![about us][7]![research][8]![people][9]![publications][10]![news][11]![photos][12]![events / talks / meetings][13]![blog][14]![tags][15]![internal][16]![more][17]
|
||
|
||
| ----- |
|
||
| ![][1] | ![][1] | ![][1] | ![][1] | ![][1] |
|
||
|
||
| ----- |
|
||
| ![][1] | ![][1] | ![][1] | ![][1] | ![][1] |
|
||
| ![][1] |
|
||
|
||
How Dr. Seuss would prove the halting problem undecidable
|
||
|
||
![][1]
|
||
|
||
« [Semantic Wave 2008: Industry Roadmap to Web 3.0][18]
|
||
|
||
[Social Web Technologies, UMBC, Spring 2008, MW 7:10pm][19] »
|
||
|
||
## [How Dr. Seuss would prove the halting problem undecidable][20]
|
||
|
||
Tim Finin, 11:12am 19 January 2008
|
||
|
||
I just discovered (via [del.icio.us/polular][21]) an extraordinary proof of the [halting problem][22] by linguist [Geoffrey Pullum][23], 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][24] 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!
|
||
|
||
### Related posts:
|
||
|
||
1. [Researchers prove Rubics Cube solvable in 20 moves or less ][25]
|
||
2. [Got a linguistic fluff problem? ][26]
|
||
3. [Parsing Perl considered undecidable ][27]
|
||
4. [Game theoretic analysis of the toilet seat problem ][28]
|
||
|
||
* * *
|
||
|
||
**Categories:** [GENERAL][29], [Humor][30] **Comments: ** Comments Off on How Dr. Seuss would prove the halting problem undecidable
|
||
|
||
Comments are closed.
|
||
|
||
| ![][1] |
|
||
|
||
![][31][Ebiquity Blog][32]
|
||
|
||
[Home][33] | [Archive][34] | [Login][35] | [ Feed ![][36]][37]
|
||
|
||
|
||
|
||
![][31][Ebiquity Recent Posts][38]
|
||
|
||
* [paper: Cleaning Noisy Knowledge Graphs][39]
|
||
* [Videos of ISWC 2017 talks][40]
|
||
* [Jennifer Sleeman receives AI for Earth grant from Microsoft][41]
|
||
* [Link Before You Share: Managing Privacy Policies through Blockchain][42]
|
||
* [paper: Automated Knowledge Extraction from the Federal Acquisition Regulations System][43]
|
||
|
||
|
||
|
||
![][31][Ebiquity rdfs:seeAlso][44]
|
||
|
||
| ![][1] |
|
||
|
||
| ----- |
|
||
| [UMBC][45] | [home][2] · [contact][46] · [about][47] · [site map][48] · [legal][49] · [privacy][50] · ©1999-2018 ebiquity · design/code ©2003-2018 [Filip Perich][51] · [XG][52]
|
||
|
||
![][1]
|
||
|
||
[1]: http://ebiquity.umbc.edu/img/d.gif
|
||
[2]: http://ebiquity.umbc.edu/
|
||
[3]: http://ebiquity.umbc.edu/img/twitter-icon-32x32.png "ebiquity on Twitter"
|
||
[4]: http://ebiquity.umbc.edu/img/facebook-32x32.png "ebiquity on Facebook"
|
||
[5]: http://ebiquity.umbc.edu/img/feed-icon-32x32.png "ebiquity RSS feed"
|
||
[6]: http://ebiquity.umbc.edu/img/email-icon-32x32.png "email ebiquity"
|
||
[7]: http://ebiquity.umbc.edu/img/mn/ab0.gif
|
||
[8]: http://ebiquity.umbc.edu/img/mn/re0.gif
|
||
[9]: http://ebiquity.umbc.edu/img/mn/pe0.gif
|
||
[10]: http://ebiquity.umbc.edu/img/mn/pu0.gif
|
||
[11]: http://ebiquity.umbc.edu/img/mn/ne0.gif
|
||
[12]: http://ebiquity.umbc.edu/img/mn/ph0.gif
|
||
[13]: http://ebiquity.umbc.edu/img/mn/ev0.gif
|
||
[14]: http://ebiquity.umbc.edu/img/mn/bl0.gif
|
||
[15]: http://ebiquity.umbc.edu/img/mn/ta0.gif
|
||
[16]: http://ebiquity.umbc.edu/img/mn/in0.gif
|
||
[17]: http://ebiquity.umbc.edu/img/mn/mo0.gif
|
||
[18]: https://ebiquity.umbc.edu/blogger/2008/01/18/semantic-wave-2008-industry-roadmap-to-web-30/
|
||
[19]: https://ebiquity.umbc.edu/blogger/2008/01/20/social-web-technologies-umbc-spring-2008-mw-710pm/
|
||
[20]: https://ebiquity.umbc.edu/blogger/2008/01/19/how-dr-suess-would-prove-the-halting-problem-undecidable/ "Permanent Link: How Dr. Seuss would prove the halting problem undecidable"
|
||
[21]: http://del.icio.us/popular/
|
||
[22]: http://en.wikipedia.org/wiki/Halting_problem
|
||
[23]: http://ling.ed.ac.uk/~gpullum/
|
||
[24]: http://www.vervloesem.eu/qed/?p=146
|
||
[25]: https://ebiquity.umbc.edu/blogger/2010/08/13/researchers-prove-rubics-cube-solvable-in-20-moves-or-less/ "Researchers prove Rubics Cube solvable in 20 moves or less"
|
||
[26]: https://ebiquity.umbc.edu/blogger/2009/05/04/got-a-linguistic-fluff-problem/ "Got a linguistic fluff problem?"
|
||
[27]: https://ebiquity.umbc.edu/blogger/2008/01/28/parsing-perl-considered-undecidable/ "Parsing Perl considered undecidable"
|
||
[28]: https://ebiquity.umbc.edu/blogger/2006/02/07/game-theoretic-analysis-of-the-toilet-seat-problem/ "Game theoretic analysis of the toilet seat problem"
|
||
[29]: https://ebiquity.umbc.edu/blogger/category/general/
|
||
[30]: https://ebiquity.umbc.edu/blogger/category/general/humor/
|
||
[31]: http://ebiquity.umbc.edu/img/up.gif
|
||
[32]: https://ebiquity.umbc.edu/blogger/
|
||
[33]: https://ebiquity.umbc.edu/blogger
|
||
[34]: https://ebiquity.umbc.edu/blogger/ebiquity-blog-archives/
|
||
[35]: https://ebiquity.umbc.edu/blogger/wp-login.php
|
||
[36]: https://www.feedburner.com/fb/images/pub/feed-icon16x16.png
|
||
[37]: https://feeds.feedburner.com/ebiquity
|
||
[38]:
|
||
[39]: https://ebiquity.umbc.edu/blogger/2018/01/27/paper-cleaning-noisy-knowledge-graphs/ "Permanent Link: paper: Cleaning Noisy Knowledge Graphs"
|
||
[40]: https://ebiquity.umbc.edu/blogger/2017/12/16/videos-of-iswc-2017-talks/ "Permanent Link: Videos of ISWC 2017 talks"
|
||
[41]: https://ebiquity.umbc.edu/blogger/2017/12/12/jennifer-sleeman-receives-ai-for-earth-grant-from-microsoft/ "Permanent Link: Jennifer Sleeman receives AI for Earth grant from Microsoft"
|
||
[42]: https://ebiquity.umbc.edu/blogger/2017/12/04/link-before-you-share-managing-privacy-policies-through-blockchain/ "Permanent Link: Link Before You Share: Managing Privacy Policies through Blockchain"
|
||
[43]: https://ebiquity.umbc.edu/blogger/2017/11/28/paper-automated-knowledge-extraction-from-the-federal-acquisition-regulations-system/ "Permanent Link: paper: Automated Knowledge Extraction from the Federal Acquisition Regulations System"
|
||
[44]: http://delicious.com/ebiquity/seealso
|
||
[45]: https://www.cs.umbc.edu/
|
||
[46]: http://ebiquity.umbc.edu/us/contact/
|
||
[47]: http://ebiquity.umbc.edu/us/
|
||
[48]: http://ebiquity.umbc.edu/map/
|
||
[49]: http://ebiquity.umbc.edu/legal/
|
||
[50]: http://ebiquity.umbc.edu/legal/privacy/
|
||
[51]: http://perich.net/
|
||
[52]: http://perich.net/work/xg_shared_spectrum.php
|
||
|