像Coq这样的非定制完整语言的实际限制是什么？
由于在那里有非图灵语言完整的语言，并且考虑到我在大学没有学习科学技术，有人可以解释一个图灵不完全语言（如Coq ）不能做的事情吗？
还是说实际上没有实际利益的完整性/不完整性（即在实践中没有太大的区别）？
编辑 – 我正在寻找一个答案， 你不能build立一个非图灵完整的语言由于X ，或类似的哈希表 ！
首先，我假定你已经听说过教会 – 图灵论文 ，它指出我们称之为“计算”的任何东西都可以用图灵机（或任何其他等效模型）来完成。 所以图灵完全语言是可以expression任何计算的语言。 相反，图灵不完全语言是一种计算不能expression的语言。
好的，这是不是很丰富。 让我举个例子。 有一件事你不能用任何图灵不完整的语言来做：你不能写一个图灵机模拟器（否则你可以在模拟的图灵机上编码任何计算）。
好的，那还不是很有用。 真正的问题是，什么有用的程序不能写在一个图灵不完整的语言？ 那么，没有人提出一个“有用的程序”的定义，其中包括某个地方某人为了一个有用的目的而编写的所有程序，并且不包括所有的图灵机计算。 所以devise一个图灵不完全的语言，你可以在其中编写所有有用的程序，这仍然是一个非常长期的研究目标。
现在有几种不同types的图灵不完全语言，他们不能做的不同。 但是有一个共同的主题。 如果你正在devise一种语言，有两种主要的方法来确保语言是图灵完整的：
-
要求语言具有任意循环（
while）和dynamic内存分配（malloc） -
要求语言支持任意recursion函数
让我们来看一些非图灵完整语言的例子，有些人可能会称之为编程语言。
-
早期版本的FORTRAN没有dynamic内存分配。 你必须事先弄清楚你的计算需要多less内存并分配它。 尽pipe如此，FORTRAN曾经是最广泛使用的编程语言。
显而易见的实际限制是您必须在运行之前预测程序的内存需求。 这可能很难，如果input数据的大小没有预先限制，这可能是不可能的。 当时，input数据的人往往是编写程序的人，所以没有什么大不了的。 但是对于今天编写的大多数程序来说，情况并非如此。
-
Coq是为了certificate定理而devise的语言。 现在certificate定理和运行程序是非常密切相关的 ，所以你可以用Coq编写程序，就像你certificate一个定理一样。 直观上，定理“A蕴含B”的certificate是一个函数，它certificate了定理A作为一个论证，并返回一个定理B的certificate。
由于系统的目标是要certificate定理，所以不能让程序员编写任意函数。 想象一下，这个语言允许你编写一个愚蠢的recursion函数，自己调用它（select使用你喜欢的语言的那一行）：
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))你不能让这种function的存在使你相信A意味着B，否则你将能够certificate任何东西，而不仅仅是真正的定理！ 所以Coq（和类似的定理certificate）禁止任意recursion。 当你写一个recursion函数的时候，你必须certificate它总是终止的 ，所以每当你运行一个定理A的certificate时，你就知道它会构造一个定理B的certificate。
Coq的直接实际限制是你不能写任意的recursion函数。 由于系统必须能够拒绝所有非终止函数，所以停止问题 （或者更一般地说赖斯定理 ）的不可判定性确保了终止函数也被拒绝。 另外一个实际的困难是你必须帮助系统certificate你的函数终止了。
有很多正在进行的研究，使得certificate系统更像编程语言，而不损害他们的保证，即如果你有从A到B的函数，就像A意味着的mathcertificate一样好B.扩展系统以接受更多终止职能是研究课题之一。 其他的扩展方向包括应对input/输出和并发这样的“现实世界”问题。 另一个挑战是使这些系统能够被普通人接受（或者说服人们实际上可以访问）。
-
同步编程语言是为实时系统编程devise的语言，也就是程序必须在less于n个时钟周期内响应的系统。 它们主要用于车辆控制或信号传输等关键任务系统。 这些语言为程序运行多久以及分配多less内存提供了强有力的保证。
当然，这样强有力的保证的副本是你不能预先编写内存消耗和运行时间不能预测的程序。 尤其是，您不能编写内存消耗或运行时间取决于input数据的程序。
-
有很多专门的语言，甚至不试图编程语言，所以可以远离图灵的完整性：正则expression式，数据语言，大多数标记语言，…
顺便说一句， 道格拉斯·霍夫斯塔特 （ Douglas Hofstadter）写了几本关于计算的非常有趣的科普书籍，特别是哥德尔，埃舍尔，巴赫：一条永恒的金辫子 。 我不记得他是否明确讨论了图灵不完整性的局限性，但是读他的书肯定会帮助你理解更多的技术材料。
最直接的答案是：一个不是图灵完整的机器/语言不能用来实现/模拟图灵机。 这来自于图灵完备性的基本定义：如果一个机器/语言能够实现/模拟图灵机，那么它是完整的。
那么，什么是实际的影响？ 那么，有证据表明任何可以certificate完全可以解决所有可计算问题的东西。 根据定义，这意味着任何不完整的东西都有一个缺点，即存在一些无法解决的可计算问题。 这些问题取决于什么function缺失，使系统非图灵完成。
例如，如果语言不支持循环或recursion，或者隐式循环不能完成图灵，因为图灵机可以被编程为永远运行。 因此，语言不能解决需要循环的问题。
另一个例子是，如果一种语言不支持列表或数组（或允许你使用文件系统来模拟它们），那么它就不能实现一个图灵机，因为图灵机需要随机访问内存。 因此，这种语言不能解决需要随机存取内存的问题。
因此，将语言分类为非图灵完整的缺失的特征实际上是限制语言的用途的事情。 所以答案是，这取决于：什么使语言非图灵完成？
你不能写一个模拟图灵机的函数。 你可以编写一个模拟2^128 （或2^2^2^2^128步）的图灵机的函数，并报告图灵机是否接受，拒绝或运行超过允许的步数。
由于“在实践中”，在计算机可以模拟2^128步骤的图灵机之前，你已经早已离开了，所以说“图灵不完整”在实践中并没有太大的区别。
一类很重要的问题，如Coq等不适合的语言是那些终止被猜测或难以certificate的问题。 在数论中可以find很多例子，也许最有名的是Collatz猜想
function collatz(n) while n > 1 if n is odd then set n = 3n + 1 else set n = n / 2 endif endwhile
这种限制导致不得不用不那么自然的方式来expression这样的问题。
