像 Coq 这样的非图灵完备语言有哪些实际限制？

Question

由于存在非图灵完整的语言，并且鉴于我没有在大学学习计算机科学，有人可以解释一些图灵不完整的语言（例如 Coq) 不能做什么？

或者完整性/不完整性是否没有真正的实际兴趣（即在实践中没有多大区别）？

编辑 - 我正在寻找答案，由于 X，您无法用非图灵完整语言构建哈希表，或类似的东西！

Answer 1

首先，我假设您已经听说过丘奇-图灵论文，其中指出任何我们所说的“计算”都可以用图灵机（或任何其他等效模型）来完成。因此，图灵完备的语言是一种可以表达任何计算的语言。相反，图灵不完备语言是一种无法表达某些计算的语言。

好吧，这不是很有信息。让我举个例子。在任何图灵不完整语言中都不能做一件事：您无法编写图灵机模拟器（否则您可以在模拟图灵机上对任何计算进行编码）。

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

现在有几种非常不同的图灵不完备语言，它们的不同之处在于它们不能做什么。然而，有一个共同的主题。如果您正在设计一种语言，有两种主要方法可以确保该语言是图灵完备的：

• 要求该语言具有任意循环 (while) 和动态内存分配 (< code>malloc)

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

让我们看一些非图灵完备语言的示例，尽管有些人可能将其称为编程语言。

• FORTRAN 的早期版本没有动态内存分配。您必须提前计算出您的计算需要多少内存并进行分配。尽管如此，FORTRAN 曾经是使用最广泛的编程语言。

  明显的实际限制是您必须在运行程序之前预测其内存需求。如果输入数据的大小没有预先限制，这可能很困难，并且可能是不可能的。当时，提供输入数据的人通常是编写程序的人，所以这没什么大不了的。但对于今天编写的大多数程序来说，情况并非如此。

• Coq 是一种为证明定理而设计的语言。现在证明定理和运行程序密切相关，所以你可以在 Coq 中编写程序就像你证明一个定理一样。直观上，定理“A 蕴涵 B”的证明是一个以定理 A 的证明为参数并返回定理 B 的证明的函数。

  由于系统的目标是证明定理，所以不能让程序员编写任意函数。想象一下，该语言允许您编写一个愚蠢的递归函数，该函数只是调用自身（选择使用您最喜欢的语言的行）：

  theorem_Boom(theorem_Aa){returnboom(a); }
  让rec繁荣（a：定理_A）：定理_B =繁荣（a）
  def 繁荣(a): 繁荣(a)
  （定义（繁荣a）（繁荣a））
  

  你不能让这样一个函数的存在让你相信 A 蕴含 B，否则你将能够证明任何东西而不仅仅是真正的定理！因此 Coq（以及类似的定理证明者）禁止任意递归。当您编写递归函数时，您必须证明它总是终止，这样每当您在定理 A 的证明上运行它时，您就知道它将构造定理 B 的证明。

  Coq 的直接实际限制是您无法编写任意递归函数。由于系统必须能够拒绝所有非终止函数，因此停止问题的不确定性（或者更一般地说赖斯定理）确保也存在被拒绝的终止函数。另一个实际困难是您必须帮助系统证明您的函数确实终止。

  有很多正在进行的研究，旨在使证明系统更像编程语言，同时又不影响其保证，即如果您有一个从 A 到 B 的函数，那么它与 A 暗示 B 的数学证明一样好。扩展系统接受更多的终止函数是研究课题之一。其他扩展方向包括处理输入/输出和并发等“现实世界”问题。另一个挑战是让这些系统对普通人来说是可以访问的（或者也许让普通人相信它们实际上是可以访问的）。

• 同步编程语言是为实时系统编程而设计的语言，即系统程序必须在少于n个时钟周期内做出响应。它们主要用于关键任务系统，例如车辆控制或信号发送。这些语言对程序运行所需的时间以及可以分配的内存量提供了强有力的保证。

  当然，与这种强有力的保证相对应的是，您不能编写无法提前预测内存消耗和运行时间的程序。特别是，您不能编写内存消耗或运行时间取决于输入数据的程序。

• 有许多专门的语言甚至不尝试成为编程语言，因此可以轻松地远离图灵完整性：正则表达式，数据语言，大多数标记语言，......

顺便说一下，Douglas Hofstadter 写了几本关于计算的非常有趣的科普书籍，特别是 哥德尔、埃舍尔、巴赫：永恒的金辫。我不记得他是否明确讨论了图灵不完备性的局限性，但阅读他的书肯定会帮助你理解更多的技术材料。

Answer 2

不适合像 Coq 这样的语言的一类重要问题是那些终止被推测或难以证明的问题。你可以在数论中找到很多例子，也许最著名的是 Collat​​z 猜想

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

这个限制导致必须在 Coq 中以不太自然的方式表达此类问题，例如，添加一个“fuel”参数，如下所示，这样您就可以表达“collat​​z up to n steps”。

Answer 3

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

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

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

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

因此，缺少将语言归类为非图灵完备的功能实际上限制了该语言的实用性。所以答案是，这取决于：什么使该语言成为非图灵完备的？

Answer 4

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

由于“在实践中”，在计算机能够模拟图灵机 2^128 步骤之前，您已经走得很远了，因此可以公平地说，图灵不完备性在“实践中”并没有产生太大的影响。