阿隆佐·邱奇

概述

美国数学家、逻辑学家（1903–1995），普林斯顿大学教授。1936年使用 λ 演算（lambda calculus）率先证明了判定问题 (Entscheidungsproblem)的否定回答，与阿兰·图灵几乎同时但独立地解决了这一悬而未决的数学难题。

关键内容

λ 演算（Lambda Calculus）

Church 在1930年代发明了一种全新的形式系统——λ 演算，用于研究函数的定义、应用和递归：

• 核心思想：一切计算都可以归结为函数的抽象（abstraction）和应用（application）
• 语法极简：只有变量、函数抽象（λx.M）和应用（M N）三种构造
• 计算能力：尽管语法极其简单，λ 演算被证明与图灵机完全等价——任何图灵可计算的函数都是 λ 可定义的，反之亦然
• 影响：λ 演算后来成为函数式编程语言（Lisp、Haskell、ML 等）的理论基础，并在现代编程语言的类型理论中扮演核心角色

判定问题的否定回答（1936）

1936年春天，Church 发表论文，使用 λ 演算证明了判定问题的答案是否定的：

• 方法：首先定义"有效可计算性"为"λ可定义性"，然后证明存在不可 λ 定义的函数
• 局限性：λ 演算是一个高度抽象的形式系统，普通人很难从中看到"计算"的直观含义
• 与 Turing 的对比：虽然 Church 先发表论文，但 Turing 的独立工作——用图灵机这种可以被想象为物理机器的模型——具有不可替代的直观性和预见性

与 Turing 的关系

• Church 是 Turing 在普林斯顿大学攻读博士学位（1936–1938）期间的导师
• 在 Turing 1936年论文发表后，Church 认可了图灵机模型的优越直观性
• 两人共同确立了"Church-Turing 论题"——所有合理的计算模型定义了同一个"可计算性"概念

学术传承

• 培养了众多杰出学生，包括 J. Barkley Rosser（Rosser 定理）、Stephen Kleene（递归函数理论）、Hartley Rogers（可计算性理论）
• 在普林斯顿大学任教数十年，影响了整整一代逻辑学家和计算机科学家

来源

• raw/books/计算机科学/01-turing-on-computable-numbers.md

相关

• λ 演算 — Church 的发明
• 判定问题 (Entscheidungsproblem) — Church 率先给出否定回答
• Church-Turing 论题 — 与 Turing 共同确立
• 阿兰·图灵 — 几乎同时独立解决同一问题
• 图灵机 — 与 λ 演算等价但更直观的计算模型