解决停顿问题比人们想象的容易吗？

虽然一般情况是不可判定的,但许多人仍然可以解决日常使用中相当不足的问题.

在科恩关于计算机病毒的博士论文中,他展示了病毒扫描如何与停止问题等效,但我们有一个完整的行业围绕着这一挑战.

我也见过微软的终结者项目 - http://research.microsoft.com/Terminator/

这让我想问一下 - 停止问题被高估 - 我们是否需要担心一般情况？

随着时间的推移,类型是否会变得完整 - 依赖类型似乎是一个很好的发展？

或者,从另一个角度来看,我们是否会开始使用非图灵完整语言来获得静态分析的好处？

解决停顿问题比人们想象的容易吗？

我认为这与人们的想法一样困难.

随着时间的推移,类型会变得完整吗？

亲爱的,他们已经是!

依赖类型看起来似乎是一个很好的发展？

非常如此.

我认为非图灵完全可证明的语言可能会有所增长.很长一段时间,SQL都在这个类别中(它不再是),但这并没有真正削弱它的实用性.我想,这样的系统肯定有一席之地.

哇,这是一个混乱的问题.

第一:停滞问题在实际意义上不是"问题",如"需要解决的问题".它更像是关于数学本质的陈述,类似于哥德尔的不完备性定理.

第二:构建一个完美的病毒扫描程序是难以处理的事实(由于它等同于停机问题)正是"整个行业围绕这一挑战建立起来的原因".如果可以设计一个完美的病毒扫描算法,那么只需要有人做一次,然后就不再需要一个行业了.故事结束.

第三:使用图灵完整语言并没有消除"静态分析的好处" - 它只是意味着静态分析存在限制.没关系 - 无论如何,我们几乎所有事情都有限制.

最后:如果停止问题可以以任何方式"解决",它肯定会"比人们想象的更容易",因为图灵证明它是无法解决的.从数学的角度来看,一般情况是唯一相关的案例.具体案例是工程问题.