简单类型 lambda 演算：最小可证明系统

上一篇打通了命题与类型的对应：命题就是类型，证明就是程序。本篇把这条同构落在最小可证明系统上——简单类型 lambda 演算（Simply Typed Lambda Calculus，STLC）。

STLC 是类型系统的"hello world"。它语法只有三种表达式、五条核心类型规则，却已经能精确对应整个直觉主义命题逻辑。读懂 STLC 之后，依值类型、归纳类型、Lean 4 都只是在它上面加构造，不会改变骨架。

本篇先写出 STLC 的语法和类型规则，再画一棵推导树，最后说清楚 STLC 能证明什么、不能证明什么。下一篇把这些规则用 Python 落地成一个真跑的类型检查器。

三种表达式 + 三种类型

STLC 的核心语法可以用 BNF 写成：

e ::= x                  -- 变量
    | λ x : τ . e        -- 函数（抽象）
    | e1 e2              -- 调用（应用）

τ ::= A                  -- 基本类型
    | τ1 → τ2            -- 函数类型

把上一篇 Curry-Howard 表里的 ∧、∨、⊤、⊥ 也加进来，得到带积、和、单位、空类型的"扩展 STLC"：

e ::= x
    | λ x : τ . e
    | e1 e2
    | (e1, e2)                  -- 配对
    | fst e | snd e             -- 投影
    | inl e | inr e             -- 注入
    | case e of inl x => e1 | inr y => e2
    | ()                        -- 单位元
    | absurd e                  -- 空类型消去

τ ::= A
    | τ1 → τ2
    | τ1 × τ2
    | τ1 + τ2
    | Unit
    | Void

这就是 STLC 的全部语法。没有循环、没有可变状态、没有副作用、没有递归（除非额外加 fix 算子）。读起来像玩具，但它能精确表达：

逻辑端	STLC 端
`P`	基本类型 `A`（解读为 `P`）
`P → Q`	`A → B`
`P ∧ Q`	`A × B`
`P ∨ Q`	`A + B`
`⊤`	`Unit`
`⊥`	`Void`
`¬P`	`A → Void`

蕴含、合取、析取、真、假、否定——直觉主义命题逻辑的全部联结词都在 STLC 里有完全对应的类型构造子。

类型判断与上下文

要谈"一段程序的类型是什么"，需要明确知道它使用的变量分别是什么类型。这就是类型上下文 Γ。一个上下文是变量到类型的有限映射：

1	`Γ ::= ∅ \| Γ, x : τ`

类型判断写作：

1	`Γ ⊢ e : τ`

读作"在上下文 Γ 下，表达式 e 具有类型 τ"。这条形式叫类型判定或类型 sequent。

整个 STLC 的类型系统就是一组关于 Γ ⊢ e : τ 的推导规则。每条规则有若干条前提（写在横线上方）和一条结论（写在横线下方）。

核心类型规则

下面把 STLC 的类型规则按"引入"和"消去"成对列出。"引入"规则告诉你怎样构造该类型的值（对应逻辑里的引入规则），"消去"规则告诉你怎样使用该类型的值（对应消去规则）。

变量

1 2	`─────────────── (Var) Γ, x : τ ⊢ x : τ`

上下文里登记过的变量直接可用。这对应逻辑里"假设可以被引用"。

函数（蕴含的引入与消去）

   Γ, x : τ1 ⊢ e : τ2
───────────────────────── (Abs)
Γ ⊢ λ x : τ1 . e : τ1 → τ2


  Γ ⊢ e1 : τ1 → τ2     Γ ⊢ e2 : τ1
────────────────────────────────────── (App)
            Γ ⊢ e1 e2 : τ2

Abs 对应蕴含引入：把假设 x : τ1 临时加入上下文，证完 τ2，得到 τ1 → τ2。App 对应蕴含消去（modus ponens）：有 τ1 → τ2 与 τ1，得 τ2。

积（合取的引入与消去）

  Γ ⊢ e1 : τ1     Γ ⊢ e2 : τ2
─────────────────────────────── (Pair)
   Γ ⊢ (e1, e2) : τ1 × τ2


Γ ⊢ e : τ1 × τ2          Γ ⊢ e : τ1 × τ2
──────────────── (Fst)   ──────────────── (Snd)
 Γ ⊢ fst e : τ1            Γ ⊢ snd e : τ2

构造一对值得到合取的证明，取分量等价于合取消去。

和（析取的引入与消去）

   Γ ⊢ e : τ1                       Γ ⊢ e : τ2
─────────────────── (InL)        ─────────────────── (InR)
Γ ⊢ inl e : τ1 + τ2              Γ ⊢ inr e : τ1 + τ2


  Γ ⊢ e : τ1 + τ2     Γ, x : τ1 ⊢ e1 : τ     Γ, y : τ2 ⊢ e2 : τ
──────────────────────────────────────────────────────────────── (Case)
              Γ ⊢ case e of inl x => e1 | inr y => e2 : τ

注入对应析取引入。case 对应析取消去：对两个分支分别给出推到同一结论 τ 的证明。

单位与空

1
2
3

─────────── (Unit)            Γ ⊢ e : Void
Γ ⊢ () : Unit               ──────────────── (Absurd)
                            Γ ⊢ absurd e : τ

Unit 总能构造（对应 ⊤ 的引入），Void 没有引入规则但有消去规则——如果不小心得到了 Void 的值（即矛盾），可以推出任何 τ。这正是逻辑里的"爆炸原理"（ex falso quodlibet）。

把这九条规则放在一起，就是 STLC 的全部类型系统。

一棵推导树的样子

证明 ((A × B) → C) → A → B → C（柯里化）：

───────────────────────── (Var)
f : (A × B) → C, ... ⊢ f : (A × B) → C

  ───────── (Var)        ───────── (Var)
  ... ⊢ a : A            ... ⊢ b : B
─────────────────────────────── (Pair)
... ⊢ (a, b) : A × B
─────────────────────────────────── (App)
f : (A × B) → C, a : A, b : B ⊢ f (a, b) : C
───────────────────────────────────── (Abs)
f : (A × B) → C, a : A ⊢ λ b : B. f (a, b) : B → C
──────────────────────────────────────────── (Abs)
f : (A × B) → C ⊢ λ a : A. λ b : B. f (a, b) : A → B → C
──────────────────────────────────────────────── (Abs)
∅ ⊢ λ f : (A × B) → C. λ a : A. λ b : B. f (a, b) : ((A × B) → C) → A → B → C

读这棵树需要从下往上看：根节点是"我们想证明的事"，子树是"为了证它需要先证什么"。整棵树的每一步都是机械地匹配规则，没有任何"启发式"成分。

这就是"类型检查 = 证明检查"的实质：检查一段程序是否类型正确，等价于检查上面这样一棵推导树能否被合法构造出来。

STLC 已经能表达哪些命题

直觉主义命题逻辑（IPC）的全部定理在 STLC 里都有对应的良类型项。例如：

命题	STLC 项
`P → P`	`λ x : A. x`
`P → Q → P`	`λ x : A. λ y : B. x`
`(P → Q → R) → (P × Q → R)`	`λ f. λ p. f (fst p) (snd p)`
`(P × Q → R) → (P → Q → R)`	`λ f. λ x. λ y. f (x, y)`
`(P ∨ Q → R) ↔ ((P → R) × (Q → R))`	两个方向都是 case + lambda
`¬(P × ¬P)`	`λ p. snd p (fst p)`，类型 `A × (A → Void) → Void`

反过来，IPC 无法证明的命题在 STLC 里也写不出对应的良类型项：

命题	为什么 STLC 写不出来
`P ∨ ¬P`	给定任意 `A`，没法构造 `A + (A → Void)` 的具体值
`¬¬P → P`	`((A → Void) → Void)` 里没法提取出 `A`
`((P → Q) → P) → P`（皮尔士定律）	同上：通往 `A` 的唯一道路是已经有 `A`

这条对应是双向的，被称为Curry-Howard 对偶：STLC 的良类型项空间与 IPC 的可证明命题空间在结构上一致。这就是为什么 STLC 被叫"最小可证明系统"——再小就连命题逻辑都不能完整覆盖。

STLC 不能表达什么

STLC 是命题逻辑的，没有 ∀、∃ 这类量词。例如：

∀ n : Nat, n + 0 = n 这条等式涉及量词与等价关系，STLC 不能直接说"任意 n"。
∃ n : Nat, n > 5 涉及存在量词与谓词依赖，STLC 也表达不了。

要表达 ∀，需要让函数的返回类型依赖输入——这就跳到依值类型。要表达"对所有类型 α"，需要让类型本身作参数——这就是 System F（多态 lambda 演算）。

系列后续会把这些扩展逐步加上去。STLC 的作用是给读者一个"最小骨架"，方便先把"类型检查 = 证明检查"的机械性看清楚。

强归一化为什么重要

STLC 有一条非平凡的元定理：

强归一化定理：每个 STLC 良类型项在任意求值策略下都能在有限步内规约到一个无法再规约的范式。

证明这条定理需要 Tait 1967 的可归约性方法。直观上：STLC 没有递归算子，函数应用的"展开次数"被类型限定，因此不会出现无穷规约。

强归一化对"类型检查 = 证明检查"很关键：

类型检查里如果出现需要比较两个表达式相等的步骤（例如 (λ x. x + 1) 2 与 3 是否相同），可以把两边归约到范式比较。归一化保证这步总能终止。
一个良类型项可以被求值，且必然在有限步内停下，意味着证明系统不会爆炸：你不能写一条"任何命题都证得了"的循环 trick。

在依值类型系统里强归一化变成"对良类型项归一化"，仍然成立。这也是为什么 Lean 4、Coq、Agda 都把"递归必须良基"作为铁律——一旦允许无穷递归，整个系统就一致性崩塌（参见后续第 09 篇关于可信基底的讨论）。

模式提炼

模式	内容
类型判断三元组	`Γ ⊢ e : τ` 是类型系统的最小单位，包含上下文、表达式、类型
引入 vs 消去	每种类型构造子都成对出现：怎么造它、怎么用它
推导树即证明	一段良类型程序对应一棵机械可构造的推导树
同构是结构性的	IPC 可证 ⟺ STLC 有项；STLC 写不出 ⟺ IPC 无证
归一化保终止	强归一化保证类型检查中所有规约步骤都能在有限时间内停

给读者的练习

写出 (P × Q) → (Q × P) 的 STLC 项，并画出对应推导树。
写出 (P → Q) → (¬Q → ¬P)（逆否律）的 STLC 项。它是直觉主义可证还是必须用古典逻辑？
想清楚：((P → Q) × (Q → P)) → ((Q → R) × (R → Q)) → (P ↔ R) 在 STLC 里怎样写？这条对应工程里的什么模式？
给一个不能写成 STLC 项的命题，并解释你卡在哪一步。

衔接到下一篇

本篇画出了 STLC 的语法、类型规则、推导树形态。下一篇把这套规则用 Python 落地：

把 Γ ⊢ e : τ 写成一个递归函数 check(env, expr, ty) -> bool。
用双向类型检查（synthesis + checking）减轻类型标注负担。
跑几条本篇出现过的定理项，验证类型检查器能机械地"重读"出每一棵推导树。

第 04 篇结束时，“类型检查 = 证明检查"会从"概念对位"变成"一段 200 行 Python 跑出来的事实”。

参考资料

Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002（第 9、11、12 章）.
Robert Harper. Practical Foundations for Programming Languages. Cambridge, 2016.
William A. Howard. The formulae-as-types notion of construction. 1980 (1969 手稿).
Morten Heine Sørensen, Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
Lean 4 文档：https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html