“可计算”的精确定义。1936年丘奇和图灵分别以λ演算和抽象机器刻画机械的计算方法，并证明希尔伯特提出的判定问题没有一般解法。
我们必须知道，我们必将知道。
—— 希尔伯特1930年9月8日在柯尼斯堡德国自然科学家与医生协会年会上的演讲《自然认识与逻辑》结语，后刻于他在哥廷根的墓碑；原文“Wir müssen wissen. Wir werden wissen.”，据德文译出
历史
所谓可计算性，讨论哪些问题能由一套有限、机械的规则在有限步内解决。莱布尼茨曾设想以符号演算裁决争论，“算法”一词源自9世纪巴格达数学家花拉子米之名。1928年，希尔伯特与阿克曼提出判定问题，要求找到一般方法，判定任意一阶逻辑公式是否普遍有效。1930年9月7日，哥德尔在柯尼斯堡的一次会议上首次透露不完全性定理，次日希尔伯特在同城演讲，以“我们必须知道，我们必将知道”作结；1931年发表的定理表明，足以表达算术的一致形式系统必含无法判定的命题。1936年，丘奇用λ演算、图灵用一种抽象机器，各自给出“能行可计算”的定义，并证明判定问题没有一般解法。图灵的机器由一条分格的纸带、一个每次读写一格的读写头和有限个内部状态构成，他说这是对人用纸笔计算的抽象，纸可设想为“像孩子的算术本那样分成方格”。他还构造出能读入任何机器的描述并模仿其运行的通用机，并在当年8月补写附录，证明两种定义等价。克莱尼后来称“直观可计算即图灵可计算”为论题，即丘奇—图灵论题；图灵的不可判定结果后被改述为“停机问题”。
关联
参考文献
- A. M. Turing，On Computable Numbers, with an Application to the Entscheidungsproblem (Proceedings of the London Mathematical Society, ser. 2, 42)（1936–37）
- Alonzo Church，An Unsolvable Problem of Elementary Number Theory (American Journal of Mathematics 58)（1936）
- Martin Davis，The Universal Computer: The Road from Leibniz to Turing（2000）
- Charles Petzold，The Annotated Turing（2008）
考据说明证据较充分
- “停机问题”之名出自后人，图灵原文讨论的是“无循环机器”的判定。
- 波斯特于1936年独立提出了与图灵机相近的模型。
- 图灵对EDVAC设计的影响程度尚有争论。
- 哥德尔的发言与希尔伯特的演讲前后相继，二人当时并无直接交锋。
史论
可计算性理论有一层反讽，人们为了证明机械方法的界限，第一次精确地定义了机械方法。图灵的定义以一位按规则工作的人类计算员为原型，当时科学与工程中的大量数值计算仍由人工完成；定义一旦给出，“计算”便脱离了具体的人和器材，成为任何合适的物理装置都可以执行的符号操作。通用机把指令与数据写在同一条纸带上，常被视为存储程序计算机的理论原型；冯·诺伊曼1945年的EDVAC报告提出了存储程序结构，他熟悉图灵的论文，但图灵的思想在多大程度上影响了这一设计，史家意见不一。另一方面，判定问题的否定答案意味着有些问题原则上无法交给机器，希尔伯特那句话所代表的乐观，在1930年代被逻辑本身划出了界限。