Is solving the halting problem easier than people think?尽管无法确定一般情况，但是许多人仍然确实解决了对于日常使用而言足够合理的问题。 在科恩关于计算机病毒的博士学位论文中，他展示了病毒扫描与停止问题是等价的，但是我们面临着整个挑战。 我也看过Microsoft的终止程序项目-http://research.microsoft.com/Terminator/ 导致我问的问题-暂停问题是否被高估了-我们是否需要担心一般情况？ 类型会随着时间的流逝而变得完整-依赖类型看起来像是一个不错的发展吗？ 或者，换一种说法，我们是否将开始使用非图灵完整语言来获得静态分析的好处？
我认为这和人们想的一样困难。
亲爱的，他们已经是！
非常非常。 我认为非图灵完整但可证明的语言可能会有所增长。在相当长的一段时间里，SQL属于这一类(不再适用)，但这并没有真正减少其实用性。我认为，这样的系统肯定有地方。 哇，这是一个困惑的问题。 第一：从实际意义上讲，"停顿问题"不是"问题"，而是"需要解决的问题"。它是关于数学性质的陈述，类似于G？del的不完全性定理。 第二：建立一个完美的病毒扫描程序非常棘手(因为它等同于停止问题)，这正是"围绕这一挑战建立整个行业"的原因。如果能够设计出用于完美病毒扫描的算法，那只不过是一个人做一次的事，那么就不再需要一个行业。故事结束了。 第三：使用Turing Complete语言并不能消除"静态分析的好处"，它只是意味着静态分析存在局限性。没关系-无论如何，几乎我们所做的每件事都有局限性。 最后：如果停止问题可以以任何方式"解决"，那肯定是"比人们想像的要容易"，图灵证明这是无法解决的。从数学的角度来看，一般情况是唯一相关的情况。具体情况与工程有关。 有许多程序可以解决暂停问题，其中许多程序很有用。 如果您的编译器会告诉您"暂停"，"不暂停"或"不知道"，那么它可以告诉您程序的哪一部分导致了"暂停"或"不知道"情况。如果您确实想要一个绝对停止或不停止的程序，那么您将以与摆脱编译器警告相同的方式来修复那些"不知道"的单元。我想我们都会为解决这个普遍不可能的问题而被证明有用的频率感到惊讶。 顺便说一句，我认为模板的图灵完整性表明停顿被高估了。大多数语言都保证其编译器将停止运行。不是C ++。这会削弱C ++作为一种语言吗？我不这么认为。它有很多缺陷，但并非总是停止的编译不是其中之一。 作为一名日常程序员，我想值得继续走下去，以解决停顿风格的问题，即使您只是达到极限而从未达到极限。正如您所指出的，病毒扫描被证明是有价值的。 Google搜索并非伪装成"为我找到Y最好的X"的绝对答案，但它也非常有用。如果我释放出一种新型病毒(muwahaha)，会产生更大的解决方案集，还是只是对现有的问题区域进行研究？无论技术上的差异如何，有些公司都会以务实的方式开发并收取后续"检测和清除"服务的费用。 对于您的其他问题，我期待着真正的科学答案。 问题无法确定的事实并不意味着它并不有趣：相反！因此，是的，我们没有一个有效且统一的程序来解决所有程序的终止问题(以及许多其他有关软件的问题)，但这并不意味着不值得寻求部分解决方案。从某种意义上讲，这就是我们需要软件工程的原因：因为我们不能仅将任务委托给计算机。
但是，您的问题的标题有些误导。我同意DrPizza的观点：终止问题确实像人们认为的那样困难。 最后，关于依赖类型和子递归语言的问题虽然部分相关，但实际上是不同的问题，我不确定将它们混合在一起的意义。
我不知道人们认为它有多难，所以我不能说它是否更容易。但是，您认为正确的是，问题的不确定性(通常)并不意味着该问题的所有实例都是不确定的。例如，我可以很容易地告诉您，像 您提到的诸如Terminator项目之类的项目显然存在(甚至在某些情况下甚至可以工作)，因此很明显，并非所有项目都是无望的。对于试图证明重写系统终止的工具，也有一场竞赛(我相信每年)，这些竞赛基本上是一种计算模型。但是，在许多情况下终止很难证明。 最简单的看待方法可能是将不确定性视为问题实例化复杂性的最大化。每个实例化在达到这个最大值的微不足道的范围内，并且通常具有较高的最大值，实例化也平均而言也较难。 如果您在一般情况下查看"停顿问题"，那么实际上只是很有趣，因为如果"停顿"问题是可以确定的，那么所有其他无法确定的问题也可以通过减少来 因此，我对这个问题的看法是，不，在重要的情况下并不容易。也就是说，在现实世界中，这可能没什么大不了的。 另请参阅：http://en.wikipedia.org/wiki/Halting_problem#Importance_and_consequences |
