数学基础

类型论

为数学与计算奠基的理论,其中每个项都带有类型,应用于证明辅助系统。

直观每个值都带有标签

在大多数编程语言中, $3$ 是 `int`,`"hello"` 是 `string`——编译器会在程序运行之前就拒绝 `3 + "hello"`。类型论把这个日常想法变成整个数学的基础:不从集合与属于关系( $x \in A$ )出发,而是从项与类型( $t : A$ ," $t$ 具有类型 $A$ ")出发。值得注意的是,一旦类型足够丰富,一个类型就能编码一个数学命题,而该类型的一个项就成为一个证明——程序与证明成了同一种对象。

类型推导表示为一棵树:每个节点是一个判断

\Gamma \vdash t : A

,每条边是把项与其子项相连的类型规则。

大学简单类型化λ演算

定义: 类型判断

类型判断 $\Gamma \vdash t : A$ 表示"在语境 $\Gamma$ (变量-类型对的列表 $x_1:A_1,\dots,x_n:A_n$ )下,项 $t$ 具有类型 $A$ "。核心规则:变量具有语境为其指定的类型;抽象 $\lambda x{:}A.\,t$ 在语境扩充 $x:A$ 后使 $t$ 具有类型 $B$ 时,具有类型 $A\to B$ ;应用 $f\,u$ 在 $f:A\to B$ 且 $u:A$ 时具有类型 $B$ 。

\dfrac{\Gamma, x{:}A \vdash t : B}{\Gamma \vdash \lambda x{:}A.\,t : A\to B} \qquad \dfrac{\Gamma \vdash f : A\to B \quad \Gamma \vdash u : A}{\Gamma \vdash f\,u : B}

马丁-洛夫依赖类型论进一步推广了这一点:函数的结果类型可以依赖于其参数的值。** $\Pi$ 类型**(依赖函数类型) $\prod_{x:A} B(x)$ 收集把每个 $x:A$ 送到类型 $B(x)$ 的项的函数——当 $B$ 不提及 $x$ 时,它退化为普通的 $A\to B$ 。对偶地,** $\Sigma$ 类型**(依赖对类型) $\sum_{x:A} B(x)$ 收集满足 $a:A$ 、 $b:B(a)$ 的对 $\langle a,b\rangle$ ——其第二分量的类型依赖于第一分量;当 $B$ 不提及 $x$ 时,它退化为普通积 $A\times B$ 。

\prod_{x:A} B(x), \qquad \sum_{x:A} B(x)

依赖类型及其Curry–Howard解读
类型构造子	非依赖特殊情形	Curry–Howard解读
$\prod_{x:A} B(x)$	$A\to B$ (当 $B$ 为常量时)	$\forall x{:}A,\ B(x)$
$\sum_{x:A} B(x)$	$A\times B$ (当 $B$ 为常量时)	$\exists x{:}A,\ B(x)$
单值公理: $(A\simeq B) \simeq (A =_{\mathcal U} B)$	—	等价的类型被等同

定理: 简单类型化λ演算的强正规化定理

在简单类型化λ演算中,若 $\Gamma \vdash t : A$ ,则 $t$ 是强正规化的:从 $t$ 出发的每一个 $\beta$ 归约序列都会在有限步内终止。

为什么成立?

这正是简单类型化λ演算尽管有函数应用和类似递归的嵌套,却不是图灵完全的原因——任何良类型的项都不可能永远循环,这正是该片段中的类型检查器总能停机的原因。

证明

(泰特的可归约性方法。)对类型的结构做归纳,为每个类型 $A$ 定义"可归约项"的集合 $\mathrm{RED}_A$ :对基本类型 $o$ ,令 $\mathrm{RED}_o$ 为所有强正规化项组成的集合 $SN$ ;对函数类型,令 $\mathrm{RED}_{A\to B} = \{t : \text{for every } u \in \mathrm{RED}_A,\ t\,u \in \mathrm{RED}_B\}$ 。

首先对 $A$ 做归纳,一并证明三条技术性质:(CR1) $\mathrm{RED}_A$ 中每个项都是强正规化的;(CR2) $\mathrm{RED}_A$ 对 $\beta$ 归约封闭(若 $t\in\mathrm{RED}_A$ 且 $t\to t'$ ,则 $t'\in\mathrm{RED}_A$ );(CR3) 任何"中性"项(变量或应用,而非抽象),若其所有一步归约结果都已在 $\mathrm{RED}_A$ 中,则它本身也在 $\mathrm{RED}_A$ 中。基本情形由 $SN$ 的定义直接得出;函数类型情形展开 $\mathrm{RED}_{A\to B}$ 的定义,并对更小的类型 $A$ 、 $B$ 使用归纳假设。

接着证明,在给自由变量代入可归约项后,每个良类型的项都是可归约的:对 $\Gamma \vdash t:A$ 的类型推导做归纳,若 $\sigma$ 给 $\Gamma$ 中每个变量 $x$ 指派一个项 $\sigma(x)\in\mathrm{RED}_{\Gamma(x)}$ ,则 $t\sigma \in \mathrm{RED}_A$ 。变量情形显然。应用情形直接由 $\mathrm{RED}_{A\to B}$ 的定义得出。抽象情形最需要小心:把 $(\lambda x.\,t)\sigma$ 作用于任意 $u\in\mathrm{RED}_A$ ,该项经一步 $\beta$ 归约为 $t(\sigma,x{:=}u)$ ,由归纳假设(应用于扩充后的代入)可知它属于 $\mathrm{RED}_B$ ;性质(CR3)——对归约结果已全部可归约的项的"展开"封闭性——由此把 $(\lambda x.\,t)\sigma\,u$ 本身也纳入 $\mathrm{RED}_B$ ,于是按定义 $(\lambda x.\,t)\sigma \in \mathrm{RED}_{A\to B}$ 。

最后,把这应用于恒等代入:每个变量 $x{:}A$ 本身就是中性的且完全没有归约结果,故由 (CR3) 它平凡地属于 $\mathrm{RED}_A$ 。于是对任意闭推导 $\Gamma \vdash t:A$ ,取 $\sigma$ 把每个 $x$ 映到自身,得到 $t = t\sigma \in \mathrm{RED}_A$ 。由 (CR1), $\mathrm{RED}_A \subseteq SN$ ,故 $t \in SN$ :每个良类型的项都是强正规化的。 $\blacksquare$

进阶Curry–Howard对应

把 $A\to B$ 读作"若 $A$ 则 $B$ ",把 $A\times B$ 读作" $A$ 且 $B$ ",一个命题的证明就成为对应类型的良类型程序——这就是命题即类型,证明即程序。检验证明归结为对一个项做类型检查;构造证明归结为写出正确类型的程序。

定理: Curry–Howard对应

设 $\varphi$ 是由原子、 $\wedge$ 与 $\to$ 构成的命题公式,设 $A_\varphi$ 是将原子翻译为基本类型、 $\wedge$ 翻译为积 $\times$ 、 $\to$ 翻译为函数类型 $\to$ 所得到的简单类型。那么 $\varphi$ 在直觉主义命题逻辑中可证,当且仅当 $A_\varphi$ 被居留:存在闭项 $t$ 满足 $\vdash t : A_\varphi$ 。

为什么成立?

这正是"证明助手不过是一个类型检查器"这句话背后的精确论断:Coq、Agda、Lean 接受一个定理的机器检验证明,恰恰是在它们接受对应类型的一个项时;而类型检查(不同于一般的定理证明)是一个小巧、快速、机械且高度可信的算法。

证明

(证明变为程序。)对 $\vdash \varphi$ 的自然演绎推导做归纳。若最后一条规则是 $\to$ -引入,由假设 $\psi$ 下 $\chi$ 的子证明推出 $\varphi=\psi\to\chi$ :由归纳假设,该子证明被翻译为项 $t$ ,满足 $x{:}A_\psi \vdash t : A_\chi$ (假设变为自由变量 $x$ );于是 $\lambda x{:}A_\psi.\,t$ 是闭的,且类型为 $A_\psi\to A_\chi=A_\varphi$ 。若最后一条规则是由 $\psi\to\chi$ 与 $\psi$ 得到的 $\to$ -消去(分离规则):由归纳假设得到项 $t_1 : A_\psi\to A_\chi$ 与 $t_2 : A_\psi$ ;于是 $t_1\,t_2 : A_\chi$ 。 $\wedge$ -引入与 $\wedge$ -消去规则对称地翻译为配对 $\langle t_1,t_2\rangle$ 与两个投影。证明系统的每条规则都有对应的项构造规则,因此对推导做归纳就能产生类型为 $A_\varphi$ 的良类型闭项。

(程序变为证明。)反过来,对类型推导 $\vdash t : A$ 做归纳。每条类型规则——变量、抽象、应用、配对、投影——与某条自然演绎规则——假设、 $\to$ -引入、 $\to$ -消去、 $\wedge$ -引入、 $\wedge$ -消去——具有完全相同的树形结构。于是取同一棵推导树,擦除所有项,并把每个类型读作它所翻译自的公式:这恰好就是 $\varphi$ 的一个合法的直觉主义证明(其中 $A=A_\varphi$ )。

由于这两个翻译(证明 $\to$ 项,以及项 $\to$ 证明)在推导树上互为结构逆——一个逐规则地精确撤销另一个所做的—— $\varphi$ 可证恰好当 $A_\varphi$ 被居留时成立。 $\blacksquare$

大学实际应用与典型例题

丰富的类型系统能在程序运行之前捕获整整一类错误:Rust 的所有权类型在编译期防止释放后使用和数据竞争,依赖类型语言能把"这个列表恰有 $n$ 个元素"或"这个下标在范围内"之类的不变量直接编码进类型,使某些运行时错误变得不可表示。最深层的应用就在证明助手内部:Coq、Agda、Lean 都拥有一个小巧、经过仔细审计的内核,只做一件事——对项做类型检查——由于 Curry–Howard 对应,接受一个定理类型的项就是接受一个经机器检验的证明,因此信任一个像费特-汤普森定理或四色定理那样规模的数学结果,就归结为信任区区几百行类型检查代码,而不是构建证明项所用的(规模大得多、审计难得多的)策略代码。

例题: 普通函数类型无法表达的 $\Pi$ 类型

设 $\mathrm{Vec}\,A\,n$ 为元素类型为 $A$ 的长度为 $n$ 的列表类型。写出一个居留 $\prod_{n:\mathbb N} (\mathrm{Vec}\,A\,n \to \mathrm{Vec}\,A\,n)$ 的项——"对每个长度 $n$ ,给出长度为 $n$ 的向量上的一个函数"——并解释为何简单类型(没有 $\Pi$ )完全无法表达这个规范。

解答

项 $\lambda n{:}\mathbb N.\,\lambda v{:}\mathrm{Vec}\,A\,n.\,v$ 是可行的:对每个自然数 $n$ ,它接受一个长度为 $n$ 的向量 $v$ 并原样返回——显然是良类型的,因为无论提供哪个 $n$ , $v : \mathrm{Vec}\,A\,n$ 都以类型 $\mathrm{Vec}\,A\,n$ 被返回。

使这成为 $\Pi$ 的真正应用而非普通函数类型的原因在于,第二个参数的类型( $\mathrm{Vec}\,A\,n$ )提及了第一个参数( $n$ )的值。在简单类型化λ演算中,函数的参数类型与结果类型一旦确定便永远固定—— $A\to B$ 中的 $A,B$ 在知道类型 $A$ 的任何具体值之前就已选定。无法只用 $\to$ 写出"给我一个自然数 $n$ ,并根据你给的数,我将要求恰好那个长度的向量":你需要某个单一的固定类型 $\mathrm{Vec}\,A\,n$ 同时适用于所有 $n$ ,而这并不是 $\mathrm{Vec}$ 的含义。

具体来说,若尝试用普通函数类型来写,最多只能得到针对某个固定占位长度的 $\mathbb N \to (\mathrm{Vec}\,A\,? \to \mathrm{Vec}\,A\,?)$ ——毫无用处,因为它会拒绝任何其他长度的向量,或者接受长度错误的向量。 $\Pi$ 类型 $\prod_{n:\mathbb N}(\cdots)$ 正是能让值域"回头看"所收到的 $n$ 的具体值的类型构造子,这正是简单类型无法表达的那种依赖性。

例题: 函数复合的Curry–Howard对应

公式 $(A\to B)\to((B\to C)\to(A\to C))$ 表达了蕴含的传递性。根据Curry–Howard,找出证明它的 $\lambda$ 项,并逐步验证其类型推导。

解答

该项为 $t = \lambda f{:}A\to B.\,\lambda g{:}B\to C.\,\lambda x{:}A.\,g\,(f\,x)$ ——正是作用于 $x$ 的函数复合 $g\circ f$ 。

从内到外推导类型。在语境 $f{:}A\to B,\,g{:}B\to C,\,x{:}A$ 中:由于 $f:A\to B$ 且 $x:A$ ,应用得 $f\,x:B$ 。由于 $g:B\to C$ 且 $f\,x:B$ ,应用得 $g\,(f\,x):C$ 。

现在从内到外解除各抽象。 $\lambda x{:}A.\,g\,(f\,x)$ 在语境 $f{:}A\to B,\,g{:}B\to C$ 下具有类型 $A\to C$ 。接着 $\lambda g{:}B\to C.\,(\cdots)$ 在语境 $f{:}A\to B$ 下具有类型 $(B\to C)\to(A\to C)$ 。最后 $\lambda f{:}A\to B.\,(\cdots)$ 不再有任何自由假设,具有类型 $(A\to B)\to((B\to C)\to(A\to C))$ ——一个闭项。

于是 $\vdash t : (A\to B)\to((B\to C)\to(A\to C))$ ,即 $t$ 是传递性的一个Curry–Howard证明:"若 $A$ 蕴含 $B$ ,且 $B$ 蕴含 $C$ ,则 $A$ 蕴含 $C$ "——这与函数式程序员为复合两个函数所写的项完全相同。

研究当前研究

研究前沿截至 2026 年

同伦类型论与沃沃斯基的单值基础项目仍在继续发展,作为与ZFC集合论并行(而非取代)的数学候选基础;立方类型论(大致从2015年起)通过直接从一个区间类型构造类型的相等性,为单值公理赋予了真正的计算内容——这是一个长期悬而未决的问题——截至2026年,这一计算处理方式仍在不断精化并扩展到更丰富的类型构造子。大规模形式化工作正在展示类型论作为实用数学基础设施的力量:基于Lean的`mathlib`库已成长为最大的形式化数学库之一,Peter Scholze与Dustin Clausen在2020—2022年的"液体张量实验"用Lean形式验证了凝聚数学中的一个困难定理,而(包括由Kevin Buzzard主导的)社区努力,致力于完整形式化费马大定理,截至2020年代中期仍然活跃。另外,关于高阶归纳类型与综合同伦论(在类型论内部直接计算球面的同伦群)的研究,以及在不牺牲可判定类型检查的前提下增强依赖类型论以支持更多常规数学实践的研究,也在持续进行。

在简单类型化λ演算中,若 $f : A \to B$ 且 $a : A$ ,那么 $f\,a$ 的类型是什么?

像Coq、Agda、Lean这样的证明助手,为何能信任一个长达数千行、经机器检验的证明?

当 $B(x)$ 实际上不依赖于 $x$ 时, $\prod_{x:A} B(x)$ 退化为什么?

单值公理 $(A\simeq B) \simeq (A =_{\mathcal U} B)$ 表明……

参考文献

The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics
Wikipedia contributors (2024). Curry–Howard correspondence
Wikipedia contributors (2024). Intuitionistic type theory