丘奇—图灵论题

这里的有效方法指有限、明确的规则，执行者按步骤操作，不必在每一步作新的创造性判断。传统背景是理想化的人用纸笔计算；讨论时忽略寿命、纸张不足等偶然限制，却不允许把“凭直觉找到答案”当成一个已解释的机械步骤。

例如通常的整数加法有明确的逐位规则；相反，“不断尝试，直到觉得答案正确”为何能结束、怎样确认正确，都还没有说明。论题关注的是这种规则化计算能做什么，而不是一次计算是否足够快，或现实中有没有足够资源执行它。

参考：[1]

丘奇在 1930 年代用 λ 可定义性及递归函数刻画有效可计算函数；图灵则从逐步符号操作出发构造抽象机器。这些形式定义的出发点不同，却得到相同的函数类别。形式模型之间的等价可以通过严格数学证明建立。

图灵机自身也有多纸带、单纸带和非确定等变体。通过模拟可以证明它们在可计算性方面等价。这种对模型细节的稳定性是重要依据：某个问题不会仅因把一条纸带换成若干条，就从不可计算变为可计算。不过模拟可能增加时间，能力等价不等于效率相同。

参考：[2] [3]

“λ 可定义函数与图灵可计算函数相同”两边都有精确定义，因此是可证明的形式命题。“所有有效方法都在这类模型之内”还涉及原先非形式的有效性概念。要把后者当成通常意义上的数学定理，首先就必须说明这个非形式概念被哪些公理或定义完整捕获。

图灵对人的机械计算过程作了分析，用每一步只能观察和改动有限信息等限制支持机器模型的充分性。这不是只凭几个算例作出的猜测；但也不能把若干模型已经等价，偷换成所有可能意义下的“计算”都已经被证明等价。

参考：[4] [1]

原始论题不直接断言任意物理系统都能由图灵机完整模拟。要提出关于物理计算的更强主张，还需规定装置可用的物理过程、精度、信息取得方式等条件。这些假设不包含在普通形式模型等价定理的结论里。

扩展丘奇—图灵论题的某些版本进一步要求有效率地模拟，通常涉及多项式开销。它与只问“是否可计算”的原始论题应当分开。判断一种新计算模型是否挑战论题，至少要先问：它改变的是计算速度、资源条件，还是可计算函数的范围；只说“比传统计算机快”并未回答这些问题。

参考：[1] [3]