停止问题理论与实践

Question

通常断言，停止问题是不可确定的。并证明它确实是微不足道的。

但仅适用于任意程序。

是否有关于人类的课程的任何研究，人类通常会制作？

有时很容易分析一个程序，并枚举其所有自由度并得出结论，它将停止。

例如，是否有努力创建编程语言（脚本真的）保证暂停？它不会广泛适用，但仍然可能对关键任务模块有用。

Answer 1

保证停止的语言已经看到广泛的频繁使用。像COQ / AGDA / IDRIS这样的语言都在此类别中。实际上，许多类型的系统确保停止诸如系统F或其中的任何变型。对于类型系统的声音来说，致力于证明所有程序的正常化是常规的。强烈的正常化是一个非常理想的属性，一般来说在编程语言研究中。

我在实践中捕捉无限循环的情况下我没有看到很多成功，然而“确保在ESFP中终止”由Telford和Turner表示更强大的终止检查器，可以证明EuclID的算法始终终止并处理部分情况。 EuclID的算法是一个着名的递归函数的着名棘手的例子，其并不直接可证明是原始递归。它失败了检查程序，即只需查找减少参数（或一些简单的减少参数的简单模式，如胎儿终止检查器）。要使用原始递归组合器实现这一点，您必须在算法中为算法编码终端证明作为函数中的参数。

我想不出任何结果的程序语言的结果，并且大多数功能语言都使用某种限制，使得明显终止而不是尝试执行某种复杂分析，以确保更多自然程序终止。

Answer 2

有过去和目前的研究。这样的问题被称为终止分析，并且快速查看谷歌（学者）提供了几个旧的以及新出版物：

1. 2005， 高阶功能程序的终止分析 ;
2. 2006， 对haskell 的自动终止分析< / a>;
3. 2008， 基于依赖性的逻辑程序终止分析图 ;
4. 2010， 循环概述和终止分析 ;
5. 2014， 终止分析通过学习终止计划 ;
6. 2015， 终止递归调用的图表 ;
7. 2019， 事件驱动分布式算法的静态终止分析 < / a>;
8. 2019， 在量子编程中实现终止分析 ;

包括具有内置机制的现有语言，例如：

• mercury ;
• idris，coq，agda;

Answer 3

Microsoft has developed a practical code checker (whose name escapes me at the moment) which performs halt-testing. It exploits the fact that the code it checks is human-written and not arbitrary, just as you suggest. More importantly, it bypasses the impossibility proof by being allowed to return the answer 'Cannot decide' if it runs into code too difficult to check.

Answer 4

There are only 2 types of infinite programs:

1. Those that repeat their own state after a point (cyclical)
2. Those that grow indefinitely in used memory

Those in 1st type, follow this pattern:

Where there is a pair of distinct indices i and j such that xi = xj, and after which the cycle repeats itself again (thanks to the deterministic nature of programs). In this case the inputs x, contain the whole memory and variables used by the algorithm, plus the current instruction pointer.

Cycle detection algorithms work very well in practice for this type and can prove that a given cyclical program will never finish, usually after a small number of steps, for most random programs.

Proving those in the 2nd type is where the challenge is. One could argue that type 2 can never exist in reality (as all computers have finite memory) but that is not very useful in practice because the memory used may grow very slowly for a regular computer to ever be full. A simple example of that is a binary counter that never stops and never repeats its full state completely.

Answer 5

There is a huge class of functions that are trivially guaranteed to halt: Everything with a finite number of loops, with an upper limit for the number of iterations for each loop determined before the loop is started.

If you have a random program, it can be difficult to prove whether or not it halts. Programs that are written for a purpose are usually much easier.

Answer 6

The smart contracts functions in the Ethereum blockchain are an example of a system that needs the guarantee of halting, not to stall the whole chain.

Every function has a gas cost, and the gas cost translates into real Ethereum coins. A transaction fee must be paid to call the contract. If the gas used in the contract exceed the gas paid with the transaction fee, the computation terminates immediately.