递归函数理论和可计算性

除了证明理论和模型理论之外,当代的第三个主要领域逻辑是关于递归函数和可计算性。许多专门的工作都属于计算机科学至于逻辑。然而,递归理论的起源完全在于逻辑。

有效的可计算性

递归理论的起点之一是决策问题对于一阶逻辑,即。的问题算法或者重复的过程,机械地(即有效地)决定一个给定的一阶逻辑公式在逻辑上是否正确。这个问题的一个积极的解决方案应该包括这样一个过程,它能使人既能列出所有(且仅)逻辑上为真的公式,也能列出所有(且仅)逻辑上为假的公式。(哥德尔第一不完备定理这意味着没有机械的程序来列出所有且仅是基本算术的真句子。)

可有效计算的函数称为“一般递归”函数。有人可能认为一个数字是有效可计算的当且仅当它是传统意义上的递归的——也就是说,它的价值对于一个给定的数,可以通过熟悉的算术运算从它的值计算出较小的数。事实证明,这种方法太窄了,以这种方式定义的函数现在被称为“原始递归”。

有效可计算性的不同特征在很大程度上由几个逻辑学家独立给出,包括西德尼教堂在1933年,库尔特·哥德尔1934年(尽管他把这个想法归功于雅克·海尔勃朗),斯蒂芬·科尔·克林而且阿兰·图灵在1936年,埃米尔的帖子1944年(尽管他的作品早在出版前就完成了),以及a·a·马尔科夫1951年。这些表面上完全不同的定义实际上是等价的,这一事实支持了丘奇(Church)提出的主张教会的论文),它们都捕获了有效可计算函数的理论前概念。

图灵机

Gödel最初反对丘奇的论文,因为它没有基于对计算和可计算性概念的彻底分析。这样的分析是由图灵提出的,他用抽象自动机定义了有效可计算性,现在被称为图灵机。

图灵机是一种双向的自动机无限被分割成单元的磁带,机器一次读取一个单元。机器有有限数量的内部状态(0,1,2,…,n-1),每个单元格有两种可能的状态,1(1)和0(空白)。这台机器可以做五件事:将胶带向左移动一个格;将磁带向右移动一个格;将单元格的状态从1更改为0;将单元格的状态从0更改为1;变成一个新的内部状态。机器在任何给定步骤中所做的事情都是由它的内部状态和它所读取的单元格的状态(1或0)唯一决定的。因此,图灵机表示一个函数,它将单元格状态(1或0)和内部状态(0、1、2、…或n-1)映射到一个新的单元格状态和内部状态,以及机器接下来读取哪个单元格的说明。

这样的图灵机定义了一个从自然数到自然数的偏函数φ。为了计算φ(x),给机器一个空白带x连续的1,从机器正在读取的单元格开始,并设置为运动。如果它在a之后停止有限的的步数y在它的纸带上连续的1(没有其他)y = φ(x)如果对于给定的值,机器在有限步数后没有停止x,则φ(x)为未定义x.如果φ(x)被定义为所有的值,则图灵机被称为计算函数φx.一个函数是可计算的如果有图灵机来计算它。这个可计算性的定义被证明与Church、Kleene和Post的定义是等价的。

图灵机可计算性的定义可以通过不同的方式变化并变得更加灵活。一个不同的概念可计算性,称为极限可计算性,是通过让图灵机一直计算φ(x)而获得的,但要求从某有限步数开始在磁带上保持一个唯一的数字。图灵机可计算性也可以定义为多个变量的函数。

丘奇的论文不是数学的,也不是逻辑的定理这是可以明确证明的,因为它所依赖的可计算或(有效地)机械函数的理论前思想并不尖锐。它在递归函数理论的完全正式发展中没有地位。然而,丘奇的论文在实际的数学论证中是被依赖的。当逻辑学家必须证明某个函数f图灵机是可计算的吗?定义这样的机器并证明它实际上是可计算的,这可能是一项艰巨的任务f.要证明这一点往往容易得多f可以直观地计算出来。然后逻辑学家可以诉诸丘奇的论点,并得出结论,存在一个图灵机,实际上可以计算函数。自然地,使用这种论证的逻辑学家必须能够在受到挑战时制造出机器。

图灵对有效可计算性概念的定义是一个重要的概念知识的成就。他的思想被改编并进一步发展约翰·冯·诺依曼和其他人,因此在理论和应用的发展中发挥了重要作用电脑和计算。然而,严格地说,有效可计算性的概念与实时可计算性相去甚远。其中一个原因是潜在的图灵机的磁带可以使其计算持续的时间比实际的计算机长得多。