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

Question

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

programming-languagesfunctional-programmingturing-completecoq

70

由于存在非图灵完备语言，而且我没有在大学学习计算机科学，能否有人解释一下图灵不完备语言（如Coq）不能做什么？

或者说完备性/不完备性在实际中并不真正重要吗？

编辑 - 我想要一个回答，类似于“由于X的原因，在非图灵完备语言中无法构建哈希表”，或者类似的回答！

- oxbow_lakes

1

顺便提一下，早先有一个类似的问题，其中有几个有趣的答案与这里的回答互补：https://dev59.com/GHRC5IYBdhLWcg3wYP-h - Gilles 'SO- stop being evil'

@ulidtko说：“能够解释图灵完备语言需要解释器宿主语言也是图灵完备的”……这是正确的。那里引用的Agda代码避免了模拟BF代码。它为任何BF程序“分配语义”，并且原则上可以在框架中使用，以允许证明在Agda中特定BF程序的终止性。 - Atsby

4个回答

6

最直接的答案是：不具备图灵完备性的机器/语言无法用于实现/模拟图灵机。这源于图灵完备性的基本定义：如果一个机器/语言可以实现/模拟图灵机，那么它就是图灵完备的。

那么，这有什么实际的影响呢？嗯，有一个证明表明，任何被证明为图灵完备的东西都可以解决所有可计算问题。按照定义，这意味着任何不具备图灵完备性的东西都有一个缺点，即它不能解决某些可计算问题。这些问题取决于系统缺少了哪些功能，使其不具备图灵完备性。

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

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

因此，导致语言不具备图灵完备性的缺失功能，实际上限制了语言的实用性。所以答案是：这取决于什么使得该语言不具备图灵完备性。

- slebetman

+1 你不能用非图灵完备的语言编写图灵完备语言的解释器。你也不能做任何等价于此的事情（其中等价意味着编写图灵完备语言的解释器可以归约为该问题）。对于所有其他可计算的事情，存在一种非图灵完备的语言，你可以在其中完成它们。 - sepp2k

我该如何“证明”某个给定的问题需要使用循环才能解决。例如，可能情况是使用循环可解决的任何问题也可以使用递归来解决？ - oxbow_lakes

@oxbow_lakes：可以证明递归和循环是可互换的。因此，我们所说的循环也包括递归。没有循环意味着无法进行递归。 - slebetman

5

@oxbow_lakes：方法一：为了证明问题P需要在语言L中解决循环，您可以定义一个没有循环的语言K，并展示问题P无法在语言K中解决。通常，这最后一部分是通过证明语言K中的每个程序都具有某些属性（例如运行时间上限），而问题P则不具备该属性来完成的。 - Gilles 'SO- stop being evil'

4

方法2：要证明问题P需要循环或某种等效特征才能解决，你可以尝试将循环编码到问题P中。例如，为了证明拥有循环需要递归（即循环和递归具有相同的能力），你可以展示任何递归程序都可以用循环来编写。 - Gilles 'SO- stop being evil'

6

一个重要的问题类别，不适合像Coq这样的语言，是那些终止被猜测或难以证明的问题。在数论中可以找到许多例子，其中最著名的可能是Collatz猜想。

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

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

- ejgallego

5

我不同意：你可以完全用Coq表达Collatz猜想：forall n, exists k, (iterate collatz k) n = 1.（其中iterate f k将函数f应用k次）。 - Olivier Verdier

@OlivierVerdier确实如此，但请注意，您正在直接书写猜想而非函数，对于许多人来说，这样做不太自然。我从未声称您无法完美地表达猜想。 - ejgallego

3

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

由于“在实践中”，在计算机可以模拟2^128步之前，您会远去，因此可以说图灵不完备性在“实践中”并没有太大的影响。

- Atsby

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Gilles 'SO- stop being evil' · Accepted Answer

首先，我假设你已经听说过邱奇-图灵论题，它声明我们称之为“计算”的任何东西都可以用图灵机（或其他许多等效模型）完成。因此，图灵完备语言是一种可以表达任何计算的语言。相反，图灵不完备语言是指存在某些无法表达的计算。

好吧，这并没有提供太多信息。让我举个例子。在任何图灵不完备的语言中，你无法编写图灵机模拟器（否则，你可以在模拟的图灵机上编码任何计算）。

好吧，那还是不太有用。真正的问题是，哪些有用的程序无法在图灵不完备的语言中编写？嗯，没有人提出了一个包括所有某个地方某人为实现有用目的而编写的程序，但不包括所有图灵机计算的“有用程序”的定义。因此，设计一种图灵不完备的语言，在其中可以编写所有有用的程序仍然是一个非常长期的研究目标。

现在，有几种非常不同的图灵不完备语言存在，并且它们在无法执行的操作上有所不同。但是，它们有一个共同点。如果你正在设计一种语言，有两种主要方法可以确保该语言是图灵完备的：

要求语言具有任意循环（while）和动态内存分配（malloc）
要求语言支持任意递归函数

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

Early versions of FORTRAN did not have dynamic memory allocation. You had to figure out in advance how much memory your computation would need and allocate that. In spite of that, FORTRAN was once the most widely used programming language.

The obvious practical limitation is that you have to predict the memory requirements of your program before running it. That can be hard, and can be impossible if the size of the input data is not bounded in advance. At the time, the person feeding the input data was often the person who had written the program, so it wasn't such a big deal. But that's just not true for most programs written today.
Coq is a language designed for proving theorems. Now proving theorems and running programs are very closely related, so you can write programs in Coq just like you prove a theorem. Intuitively, a proof of the theorem “A implies B” is a function that takes a proof of theorem A as an argument and returns a proof of theorem B.

Since the goal of the system is to prove theorems, you can't let the programmer write arbitrary functions. Imagine the language allowed you to write a silly recursive function that just called itself (pick the line that uses your favorite language):
```
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))
```
You can't let the existence of such a function convince you that A implies B, or else you would be able to prove anything and not just true theorems! So Coq (and similar theorem provers) forbid arbitrary recursion. When you write a recursive function, you must prove that it always terminates, so that whenever you run it on a proof of theorem A you know that it will construct a proof of theorem B.

The immediate practical limitation of Coq is that you cannot write arbitrary recursive functions. Since the system must be able to reject all non-terminating functions, the undecidability of the halting problem (or more generally Rice's theorem) ensures that there are terminating functions that are rejected as well. An added practical difficulty is that you have to help the system to prove that your function does terminate.

There is a lot of ongoing research on making proof systems more programming-language-like without compromising their guarantee that if you have a function from A to B, it's as good as a mathematical proof that A implies B. Extending the system to accept more terminating functions is one of the research topics. Other extension directions include coping with such “real-world” concerns as input/output and concurrency. Another challenge is to make these systems accessible to mere mortals (or perhaps convince mere mortals that they are in fact accessible).
Synchronous programming languages are languages designed for programming real-time systems, that is, systems where the program must respond in less than n clock cycles. They are mainly used for mission-critical systems such as vehicle controls or signaling. These languages offer strong guarantees on how long a program will take to run and how much memory it may allocate.

Of course, the counterpart of such strong guarantees is that you can't write programs whose memory consumption and running time you're not able to predict in advance. In particular, you can't write a program whose memory consumption or running time depends on the input data.
There are many specialized languages that don't even try to be programming languages and so can remain comfortably far from Turing completeness: regular expressions, data languages, most markup languages, ...

顺便提一下，Douglas Hofstadter 写了几本非常有趣的关于计算的科普书，特别是 Gödel, Escher, Bach: an Eternal Golden Braid。我不记得他是否明确讨论了图灵不完备性的限制，但阅读他的书肯定会帮助您更好地理解技术材料。