邱奇－图灵论题

已知的三种计算过程（递归，λ演算和图灵机）都是等价的--这三种方法定义了同一类函数。这导致数学家和计算机科学家相信可计算性的概念可由上述三种等价的计算过程描述。简单来讲，邱奇-图灵论题认为如果某种方法（算法）可进行运算，那么该运算也可被图灵机执行（也可被递归定义的函数或λ函数执行）。

邱奇-图灵论题是对计算特性进行描述的一种陈述，故而不能被严格证明。虽然上面提到的三种计算过程可被证明为等价的，但是邱奇-图灵论题最根本的前提--声称一个函数是“可有效计算的”究竟意味着什么--在某种意义上是不甚明确的直觉结果。所以，该论题依然是一个假想。

尽管邱奇-图灵论题不能被证明，到目前为止它仍然受到近乎全面的接受。

Rosser于1939年对“可有效计算性”进行了如下的解读：“很明显CC和RC（邱奇和Rosser的论据）的成立依赖于对‘有效性’的严格定义。‘有效的方法’主要是指该方法的每一步都可被事先确定，而且该方法可在有限的步数之内生成结果”。因此，‘有效性’实际上包含两层含义：

1. 产生一种确定的，或者所需的效果
2. 能够产生计算结果

接下来， 术语“可有效演算的”意味着“由任何直观上有效的方法产生的”，而术语“可有效计算的”意味着“由图灵机或任何等价的机械设备产生的”。图灵本人对此的定义由他在1939年的博士论文“基于有序数的逻辑系统”的脚注中给出：

“^†我们应该使用‘可计算函数’来表示一个可被机器计算的函数， 使用‘可有效演算的’来指代那些并未特别指明的直观想法。”

这可以转述如下：

任何可有效演算的函数都是可计算函数。

图灵则是如此描述的：

“当一个函数的值可由某种纯机械计算步骤得到时， 它就是可有效演算的函数...应该这样认识： 可计算性和可有效演算性是不同的。”

本论题的另外一种说法就是逻辑和数学中的有效或机械方法可由图灵机来表示。通常我们假定这些方法必须满足以下的要求：

1. 一个方法由有限多简单和精确的指令组成，这些指令可由有限多的符号来描述。
2. 该方法总会在有限的步骤内产生出一个结果。
3. 基本上人可以仅用纸张和铅笔来执行。
4. 该方法的执行不需人类的智慧来理解和执行这些指令。

此类方法的一个范例便是用于确定两个自然数的最大公约数的欧基里德算法。

“有效方法”这个想法在直觉上是清楚的，但却没有在形式上加以定义，因为什么是“一个简单而精确的指令”和什么是“执行这些指令所需的智力”这两个问题并没有明确的答案。（如需欧几里得算法之外的范例，请参见数论中的有效结果。）

在他1936年的论文“论可计算数字，及其在判定性问题（德语：Entscheidungsproblem）中的应用”中，阿兰·图灵试图通过引入图灵机来形式地展示这一想法。在此篇论文中，他证明了“判定性问题”是无法解决的。几个月之前，阿隆佐·邱奇在“关于判定性问题的解释”（A Note on the Entscheidungsproblem）一文中证明出了一个相似的论题，但是他采用递归函数和Lambda可定义函数来形式地描述有效可计算性。Lambda可定义函数由阿隆佐·邱奇和斯蒂芬·克莱尼（Church 1932, 1936a, 1941, Kleene 1935）提出，而递归函数由库尔特·哥德尔（Kurt Gödel）和雅克·埃尔布朗（Jacques Herbrand，Gödel 1934, Herbrand 1932）提出。这两个机制描述的是同一集合的函数，正如邱奇和克林（Church 1936a, Kleene 1936）所展示的正整数函数那样。在听说了邱奇的建议后，图灵很快就证明了他的图灵机实际上描述的是同一集合的函数（Turing 1936, 263ff）.y

之后用于描述有效计算的许多其他机制也被提了出来，比如寄存器机、埃米尔·波斯特（Emill Post）的波斯特系统，组合子逻辑以及马尔可夫算法（Markov 1960）等。所有这些体系都已被证明在计算上和图灵机拥有基本相同的能力；类似的系统被称为图灵完全。因为所有这些不同的试图描述算法的努力都导致了等价的结果，所以现在普遍认为邱奇－图灵论题是正确的。但是，该论题不具有数学定理一般的地位，也无法被证明；说是定理不如说是个将可计算性等同于图灵机的提议。如果能有一个方法能被普遍接受为一个有效的算法但却无法在图灵机上允许，则该论题也是可以被驳斥的。

在20世纪初期，数学家们经常使用一种非正式的说法即可有效计算，所以为这个概念寻找一个好的形式描述也是十分重要的。当代的数学家们则使用图灵可计算（或简写为可计算）这一定义良好的概念。由于这个没有定义的用语在使用中已经淡去，所以如何定义它的问题已经不是那么重要了。

邱奇－图灵论题对于心智哲学（philosophy of mind）有很多寓意，但是对于该论题的很多哲学解读存在曲解。哲学学者B. Jack Copeland认为关于图灵机是否可模拟确定的物理过程的问题仍没有得到解答。他进一步声称关于这些物理过程是否在人类的智能机制中起到作用的问题也是未决的。有很多重要而悬而未决的问题也涵盖了邱奇－图灵论题和物理学及超计算（hypercomputation）的可能性之间的关系。应用到物理学上，该论题有很多可能的意义：

1. 宇宙是一台图灵机（由此，在物理上对非递归函数的计算是不可能的）。该论述被定义为大邱奇－图灵论题。
2. 宇宙不是一台图灵机（也就是说，物理的定律不是图灵可计算的），但是不可计算的物理事件却不能阻碍创建超计算机（hypercomputer）的可能性。比如，一个在物理上包含实数而非可计算实数的宇宙就可以被划为此类。
3. 宇宙是一台超计算机，而且建造物理设备来实现这一特性并以之计算非递归函数是可能的。比如，一个悬而未决的问题是我们无法确定量子力学（quantum mechanical）的事件是否图灵可计算的，尽管诸如量子图灵机之类的严格模型实际上等价于确定性图灵机（但并不一定在效率上等价）。约翰·卢卡斯和名气更大一点的罗杰·潘洛斯曾经建议说人的心灵可能是量子力学和非算法计算的结果， 尽管并没有科学证据支持这一提议。

实际上在这三类之外或其中还有许多其他的技术上的可能性，但这三类只是为了阐述这一概念。

我们可以正式定义不可计算的函数。一个有名的例子是忙碌的海狸函数。该函数接受输入n，返回具有n个状态的图灵机在停机之前所能打印的最大符号数量。找到忙碌的海狸函数的上限等于解决停机问题，该问题已被确定不能使用图灵机解决。由于海狸很忙函数不能被图灵机计算， 邱奇-图灵论题断言该函数不能使用任何方法进行有效计算。

有一些模型可用于计算（邱奇-图灵）不可计算函数：即所谓的超计算机。Mark Burgin认为类似归纳性图灵机的超递归算法（super-recursive algorithms）可用于反证邱奇-图灵论题。他的论述依赖于对算法更广泛的定义， 这种定义上的扩展使得一些归纳性图灵机包含的不可计算函数变得可计算。这种对邱奇-图灵论题的解读与计算机科学的常规解读不同，把超递归算法归于邱奇-图灵意义上的算法的这种看法并未受到相关领域的广泛接受。

• An unsolvable problem of elementary number theory 中译本 （页面存档备份，存于互联网档案馆）
• Church, Alonzo. A set of Postulates for the Foundation of Logic. Annals of Mathematics. 1932, 33 (2): 346–366. JSTOR 1968337. doi:10.2307/1968337. 
• Church, Alonzo. An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics. 1936, 58 (58): 345–363. JSTOR 2371045. doi:10.2307/2371045. 
• Church, Alonzo. A Note on the Entscheidungsproblem. Journal of Symbolic Logic. 1936, (1): 40–41. 
• Church, Alonzo. The Calculi of Lambda-Conversion. Princeton: Princeton University Press. 1941. 
• Gödel, Kurt. On Undecidable Propositions of Formal Mathematical Systems. Davis, M. (编). The Undecidable. Kleene and Rosser (lecture note-takers); Institute for Advanced Study (lecture sponsor). New York: Raven Press. 1965 [1934]. 
• Herbrand, Jacques. Sur la non-contradiction de l'arithmétique. Journal fur die reine und angewandte Mathematik. 1932, (166): 1–8. 
• Hofstadter, Douglas R. Chapter XVII: Church, Turing, Tarski, and Others. Gödel, Escher, Bach: an Eternal Golden Braid. 
• Kleene, Stephen Cole. A Theory of Positive Integers in Formal Logic. American Journal of Mathematics. 1935, 57 (57): 153–173 & 219–244. JSTOR 2372027. doi:10.2307/2372027. 
• Kleene, Stephen Cole. Lambda-Definability and Recursiveness. Duke Mathematical Journal. 1936, (2): 340–353. 
• The Theory of Algorithms. American Mathematical Society Translations. 1960, 2 (15): 1–14 [1954]. 
• Turing, A.M. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2. 1936, 42: 230–2651937. doi:10.1112/plms/s2-42.1.230. （and Turing, A.M. On Computable Numbers, with an Application to the Entscheidungsproblem: A correction. Proceedings of the London Mathematical Society. 2. 1938, 43 (6): 544–5461937. doi:10.1112/plms/s2-43.6.544. ）
• Pour-El, M.B.; Richards, J.I. Computability in Analysis and Physics. Springer Verlag. 1989.  引文使用过时参数coauthors (帮助)