史上最牛诗歌:一个停机问题不可判定的证明
icon2 Internet Vision | icon4 2009-03-05 11:44| icon310 Comments | 本文内容遵从CC版权协议 转载请注明出自matrix67.com

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 succeeds.
Now, I won't just assert that, I'll show where it leads:
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.
By 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!

 
来源:http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

10 条回复

  • 楼层: 沙发 | | 小精灵 说:

    -_,- 计算理论刚挂掉的飘过

  • 楼层: 板凳 | | NULL 说:

    (School of Philosophy, Psychology and Language Sciences, University of Edinburgh)

    这个背景的作者居然能明白halting problems以及那么多计算技术语,佩服佩服。。

  • 楼层: 地毯 | | gnaggnoyil 说:

    to LS:更重要的是他能把它写成诗歌...

  • 楼层: 地板 | | gnaggnoyil 说:

    最后一句话经典...把计算机科学的本质说出来了...

  • 楼层: 地下室 | | 燕仰 说:

    嚯哟~~你这里也有看到诗的时候~~这个好强~~

  • 楼层: 地基 | | 说:

    t

  • 楼层: 地壳 | | 严酷的魔王 说:

    不知道有没有人想把它改成Rap……

  • 楼层: 地幔 | | 小单 说:

    我们学校的。。。要re一下 很强大

  • 楼层: 地核 | | lolo 说:

    i like~

  • 楼层: 10楼 | | Recover 说:

    飘过……话说3月13又是黑色星期五

  • 楼层: 11楼 | | f(Program,Poet)=Programet » 黎曼假设之歌:Zeta函数的零点在哪里? 说:

    [...] 这两天我在瘾Malloc新买的《素数之恋》,看到附录里面有一个非常有意思的“周边”,便拿过来和大家分享一下。歌曲的名称叫做”Where are the zeros of zeta of s ?“,这首歌的歌词是加利福尼亚理工学院的荣誉退休数学教授Tom Apostol在1955年写的(大概是目前为止我发过的最火星的东西了)。这首歌会让我想起Matrix67的“史上最牛诗歌”,我想我这个应该也不差吧~ [...]

您也随便说几句吧:

您可以在 Gravatar 设置您的头像。