上一篇用 BHK 解释把"证明"重新定义成"构造一个见证物"，并提到那份翻译表"看起来就是一组类型"。本篇正式给出这个直觉的精确版本：Curry-Howard 同构——命题就是类型，证明就是程序，证明检查就是类型检查。

这条同构是形式化方法的基石。理解了它，"为什么形式化编译器编译通过就是定理得证"这条主线问题第一层翻译就被打通：检查证明这件事被压成了机械的类型检查。

本篇不假设读者会 Coq 或 Agda，但要求理解上一篇的 BHK 表，并能读简单的 Python 类型注解。中段会用 Lean 4 写两段简短代码做对照。

同构的对照表

把上一篇 BHK 表整理成"逻辑端 ↔ 类型端"的并列形式：

逻辑端 类型端 程序端的项构造 程序端的项消费
原子命题 A 基本类型 A 公理/假设变量 当作变量使用
⊥ 空类型 Void / Empty 没有构造子 absurd : Void → C
⊤ 单位类型 Unit () 无信息可消费
P ∧ Q 积类型 P × Q ⟨p, q⟩ .1 / .2
P ∨ Q 和类型 P ⊕ Q InL p / InR q `match … with InL p => …
P → Q 函数类型 P → Q fun p => e f x
¬P P → Void 把 P 的证据映成 Void 的函数 同上
∀ x : A, P(x) 依值函数 (x : A) → P(x) fun x => e f a
∃ x : A, P(x) 依值积 (x : A) × P(x) ⟨a, p⟩ .1 取见证、.2 取证明
证明检查 类型检查 — —

读这张表的方式有两种：

  1. 逻辑视角：每条联结词对应一种数据结构，每一步推理对应一次构造。
  2. 编程视角：常见数据类型其实在偷偷表达逻辑命题；以前以为只是组织数据，其实是在写证明。

两种视角说的是同一件事。Curry-Howard 之所以被叫"同构"，是因为这种翻译两边可逆，且保持结构。

同一段代码的两种读法

Lean 4 里把 BHK 的 (P ∧ Q) → (Q ∧ P) 和"二元组反转"写出来，几乎是同一段代码：

1
2
3
4
5
6
7
-- 命题逻辑视角：∧ 的交换律
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

-- 类型视角：二元组反转
def pair_swap {α β : Type} : α × β → β × α :=
  fun p => (p.2, p.1)

两段代码的结构同形：

元素 theorem 版 def 版
主体 fun h => ⟨h.right, h.left⟩ fun p => (p.2, p.1)
输入类型 P ∧ Q（命题） α × β（类型）
输出类型 Q ∧ P（命题） β × α（类型）
解构 .right / .left .2 / .1
构造 ⟨_, _⟩ (_, _)
关键字 theorem def

theorem 和 def 在 Lean 4 内部几乎是同一种声明，区别仅在于：theorem 期望返回类型在 Prop 这个特殊宇宙里，def 在 Type 宇宙里。Prop 与 Type 共享一套表达式语法，所以"证明命题"和"写程序"在编辑器里看上去就是一样的事。

这正是 Curry-Howard 同构在工具层的落实：一份编译器同时充当类型检查器与证明检查器。

三组典型对应

把表里几条最常见的对位单独展开。

蕴含与函数

证明 P → Q 在 BHK 里要给出"把 P 的证明转成 Q 的证明的方法"。在程序端，就是一个把 P 类型的值映成 Q 类型的值的函数。

1
2
theorem modus_ponens (P Q : Prop) (h1 : P) (h2 : P → Q) : Q :=
  h2 h1

modus_ponens 的证明就是 h2 h1，纯粹是函数应用。逻辑里"假言推理"的整个机制被等价为程序里"调用函数"。

合取与积

1
2
3
4
5
theorem and_intro (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
  ⟨hp, hq⟩

theorem and_elim_left (P Q : Prop) (h : P ∧ Q) : P :=
  h.left

“P ∧ Q 的证明"等价于"P × Q 类型的值”。⟨_, _⟩ 构造对，.left / .right 取分量。证明的合取消去就是元组的字段访问。

析取与和类型

1
2
3
4
5
6
7
theorem or_intro_left (P Q : Prop) (hp : P) : P ∨ Q :=
  Or.inl hp

theorem or_elim (P Q R : Prop) (h : P ∨ Q) (hp : P → R) (hq : Q → R) : R :=
  match h with
  | Or.inl p => hp p
  | Or.inr q => hq q

P ∨ Q 的证明是带标签的：要么 Or.inl p，要么 Or.inr q。析取消去就是模式匹配。CS 学生常用 enum 或 sealed class 表达这种"二选一"结构——它正是逻辑里的 ∨。

全称与依值函数

1
2
theorem refl_implies_self (A : Type) : ∀ x : A, x = x :=
  fun x => rfl

∀ x : A, P(x) 的证明是一个函数，对每个 x : A 都给出 P(x) 的证明。这条函数比普通函数额外的一点是：返回类型 P(x) 可以依赖输入 x。这种"返回类型依赖输入"的函数叫依值函数，专门处理 ∀。

存在与依值积

1
2
theorem exists_zero : ∃ n : Nat, n + 1 = 1 :=
  ⟨0, rfl⟩

∃ n : Nat, n + 1 = 1 的证明是一对：见证 0 和它满足性质的证明 rfl。直觉主义不许只说"存在"，必须给见证；类型层就反映为"必须构造出 ⟨a, p⟩"。

类型检查 = 证明检查

打通同构后，要把"编译通过就是定理得证"撑起来还差一步：让证明检查变成一个机械、可终止、可被实现的算法。

类型检查恰好就是这个算法。Lean 4 的内核拿到一段表达式 e 和一个期望类型 T，会按一组固定的类型规则做以下事：

  1. 把 e 拆开成子表达式。
  2. 对每个子表达式做局部类型推导，得到它的"实际类型"。
  3. 比较"实际类型"与上下文期望的类型，必要时按规则规约（β-规约、δ-规约、ι-规约）。
  4. 所有约束都成立，输出"类型正确"；任意一步失败，输出"类型错误"并定位。

整个过程不需要"创造性"。在 STLC 这样的系统里它是可判定的；在依值类型系统里它依赖归一化，但对良类型程序仍然可判定。

读到这里，"为什么编译通过就是定理得证"的第一层答案出现了：

同构的左侧（命题与证明）和右侧（类型与程序）一一对应。检查"证明是否成立"等价于检查"程序是否良类型"。后者是编译器内核每天在做的事。

第三层（“我们到底信什么”——可信内核、坏公理、一致性）后续文章再展开。

历史脉络

年份 人物 贡献
1934 Curry 注意到组合子逻辑里某些组合子的类型与命题逻辑的公理同形
1958 Curry 在 Combinatory Logic, Vol. I 中系统化了这种对应
1969 Howard 给 STLC 与一阶直觉主义命题逻辑给出完整对应（手稿先在小范围流传）
1972 de Bruijn 在 AUTOMATH 系统中第一次把这种对应工程化为可运行的证明检查器
1980+ Lambek 把对应推广到笛卡尔闭范畴，形成 Curry-Howard-Lambek 三角
1985 Coquand & Huet Calculus of Constructions，依值类型系统首次落地
1989 Coq 1.0 工业级证明助手开始扩散
2015 Wadler Propositions as Types 总结同构在 CS 50 年里的演化

工程版本（Coq、Lean、Agda、Idris）追求的是同一件事：把这条同构铸成可运行的工具。

同构不是平凡同义反复

读者可能会怀疑这条同构是不是"换了说法的同义反复"。它不是。它带出了三件具体的好处：

  1. 可机器检查。证明被拆成一棵语法树，类型规则按树结构归纳判断。没有任何步骤需要"人类直觉"。
  2. 可组合。证明就是程序，程序可以复用、参数化、抽象。Lean 的 Mathlib 之所以能积累几百万行可信引用的数学，是因为定理可以像函数一样被 import、被组合。
  3. 可与算法共生。需要在证明里"算"一个具体值（比如判断 1 + 1 = 2）时，类型检查器直接调求值器跑出结果。证明里嵌入计算变得自然。

古典数学里"证明"和"计算"是两件事；构造类型论里它们被压成一个对象。这件事的工程含义是巨大的：CompCert 编译器的正确性证明在 Coq 里既是定理也是程序，Coq 可以从证明里抽取出可运行的 OCaml 编译器二进制，并保证它的行为符合证明所述。

Lean 4 中怎么直接看到同构

打开 Lean 4 Web 编辑器，跑：

1
2
#check (fun (p : Nat × Nat) => (p.2, p.1))
#check (fun {P Q : Prop} (h : P ∧ Q) => ⟨h.right, h.left⟩ : ∀ {P Q : Prop}, P ∧ Q → Q ∧ P)

两条 #check 输出的类型分别在 Type 与 Prop 宇宙，但语法骨架同构。Lean 把两件事用同一套机制处理。

也可以倒过来：把一个证明当成函数调用。

1
2
3
4
theorem swap : ∀ {P Q : Prop}, P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

example (p : True ∧ False) : False ∧ True := swap p

swap p 是函数应用，但读者也可以把它读成"使用定理 swap 把 True ∧ False 转成 False ∧ True"。两种读法在 Lean 内部是同一条 β-规约。

模式提炼

模式 内容
命题即类型 写命题时，找到对应的类型构造；写类型时，反过来读成命题
证明即程序 写证明等价于写表达式；表达式的求值即证明的规约
解构对应消去 模式匹配 / 字段访问 = 逻辑规则的消去
构造对应引入 构造子 / lambda = 逻辑规则的引入
检查即推导 类型检查器走完类型规则就是走完证明树

后续 STLC、依值类型、归纳类型、Lean 实战、可信基底，本质上都是把这五条模式中的某一面继续精细化。

给读者的练习

  1. 用 Lean 4 Web 编辑器写出 (P → Q → R) → (P ∧ Q → R) 的证明，并把它的"程序对偶"——一个普通的 Curry/Uncurry 函数——写出来。
  2. 思考 ((P → Q) ∧ (Q → P)) 的程序对偶。它对应什么常见的工程模式？
  3. 用 Python 的 Optional[T] 类比，P ∨ ⊤ 对应什么？为什么这条命题在直觉主义下仍然平凡可证？
  4. 想清楚：P → ⊥ 与"函数返回值类型是不可达类型"在 Rust / Haskell 里分别长什么样。

衔接到下一篇

本篇打通了命题与类型的对应。下一篇把焦点缩到最小可证明系统——简单类型 lambda 演算（STLC）：

  • STLC 的语法是什么。
  • 类型规则 Γ ⊢ e : τ 怎么读。
  • 为什么 STLC 已经能表达整个直觉主义命题逻辑。
  • 强归一化（每个良类型项都能终止）为什么是"类型检查 = 证明检查"得以可判定的关键。

那之后第 04 篇会用 Python 写一个真能跑的 STLC 双向类型检查器，把"类型检查就是证明检查"从概念落到机械实现。

参考资料