类型论——从简单类型到依赖类型

上级：logic

给 λ 演算 加上类型，再通过 Curry–Howard 对应，就得到一个逻辑——而如果让类型依赖于值，就得到整个数学的一个基础。

简单类型 λ 演算（STLC）

类型 = 基本类型 + 箭头类型 A → B。关键事实：STLC 是强正规化的——每一个项都会终止。你因此失去图灵完备性，换来一致性：作为一个逻辑（Curry–Howard 对应），STLC 就是直觉主义命题逻辑。完全性 ⟺ 一致性，这正是反复出现的那道阈值——引入一般递归就会重新带来 ⊥。

λ 立方体（Barendregt）——三种增加表达力的方式

• 项依赖于类型 → 多态性（System F：∀α. α→α）；
• 类型依赖于类型 → 类型算子；
• 类型依赖于项 → 依赖类型。 三者合一，就是构造演算（Calculus of Constructions, CoC）——立方体那个最远的角，也是 Lean/Coq 的核心。

（STLC 在最近的角；每一条轴增加一种依赖关系；CoC 在最远的角，同时拥有全部三种依赖。）

依赖类型——由值索引的类型

Vec A n = 长度为 n 的 A 列表；Π(x:A). B x = 一个返回类型依赖于参数的函数；Σ(x:A). B x = 一对值，其第二个的类型依赖于第一个。由 Curry–Howard 对应，Π = ∀，Σ = ∃，所以一个类型可以表达任意命题，而该类型的一个项就是这个命题的证明。

Martin-Löf 类型论（MLTT）

一种构造性的数学基础：依赖类型 + 归纳类型（构造出 ℕ、列表、树）+ 同一性类型（a = b 本身就是一个类型——把"相等"当作一个待证明的命题）+ 一个宇宙层级（Type 0 : Type 1 : …，避免罗素式悖论）。它是集合论的一个替代方案——因其构造方式而天然可计算（证明是可以运行的）。

这笔权衡

一个完全的类型论（所有项都会终止）是一个一致的逻辑，但不是图灵完备的；允许不终止能换来一般递归，代价是一致性。证明助手在证明层保留完全性，把偏函数隔离到别处沙盒运行。→ proof-theory, lean4。