SCOOPING THE LOOP SNOOPER

計算理論 詩歌

SCOOPING THE LOOP SNOOPER

A proof that the Halting Problem is undecidable
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!

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 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. The same holds for the Ukrainian version which you can see if you click here, and the Czech version for which you can click here, and the Polish version for which you can click here. (There was a Belorussian version too, atthis site, but the link seems to be dead.) Poetic restatement of classic computability theory results seems to be huge in the Slavic world for some reason.

原文出自：http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

解读一下，帮助理解：

1. 算法P，它的输入是任意程序A及其输入In，P在有限的时间内会停止运行并得出判断：如果程序A在输入In下不死循环则输出Good，否则输出Bad。现在需要证明这种算法不存在。
   简单记为：P(A, In) --> Good/Bad .

2. 假设P存在，构造Q，输入任意程序A，调用P去判断A在输入为A下是否死循环。如果A死循环，则Q结束运行；否则，Q自己进入死循环。
   简单记为：Q(A) : If P(A, A) -->Bad, Stop; else Loop.

3. 现在运行Q，输入是自己本身，即Q，请问答案是什么？ 如果Q死循环，则Q结束运行；如果Q不死循环，则Q进入死循环；矛盾！
   即：Q(Q): If P(Q, Q) -->Bad, Stop; else Loop. 翻译成悖论就是：如果P判断Q在输入为Q不停机的话，则Q立即停机；如果P判断Q在输入为Q停机的话，则Q进入死循环。

这首诗歌的主要意义在于，它确实是一首诗。注意，图灵机的形式化定义是确保在第一步的假设下，之后的所有构造都是合法构造，这一点其实是难点，需要认真体会。这就不是一首诗可以帮忙解决的问题了。《圖靈的祕密》整本書都在講解這個構造，很顯然，嚴格的論證還需要更多的技術細節。推薦大家看看這本書，可浮一白。