证明停止问题是不可判定的
杰弗里·K·基奇
(爱丁堡大学哲学、心理学和语言科学学院）
| 没有通用的错误检查程序可以做到。 现在，我不会只是断言这一点，我会向你证明这一点。 我会证明，虽然你可能会工作到倒下， 你无法判断计算是否会停止。 |
| 想象一下我们有一个名为 磷 对于指定的输入，您可以看到 是否指定源代码及其所有错误， 定义最终停止的例程。 |
| 您在程序中输入合适的数据， 和 磷 开始工作，过了一会儿 （在有限的计算时间内）正确推断 是否发生无限循环行为。 |
| 如果不会出现循环，那么 磷 打印出“好”。 这意味着该输入的工作将停止，正如它应该的那样。 但如果它检测到不可停止的循环， 然后 磷 报告“糟糕！” ——这意味着你已经陷入困境了。 |
| 嗯，事实是这样的 磷 不可能是， 因为如果你写了它并把它交给我， 我可以用它来设置逻辑绑定 那会粉碎你的理智并扰乱你的思想。 |
| 这是我将使用的技巧——而且很简单。 我将定义一个过程，我将调用它 问, 将会使用 磷对停止成功的预测 挑起可怕的逻辑混乱。 |
| 对于指定的程序，比如说 A一件用品, 该程序的第一步称为 问 我设计 是为了找出 磷 什么是正确的说法 的循环行为 A 运行 A。 |
| 如果 磷的答案是“不好！”， 问 会突然停止。 然而在其他方面， 问 将会回到顶部， 然后重新开始，无限循环， 直到宇宙死亡并变得冰冻和黑色。 |
| 这个程序叫做 问 不会留在货架上； 我会要求它预测其运行情况 本身。 当它读取自己的源代码时，它会做什么？ 什么是循环行为 问 运行 问？ |
| 如果 磷 警告无限循环， 问 会退出； 然而 磷 应该说的是实话吧！ 而如果 问那就退出吧 磷 应该说“好”。 这使得 问 开始循环！ (磷 否认会。） |
| 不管怎样 磷 可能会表演， 问 将舀它： 问 用途 磷的输出 磷 看起来很愚蠢。 任何 磷 说，它无法预测 问: 磷 错的时候就是对的，真的时候就是假的！ |
| 我创造了一个悖论，尽可能简洁—— 并简单地使用你的假设 磷。 当你提出 磷 你踏入了网罗； 你的假设已经把你带进了我的巢穴。 |
| 那么这个论点可能会走向何方呢？ 我不必告诉你； 我相信你一定知道。 我们已经证明不可能有 一个像神话一样的过程 磷。 |
| 你永远找不到通用的机械手段 用于预测计算机器的行为； 这是无法完成的事情。 所以我们用户 必须找到我们自己的bug。 我们的电脑是失败者！ |
这个诗意证明的早期版本发表于 数学杂志 (73， 不。 4, 319-320）于 2000 年 10 月。但是，尽管评审过程花费了近一年的时间，但还是出现了一个未被注意到的错误。 我感谢 Philip Wadler（爱丁堡大学信息学）和 Larry Moss（印第安纳大学数学）帮助开发了这个修正版本。
感谢 Anuj Dawar 的善意，我非常荣幸和高兴地在 2012 年 6 月在剑桥大学举行的纪念艾伦·图灵的会议上大声朗读了这篇文章。（请注意，用英国南部标准英语大声朗读它效果最好：第三节前两行的韵律要求使用非rhotic方言。）然而，该会议的一位与会者，巴黎综合理工学院的达米亚诺·马扎（Damiano Mazza），很久以后指出我的修订版本还有另一个小错误：它提到了证明是 减少，当它确实不是时（这是通过假设某些东西来证明矛盾结果的证明）。 所以我在 2022 年 4 月 7 日修改了一行。（我试图安慰自己这段粗心的历史，但没有成功，因为我认为图灵 1936 年的原始论文也有一些错误；他在 1937 年发表了一个简短的更正。）经我许可，更正后的版本已在大卫·利本-诺厄尔（David Liben-Nowell）编写的精美教科书中重印，
连接离散数学和计算机科学
（剑桥大学出版社，2022 年），第 14 页。 196.
我感谢已故的苏斯博士的风格，感谢艾伦图灵的内容开创性工作，感谢马丁戴维斯对其进行了易于理解的简化演示，并感谢菲利普瓦德勒、拉里莫斯和达米亚诺马扎的帮助。
版权所有 © 2008、2012、2022，作者：Geoffrey K. Pullum。 特此允许在任何媒体上复制或分发本作品，用于与计算机科学、数学或逻辑教学相关的非商业、教育目的，前提是我已获悉并包含上述版权归属。
