✎ scooping_the_loop_snooper [the libarynth]

You've loaded an old revision of the document! If you save it, you will create a new version with this data.

====Scooping the Loop Snooper====

A proof that the Halting Problem is undecidable

[[http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html|Geoffrey K. Pullum]] (School of Philosophy, Psychology and Language Sciences, University of Edinburgh)

//No general procedure for bug checks will do.//\\
Now, I won’t just assert that, I’ll prove it to you.\\
I will prove that although you might work till you drop,\\
you cannot tell if computation will stop.\\
 \\
For imagine we have a procedure called //P//\\
that for specified input permits you to see\\
whether specified source code, with all of its faults,\\
defines a routine that eventually halts.\\
 \\
You feed in your program, with suitable data,\\
and P gets to work, and a little while later\\
(in finite compute time) correctly infers\\
whether infinite looping behavior occurs.\\
 \\
If there will be no looping, then P prints out ‘Good.’\\
That means work on this input will halt, as it should.\\
But if it detects an unstoppable loop,\\
then P reports ‘Bad!’ — which means you’re in the soup.\\
 \\
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 that I’ll use — and it’s simple to do.\\
I’ll define a procedure, which I will call Q,\\
that will use P’s predictions of halting success\\
to stir up a terrible logical mess.\\
 \\
For a specified program, say A, one supplies,\\
the first step of this program called Q I devise\\
is to find out from P what’s the right thing to say\\
of the looping behavior of A run on A.\\
 \\
If P’s answer is ‘Bad!’, Q will suddenly stop.\\
But otherwise, Q will go back to the top,\\
and start off again, looping endlessly back,\\
till the universe dies and turns frozen and black.\\
 \\
And this program called Q wouldn’t stay on the shelf;\\
I would ask it to forecast its run on itself.\\
When it reads its own source code, just what will it do?\\
What’s the looping behavior of Q run on Q?\\
 \\
If P warns of infinite loops, Q will quit;\\
yet P is supposed to speak truly of it!\\
And if Q’s going to quit, then P should say ‘Good.’\\
Which makes Q start to loop! (P denied that it would.)\\
 \\
No matter how P might perform, Q will scoop it:\\
Q uses P’s output to make P look stupid.\\
Whatever P says, it cannot predict Q:\\
P is right when it’s wrong, and is false when it’s true!\\
 \\
I’ve created a paradox, neat as can be —\\
and simply by using your putative P.\\
When you posited P you stepped into a snare;\\
Your assumption has led you right into my lair.\\
 \\
So where can this argument possibly go?\\
I don’t have to tell you; I’m sure you must know.\\
A reductio: There cannot possibly be\\
a procedure that acts like the mythical P.\\
 \\
You can never find general 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!\\
\\

**Author's note**

In October 2000, after a refereeing delay of nearly a year, an earlier and incorrect version of this poetic proof was published in Mathematics Magazine (73, no. 4, 319–320). But it had an error. I am very grateful to Philip Wadler (Informatics, University of Edinburgh) and Larry Moss (Mathematics, Indiana University) for helping with the development of this corrected version, which is now free of bugs (trust me; you can check it). Thanks also to the late Dr. Seuss for the style, and of course to the pioneering work of Alan Turing (and Martin Davis’s nice simplified presentation) for the content. I had the privilege of reading this aloud at a conference in honour of the memory of Alan Turing at Cambridge University in June 2012. Notice that reading it aloud works best in southern British standard English: the rhyme of the first two lines of the third stanza call for a non-rhotic dialect. Copyright © 2008, 2012 by Geoffrey K. Pullum. Permission is hereby granted to reproduce or distribute this work for non-commercial, educational purposes relating to the teaching of computer science, mathematics, or logic, provided this attribution is included.

==== version n-1====
an elementary proof of the undecidability of the halting problem

<blockquote>
<file>
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 the 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 and 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!
</file>

<cite>Geoffrey K. Pullum. From Mathematics magazine VOL73. No. 4, Oct 2000 319-320</cite>
</blockquote>

Please fill all the letters into the box to prove you're human. Please keep this field empty:

Edit summary

Note: By editing this page you agree to license your content under the following license: CC Attribution-Share Alike 4.0 International