oxb*_*kes 62 programming-languages functional-programming turing-complete coq
因为那里有非图灵完整的语言,并且鉴于我没有在大学学习Comp Sci,有人可以解释一下Turing-incomplete语言(如Coq)不能做的事情吗？
或者是没有实际利益的完整性/不完整性(即它在实践中没有太大的区别)？
编辑 - 我正在寻找一个答案,你不能用非Turing完整语言构建一个哈希表,因为X或类似的东西!
Gil*_*il' 103
首先,我假设你已经听说过Church-Turing论文,该论文指出我们称之为"计算"的任何东西都可以用图灵机(或许多其他等效模型)来完成.因此,图灵完备语言是可以表达任何计算的语言.相反,图灵不完整的语言是一种无法表达的计算.
好的,这不是很有用.让我举个例子.在任何图灵不完整的语言中都有一件事你不能做:你不能写图灵机模拟器(否则你可以在模拟的图灵机上编码任何计算).
好的,那还不是很有用.真正的问题是,什么有用的程序不能用图灵不完整的语言写？好吧,没有人提出"有用程序"的定义,其中包括某人为某个目的编写的所有程序,并且不包括所有图灵机计算.因此,设计一种图灵不完整的语言,您可以编写所有有用的程序,这仍然是一个非常长期的研究目标.
现在有几种截然不同的图灵不完全语言,它们在不能做的事情上有所不同.但是有一个共同的主题.如果您正在设计一种语言,有两种主要方法可以确保该语言是图灵完备的:
要求语言具有任意循环(while)和动态内存分配(malloc)
要求该语言支持任意递归函数
让我们看一些非图灵完整语言的例子,有些人可能会称之为编程语言.
早期版本的FORTRAN没有动态内存分配.你必须事先弄清楚你的计算需要多少内存并分配它.尽管如此,FORTRAN曾经是使用最广泛的编程语言.
显而易见的实际限制是,您必须在运行程序之前预测程序的内存要求.这可能很难,如果输入数据的大小没有提前限制,则可能是不可能的.当时,输入数据的人通常是编写程序的人,所以这并不是什么大问题.但对于今天编写的大多数程序来说,情况并非如此.
Coq是一种用于证明定理的语言.现在证明定理和运行程序是非常密切相关的,所以你可以在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的直接实际限制是你不能写任意的递归函数.由于系统必须能够拒绝所有非终止功能,该的不可判定停机问题(或更一般Rice定理)确保有被拒绝以及终止功能.一个额外的实际困难是你必须帮助系统证明你的功能终止.
有很多正在进行的研究上作出证明系统更多的编程语言,就像没有影响他们保证,如果你有从A到B的功能,它是作为一个数学证明,一个蕴涵B.扩展系统接受更加良好终止功能是研究课题之一.其他扩展方向包括应对诸如输入/输出和并发之类的"现实世界"问题.另一个挑战是使这些系统对于凡人来说是可以接近的(或者可能使凡人相信他们实际上是可以访问的).
同步编程语言是为实时系统编程而设计的语言,即程序必须在少于n个时钟周期内响应的系统.它们主要用于关键任务系统,如车辆控制或信号.这些语言为程序运行所需的时间和可分配的内存提供了强有力的保证.
当然,这种强有力保证的对应物是你不能编写你无法事先预测的内存消耗和运行时间的程序.特别是,您无法编写其内存消耗或运行时间取决于输入数据的程序.
有许多专业语言甚至不会尝试编程语言,因此可以远离图灵完整性:正则表达式,数据语言,大多数标记语言,...
顺便说一句,Douglas Hofstadter写了几本关于计算的非常有趣的科普书籍,特别是哥德尔,埃舍尔,巴赫:永恒的金色辫子.我不记得他是否明确地讨论了图灵不完全的局限性,但阅读他的书肯定会帮助你理解更多的技术资料.
不适合像 Coq 这样的语言的一类重要问题是那些终止被推测或难以证明的问题。你可以在数论中找到很多例子，也许最著名的是科拉茨猜想
function collatz(n)
while n > 1
if n is odd then
set n = 3n + 1
else
set n = n / 2
endif
endwhile
这种限制导致必须在 Coq 中以不太自然的方式表达此类问题。
最直接的答案是:不是图灵完整的机器/语言不能用于实现/模拟图灵机.这来自图灵完整性的基本定义:如果机器/语言可以实现/模拟图灵机,那么它就是完整的.
那么,实际意义是什么？嗯,有一个证据表明任何可以显示为图灵完成的东西都可以解决所有可计算的问题.根据定义,这意味着任何不完整的东西都存在一些障碍,即它有一些无法解决的可计算问题.这些问题取决于缺少哪些功能使系统无法完成.
例如,如果一种语言不支持循环或递归,或者隐式循环不能使图灵完成,因为图灵机可以编程为永久运行.因此,该语言无法解决需要循环的问题.
另一个例子是,如果一种语言不支持列表或数组(或者允许您使用文件系统模拟它们),那么它就无法实现图灵机,因为图灵机需要对内存进行任意随机访问.因此,该语言无法解决需要随意随机访问内存的问题.
因此,缺少将语言归类为非图灵完备的功能实际上限制了语言的有用性.所以答案是,这取决于:什么使非图灵语言完整？