由于那里有非图灵完整的语言，而且我在大学没有学习 Comp Sci，有人可以解释一些图灵不完整的语言(如 Coq)不能做的事情吗？
或者是没有真正实际利益的完整性/不完整性(即它在实践中没有太大区别)？
编辑 - 我正在寻找一个答案，因为 X 或类似的原因，您无法用非图灵完整语言构建哈希表!
最佳答案
首先，我假设您已经听说过 Church-Turing thesis ，这表明我们称之为“计算”的任何事情都可以用图灵机(或许多其他等效模型中的任何一个)来完成。因此，图灵完备语言是一种可以表达任何计算的语言。相反，图灵不完备语言是一种无法表达的计算。
好吧，那不是很有信息性。让我举个例子吧。在任何图灵不完备语言中，有一件事情是你不能做的:你不能写一个图灵机模拟器(否则你可以在模拟的图灵机上编码任何计算)。
好吧，这仍然不是很有用。真正的问题是，哪些有用的程序不能用图灵不完备语言编写？好吧，没有人提出“有用程序”的定义，该定义包括某人在某处为有用目的编写的所有程序，而不包括所有图灵机计算。因此，设计一种可以编写所有有用程序的图灵不完备语言仍然是一个非常长期的研究目标。
现在有几种非常不同的图灵不完备语言，它们的不同之处在于它们不能做什么。然而，有一个共同的主题。如果您正在设计一种语言，有两种主要方法可以确保该语言是图灵完备的:
while )和动态内存分配( malloc )让我们看一些非图灵完备语言的例子，有些人可能仍将它们称为编程语言。
明显的实际限制是您必须在运行之前预测程序的内存需求。这可能很困难，如果输入数据的大小没有预先限制，则可能是不可能的。当时，提供输入数据的人通常是编写程序的人，所以这没什么大不了的。但对于今天编写的大多数程序来说，情况并非如此。
由于系统的目标是证明定理，所以不能让程序员随意编写函数。想象一下，该语言允许您编写一个愚蠢的递归函数，该函数只是调用自身(选择使用您最喜欢的语言的行):
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 )确保也存在被拒绝的终止函数。一个额外的实际困难是你必须帮助系统证明你的函数确实终止了。
有很多正在进行的研究使证明系统更像编程语言，同时又不影响他们的保证:如果你有一个从 A 到 B 的函数，它就像数学证明 A 隐含 B 一样好。 扩展系统以接受更多终止函数是研究课题之一。其他扩展方向包括处理输入/输出和并发性等“现实世界”问题。另一个挑战是让普通人可以访问这些系统(或者让普通人相信它们实际上是可以访问的)。
当然，如此强大的保证的对应物是您无法编写其内存消耗和运行时间无法提前预测的程序。特别是，您不能编写内存消耗或运行时间取决于输入数据的程序。
顺便说一句，Douglas Hofstadter写了几本非常有趣的计算科普书籍，特别是Gödel, Escher, Bach: an Eternal Golden Braid .我不记得他是否明确讨论了图灵不完备性的局限性，但阅读他的书肯定会帮助您了解更多技术资料。
关于programming-languages - 像 Coq 这样的非图灵完备语言的实际限制是什么？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/3492188/