数学中的函数，在教科书里通常被写成 的形式——$f$ 有个名字，$x$ 是变量，结果是某个表达式。1936 年，阿隆佐·邱奇（Alonzo Church）提出了一种不需要函数名字的写法：把函数本身当作一个对象，写成 。这个 （lambda），后来成为函数式编程、类型论和形式逻辑深层统一的符号。
λ 演算和类型理论，是现代编程语言理论的双重基础：前者定义了"计算是什么"，后者定义了"什么样的程序是安全的"。它们之间那条被称为 Curry-Howard 对应的深刻联系，揭示了程序和数学证明之间令人惊讶的同构关系。
破除误解：λ 演算不只是函数式语言的"语法糖"
Haskell、OCaml、Lisp、甚至 Python 的 lambda 表达式，让人以为 λ 演算只是函数式编程语言的语法特性。这是对它地位的大幅低估。
λ 演算是一套与图灵机等价的计算模型——任何图灵机能计算的，λ 演算都能计算，反之亦然（这是邱奇-图灵论题的一个分支）。它不依赖于内存、状态、指令序列，只用函数定义和函数应用就能表达一切计算。这使它成为研究计算本质最干净的数学框架之一。
核心一：无类型 λ 演算
无类型 λ 演算（Untyped Lambda Calculus）的语法极为简洁，只有三种构造：
- 变量：$x$、$y$、$z$（代表某个值）
- 抽象（函数定义）：（参数为 $x$，函数体为 $M$）
- 应用（函数调用）：（把函数 $M$ 应用于参数 $N$）
计算通过β 规约（beta reduction）进行：
把 $M$ 中所有自由出现的 $x$ 替换为 $N$。
这三条规则，足以表达加法、乘法、布尔逻辑、条件分支、递归（通过不动点组合子 $Y$），乃至整个自然数系统（通过邱奇数编码）。
Y 组合子（Y combinator）是表达递归的关键：
——$Y$ 让函数 $f$ 能"调用自身"，而 $f$ 本身无需知道自己的名字。著名创业孵化器 Y Combinator 的名字正取自这个组合子（创始人 Paul Graham 出身 Lisp 程序员，把它视为编程中最酷的思想之一）。
Church-Rosser 定理：殊途同归的自由
一个 λ 项里往往同时有多个可规约的子表达式，先算哪个？邱奇与他的学生 Barkley Rosser 在 1936 年证明的合流定理（Church-Rosser Theorem，也称菱形性质）给出了令人安心的答案：如果一个项沿两条不同的规约路径分别变成 和 ，那么一定存在一个项 $N$，使 和 都能继续规约到它。推论是：正规形（无法再规约的项）若存在，必然唯一——计算结果不依赖于规约顺序。
这不等于"怎么算都一样快"，更不等于"怎么算都能停"。看两个例子：
- ：自我应用产生自身，永远规约下去，对应"死循环"。
- ：一个丢弃参数、直接返回 $y$ 的常函数，作用在死循环上。若先算参数（传值，applicative order），先掉进 的死循环；若先展开函数、发现参数根本用不上（传名，normal order），一步得到 $y$。
标准化定理（Standardization Theorem）保证了最左最外序的完备性：只要正规形存在，按这个顺序一定能到达它。代价是参数可能被复制多次、重复求值。这个权衡直接进入现实语言：Haskell 的惰性求值（传需，call-by-need）在传名的基础上加了共享记忆，用空间换"只算一次"；OCaml、Scheme 默认传值，换来可预测的性能与副作用顺序。"求值顺序"由此从一个实现细节，变成语言设计的核心决策。
组合子：连变量都可以不要
λ 演算有变量、有抽象。还能更省吗？1924 年，Moses Schönfinkel 证明：只需要两个函数就能表达全部可计算的东西（Curry 后来独立重新发展了这一体系，称为组合逻辑）：
$K$ 是常函数，$S$ 负责"分发"：把参数 $z$ 同时喂给两个函数再组合。恒等函数可以免费得到：，所以 。
关键在于括号抽象（bracket abstraction）：任何 λ 项都可以机械地翻译成只含 $S$、$K$ 的式子。规则大致是： 译成 $I$；（$M$ 不含 $x$）译成 ； 译成 。递归应用下去，变量被逐一消去。
这个结果的意义超出语法游戏：它说明计算不需要命名——绑定变量只是一种记号便利，函数的组合结构本身就承载了全部信息。这也解释了组合逻辑为何能成为某些函数式语言编译器的中间表示，以及为什么柯里会首先在组合子的类型上瞥见命题逻辑的影子——那是 Curry-Howard 对应最早的线索。
核心二：类型系统——给程序加上安全网
无类型 λ 演算强大但危险：任何表达式都可以被应用于任何其他表达式，这意味着"一个数字加上一个布尔值"在语法上是合法的，但在语义上没有意义，甚至可能发散（无限循环）。
类型系统给每个表达式分配一个"类型"，并通过类型检查在程序运行前排除一大类错误。
简单类型 λ 演算（Simply Typed Lambda Calculus，STLC，Church 1940 年提出）是最基础的有类型版本：
- 基础类型：、 等
- 函数类型：（接受 $A$ 类型参数，返回 $B$ 类型结果）
- 类型规则： 的类型为 ，当且仅当 $M$ 在 $x : A$ 的假设下具有类型 $B$
STLC 的代价是失去了图灵完备性——可以检查的程序范围变窄，但换来的是：所有类型正确的程序都能终止（强归一化定理）。
代价有一个具体的形状：Y 组合子在 STLC 里无法定型——它的自应用结构（）要求一个类型等于以自身为参数的类型，而 STLC 的类型是有限的语法树，容不下这种循环。所以实用的类型化语言都把递归作为显式原语加回来（letrec、不动点算子），等于在"必然终止"的保险箱上开一个受控的口子。
更丰富的类型系统在安全性和表达力之间寻找不同平衡：
| 系统 | 代表语言 | 特点 |
|---|---|---|
| Hindley-Milner 类型推断 | Haskell, OCaml, ML | 多态类型，自动推断，不需要显式标注 |
| 依赖类型（Dependent Types） | Coq, Agda, Lean | 类型可以依赖于值，可表达任意数学命题 |
| 线性类型（Linear Types） | Rust（近似） | 每个值只能用一次，用于资源管理 |
核心三：Curry-Howard 对应——程序即证明
早在 1934 年，哈斯凯尔·柯里（Haskell Curry）就注意到：组合子逻辑中函数的类型，与直觉主义命题逻辑中的命题，有一种令人惊讶的对应（他在 1958 年的《组合逻辑》一书中系统阐述了命题片段的版本）。1969 年，威廉·霍华德（William Howard）把它扩展到一阶谓词逻辑（他的手稿 1980 年才正式发表）。
Curry-Howard 对应（也称"命题即类型"，Propositions as Types）：
| 类型论 | 逻辑 |
|---|---|
| 类型 $A$ | 命题 $A$ |
| 类型 $A$ 的项（term）$t$ | 命题 $A$ 的一个证明 |
| 函数类型 | 蕴含 |
| 乘积类型 | 合取 |
| 和类型 $A + B$ | 析取 |
| 空类型 | 假命题（矛盾） |
| 函数应用 | 肯定前件（Modus Ponens）推理规则 |
| β 规约 | 证明化简 |
这个对应不是类比，而是严格的数学同构：写一个类型为 $A$ 的程序，等价于构造命题 $A$ 的一个证明。程序和证明是同一件事的两种说法。
准确的陈述（对简单类型 λ 演算）是：类型 $A$ 被某个闭项占据，当且仅当命题 $A$ 在直觉主义蕴含逻辑中可证。判定"一个类型有没有居民"和判定"一个命题可不可证"，是同一个问题。更进一步，β 规约对应证明论中的归一化——消去证明里"先引入再立即消去"的迂回。STLC 的强归一化定理因此同时是两个领域的定理：所有类型正确的程序必然终止；每个直觉主义证明都能化简为无迂回的正规形式。代码优化与证明化简，是同一场电影的两个配音版本。
Curry-Howard 对应的实践结果是证明辅助系统（Proof Assistants）：Coq、Agda、Lean 等工具，把数学证明作为程序来编写，由计算机验证其正确性。四色定理（2005 年的 Coq 机器验证版本）、Feit-Thompson 定理（2012 年的 Coq 验证）等重要数学结果，都已通过这种方式得到形式验证。
核心四：依赖类型与定理证明
依赖类型（Dependent Types）允许类型依赖于值——例如，"长度为 $n$ 的向量"可以是一个以自然数 $n$ 为参数的类型：。
这使类型系统能表达任意精确的程序性质：
- "这个排序函数返回与输入等长的数组，且元素是输入的置换"
- "这个除法函数只接受除数不为零的参数"
依赖类型的 Curry-Howard 对应更丰富：全称量词 对应依赖函数类型 ，存在量词 对应依赖对类型 。
佩尔·马丁-洛夫（Per Martin-Löf）的直觉主义类型论（Intuitionistic Type Theory，1975–1984）是依赖类型理论的奠基工作，也是 Coq、Agda 的直接理论前驱。
代价与争议
可用性鸿沟：高阶类型系统（特别是依赖类型）在实用工程项目中的采用非常有限，主要原因是学习曲线陡峭、类型错误难以阅读、编程负担重。Rust 的成功部分来自于引入了线性类型（所有权系统）而没有依赖类型——在安全性和可用性之间找到了更好的平衡点。
证明辅助的局限：形式验证并不能消灭所有 bug。规范（specification）本身可能是错的；形式化工作量往往是非形式化的数倍。主流软件工程实践中，形式验证主要用于关键安全领域（密码学协议、操作系统微内核）。
经典逻辑 vs. 直觉主义：Curry-Howard 对应对应的是直觉主义逻辑（不承认排中律的一般有效性），而非经典逻辑。排中律 对应的程序是call/cc（call-with-current-continuation），引入了复杂的控制流。经典逻辑的完整类型论语义至今仍是活跃研究课题。
跨域连接
- 数学哲学：构造主义要求"存在"必须给出见证，而不能只靠反证。类型即命题把这条要求变成可执行的东西：一个证明就是一个能算出值的程序。排中律因此没有直接的计算内容——它对应的是控制流跳转，而不是一个构造出的对象。
- 证明：证明在这里从"说服同行的论述"变成"能被检查器逐步验证的项"。这把可靠性和可理解性拆成了两件事：机器验证的证明可以长到无人通读，却仍然可信；而人写得优美的证明，未必经得起逐步检查。数学共同体接受哪一种，是社会问题而非逻辑问题。
- 集合论：类型论提供了另一套数学基础，与集合论的差别不在能证多少，而在类型论自带计算内容：证明可以被求值，等式可以被化简。集合论里"存在一个函数"是断言，类型论里同一句话必须交出那个函数本身。
- 函数式编程：只有函数定义与函数应用两条构造，就足以编出数、布尔值、分支与递归。这说明"计算"不必依赖内存、状态与指令序列——它可以完全由替换驱动，而这正是函数式语言把求值顺序、副作用当成可选项来设计的理论依据。
- 形式化验证：依赖类型允许类型依赖于值，于是规约可以直接写成类型，"通过类型检查"即"满足规约"。代价是表达力与可判定性的对冲：类型系统越强，类型检查越可能不可判定或代价极高，工程上因此总要在某处停手。
参考文献
- Church, A. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5 (1940): 56–68.
- Church, A. & Rosser, J. B. Some Properties of Conversion. Transactions of the American Mathematical Society 39(3) (1936): 472–482. （合流定理）
- Schönfinkel, M. Über die Bausteine der mathematischen Logik. Mathematische Annalen 92 (1924): 305–316. （组合逻辑的开端）
- Howard, W. A. The Formulae-as-Types Notion of Construction. 手稿 1969 年；发表于 Seldin & Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press (1980).
- Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North-Holland (1984). （λ 演算标准专著）
- Martin-Löf, P. An Intuitionistic Theory of Types. In Sambin & Smith (eds.), Twenty-Five Years of Constructive Type Theory. Oxford University Press (1998).
- Pierce, B. C. Types and Programming Languages. MIT Press (2002). （最广泛使用的教材）
- Wadler, P. Propositions as Types. Communications of the ACM 58 (2015): 75–84. （优秀的综述，免费在线）
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013). （HoTT 书，免费在线版）