这个证明说明停机问题是无法决定的，它是关于IT技术的。请问如何工作？

Question

我正在审查Sipser的《计算理论导论》中停机问题的证明，我主要关注以下证明：

如果TM M不知道它何时循环（它不能接受或拒绝任何字符串，这就是为什么TM对于所有字符串都是图灵可识别的），那么决策器H如何确定M是否可能进入循环？当TM D进行处理时，同样的问题也会出现。

- jfisk

---

Kay，那不正确：为了评论的目的，从整个文本中复制一页内容肯定是合理使用。 - Charlie Martin

作为社区管理员，我没有权力判断这是否构成版权侵犯。所有版权侵犯都应该由版权持有人通过DMCA版权通知向Stack Exchange, Inc.报告。 - Adam Lear

@cstheory.se 是关于研究级别的理论计算机科学的，如其FAQ所示。在教材中解释证明并不是一个研究级别的问题。官方上，计算机科学问题可以在[so]上讨论，尽管有一个计算机科学站点的提议，它会给它们一个更好的家园。 - Gilles 'SO- stop being evil'

首先，这是符合主题的。其次，粘贴教科书页面的扫描件显然不太好 - 我不在意它是否侵犯版权，但是请至少引用或改写相关部分作为实际的文本。最后，我们不在这里替你做功课。拜托了，伙计...展示一下你的工作吧！你认为怎样？ - Shog9

@Shog9，我明白，但在这种特殊情况下，尤其是因为在Markdown中重现数学符号本身就是一个有趣的问题，我认为这是正确的选择。 - Charlie Martin

Answer 1

在阅读并尝试理解证明后，我编写了以下代码，这是此答案中类似问题代码的简化版本：

function halts(func) {
  // Insert code here that returns "true" if "func" halts and "false" otherwise.
}

function deceiver() {
  if(halts(deceiver))
    while(true) { }
}

如果 halts(deceiver) 返回 true，deceiver 将永远运行，如果返回 false，deceiver 将停止，这与 halts 的定义相矛盾。因此，函数 halts 是不可能的。

- Juan

---

非常优雅，就我所知（作为一个程序员而不是计算机科学家），这是一个正确的阐述为什么停机问题是无法决定的例证，即使对于不需要输入的程序也是如此。 - Paul Manta

我认为这不是正确的答案，因为你不能像 halts(deceiver) 那样执行停机命令。你应该使用特定的代码来调用它，比如 维基百科中所示的代码。 - Yai0Phah

事实上，递归定理保证了存在一个具有这些语义的函数。 - Yuval Filmus

@YuvalFilmus 我不知道那个定理。浏览维基页面后，我认为原始停机问题的证明只是使用了Y组合子相同的技巧，但它使用了输入数据存在的条件。 - Yai0Phah

@Gudradain，这里没有递归。在“halts”调用中，只传递了函数“deceiver”作为参数，但它并没有被调用。 - Gonzalo Solera

这已经是一个足够好的演示，虽然它不符合图灵机问题的表述方式。 - user253751

Answer 2

这是一种“反证法”，一种“归谬法”（拉丁短语在理论课上总是不错的，当然前提是它们有意义）。

这个程序 H 只是一个带有两个输入的程序：一个表示某个机器程序的字符串和一个输入。为了证明目的，你只需要假设程序H是正确的：如果M接受w，则它将简单地停止并接受。你不需要考虑它如何做到这一点；事实上，我们即将证明它不能这样做，没有这样的程序H 存在...

因为

如果这样的程序存在，我们可以立即构造另一个程序H', 使得H无法决定。但是，根据假设，没有这样的程序：H能决定所有东西。因此，我们被迫得出结论：我们定义的程序H 不存在。

顺便说一下，证明方法中的“归谬法”比你想象的更有争议，特别是在计算机科学中经常使用。如果你觉得它有点奇怪，也不用感到尴尬。这种魔术术语是“非构造性的”，如果你非常有雄心壮志，可以问一下你的教授关于Errett Bishop对非构造性数学的批评。

- Charlie Martin

---

我有点困惑于你对反证法的争议性说法。在数学中，它们非常普遍，并且完全符合逻辑。虽然这不是讨论的场所，但你的写法似乎很危险：它可能会导致经验不足的读者得出结论，即反证法证明的结果可能存在问题。从快速阅读中可以看出，“争议”似乎是关于反证法是否优雅、是否适合教学的问题，同时Bishop也可能批评了其他事情。 - Cascabel

@Jefromi 不，争议不是关于教学的，而是关于数学基础。如果你有兴趣，起点应该是直觉主义，尽管维基百科的文章很难理解。我认为争议有点过时了；所有这些逻辑都可以用来建立彼此。在某种意义上，直觉主义逻辑作为一种实用工具已经重新流行起来，用于模拟计算机辅助证明。 - Gilles 'SO- stop being evil'

@Jefromi，我说“比你想象的更有争议。” 我是某种逻辑学家，对基础知识很感兴趣，所以我比其他人更关注这个问题，但重点是怀疑_reductio_证明是否完全合法并不是不合理的。 对于初学者来说，它们似乎有一定的循环性。 - Charlie Martin

@ Giles，我不太舒服将建构主义与直觉主义联系起来；直觉主义是建构主义的一个子集。我会将其基于排除中间定律的拒绝作为出发点。另一个有趣的观点是可计算分析; 我非常喜欢它，因为在本科时，我认为整个不连续性是愚蠢的，并试图独立发明计算机可行分析。虽然没有成功，但很有趣看到它多年后出现。 - Charlie Martin

否则区分这两者就是纯粹的迂腐。 - Charlie Martin