方永、南天紫云

道亦有道

停机问题通俗说明
作者 vinoca 發布於 2018年10月10日

去年十月份做过一次名为“停机问题的小故事”的分享,由于听众基本都是程序员, 所以用伪代码表述证明过程。

最近想温习一下,看了一遍维基百科上的证明,并没有完全的捋顺。然后看知乎, 再看之前的演示文稿,回想起来了,故重新整理一下,做个备忘。

在编程语言中,一段程序一般可用一个函数来表示,而函数,通常会 有三部分组成,输入,执行体,输出。输入和输出,既可以是数据,也可以是函数, 甚至是自身(自身也是函数嘛)。

有个人某天忽然想,我能不能写一个程序,来判断其他人写的程序是否正常,比如有 没有死循环,能否正常结束。用一个函数来代表这个程序,并取名为甲,那么它的 输入就是函数,执行体判断输入的函数是否能正常结束,输出是或否。

于是,现在开始思考怎么写这个执行体呢?非也。凭直觉,这个执行体将会非常的复杂, 现有的编程语言就非常多,况且每时每刻都有很多程序被写出来。先想一想这样的程序 存不存在,如果不存在,那就不用费这个力气了。

天下雨,地面就湿,这是一个常识。假设天下雨,地面是干的,那么显然这个假设是 违背常识的,是不成立的。反证法就是这样的套路,先假设某个命题成立,然后根据 这个命题推出矛盾,那么这个命题就是不成立的。

前面说的甲程序存不存在,有人就用反证法证明了。

假设甲程序存在,也就是存在一个程序能判断所有的程序能否正常结束,那么找出一个 反例,假设就不成立了。还真被人找着了一个这样的反例程序,称之为乙。

乙是这样的一个程序,它的输入是一个程序,输出和甲相反,也就是甲判断某程序丙会 正常结束,那么乙就会判断程序丙不能正常结束,甲判断程序丙不能正常结束,乙又会 判断丙能正常结束。总之,同样的输入,乙和甲的输出结果正好相反。

然后,用乙程序去判断乙程序自己是否能正常结束,也就是乙的输入是乙。如果乙输出的 是能正常结束,那么根据乙的定义,甲输入乙,得到的结果是不能正常结束。也就是乙 能正常结束,甲会判断乙不能正常结束。如果乙不能正常结束,甲又会判断乙能正常结束。 这就导出了矛盾,那么甲程序存在这个假设就不成立了。

结论就是不存在能判断任意程序能否正常结束的程序。