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

首先,我想你已经听说了 Church-Turing thesis

好吧,那不是很有用。让我举个例子。有一件事你不能在任何图灵不完整的语言:你不能写一个图灵机器模拟器(否则你可以在模拟图灵机器上编码任何计算)。

仍然 信息量不大。真正的问题是,什么 程序不能用图灵不完全语言编写?好吧,没有人提出一个有用程序的定义,它包括某个地方为一个有用的目的而编写的所有程序,而且它不包括所有的图灵机器计算。因此,设计一种图灵不完全语言来编写所有有用的程序仍然是一个非常长期的研究目标。

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

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

让我们看一些非图灵完全语言的例子,尽管有些人可能称之为编程语言。

• FORTRAN的早期版本没有动态内存分配。你必须事先计算出你的计算需要多少内存,然后分配这些内存。尽管如此,FORTRAN曾经是使用最广泛的编程语言。

• proving theorems proving theorems and running programs are very closely related 所以你可以用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的直接实际限制是不能编写任意的递归函数。由于系统必须能够拒绝所有非终止函数,因此 halting problem (或者更一般地说 Rice's theorem )确保也有被拒绝的终止函数。另一个实际困难是,您必须帮助系统证明您的函数确实终止。

• Synchronous programming languages 是为实时系统编程而设计的语言,也就是说,程序必须在少于 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 公平地说,图灵的不完全性在“实践”中并没有太大的区别。