像 Coq 这样的非图灵完备语言的实际限制是什么？

首先，我假设您已经听说过 Church-Turing thesis，它指出我们称之为“计算”的任何事情都可以用图灵机（或许多其他等效模型中的任何一个）来完成。因此，图灵完备的语言是可以表达任何计算的语言。相反，图灵不完全语言是一种无法表达的计算。

好的，这不是很丰富。让我举个例子。在任何图灵不完备的语言中，有一件事是你不能做的：你不能编写图灵机模拟器（否则你可以在模拟的图灵机上编码任何计算）。

好的，这仍然不是很丰富。真正的问题是，什么有用的程序不能用图灵不完备的语言编写？好吧，没有人提出“有用程序”的定义，其中包括某人为有用目的而编写的所有程序，并且不包括所有图灵机计算。所以设计一种图灵不完备的语言，让你可以编写所有有用的程序，仍然是一个非常长期的研究目标。

现在有几种非常不同类型的图灵不完全语言，它们在不能做的事情上有所不同。然而，有一个共同的主题。如果您正在设计一种语言，有两种主要方法可以确保该语言是图灵完备的：

要求语言具有任意循环（while）和动态内存分配（malloc）

要求语言支持任意递归函数

让我们看一些非图灵完备语言的例子，有些人可能仍然称之为编程语言。

FORTRAN 的早期版本没有动态内存分配。您必须提前弄清楚您的计算需要多少内存并分配它。尽管如此，FORTRAN 曾经是使用最广泛的编程语言。明显的实际限制是您必须在运行程序之前预测程序的内存需求。这可能很难，如果输入数据的大小事先没有限制，那也是不可能的。当时，提供输入数据的人通常是编写程序的人，所以这没什么大不了的。但对于今天编写的大多数程序来说，情况并非如此。

Coq 是一种为证明定理而设计的语言。现在证明定理和运行程序密切相关，所以你可以像证明一个定理一样在 Coq 中编写程序。直观地说，定理“A 蕴含 B”的证明是将定理 A 的证明作为参数并返回定理 B 的证明的函数。由于系统的目标是证明定理，所以不能让程序员编写任意函数。想象一下，这种语言允许你编写一个愚蠢的递归函数，它只是调用自己（选择使用你最喜欢的语言的那一行）： theorem_B boom (theorem_A a) { return boom(a); } let rec boom (a : theorem_A) : theorem_B = boom (a) def boom(a): boom(a) (define (boom a) (boom a)) 你不能让这样一个函数的存在说服你A 蕴含 B，否则你将能够证明任何事情，而不仅仅是真定理！所以 Coq（和类似的定理证明者）禁止任意递归。当你写一个递归函数时，你必须证明它总是终止，这样每当你在定理 A 的证明上运行它时，你就知道它将构造一个定理 B 的证明。 Coq 直接的实际限制是你不能写任意递归函数。由于系统必须能够拒绝所有非终止函数，因此停止问题（或更一般地说，赖斯定理）的不可判定性确保了也有终止函数被拒绝。另一个实际困难是您必须帮助系统证明您的函数确实终止了。有很多正在进行的研究使证明系统更像编程语言而不损害他们的保证，即如果你有一个从 A 到 B 的函数，它与 A 隐含 B 的数学证明一样好。扩展系统以接受更多终止函数是研究课题之一。其他扩展方向包括处理输入/输出和并发等“现实世界”问题。另一个挑战是让普通人可以访问这些系统（或者让普通人相信它们实际上是可以访问的）。

同步编程语言是为实时系统编程而设计的语言，即程序必须在少于 n 个时钟周期内响应的系统。它们主要用于关键任务系统，例如车辆控制或信号。这些语言为程序运行需要多长时间以及它可以分配多少内存提供了强有力的保证。当然，与这种强有力的保证相对应的是，您不能编写无法提前预测内存消耗和运行时间的程序。特别是，您不能编写内存消耗或运行时间取决于输入数据的程序。

有许多专门的语言甚至不尝试成为编程语言，因此与图灵完备性相去甚远：正则表达式、数据语言、大多数标记语言……

顺便说一句，Douglas Hofstadter 写了几本非常有趣的关于计算的科普书籍，尤其是 Gödel, Escher, Bach: an Eternal Golden Braid。我不记得他是否明确讨论过图灵不完备的局限性，但是阅读他的书肯定会帮助您了解更多的技术资料。

---

最直接的答案是：不能使用图灵完备的机器/语言来实现/模拟图灵机。这来自图灵完备性的基本定义：如果机器/语言能够实现/模拟图灵机，那么它就是图灵完备的。

那么，有哪些实际意义呢？好吧，有证据表明任何可以证明是图灵完备的东西都可以解决所有可计算的问题。从定义上讲，这意味着任何不完整的事物都会存在一些无法解决的可计算问题。这些问题是什么取决于缺少哪些使系统非图灵完备的功能。

例如，如果一种语言不支持循环或递归，或者隐式循环不能是图灵完备的，因为图灵机可以被编程为永远运行。因此，该语言无法解决需要循环的问题。

另一个例子是，如果一种语言不支持列表或数组（或允许您模拟它们，例如使用文件系统），那么它就无法实现图灵机，因为图灵机需要对内存的任意随机访问。因此，该语言无法解决需要任意随机访问内存的问题。

因此，将语言分类为非图灵完备的缺失特征实际上限制了语言的实用性。所以答案是，这取决于：是什么让语言非图灵完备？

---

不适合 Coq 等语言的一类重要问题是那些终止是推测或难以证明的问题。您可以在数论中找到大量示例，其中最著名的可能是 Collatz conjecture

function collatz(n)
  while n > 1
    if n is odd then
      set n = 3n + 1
    else
      set n = n / 2
    endif
 endwhile

这种限制导致不得不在 Coq 中以不太自然的方式表达这些问题。

---

您不能编写模拟图灵机的函数。您可以编写一个函数来模拟图灵机的 2^128 步（或 2^2^2^2^128 步），并报告图灵机是否接受、拒绝或运行时间超过了允许的步数。

由于“在实践中”，在您的计算机可以模拟图灵机进行 2^128 步之前，您将早已不复存在，因此可以公平地说，图灵不完备性在“实践”中并没有太大的影响。

---