像Coq这样的非图灵语言的实际限制是什么？ [英] What are the practical limitations of a non-turing complete language like Coq?

问题描述

由于那里有非图灵完备语言，并且考虑到我在大学时没有学习科幻科幻，有人可以解释一些图灵不完整的语言（比如 Coq ）做不到？

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

编辑 - 我正在寻找一个符合由于X 或类似的东西，你不能在非Turing完全语言中构建一个哈希表！

解决方案

首先，我假设你已经听说过教会图灵论文，其中规定我们称之为计算的任何东西都可以用图灵机（或任何其他等效模型）完成。所以图灵完全语言是可以表达任何计算的语言。相反，图灵不完全语言是一种计算方式无法表达的计算方式。

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

<好的，仍然不是很丰富。真正的问题是，什么有用的程序不能用图灵不完整的语言编写？那么，没有人提出过一个有用的程序的定义，其中包括某人在某处为某个有用目的而编写的所有程序，并且不包括所有的图灵机计算。因此，设计一个图灵不完全的语言，您可以在其中编写所有有用的程序，这仍然是一个非常长期的研究目标。

现在有几种非常不同的图灵 - 不完整的语言在那里，他们不能做的不同。但是有一个共同的主题。如果你正在设计一门语言，有两种主要的方法可以确保语言是图灵完整的：

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




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

一些人可能会称之为编程语言的非图灵完全语言的例子。





• 早期版本的FORTRAN没有动态内存分配。你必须事先弄清楚你的计算需要多少内存并分配它。尽管如此，FORTRAN曾经是最广泛使用的编程语言。

  
  
  

  明显的实际限制是您必须在运行程序之前预测程序的内存需求。这可能很难，如果输入数据的大小没有预先限制，这可能是不可能的。当时，输入数据的人往往是编写程序的人，所以这不是什么大不了的事。但对于今天编写的大多数程序来说，这是不正确的。

Coq是一种为证明定理。现在证明定理和正在运行的程序密切相关，因此您可以在Coq中编写程序就像你证明一个定理一样。直觉上，定理A蕴含B的证明是一个函数，它将定理A的一个证明作为一个参数并返回一个定理B的证明。



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

pre $ 定理_B景气（定理_A）{返回景气（a）; }
令rec boom（a：theorem_A）：theorem_B = boom（a）
def boom（a）：boom（a）
（定义（boom a）（boom a））


你不能让这样的函数的存在让你相信A意味着B，否则你会能够证明任何事情而不仅仅是真正的定理！所以Coq（和类似的定理证明）禁止任意递归。当你写一个递归函数时，你必须证明它总是终止，以便每当你运行一个定理证明A时，你就知道它会构造一个定理B的证明。





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





关于使证明系统更多的编程语言有很多正在进行的研究而不会损害他们的保证，即如果你有从A到B的功能，那么它就像A意味着B的数学证明一样好。扩展系统以接受更多的终止功能是研究课题之一。其他扩展方向包括应对输入/输出和并发等真实世界关注。另一个挑战是让这些系统能够被普通人接受（或者说服人们知道他们实际上是可以访问的）。

//en.wikipedia.org/wiki/Synchronous_programming_languagerel =noreferrer>同步编程语言是为实时系统编程设计的语言，也就是说，程序必须响应的语言少于 n个时钟周期。它们主要用于车辆控制或信号等关键任务系统。这些语言为程序运行的时间以及分配的内存量提供了强有力的保证。




当然，与这种强大保证相对应的是，您可以不要编写内存消耗和运行时间无法提前预测的程序。特别是，你不能编写一个程序，它的内存消耗或运行时间取决于输入数据。 有很多专门的语言甚至不能试图成为编程语言，因此可以远离Turing的完整性：正则表达式，数据语言，大多数标记语言... ...




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


As there are non-Turing complete languages out there, and given I didn't study Comp Sci at university, could someone explain something that a Turing-incomplete language (like Coq) cannot do?

Or is the completeness/incompleteness of no real practical interest (i.e. does it not make much difference in practice)?

EDIT - I'm looking for an answer along the lines of you cannot build a hash table in a non-Turing complete language due to X, or something like that!

解决方案

First, I assume you've already heard of the Church-Turing thesis, which states that anything we call "computation" is something that can be done with a Turing machine (or any of the many other equivalent models). So a Turing-complete language is one in which any computation can be expressed. Conversely, a Turing-incomplete language is one in which there is some computation that cannot be expressed.

Ok, that wasn't very informative. Let me give an example. There is one thing you cannot do in any Turing-incomplete language: you can't write a Turing machine simulator (otherwise you could encode any computation on the simulated Turing machine).

Ok, that still wasn't very informative. the real question is, what useful program cannot be written in a Turing-incomplete language? Well, nobody has come up with a definition of "useful program" that includes all the programs someone somewhere has written for a useful purpose, and that doesn't include all Turing machine computations. So designing a Turing-incomplete language in which you can write all useful programs is still a very long-term research goal.

Now there are several very different kinds of Turing-incomplete languages out there, and they differ in what they can't do. However there is a common theme. If you're designing a language, there are two major ways to ensure that the language will be Turing-complete:

• require that the language has arbitrary loops (while) and dynamic memory allocation (malloc)

• require that the language supports arbitrary recursive functions

Let's look at a few examples of non-Turing complete languages that some people might nonetheless call programming languages.

• 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, ...

By the way, Douglas Hofstadter wrote several very interesting popular science books about computation, in particular Gödel, Escher, Bach: an Eternal Golden Braid. I don't recall whether he explicitly discusses limitations of Turing-incompleteness, but reading his books will definitely help you understand more technical material.

这篇关于像Coq这样的非图灵语言的实际限制是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！