∑ 数学名人档案库
← 返回 阿朗佐·丘奇 简介档案 深度档案
数理逻辑计算机科学

阿朗佐·丘奇（Alonzo Church）

他把「能行可计算」这一直觉概念写成了可演算的 λ 项，又用它证明了一阶逻辑没有万能判定程序——与图灵各自独立地为「算法」划定了边界，从而为整个计算机科学铺下第一块理论基石。

一、生平与时代背景

阿朗佐·丘奇于 1903 年 6 月 14 日出生在美国华盛顿哥伦比亚特区。父亲塞缪尔·罗宾斯·丘奇（Samuel Robbins Church）是哥伦比亚特区的治安法官（justice of the peace）兼市法院法官；母亲是米尔德里德·汉娜·莱特曼·帕克（Mildred Hannah Letterman Parker）。其家族学术渊源颇深：祖父阿朗佐·韦伯斯特·丘奇（Alonzo Webster Church，1829—1909）于 1881—1901 年任美国参议院图书馆馆长，曾祖父阿朗佐·丘奇是佐治亚大学第六任校长、数学与天文学教授。

丘奇幼年时因一次气枪事故导致一只眼睛部分失明（存疑：事故细节与具体哪只眼，不同来源记述不一）。父亲因视力衰退失去教职后，全家迁居弗吉尼亚。在同名叔父的资助下，丘奇进入康涅狄格州里奇菲尔德的私立男校 Ridgefield School for Boys 就读，1920 年毕业。

1920 年秋，丘奇入读普林斯顿大学，成绩优异，1924 年以数学学位毕业（A.B.），同年在《美国数学月刊》发表第一篇论文《洛伦兹变换的唯一性》。他留在普林斯顿攻读博士，导师是拓扑学家奥斯瓦尔德·维布伦（Oswald Veblen），1927 年以论文《策梅洛假设的替代方案》（Alternatives to Zermelo's Assumption）获博士学位。读博期间，他于 1925 年与玛丽·朱莉娅·库钦斯基（Mary Julia Kuczinski）结婚（存疑：MacTutor 记为 1926 年，维基百科与若干家谱记作 1925 年，年份存争议）；二人育有三子：小阿朗佐（1929）、玛丽·安（1933）、米尔德里德（1938）。

1927—1929 年，丘奇获美国国家研究委员会（NRC）奖学金访问：1927—1928 年在哈佛大学，随后一年在哥廷根与阿姆斯特丹（期间还短暂在芝加哥大学任讲师）。1929 年回到普林斯顿任数学助理教授，从此在普林斯顿服务近四十年：1939 年升副教授，1947 年升正教授，1961—1967 年任数学与哲学教授。

20 世纪 30 年代的普林斯顿是逻辑学的世界中心：丘奇身边有学生克林（Kleene）、罗瑟（Rosser），有同在普林斯顿的冯·诺依曼；哥德尔 1933、1935 年访问高等研究院，1939 年起永久移居；图灵则于 1936 年以访问研究生身份来到普林斯顿，并留下在丘奇门下完成博士学位。正是在这个环境里，丘奇做出了他一生最重要的工作。

1936 年，丘奇与朗福德（C. H. Langford）共同创办《符号逻辑杂志》（Journal of Symbolic Logic），并任其「评论」栏目的编辑，一干就是 43 年（1936—1979）。1967 年从普林斯顿退休后，他转赴加州大学洛杉矶分校（UCLA）任哲学教授（Flint / Kent 讲席，存疑：MacTutor 作 Kent Professor，维基作 Flint Professorship，讲席名称记载不一）兼数学教授，一直任教到 1990 年「第二次退休」——此时距他第一次退休已过去了 23 年。1992 年，他从洛杉矶迁居俄亥俄州哈德逊（Hudson）安度晚年。1995 年 8 月 11 日，丘奇在哈德逊去世，享年 92 岁，葬于普林斯顿公墓。他终身是长老会信徒。

丘奇一生获得多项荣誉：1962 年在斯德哥尔摩国际数学家大会（ICM）作全会报告；1966 年当选英国科学院通讯院士，1967 年当选美国艺术与科学院院士，1978 年当选美国国家科学院院士；获凯斯西储大学（1969）、普林斯顿大学（1985）、纽约州立大学布法罗分校（1990）荣誉博士。2015 年，ACM SIGLOG、EATCS、EACSL 与哥德尔学会联合设立「阿朗佐·丘奇逻辑与计算杰出贡献奖」以纪念他。

二、学术生涯年表

年份 事件
1903 6 月 14 日生于美国华盛顿特区；父为特区法官
1920 毕业于康涅狄格 Ridgefield School for Boys，入普林斯顿大学
1924 以数学 A.B. 毕业；发表首篇论文《洛伦兹变换的唯一性》
1925 与 Mary Julia Kuczinski 结婚（存疑：一说 1926 年）
1927 在 Veblen 指导下获普林斯顿博士，论文《策梅洛假设的替代方案》
1927—1929 NRC 研究员：哈佛大学，后哥廷根与阿姆斯特丹；短暂任教芝加哥大学
1929 回普林斯顿任数学助理教授
1932—1933 发表《逻辑基础的一组公设》，提出后来演变为 λ 演算的系统
1934 学生 Kleene、Rosser 获博士学位
1935 Kleene–Rosser 悖论揭示其原系统不一致，遂退守纯 λ 演算
1936 发表《初等数论的一个不可解问题》提出丘奇论题；发表《论判定问题》证明一阶逻辑不可判定（丘奇定理）；与朗福德创办《符号逻辑杂志》，任评论栏编辑至 1979 年；图灵来普林斯顿，后在其门下读博
1936 与 Rosser 证明 Church–Rosser 定理（合流性）
1938 图灵获博士学位（丘奇指导）；子 Mildred 出生
1939 升普林斯顿副教授
1940 发表《简单类型论的一个表述》（简单类型 λ 演算）
1941 出版《λ 转换演算》（The Calculi of Lambda-Conversion）
1944 出版《数理逻辑导论》初版（1956 年大幅扩修订）
1947 升普林斯顿正教授；学生 Henkin 获博士
1951 发表《涵义与指称逻辑的一个表述》，开创弗雷格—丘奇内涵语义
1961 任普林斯顿数学与哲学教授
1962 斯德哥尔摩 ICM 全会报告
1967 从普林斯顿退休，转任 UCLA 哲学与数学教授
1978 当选美国国家科学院院士
1990 从 UCLA 第二次退休；获 SUNY 布法罗荣誉博士
1992 迁居俄亥俄州 Hudson
1995 8 月 11 日于 Hudson 去世，享年 92 岁

三、核心成果（逐条技术解析）

1. λ 演算（λ-calculus，1932—1936）——用函数改写全部数学与计算

问题背景：20 世纪初逻辑学为数学奠基，希尔伯特纲领要求给出严格的形式系统。丘奇想构造一个以「函数」而非「集合」为基本概念的逻辑系统，来避开朴素集合论的悖论。1932—1933 年他在《逻辑基础的一组公设》中引入了一种带变量绑定的记号，这就是 λ 演算的雏形。

关键思想：系统只有三种表达式——变量 $x$、抽象（abstraction）$\lambda x.M$（表示把 $x$ 映射为 $M$ 的函数）、应用（application）$M\,N$。核心运算规则是 β-归约：$(\lambda x.M)\,N \rhd_\beta M[x:=N]$，即用参数替换函数体中所有自由的 $x$。丘奇还设计了丘奇编码：用闭 λ 项表示数据——例如丘奇数 $\overline{n} = \lambda f.\lambda x.f^n(x)$（把 $f$ 作用 $n$ 次），于是加法、乘法、幂、前驱、条件分支等全都可写成 λ 项。

精确表述：Church–Rosser 定理（1936，与 Rosser 合作）——若一个 λ 项 $M$ 可以分别归约到 $M_1$ 和 $M_2$，则存在某个 $N$ 使 $M_1$ 和 $M_2$ 都能归约到 $N$（合流性 / confluence）。由此推出正规形唯一：若归约终止，则结果与归约顺序无关。这一定理为 λ 演算作为「计算」模型提供了一致性保证。

与前人的关系：弗雷格、皮亚诺已有函数抽象的思想；组合子逻辑（Schönfinkel 1924、Curry 1930 起）是无变量的另一条进路。丘奇的贡献是把变量绑定、抽象与归约整合成一个可计算的演算，并证明其表达力与递归函数、图灵机等价。

局限性：1935 年 Kleene 与 Rosser 证明丘奇最初那个「带逻辑常量的完整系统」是不一致的（Kleene–Rosser 悖论，推广了罗素悖论与理查德悖论）。丘奇随即剥离掉逻辑部分，只保留纯函数演算（纯 λ 演算），后者是一致的，但表达「一般递归」需要借助不动点组合子（如 $Y$），不能直接在有类型的版本中无限制递归。

2. 丘奇论题（Church's Thesis，1936）——把「能行可计算」等同于递归 / λ-可定义

问题背景：「有没有算法判定某件事」是 20 世纪 30 年代逻辑学与数学基础的核心问题，但「算法 / 能行过程」本身只是个直觉概念，没有严格定义。哥德尔 1934 年在普林斯顿讲演中推广了 Herbrand 提出的「一般递归函数」概念，但他本人当时并不确信递归性足以刻画全部可计算性。

关键思想：丘奇在 1936 年《美国数学杂志》上的《初等数论的一个不可解问题》中明确提出：将「正整数的能行可计算函数」定义为「正整数的递归函数（或 λ-可定义函数）」。他与克林证明了 λ-可定义函数类与一般递归函数类完全相同，两个看似无关的刻画殊途同归，这一等价性是支持论题的最强经验证据。

精确表述（丘奇 1936a，第 356 页原话）：

We … define the notion … of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a λ-definable function of positive integers).

与前人的关系：图灵几乎同时（1936）独立提出用「图灵机可计算」刻画可计算性，并在得知丘奇的工作后迅速证明了 λ-可定义性与图灵可计算性等价（等价性定理）。三种刻画（递归、λ-可定义、图灵可计算）外延相同，共同构成「丘奇—图灵论题」。

局限性：这是一个论题而非定理——它把一个非形式概念（能行可计算）等同于形式概念，因此「很可能为真，却无法被严格证明」（Folina 1998 所综述的学界主流观点）。Post 曾批评丘奇「把这一等同伪装成定义」，会让人忽视它需要持续验证；哥德尔则认为图灵对「计算」的分析比丘奇的「定义式」提法更令人信服（这也解释了为何今天图灵的版本更广为人知）。

3. 丘奇定理（Church's Theorem，1936）——一阶逻辑的判定问题不可解

问题背景：希尔伯特的「判定问题」（Entscheidungsproblem）问：是否存在一个能行程序，对任意给定的一阶逻辑公式，都能在有限步内判定它是否普遍有效（或可满足）？命题逻辑有真值表判定法，那么一阶逻辑呢？

关键思想：丘奇先构造了一个有限可公理化的一阶子系统（本质上是递归函数理论的一个片段），然后证明：若一阶逻辑有判定程序，则该子系统也有；但该子系统中存在递归不可解的问题（由他在同一篇论文中证明的「初等数论的不可解问题」给出），故一阶逻辑不可能有判定程序。

精确表述：不存在一个能行（算法）过程，对任意一阶谓词逻辑公式 $A$，判定 $A$ 是否为逻辑有效式。这与命题逻辑形成鲜明对比——后者的永真性可由真值表在有限步内判定。

与前人的关系：该结果是哥德尔 1931 年不完备定理的延伸：哥德尔证明了足够强的形式系统不可完备，丘奇则进一步证明一阶逻辑本身不可判定。图灵在 1936—1937 年用图灵机与停机问题独立证明了同一结论。

局限性：该定理只断言「没有统一的全判定程序」，并不排除对某些特殊子类（如一元谓词公式、只含若干量词的前束范式片段）存在判定程序——事实上一阶逻辑存在可判定的「前缀类」谱系，研究这些片段的判定性是后来模型论与理论计算机科学的活跃方向。

4. 简单类型论与简单类型 λ 演算（1940）——用类型化解悖论

问题背景：罗素与怀特海在《数学原理》中用「分支类型论」规避悖论，但系统繁复、难以使用。丘奇希望给出一个建立在 λ 演算之上、简洁且无矛盾的类型系统。

关键思想：1940 年《简单类型论的一个表述》中，丘奇为每个 λ 项指派类型：基本类型（如个体类型 $\iota$、真值类型 $o$），以及函数类型 $\alpha\to\beta$；抽象 $\lambda x_\alpha.M_\beta$ 具有类型 $\alpha\to\beta$。类型规则禁止「自指」式的应用，从而从根源上排除了罗素悖论之类的自指构造。

精确表述：简单类型 λ 演算（STLC / Church-style） 是带类型的函数演算，满足强正规化（所有归约序列都终止），其逻辑对应（Curry–Howard 对应）是极小蕴涵逻辑。它既能表达经典高阶逻辑（丘奇用它表述简单类型论），又是今天几乎所有类型化函数式语言与证明助手（Coq、Lean、Agda）的直接祖先。

局限性：简单类型论不能直接归纳定义任意递归函数（强正规化意味着不存在一般递归），表达数学需要外加公理（如无穷公理、选择公理）；其集合论强度弱于 ZF。后来的依赖类型论、Martin-Löf 类型论是在它基础上的深化。

5. 弗雷格—丘奇本体论与内涵逻辑（1951 起，持续约 40 年）

问题背景：弗雷格区分了语言表达式的「涵义」（Sinn / sense）与「指称」（Bedeutung / denotation）——「晨星」与「昏星」指称相同（金星）但涵义不同。但把「涵义」对象化、形式化却很难。

关键思想：丘奇在 1951 年《涵义与指称逻辑的一个表述》中，把涵义本身当作一类实体，构造了一种内涵逻辑：同一指称对象在不同「可能涵义」下对应不同的内涵实体，命题态度句（「某人相信……」）的真值依赖于子句的涵义而非指称。这一构想被称为弗雷格—丘奇本体论（Frege–Church ontology）。他还被认为提出了「弹弓论证」（Slingshot Argument），试图证明语句的指称只能是真值而不能是命题。

与前人的关系：直接继承弗雷格的涵义—指称二分；与卡尔纳普的内涵—外延方法、蒙塔古语法相关联，但丘奇坚持「涵义作为独立实体」的实在论立场。

局限性：丘奇为这套逻辑给出了多个相互竞争的版本（Alternative (0)、(1)、(2)），始终未能确定一个令人完全满意的公理化；其中某些版本被证明会导致矛盾或意外后果。后来的可能世界语义学（克里普克、蒙塔古）提供了更简洁的内涵处理方式，使丘奇的精细方案影响力相对下降，但其对语言哲学与形式语义学的奠基意义仍被公认。

6. 随机序列的概念（1940）——可计算性渗入概率论

1940 年丘奇发表《论随机序列的概念》，尝试用递归函数给出「随机序列」的逻辑上令人满意的定义：一个 0-1 序列被称为（丘奇）随机，若不存在递归可计算的位置选择规则能选出一个子序列使其频率偏离整体。这是算法随机性理论的重要先驱（Von Mises 1919 提出直觉想法，丘奇用递归论把它精确化），但后来被 Martin-Löf（1966）用「可计算可枚举的测度为零的集合」给出的更强定义所取代——丘奇随机序列不满足某些大数定律的「随机性」要求，是其局限。

四、代表著作与文献

五、师承、学派与同时代交往

六、争议、公案与历史评价

七、身后影响与学术谱系

八、延伸阅读与权威来源