theory - 在非图灵完备语言中停止

Question

对于图灵完备的语言，停止问题无法解决，而对于某些非 TC 语言（如它总是停止的正则表达式），它可以轻松解决。

我想知道是否有任何语言同时具有停止和不停止的能力，但承认可以确定它是否停止的算法。

Answer 1

停止问题不适用于语言。相反，它作用于机器（即程序）：它询问给定程序是否在给定输入时停止。

也许您的意思是问它是否可以解决其他计算模型（例如您提到的正则表达式，以及 下推自动机）。

通常，可以在具有有限资源的模型中检测到停止（如正则表达式或等效的有限自动机，它们具有固定数量的状态且没有外部存储）。这很容易通过枚举所有可能的配置并检查机器是否两次进入相同的配置（表示无限循环）来完成；在资源有限的情况下，如果机器没有停止，我们可以在必须看到重复配置之前设置一个时间上限。

通常，具有无限资源的模型（例如，无限的 TM 和 PDA）不能进行停止检查，但最好单独调查模型及其未解决的问题。

（对不起所有的维基百科链接，但它实际上是这类问题的一个很好的资源。）

Answer 2

是的。这种类型的一个重要类是原始递归函数。此类包括您希望能够对数字进行的所有基本操作（加法、乘法等），以及@adrian 提到的一些复杂类（正则表达式/有限自动机、上下文无关语法/下推自动机）。但是，确实存在非原始递归的函数，例如Ackermann 函数。

理解原始递归函数实际上很容易。它们是您可以在没有真正递归的编程语言中获得的函数（因此函数 f 不能调用自身，无论是直接调用还是通过调用另一个函数 g 然后调用 f 等）并且没有 while 循环，而是有界的for循环。有界 for 循环类似于“for i from 1 to r”，其中 r 是程序前面已经计算过的变量；另外，我不能在 for 循环中修改。这种编程语言的要点是每个程序都会停止。

我们编写的大多数程序实际上都是原始递归的（我的意思是，可以翻译成这样的语言）。

Answer 3

简短的回答是肯定的，这样的语言甚至可以非常有用。

几个月前在 LtU 上有一个讨论：http: //lambda-the-ultimate.org/node/2846