programming-languages - 存在一种编程语言 - 保证终止

Question

就目前而言，这个问题不适合我们的问答形式。我们希望答案得到事实、引用或专业知识的支持，但这个问题可能会引起辩论、争论、投票或扩展讨论。如果您觉得这个问题可以改进并可能重新打开，visit the help center为指导。




8年前关闭。




是否存在一种编程语言，您总是可以保证终止？

如果你只有 if/else 语句，你能确定程序会终止吗？

Answer 1

是的，当然有一些非图灵完备的语言可以保证终止(或至少为子集提供这样的保证):

ACL2

Coq

Agda2和类似的

在大多数情况下，它是通过只允许对严格的子项进行递归调用来实现的(并且，对于 Church 算术，它也意味着总是减少正整数计数器)。

而且，令人惊讶的是，这并不像看起来那么有限，而且这些语言非常适合解决非常广泛的问题。

Terminator项目也可能很有趣。