Church-Turing论题

1. 从可计算性的直觉到形式化
   当我们谈论“计算”时，直觉上指的是一个机械的、确定的步骤序列，它能在有限时间内，根据明确的规则，从输入得到输出。在20世纪初，希尔伯特计划等推动了对“有效可计算性”或“能行可计算性”的精确数学定义的需求。不同的数学家和逻辑学家从不同角度提出了形式化模型，如：

   • 递归函数（哥德尔、Kleene）：基于数论函数的递归定义。
   • λ-可定义函数（丘奇、Kleene）：基于λ演算的函数抽象与应用。
   • 图灵机（图灵）：一个抽象机器，包含无限长的纸带、读写头和有限状态控制。

2. 不同模型之间的等价性证明
   一个关键的理论突破是，上述不同模型被证明在可计算的函数类上是相互等价的。例如：

   • 任何图灵机可计算的函数，都是λ-可定义的，反之亦然。
   • 任何一般递归函数，都可以由图灵机计算。
     这意味着，尽管这些模型在形式上差异很大，但它们刻画了同一类函数——这是一个强烈的证据，表明它们捕捉到了“有效可计算性”这个直观概念的本质。

3. Church-Turing论题的提出与内涵
   基于上述等价性，阿隆佐·丘奇（Alonzo Church）和阿兰·图灵（Alan Turing）分别独立提出了一个论断，现统称为Church-Turing论题。它不是一个可以被证明的数学定理，而是一个关于直观概念与形式模型关系的哲学假说或科学论断。

   Church-Turing论题：任何直观上（或物理上）可计算的函数，都可以被图灵机计算（或者等价地，是λ-可定义的，是一般递归的）。
   它建立了直观的、非形式的“能行可计算”概念与形式化的图灵可计算性（或递归函数等）之间的桥梁。几乎所有现代计算理论（包括可判定性、复杂性理论）都建立在这个论题被广泛接受的基础上。

4. 论题的支持证据与稳固性
   支持Church-Turing论题的主要证据包括：

   • 稳健性：所有看似合理的、不同的形式化计算模型（如寄存器机器、部分递归函数、甚至量子计算的标准电路模型等）都被证明与图灵机在可计算函数类上等价。这种对模型细节不敏感的特性，加强了图灵机确实抓住了计算本质的观点。
   • 物理可实现性：迄今为止，没有任何一个在物理上实现的、符合“能行过程”概念的计算装置，被发现能计算超出图灵可计算范围的函数。这包括所有现代数字计算机。
   • 认知论证（图灵）：图灵通过分析人类“计算者”进行笔算时的心理过程，论证了任何这样的过程都可以由图灵机模拟，从而为“直观可计算”提供了一个令人信服的形式对应物。

5. 论题的延伸与相关概念

   • Church-Turing-Deutsch论题：这是对原论题在物理语境下的一个强化版本，声称任何物理上可实现的（有限）计算过程，都可以由一台通用图灵机高效地模拟。它为计算理论物理学提供了基础。
   • 超计算：指那些在理论上可能超越图灵机计算能力的计算模型（如使用无限精度实数、某些非传统物理过程的模型等）。但这些模型通常不被认为是“能行可计算”的，因为它们违反了有限性、确定性或离散性等直观约束。Church-Turing论题的一个核心作用就是划清了“能行可计算”与“数学上可定义”之间的界限。