ACM通信
ACM通信
解决无法解决的问题
1902年6月16日，英国哲学家伯特兰·罗素(Bertrand Russell)给德国逻辑学家戈特洛布·弗雷格(Gottlob Frege)写了一封信，他在信中使用了后来被称为“罗素悖论”的方法，认为弗雷格的逻辑体系是不一致的。这封信引发了数学的“基础危机”，引发了对数学正确基础的近乎痛苦的探索。1921年，德国杰出数学家大卫·希尔伯特(David Hilbert)发起了一项研究计划，旨在“一劳永逸地解决基本问题”。希尔伯特纲领失败了;1931年，奥地利逻辑学家库尔特·哥德尔证明了两个不完备定理，证明了希尔伯特纲领的无用。
希尔伯特纲领中的一个元素是数学的机械化:“一旦建立了逻辑形式主义，人们就可以期望对逻辑公式进行系统的，或者说计算性的处理，这在某种程度上与代数中的方程理论相对应。”1928年，希尔伯特(Hilbert)和阿克曼(Ackermann)提出了“决策问题”(Entscheidungsproblem)，即是否存在一种算法来检查(一阶)逻辑中的给定公式是否有效;这是必然的。1936年至1937年，美国逻辑学家阿朗佐·丘奇和英国逻辑学家艾伦·图灵分别证明了一阶逻辑的决策问题为无法解决的；没有算法可以检查逻辑公式的有效性。丘奇-图灵定理可以被视为理论计算机科学的诞生。为了证明这个定理，丘奇和图灵分别引入了计算模型、递归函数和图灵机，并证明了停止的问题检查给定的递归函数或图灵机是否在给定的输入上产生输出是无法解决的。
当德国的康拉德·祖泽、美国的约翰·阿塔纳索夫和克利福德·贝里着手建造他们的数字计算机——Z3和阿塔纳索夫-贝里计算机时，“停止问题”被证明是不可解的，这意味着计算机科学是在认识到机械计算的固有局限性的基础上诞生的。虽然希尔伯特相信“每个数学问题都必须能够严格解决，”我们知道这一点无法解决的是无法突破的障碍。当我作为一个刚毕业的学生遇到“无法解决”的问题时，它对我来说似乎是一堵不可逾越的墙。这些年来，我的大部分研究都致力于划定可解决问题和不可解决问题之间的界限。
因此，2011年5月的《通信其中包括拜伦·库克(Byron Cook)、安德烈·波德尔斯基(Andreas Podelski)和安德烈·雷巴尔琴科(Andrey Rybalchenko)的一篇题为《证明终止程序》(第88页)的文章，他们在文章中认为，“与流行的观点相反，证明终止程序并非总是不可能的。”他们肯定搞错了!停止问题(终止等同于停止)是无法解决的!当然，Cook等人并没有真正声称已经解决了停止问题。他们在文中所描述的是一种证明程序终止的新方法。方法本身并不保证会终止，如果它终止了，这将与丘奇-图灵定理相矛盾。Cook等人说明，该方法在实践中非常有效，可以处理大量的实际程序。事实上，一个叫做终结者的软件工具，用来实现他们的方法，已经能够在微软软件中找到一些非常微妙的终止错误。
我相信，在证明程序终止方面的这一显著进展应该迫使我们重新考虑不可解性的含义。在我2010年11月的社论《论P、NP和计算复杂度》中，我指出NP完全问题，如布尔可满足性，在今天看来并不像20世纪70年代初那样棘手，工业SAT求解器在实践中表现令人印象深刻。“证明程序终止”表明，无法解决的问题可能并不像我们曾经认为的那样无法解决。理论上，不可解性确实对可计算性施加了严格的障碍，但在实践中，这种障碍有多重要还不太清楚。与Cook等人在文章中描述的Collatz问题不同，大多数现实生活中的程序，如果它们终止，是因为相当简单的原因，因为程序员几乎从来没有想到非常深刻和复杂的终止原因。因此，像终结者这样的工具可以证明这类程序的终止就不足为奇了。
最终，软件开发是一种工程活动，而不是一种数学活动。工程设计和分析技术提供的不是数学保证，而是信心。我们不需要解决停止问题，我们只需要能够成功地推理现实生活中的程序的终止。是时候放弃我们的“无法解决恐惧症”了。是时候解决无法解决的问题了。
Moshe Y. Vardi主编
©2011 acm 0001-0782/11/0700 $10.00
本论文部分或全部的电子版或硬拷贝供个人或课堂使用的许可是免费的，前提是副本不是为了盈利或商业利益而制作或分发的，并且副本的第一页上必须有本通知和完整的引用。除ACM外，本作品的其他组件的版权必须受到尊重。允许有署名的摘要。以其他方式复制，重新发布，在服务器上发布，或重新分发到列表，需要事先特定的许可和/或费用。请求发布权限permissions@acm.org或传真(212)869-0481。
数字图书馆是由计算机协会出版的。版权所有©2011 ACM, Inc.
评论
Marc van Woerkom
你好,摩西,
当我了解到停止问题时，我得出了一个类似的结论，即人们不应该过度反应它对现实编程的影响。
该定理涵盖了所有可能的程序，其中可能包括一些非常奇怪的情况。
LINT (C编程语言的语法检查器)和编译器警告和错误等出色工具的存在总体上表明，创建这样的分析程序仍然是有用的。
感谢丘奇和图灵，我知道这些工具可能会在一些程序上失败，不仅是因为工具内部的编程错误，还因为一些主要的原因，然而经验告诉我，它们对我通常使用的那些程序非常有效。所以他们很有帮助。
我的直觉是，我需要想出一个非常疯狂的案例来让这些工具发疯。
然而，事情不应该是这样的。罗素收缩并不是一个奇怪的逻辑公式。也许存在一些非常简单的程序，可以让我提到的工具在无限循环中发送它们。
所以我们有两个相反的支柱，一边是数学事实，另一边是现实世界的经验。如果能在与现实世界保持联系的同时更严谨一点就好了。
是否有方法量化给定分析工具的成功率(将工作于给定的“正常”程序的99.99999%)?
是什么让一个普通开发者写的程序“正常”?
等等......: -)
感谢文章!
埃里克古水盆海湾
摩西，谢谢你这篇有趣的文章。
我做静态程序分析已经有很长时间了。许多人没有意识到的是，在这个领域中几乎所有有趣的决策问题都是不可判定的，但静态分析在许多情况下非常有用。
不过，我不太理解你对“与普遍的信念相反，证明终止并不总是不可能的”这句话的说法。对我来说，这句话是对的。它并不总是不可能的，或者换句话说，它经常是可能的。当然，我可以从字面上证明许多(甚至真实世界)程序的终止。事实上，对于任何一组固定的程序，我们都可以编写一种算法来证明所有这些程序的终止。但问题是，对于任何这样的算法，人们总是能够找到另一个程序，该程序确实终止，但算法却没有显示终止。
如果我没记错的话，这就是不可判定性的真正含义……对于任何确定一个固定(但不一定是有限)程序集的不可定属性的算法，都可以构造至少一个该算法会给出错误答案的其他程序。这同样适用于终止分析，因此我看不出Cook等人的陈述有任何错误。
匿名
摩西
我得说你的信引起我的注意首先是因为它的标题。事实上，连同你提到的发表在5月号上的文章(第88页)，它与我的论文标题“编目无法找到的东西”相呼应(11月提交给同行评审的杂志发表，2011年1月以自我存档的初步草稿作为工作论文在开放资源库中发表，它在几个学术和专业领域具有难以置信的影响和影响，超出了我的想象)。
说到无法解决和不完整的问题，我发现令人震惊的是，你和你提到的作者都没有考虑到库尔特·哥德尔的作用和重要性。
问候
布鲁内拉·朗戈，4.8.2011
匿名
我觉得没有什么比“无法解决”更重要的了。问题得不到解决的能力，或者说，悖论或猜想出现的能力，本身就是问题的解决方案。
CACM管理员
以下信件发表在2011年9月的《给编辑的信》(//www.eqigeno.com/magazines/2011/9/122792)中。
——CACM管理员
瓦迪(Moshe Y. Vardi)的编辑信《解决无法解决的问题》(2011年7月)提出了一个重要的观点，即我们应该重新考虑不可解决的意义，特别是在其实际应用方面。即使一个问题(如停止问题)理论上是无法解决的，我们仍然应该尝试解决它。
不可判性的证明是基于自我适用的可能性;也就是说，一个程序不能查看自己并判断自己是否陷入了循环;从实际的角度来看，这种情况无关紧要。为什么要写这样一个程序呢?这个证明并不是说我不能编写一个服务器程序来查看正在运行的应用程序，以确定它们中的任何一个是否处于循环中。
对自应用的依赖同样适用于Post Correspondence Problem (PCP)，这是一个理论上也无法解决的字符串匹配问题。该证明并没有说PCP对于任何实际问题都是不可判定的，只是对于一个使用自我应用的问题。然而，证明确实表明，如果我试图模拟一个图灵机程序，看看它本身是否在一个循环中，那么，就像在停止问题中一样，PCP理论上是不可解的。但是从字符串匹配的角度来看，这种关于不可解性的潜在见解同样与程序员无关。也许，对于所有实际利益的案例，PCP确实是可以解决的。
同样的观点也适用于许多其他与某些问题的不可解性有关的定理。可能是问题很难解决;同样，为一个合理的子问题设计一个解决方案或在多项式时间内解决一个子问题可能非常困难。无论如何，无法解决的问题可能只是转移注意力。
亨利Ledgard
托莱多,哦
---------------------------------------------
作者的回应:
我不认为不可解性是“转移注意力”，而是对可计算性的基本限制。我们没有程序终止的算法。我的观点是，我们应该清醒地看待无法解决的问题，认识到许多无法解决的问题实际上是可以解决的。
Moshe Y. Vardi
主编
彼得•奥尔科特
下面链接的论文通过识别和拒绝所有图灵机描述来提出停止问题的解决方案，否则将显示停止是不可判定的。
使用Peter Linz符号约定来指定图灵机描述图灵机H在其输入上的状态转换序列，在它们到达矛盾的最终状态之前，被认为是无限递归的。这是前所未见的全新观点。
Prolog谓词unify_on_occurrence s_check/2检测并拒绝这样的无限递归序列。(Clocksin和Mellish 2003)
https://www.researchgate.net/publication/323384939_Halting_Problem_Proof_from_Finite_Strings_to_Final_States
Clocksin和Mellish 2003，使用ISO标准第五版的Prolog编程，第10章Prolog与逻辑的关系，第254页。
彼得•奥尔科特
*停止问题不可判定性和无限嵌套模拟*
当停止决策器的停止状态决策是模拟其输入时，则可以正确地将传统的停止问题证明不可判定反例模板判定为永不停止的输入。它们永远不会停止，因为它们为任何模拟停止决定器指定了无限嵌套的模拟。
在下面的具体示例中，模拟暂停决定器是基于x86模拟器的。在图灵机模型中，它基于通用图灵机(UTM)。在这两种情况下，输入都是一次模拟一条指令。然后将存储的执行跟踪与从未停止的行为模式进行比较。
这里只考察了两种模式:(a)无限循环(b)无限递归/无限嵌套模拟。当模拟停止决定器匹配这些模式之一时，它将中止其输入的模拟，并报告其输入没有停止。
因为模拟暂停决定程序必须总是中止每个从未停止其暂停的输入的模拟，所以必须调整其暂停决定条件。[输入在输入时停止吗?]输入停止而不中止模拟吗?这一更改是必需的，因为模拟停止决定器的每个输入要么自己停止，要么因为模拟被中止而停止。
标准伪代码停止问题模板“证明”停止问题永远无法解决，因为true(停止)或false(不停止)的值都不能正确地返回给混淆输入。
过程compute_g(我):
如果f(i, i) == 0，则
返回0
其他的
循环永远//(维基百科:停止问题)
这个问题是基于模拟停止决定器在向输入返回任何值之前会中止对其输入的模拟而克服的。它中止了对其输入的模拟，因为它的输入指定了对任何模拟暂停决定器的本质上是无限递归(无限嵌套模拟)。
创建了x86utm操作系统，这样就可以在高级语言C和x86中具体地检查停止问题。当以这种方式检查停止问题时，可以显式地指定每个细节。UTM磁带元素是32位无符号整数。
//简化的Linz (Linz:1990:319)
void P(u32 x)
｛
u32 input_halt = H(x, x);
如果(Input_Halts)
这里:到这里;
｝
int main ()
｛
u32 input_halt = H((u32)P， (u32)P);
输出("Input_Halts = "， Input_Halts);
｝
H在模拟输入(P, P)的每个指令之后，分析其x86模拟P(P)的存储执行跟踪(当前更新)。一旦匹配到非停止行为模式，H就会中止其输入的模拟，并确定其输入不会停止。
模拟停止决定器必须中止从未停止的每个输入的模拟。对于H来说，要识别P的无限重复模式，它只需要看到与人类在检查模拟P的x86执行跟踪时看到的相同的东西。所有这些细节，包括P(P)的完整x86执行跟踪，如下所示。
*停止问题不可判定性和无限嵌套模拟*
https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation
显示所有7评论