Pure Type System 教程：从基础到进阶

本教程基于学习笔记整理而成，旨在为读者提供一个从基础到进阶的 Pure Type System 学习路径。

第一章引言与动机

1.1 什么是 Pure Type System？

Pure Type System（PTS）是一种用于定义依赖类型 λ 演算的通用框架。它之所以被称为"Pure"（纯粹），是因为其语法和推导规则非常简洁统一：

所有东西（项、类型、种类、命题）都是"项"（term）
类型关系仅由少数几条抽象和应用规则来定义

这种统一性使得 PTS 成为一个极其简洁而强大的框架。

1.2 为什么需要 PTS？

在计算机科学和数理逻辑的发展过程中，我们遇到了各种各样的类型系统：

简单类型 λ 演算：用于命题逻辑
System F（多态 λ 演算）：用于参数多态
依赖类型系统：类型可以依赖于值
构造演算（CoC）：统一逻辑与计算

这些系统看起来各不相同，但实际上它们有着共同的结构。PTS 的目标就是：

统一框架：提供一个统一的框架来定义和研究这些类型系统
模块化分析：清晰地分析不同类型系统的表达能力
形式化基础：为复杂的类型系统（如 CoC/CIC）提供简洁、形式化的基础定义

1.3 从一个简单例子开始

让我们从一个最简单的类型系统开始，逐步理解 PTS 的思想。

在简单类型 λ 演算中，我们有一些基础类型（如 Nat、Bool）和函数类型构造器 →：

text

类型 τ ::= Nat | Bool | τ → τ
项  e ::= x | λx:τ. e | e e

这对应于命题逻辑：类型 A → B 对应命题"A 蕴含 B"。

现在，如果我们想要：

多态：让类型可以依赖于类型（如 List<T> 中的 T）
依赖类型：让类型依赖于值（如 Vector n 表示长度为 n 的向量）

我们需要一种更灵活的类型构造方式。这正是 PTS 要解决的问题。

1.4 学习路线图

text

λ-演算基础
     ↓
简单类型 λ-演算 (λ→)
     ↓
Pure Type System (PTS) 框架
     ↓
┌────┴────┐
↓         ↓
λ-Cube   依赖类型
     ↓
构造演算 (CoC)
     ↓
归纳构造演算 (CIC)
     ↓
证明助理 (Coq, Lean)

第二章 PTS 核心定义

2.1 三元组定义

一个 PTS 由三元组 $(\mathcal{S}, \mathcal{A}, \mathcal{R})$ 唯一定义：

$\mathcal{S}$ (Sorts) - 宇宙/种类

一组特殊的常量，称为"宇宙"（universe）或"种类"（sort）。它们是类型的类型，构成了类型的层级。

例子：

在 CoC 中：$\mathcal{S} = {*, \square}$
- $*$ 通常代表命题宇宙 Prop
- $\square$ 代表类型宇宙 Type
在 CIC 中：$\mathcal{S} = {Prop} \cup {Type_i}_{i \in \mathbb{N}}$
- 有无限层级：Prop, Type₀, Type₁, ...

$\mathcal{A}$ (Axioms) - 公理

一组形如 $s_1 : s_2$ 的公理，其中 $s_1, s_2 \in \mathcal{S}$。它规定了宇宙之间的层级关系。

例子：

${* : \square}$ 表示"命题是一种类型"
在 CIC 中：Prop : Type₀ : Type₁ : Type₂ : ...

$\mathcal{R}$ (Rules) - 规则

一组形如 $(s_1, s_2, s_3)$ 的规则，其中 $s_1, s_2, s_3 \in \mathcal{S}$。它规定了在哪个宇宙中可以形成依赖乘积类型，以及这个乘积类型本身属于哪个宇宙。

理解规则 $(s_1, s_2, s_3)$：

如果 $A$ 属于宇宙 $s_1$
并且在假设 $x:A$ 下 $B$ 属于宇宙 $s_2$
那么依赖乘积类型 $\Pi x:A. B$ 就属于宇宙 $s_3$

2.2 语法

在 PTS 中，所有东西——无论是变量、函数、类型，还是类型本身的类型（Sort）——都是用同一种语法定义的，统称为项 (Term)。

$$ \mathcal{T} ::= \mathcal{S} \ | \ \mathcal{V} \ | \ \Pi \mathcal{V} : \mathcal{T} . \mathcal{T} \ | \ \lambda \mathcal{V} : \mathcal{T} . \mathcal{T} \ | \ \mathcal{T}\ \mathcal{T} $$

让我们逐一解释这五种构造：

构造	语法	含义
种类	$\mathcal{S}$	宇宙常量，如 $*$（Prop）、$\square$（Type）
变量	$\mathcal{V}$	可变标识符，如 $x, y, A, B$
依赖乘积	$\Pi x:A. B$	依赖函数类型，当 $B$ 不依赖 $x$ 时退化为 $A \to B$
抽象	$\lambda x:A. t$	函数定义，引入参数 $x$
应用	$t\ u$	函数调用

2.3 依赖乘积类型详解

依赖乘积类型 $\Pi x:A. B(x)$ 是 PTS 中唯一的"箭头"或"函数"类型构造器。它是简单函数类型 $A \to B$ 的泛化。

从简单函数到依赖函数

简单函数类型：$A \to B$

对于任意输入 $a: A$，函数都返回一个相同类型 $B$ 的值
例子：length : List Int -> Nat，无论输入什么列表，都返回一个自然数

依赖函数类型：$\Pi x:A. B(x)$

对于每个特定的输入 $a: A$，函数返回一个特定类型 $B(a)$ 的值
返回类型 $B$ 是输入值 $x$ 的一个函数
例子：head : Π (n: Nat) (v: Vector A (S n)), A

逻辑对应

在 Curry-Howard 对应下：

$\Pi x:A. B(x)$ 对应逻辑中的全称量化：$\forall x \in A, B(x)$
一个类型为 $\Pi x:A. B(x)$ 的项（程序）$f$，就是一个构造性证明，证明对于所有 $x:A$，命题 $B(x)$ 都成立

具体例子

假设我们有：

Nat：自然数类型
Even(n)：依赖于 n: Nat 的命题，表示"n 是偶数"

考虑类型：

text

Π (n: Nat), Even(n) -> Even(n+2)

解读：

输入：一个自然数 n 和一个"n 是偶数"的证明
输出：一个"n+2 是偶数"的证明
逻辑含义：$\forall n \in \mathbb{N}, (\text{Even}(n) \to \text{Even}(n+2))$

2.4 推导规则

PTS 的推导规则基于上下文 $\Gamma$，它是一系列变量及其类型的声明序列（如 $x_1:A_1, x_2:A_2, ...$）。

七条核心规则

1. 排序公理 (Axiom)

$$\frac{}{\vdash s_1 : s_2} \quad \text{如果 } (s_1, s_2) \in \mathcal{A}$$

这是类型系统的起点。例如，从 ${* : \square} \in \mathcal{A}$，我们可以推导出 $\vdash * : \square$。

2. 变量声明 (Start)

$$\frac{\Gamma \vdash A : s}{\Gamma, x:A \vdash x : A} \quad \text{如果 } x \text{ 不在 } \Gamma \text{ 中}$$

这允许我们在上下文中引入新变量。

3. 弱化规则 (Weakening)

$$\frac{\Gamma \vdash A : B \quad \Gamma \vdash C : s}{\Gamma, x:C \vdash A : B}$$

确保上下文扩展的有效性。

4. 乘积形成规则 (Product / Π-formation) ⭐核心

$$\frac{\Gamma \vdash A : s_1 \quad \Gamma, x:A \vdash B : s_2}{\Gamma \vdash (\Pi x:A. B) : s_3} \quad \text{如果 } (s_1, s_2, s_3) \in \mathcal{R}$$

这是 PTS 的核心规则，引入依赖乘积类型。

5. 抽象规则 (Abstraction / λ-formation)

$$\frac{\Gamma, x:A \vdash t : B \quad \Gamma \vdash (\Pi x:A. B) : s}{\Gamma \vdash (\lambda x:A. t) : (\Pi x:A. B)}$$

构造函数。如果 $t$ 在假设 $x:A$ 下具有类型 $B$，那么 $\lambda x:A. t$ 就具有类型 $\Pi x:A. B$。

6. 应用规则 (Application)

$$\frac{\Gamma \vdash t : (\Pi x:A. B) \quad \Gamma \vdash u : A}{\Gamma \vdash t\ u : B[x := u]}$$

函数调用。将函数 $t$ 应用于参数 $u$，结果的类型是 $B$ 中所有 $x$ 替换为 $u$。

7. 转换规则 (Conversion)

$$\frac{\Gamma \vdash t : A \quad \Gamma \vdash B : s \quad A =_\beta B}{\Gamma \vdash t : B}$$

如果两个项在 $\beta$-规约下等价，则它们的类型可以互换。

2.5 类型判断的含义

在 PTS 中，"项"是一个统一的概念：

当项被...	它是...
赋予一个类型时	程序或证明
用作其他项的类型时	类型或命题
用作类型的类型时	种类 (Sort)

这种统一性是理解 PTS 的关键。

2.6 PTS 实例化示例

通过选择不同的 $(\mathcal{S}, \mathcal{A}, \mathcal{R})$，我们可以得到不同的类型系统：

简单类型 λ 演算 (λ→)

$$\mathcal{S} = {}$$ $$\mathcal{A} = \emptyset$$ $$\mathcal{R} = {(, *, *)}$$

只允许形成命题（类型）之间的函数类型，对应命题逻辑。

System F (λ2)

$$\mathcal{S} = {, \square}$$ $$\mathcal{A} = { : \square}$$ $$\mathcal{R} = {(*, *, *), (\square, *, *)}$$

允许对类型变量进行全称量化，支持参数多态。

构造演算 (CoC)

$$\mathcal{S} = {, \square}$$ $$\mathcal{A} = { : \square}$$ $$\mathcal{R} = {(*, *, *), (\square, *, ), (, \square, \square), (\square, \square, \square)}$$

包含了所有可能的规则，允许所有形式的依赖。

第三章 λ-Cube 类型系统谱系

3.1 什么是 λ-Cube？

λ-Cube 是一个由 8 个 PTS 组成的立方体，它们共享相同的基础集合和公理，但通过不同的规则集来区分：

$$\mathcal{S} = {, \square}$$ $$\mathcal{A} = { : \square}$$

每个系统都代表了在简单类型 λ 演算基础上增加不同"维度"的依赖关系。

3.2 三个维度的依赖

立方体的三个轴分别代表三种不同的依赖关系：

轴	依赖方向	含义	对应特性
x 轴	类型依赖项	类型可以依赖于值	谓词逻辑
y 轴	类型依赖类型	类型可以依赖于类型	多态性
z 轴	项依赖类型	项可以依赖于类型	高阶类型

3.3 八个系统详解

1. λ→ (Simply Typed Lambda Calculus) - 简单类型 λ 演算

位置：立方体原点 (0,0,0)
规则集 $\mathcal{R}$: ${(*, *, *)}$
描述：最基础的系统
能力：只能表达命题逻辑的证明
对应逻辑：直觉主义命题逻辑

示例：

coq

(* 命题 A → A 的证明 *)
fun (A : Prop) (a : A) => a

2. λ2 (System F) - 二阶多态 λ 演算

位置：y 轴顶端 (0,1,0)
规则集 $\mathcal{R}$: ${(*, *, *), (\square, *, *)}$
新增规则：$(\square, *, *)$
能力：引入参数多态性
对应逻辑：二阶命题逻辑

新增规则的理解：

$(\square, *, *)$ 允许形成 $\Pi X:\square. P$ 这样的类型
其中 $X$ 是类型变量，$P:*$ 是命题
这对应于对类型变量进行全称量化

示例：

coq

(* 多态恒等函数 *)
fun (X : Type) (x : X) => x
(* 类型：∀ X : Type. X → X *)

3. λP (LF - Logical Framework) - 依赖类型

位置：x 轴顶端 (1,0,0)
规则集 $\mathcal{R}$: ${(*, *, ), (, \square, \square)}$
新增规则：$(*, \square, \square)$
能力：引入依赖类型
对应逻辑：一阶谓词逻辑

示例：

coq

(* 依赖类型：向量的长度在类型中 *)
Inductive Vector (A : Type) : Nat -> Type :=
| vnil : Vector A O
| vcons : forall n, A -> Vector A n -> Vector A (S n).

4. λω (System Fω) - 高阶类型

位置：z 轴顶端 (0,0,1)
规则集 $\mathcal{R}$: ${(*, *, *), (\square, \square, \square)}$
新增规则：$(\square, \square, \square)$
能力：引入类型构造子
对应逻辑：弱高阶命题逻辑

示例：

coq

(* 类型构造子 *)
Definition List : Type -> Type := ...
Definition Tree : Type -> Type := ...

5. λP2 (System FP) - 多态依赖类型

位置：x-y 平面右上角 (1,1,0)
规则集 $\mathcal{R}$: ${(*, *, *), (\square, *, ), (, \square, \square)}$
描述：结合了 λ2（多态）和 λP（依赖类型）
能力：既可以对类型进行量化，又可以让类型依赖于项
对应逻辑：二阶谓词逻辑

6. λPω (Dependent Fω) - 依赖高阶类型

位置：x-z 平面右上角 (1,0,1)
规则集 $\mathcal{R}$: ${(*, *, ), (, \square, \square), (\square, \square, \square)}$
描述：结合了 λP（依赖类型）和 λω（高阶类型）
能力：类型可以依赖于项，并且可以操作高阶类型构造子

7. λω (Full) - 高阶多态

位置：y-z 平面右上角 (0,1,1)
规则集 $\mathcal{R}$: ${(*, *, *), (\square, *, *), (\square, \square, \square)}$
描述：结合了 λ2（多态）和 λω（高阶类型）
能力：完整的 System Fω，支持高阶多态
对应逻辑：高阶命题逻辑

8. λC (CoC) - 构造演算 ⭐

位置：立方体最远的顶点 (1,1,1)
规则集 $\mathcal{R}$: ${(*, *, *), (\square, *, ), (, \square, \square), (\square, \square, \square)}$
描述：包含了所有可能的规则
能力：表达能力最强的系统
对应逻辑：高阶谓词逻辑（构造性）
重要性：这是 Coq 证明助理早期版本的核心演算

3.4 规则详解

让我们理解 CoC 中的四条规则：

规则	含义	示例
$(, , *)$	命题间的蕴含	$Prop \to Prop$
$(\square, , )$	从类型到命题的量化	$\forall (x:Type), P(x)$（多态命题）
$(*, \square, \square)$	从命题到类型的函数	依赖命题的类型
$(\square, \square, \square)$	类型构造子	高阶类型

3.5 总结表格

系统	坐标	关键规则	核心能力	对应逻辑
λ→	(0,0,0)	$(, , *)$	简单函数类型	命题逻辑
λ2	(0,1,0)	$(\square, , )$	参数多态	二阶命题逻辑
λP	(1,0,0)	$(*, \square, \square)$	依赖类型	一阶谓词逻辑
λω	(0,0,1)	$(\square, \square, \square)$	高阶类型	弱高阶逻辑
λP2	(1,1,0)	$(\square, , ), (*, \square, \square)$	多态依赖类型	二阶谓词逻辑
λPω	(1,0,1)	$(*, \square, \square), (\square, \square, \square)$	依赖高阶类型	—
λω	(0,1,1)	$(\square, , ), (\square, \square, \square)$	高阶多态	高阶命题逻辑
λC (CoC)	(1,1,1)	全部规则	全依赖，统一逻辑与计算	高阶谓词逻辑

3.6 λ-Cube 的意义

λ-Cube 清晰地展示了类型系统如何通过逐步增加不同维度的"依赖"能力，从一个简单的逻辑系统（λ→）演进为一个足以作为数学基础（λC/CoC）的强大系统。

理解 λ-Cube 是理解现代依赖类型理论和证明助理（如 Coq, Lean）理论根基的关键一步。

第四章构造演算 CoC

4.1 什么是构造演算？

Calculus of Constructions (CoC)，即构造演算，是由 Thierry Coquand 在 1985 年提出的一种高阶依赖类型 λ 演算系统。它是：

λ-Cube 中表达能力最强的系统
CIC（归纳构造演算）的前身和理论基础
统一了程序、数学命题和证明的表达

4.2 CoC 的核心组件

语法

CoC 使用极简语法定义项（terms）：

coq

𝒯 ::= 𝒮       (宇宙/Sorts)
    | 𝒱       (变量)
    | Π𝒱:𝒯.𝒯  (依赖乘积类型)
    | λ𝒱:𝒯.𝒯  (函数抽象)
    | 𝒯 𝒯     (函数应用)

核心组成部分

组件	描述	逻辑对应	编程对应
依赖乘积类型 `Πx:A. B`	当 `B` 不依赖 `x` 时：`A → B`；当 `B` 依赖 `x` 时：依赖函数	全称量化 `∀x:A, B(x)`	泛型函数
宇宙层级 `𝒮 = {Prop} ∪ {Type_i}`	`Prop`: 命题宇宙；`Type_i`: 数据类型宇宙；层级：`Prop : Type₀ : Type₁ : ...`	避免罗素悖论	类型分类
Curry-Howard 同构	命题 `P` ↔ 类型 `P`；证明 `p` ↔ 程序项 `p`	证明即构造	程序即证明

4.3 逻辑表达能力

CoC 可直接编码高阶逻辑：

coq

⊥ := ΠP:Prop. P                       (假)
⊤ := ΠP:Prop. P→P                     (真)
A ∧ B := ΠC:Prop. (A→B→C)→C           (合取)
A ∨ B := ΠC:Prop. (A→C)→(B→C)→C       (析取)
∀x:A.P := Πx:A. P                     (全称量化)
∃x:A.P := ΠC:Prop. (Πx:A. P→C)→C     (存在量化)

这些编码展示了 CoC 的强大表达能力。

4.4 计算规则

β-规约

$$(\lambda x:A. t)\ u \rightarrow_\beta t[x:=u]$$

这是 λ 演算的基本计算规则。

类型推导示例

coq

Γ ⊢ A : s    Γ, x:A ⊢ B : s'
---------------------------- (s,s') ∈ R
Γ ⊢ Πx:A.B : s'

4.5 CoC 的局限性

1. 缺乏原生归纳类型

需用高阶编码表示数据结构（如自然数、链表），导致代码冗长。

Church 编码的自然数：

coq

Nat := ΠT:Type. T → (T→T) → T
O := λT. λz:T. λs:T→T. z
S := λn:Nat. λT. λz:T. λs:T→T. s (n T z s)

2. 证明复杂性高

归纳证明需手动实现归纳原理：

coq

NatInd := λP:Nat→Prop.
          P O →
          (∀n:Nat. P n → P (S n)) →
          ∀n:Nat. P n

3. 终止性无保证

允许非终止递归（如 ω := λx. x x），可能破坏逻辑一致性。

4.6 与 CIC 的关键区别

特性	CoC	CIC
归纳类型	❌ 不支持	✅ 核心特性
递归函数	有限支持	✅ 结构递归
归纳证明	需手动编码	✅ 自动生成归纳原理
终止性保证	弱	✅ 强（结构递归）

4.7 历史意义

理论奠基：为 CIC 提供核心框架（依赖类型 + Curry-Howard）
影响系统：Coq 早期版本直接基于 CoC
形式验证：用于研究类型系统元理论（如一致性证明）

第五章归纳构造演算 CIC

5.1 什么是 CIC？

CIC（Calculus of Inductive Constructions），即归纳构造演算，是 CoC 的扩展，增加了归纳类型作为核心特性。它是：

现代交互式定理证明器（如 Coq、Lean）的理论基础
统一了程序构造、数学证明和类型系统
能够自然地定义递归数据结构和进行归纳证明

核心公式：$$CIC = CoC + Inductive Types$$

5.2 CIC 的核心组成

组成部分	描述	作用
λ-演算与依赖类型	支持依赖函数类型 `Πx:A. B(x)`	统一函数、类型和逻辑命题
归纳类型 (Inductive Types)	通过构造子递归定义数据类型	提供结构化数据和归纳证明能力
Curry-Howard 同构	命题 ↔ 类型，证明 ↔ 程序	逻辑推理可计算化
类型层级 (Sorts)	`Prop`（命题）、`Type₀`（数据类型）、`Type₁`（更高阶类型）	避免逻辑悖论

5.3 归纳类型详解

这是 CIC 超越 CoC 的关键特性，允许递归定义数据类型和逻辑谓词。

基本语法

coq

Inductive T : Type :=
| c₁ : A₁ → T   (* 构造子 1 *)
| c₂ : A₂ → T   (* 构造子 2 *)
...

经典示例

自然数（Nat）

coq

Inductive Nat : Type :=
| O : Nat          (* 零 *)
| S : Nat → Nat.   (* 后继函数 *)

自动生成的归纳原理：

coq

Nat_ind : ∀P : Nat → Prop,
  P O →
  (∀n : Nat, P n → P (S n)) →
  ∀n : Nat, P n

这正是数学归纳法！

链表（List）

coq

Inductive List (A : Type) : Type :=
| nil : List A
| cons : A → List A → List A.

逻辑谓词（Even）

coq

Inductive Even : Nat → Prop :=
| Even_O : Even O
| Even_SS : ∀n, Even n → Even (S (S n)).

5.4 依赖类型示例

coq

Inductive Vector (A : Type) : Nat → Type :=
| vnil : Vector A O
| vcons : ∀n, A → Vector A n → Vector A (S n).

Vector A n：长度为 n 的向量（依赖 n 的具体值）

5.5 递归函数

coq

Fixpoint plus (n m : Nat) : Nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)  (* 递归调用在更小的 n' 上 *)
  end.

终止性检查：Coq 会检查递归调用只在严格子项上进行。

5.6 命题即类型，证明即程序

coq

Theorem plus_assoc : ∀a b c, plus a (plus b c) = plus (plus a b) c.
Proof.
  intros a b c.
  induction a as [|a' IH].  (* 对 a 归纳 *)
  - simpl. reflexivity.      (* 情况 a = O *)
  - simpl. rewrite IH. reflexivity. (* 情况 a = S a' *)
Qed.

这个证明过程，在底层实际上是在构造一个 λ 项。

5.7 类型层级

为避免罗素悖论，CIC 采用层级化的宇宙：

Prop：命题宇宙（证明可擦除）
Type₀（或 Set）：小数据类型（如 Nat、Bool）
Type₁、Type₂...：更高阶类型

coq

Check Nat.     (* Nat : Type₀ *)
Check Type₀.   (* Type₀ : Type₁ *)
Check Prop.    (* Prop : Type₀ *)

5.8 CIC 的计算规则

β-规约

$$(\lambda x. t)\ u \rightarrow_\beta t[x:=u]$$

函数应用。

ι-规约

模式匹配/递归展开：

coq

plus (S O) (S O) → S (plus O (S O)) → S (S O)

强规范性

所有良类型项均可规约到唯一正规形式，这保证了逻辑的一致性。

5.9 完整示例

coq

(* 1. 定义依赖类型：长度索引的向量 *)
Inductive Vector (A : Type) : Nat → Type :=
| vnil : Vector A O
| vcons : ∀n : Nat, A → Vector A n → Vector A (S n).

(* 2. 定义依赖函数：向量连接 *)
Fixpoint vappend {A : Type} {n m : Nat}
         (v1 : Vector A n) (v2 : Vector A m) : Vector A (plus n m) :=
  match v1 with
  | vnil => v2
  | vcons n' x v1' => vcons (plus n' m) x (vappend v1' v2)
  end.

(* 3. 证明性质：连接的长度正确 *)
Theorem vappend_length :
  ∀(A : Type) (n m : Nat) (v1 : Vector A n) (v2 : Vector A m),
    let v3 := vappend v1 v2 in
    length v3 = plus n m.
Proof.
  intros A n m v1 v2.
  induction v1 as [| n' x v1' IH].
  - simpl. reflexivity.  (* v1 = vnil *)
  - simpl. f_equal. apply IH.  (* v1 = vcons ... *)
Qed.

这个例子展示了：

依赖归纳类型：Vector A n 的类型依赖于值 n
依赖函数：vappend 的返回类型依赖于输入值
归纳证明：对向量的结构进行归纳
Curry-Howard：证明就是构造一个特定类型的程序

5.10 CIC 的意义与应用

形式化数学：四色定理、费马大定理的部分证明已在 Coq 中形式化
程序验证：证明程序满足规范（如操作系统内核、加密算法）
编程语言设计：Agda、Idris 等依赖类型语言受 CIC 启发
现代证明助理的核心：Coq、Lean、Agda 的内核都是 CIC 或其变体

第六章 Curry-Howard 同构

6.1 什么是 Curry-Howard 同构？

Curry-Howard 同构是连接逻辑学与计算机科学的桥梁，揭示了逻辑系统中的"证明"与计算系统中的"程序"在结构上是完全相同的。

它建立了直觉主义逻辑与类型化 λ 演算之间的一一对应。

6.2 核心对应关系

逻辑侧 (Logic)	程序侧 (Programming)	解释
命题 (Proposition)	类型 (Type)	一个待证的逻辑公式，对应一个待构造的程序类型
证明 (Proof)	程序项/项 (Term)	对该命题的证明过程，对应一个具有该类型的程序
命题为真	类型可居 (Inhabited)	命题存在证明，等价于该类型存在一个项
蕴含 (Implication, $A \to B$)	函数类型 (Function Type, $A \to B$)	从 $A$ 推出 $B$ 的证明，对应一个从类型 $A$ 到类型 $B$ 的函数
合取 (Conjunction, $A \land B$)	积类型 (Product Type, $A \times B$)	同时证明 $A$ 和 $B$，对应一个包含 $A$ 和 $B$ 的二元组
析取 (Disjunction, $A \lor B$)	和类型 (Sum Type, $A + B$)	证明 $A$ 或 $B$，对应一个要么是 $A$ 要么是 $B$ 的标签联合体
全称量词 (Universal, $\forall x \in X. P(x)$)	依赖乘积类型 (Dependent Product, $\Pi x:X. P(x)$)	对集合 $X$ 中所有 $x$ 都证明 $P(x)$
存在量词 (Existential, $\exists x \in X. P(x)$)	依赖和类型 (Dependent Sum, $\Sigma x:X. P(x)$)	找到某个 $x$ 并证明 $P(x)$
真 ($\top$)	单元类型 (Unit Type, `()`)	无需前提的平凡真理
假 ($\bot$)	空类型 (Empty Type, `Void`)	无法证明的矛盾

6.3 如何理解"证明即程序"？

这是最精妙的部分。让我们通过一个具体例子来理解。

逻辑规则：蕴含引入

在自然演绎中，要证明 $A \to B$，我们可以：

假设 $A$ 成立（作为临时前提）
基于这个假设，推导出 $B$ 成立
因此，我们得到了 $A \to B$ 的证明

用推导树表示：

$$ \frac{ \begin{array}{c} [A] \ \vdots \ B \end{array} }{A \to B} $$

程序对应：函数抽象

在 λ 演算中，要构造一个类型为 $A \to B$ 的项，我们可以：

引入一个类型为 $A$ 的形式参数 $x$
在函数体中使用这个参数 $x$ 来构造一个类型为 $B$ 的表达式
得到一个函数 $\lambda x: A. t$

用类型判断表示：

$$ \frac{\Gamma, x:A \vdash t : B}{\Gamma \vdash (\lambda x:A. t) : A \to B} $$

对应关系

这两个规则的结构一模一样！

逻辑中的概念	程序中的概念
假设 $A$	形式参数 $x:A$
推导出 $B$	构造出项 $t:B$
得到 $A \to B$ 证明	得到函数 $\lambda x:A. t$

6.4 在 Coq/CIC 中的具体例子

coq

(* 逻辑命题: (A ∧ B) → A *)
(* 程序类型: A * B -> A *)

Lemma and_proj_left : forall A B : Prop, A /\ B -> A.
Proof.
  intros A B H.        (* 假设我们有 A /\ B *)
  destruct H as [HA HB].  (* 分解合取 *)
  exact HA.            (* 返回 A 的证明 *)
Qed.

(* 对应的程序项 *)
Print and_proj_left.
(* 输出:
and_proj_left =
fun (A B : Prop) (H : A /\ B) => match H with
                                 | conj HA HB => HA
                                 end
     : forall A B : Prop, A /\ B -> A
*)

6.5 为什么是"直觉主义"逻辑？

Curry-Howard 同构天然对应直觉主义逻辑，而非经典逻辑。

关键区别在于对"真"的理解：

经典逻辑	直觉主义逻辑
一个命题 $P$ 为真，如果它在所有可能世界中都为真	一个命题 $P$ 为真，当且仅当我们能显式地构造出它的一个证明
排中律 $P \lor \neg P$ 成立	排中律不一定成立
证明可以是间接的、非构造性的（如反证法）	证明必须是构造性的

这种"构造性"的要求，正好与编程中"一个函数必须能计算出具体结果"的要求完美契合。

在 Coq 中，你不能用反证法证明存在性，你必须构造出那个存在的对象。

6.6 Curry-Howard 在 CIC 中的完整体现

在 CIC 中，Curry-Howard 同构是活生生的现实：

统一的语法：在 Coq 中，写证明和写程序使用相同的语法
证明状态即编程环境：当你开始证明时，Coq 显示的目标正是"需要构造的类型"
策略 (Tactics) 即程序构造器：intros, apply, destruct 等策略帮你构造底层的 λ 项
计算即证明规约：你可以用 Compute 命令"运行"一个证明

6.7 实践意义

程序验证

验证一个程序是否满足其类型规范，等价于证明一个逻辑定理。

证明构造

做数学证明的过程，本质上是在为一个特定类型（命题）编写一个程序（证明项）。

形式化方法

将"证明"从一个神秘的、仅存在于数学家脑海中的概念，转变为了一个可计算、可操作、可由机器严格检查的数据对象。

6.8 与程序综合的关联

程序综合 (Program Synthesis) 是指从高级规范自动生成满足该规范的程序代码。

在 Curry-Howard 的视角下：

规范就是逻辑命题（类型）
生成的代码 就是证明项
验证就是类型检查

这为"基于 LLM 和形式化 spec，自动生成代码 => Coq 中证明（proof-term）构造"提供了理论基础。

第七章实践应用与工具

7.1 证明助理

基于 CIC 的证明助理是 PTS 理论最重要的实践应用。

Coq

Coq 是最成熟的 CIC 实现：

核心语言 Gallina 直接实现 CIC
策略语言 Ltac 辅助构造证明项
支持程序提取（到 OCaml、Haskell、Scheme）
活跃的社区和丰富的库

Lean

Lean 是较新的证明助理，由 Leonardo de Moura 开发：

支持经典逻辑和构造性逻辑
强大的自动化策略
与数学社区（如 Xena 项目）紧密结合
数学库 Mathlib 非常活跃

Agda

Agda 是依赖类型编程语言：

强调编程而非证明
支持 Unicode 字符
用于教学和研究

7.2 De Bruijn 索引

在实现 PTS 相关工具时，De Bruijn 索引是处理变量绑定的重要技术。

传统表示	De Bruijn 索引	解释
`λx. x`	`λ 0`	`0` 指向最近的 λ 绑定（即自身）
`λx. λy. x`	`λ λ 1`	`1` 指向外层 λ（跳过内层 λ）
`λx. λy. y`	`λ λ 0`	`0` 指向最近的 λ 绑定（内层 y）

7.3 形式化数学

许多重要的数学定理已在 Coq/Lean 中形式化：

四色定理：2005 年，Georges Gonthier 在 Coq 中形式化
Feit-Thompson 定理：2012 年，Gonthier 等人在 Coq 中形式化
Kepler 猜想：2017 年，Thomas Hales 等人在 HOL Light 和 Isabelle 中形式化

7.4 程序验证

CIC 已用于验证关键软件：

CompCert：经过形式化验证的 C 编译器
seL4 微内核：经过形式化验证的操作系统微内核
加密算法：多种加密算法已在 Coq/Lean 中验证正确性

7.5 程序综合与 LLM

结合 Curry-Howard 同构和程序综合，可以利用 LLM 自动生成证明：

将规范表达为类型（命题）
让 LLM 构造具有该类型的项（证明）
用类型检查器验证正确性

潜在路径：

引导式综合：让 LLM 在交互式证明助理环境中工作
类型驱动生成：将规范表达为依赖类型
验证后过滤：生成多候选，类型检查器过滤

附录

A. 术语表

术语	英文	解释
项	Term	PTS 中统一的概念，可以是程序、类型或种类
种类	Sort	类型的类型，如 `Prop`、`Type`
宇宙	Universe	种类的同义词，表示类型的层级
依赖乘积类型	Dependent Product Type	返回类型依赖于输入值的函数类型
归纳类型	Inductive Type	通过构造子递归定义的数据类型
构造子	Constructor	用于构造归纳类型实例的函数
规约	Reduction	计算过程，如 β-规约、ι-规约
上下文	Context	变量及其类型的声明序列
类型判断	Type Judgement	声明一个项具有某个类型

B. 推荐阅读

书籍

Types and Programming Languages - Benjamin C. Pierce
Software Foundations - Benjamin C. Pierce et al.
Certified Programming with Dependent Types - Adam Chlipala
Homotopy Type Theory: Univalent Foundations of Mathematics - The Univalent Foundations Program

论文

Thierry Coquand, Gérard Huet. "The Calculus of Constructions" (1988)
Henk Barendregt. "Lambda Calculi with Types" (1992)
Christine Paulin-Mohring. "Inductive Definitions in the System Coq" (1993)

在线资源

C. 工具链接

工具	网址	说明
Coq	https://coq.inria.fr/	成熟的证明助理
Lean	https://leanprover.github.io/	现代证明助理
Agda	https://wiki.portal.chalmers.se/agda/	依赖类型编程语言
Idris	https://www.idris-lang.org/	依赖类型通用编程语言

结语

Pure Type System 为我们提供了一个优雅的框架来理解和研究类型系统。从最简单的 λ→ 到最强大的 CIC，我们看到了类型系统如何通过增加"依赖"能力而不断演进。

理解 PTS 不仅是理解现代证明助理（如 Coq、Lean）的理论基础，更是理解计算与逻辑之间深刻联系的关键。通过 Curry-Howard 同构，我们看到：

证明即程序
命题即类型
类型检查即证明验证

这些思想正在改变我们编写软件和做数学的方式。形式化验证、依赖类型编程、程序综合等领域的进展，都建立在这些理论基础之上。

第一章 引言与动机

1.1 什么是 Pure Type System？

1.2 为什么需要 PTS？

1.3 从一个简单例子开始

1.4 学习路线图

第二章 PTS 核心定义

2.1 三元组定义

$\mathcal{S}$ (Sorts) - 宇宙/种类

$\mathcal{A}$ (Axioms) - 公理

$\mathcal{R}$ (Rules) - 规则

2.2 语法

2.3 依赖乘积类型详解

从简单函数到依赖函数

逻辑对应

具体例子

2.4 推导规则

七条核心规则

1. 排序公理 (Axiom)

2. 变量声明 (Start)

3. 弱化规则 (Weakening)

4. 乘积形成规则 (Product / Π-formation) ⭐核心

5. 抽象规则 (Abstraction / λ-formation)

6. 应用规则 (Application)

7. 转换规则 (Conversion)

2.5 类型判断的含义

2.6 PTS 实例化示例

简单类型 λ 演算 (λ→)

System F (λ2)

构造演算 (CoC)

第三章 λ-Cube 类型系统谱系

3.1 什么是 λ-Cube？

3.2 三个维度的依赖

3.3 八个系统详解

1. λ→ (Simply Typed Lambda Calculus) - 简单类型 λ 演算

2. λ2 (System F) - 二阶多态 λ 演算

3. λP (LF - Logical Framework) - 依赖类型

4. λω (System Fω) - 高阶类型

5. λP2 (System FP) - 多态依赖类型

6. λPω (Dependent Fω) - 依赖高阶类型

7. λω (Full) - 高阶多态

8. λC (CoC) - 构造演算 ⭐

3.4 规则详解

3.5 总结表格

3.6 λ-Cube 的意义

第四章 构造演算 CoC

4.1 什么是构造演算？

4.2 CoC 的核心组件

语法

核心组成部分

4.3 逻辑表达能力

4.4 计算规则

β-规约

类型推导示例

4.5 CoC 的局限性

1. 缺乏原生归纳类型

2. 证明复杂性高

3. 终止性无保证

4.6 与 CIC 的关键区别

4.7 历史意义

第五章 归纳构造演算 CIC

5.1 什么是 CIC？

5.2 CIC 的核心组成

5.3 归纳类型详解

基本语法

经典示例

5.4 依赖类型示例

5.5 递归函数

5.6 命题即类型，证明即程序

5.7 类型层级

5.8 CIC 的计算规则

β-规约

ι-规约

强规范性

5.9 完整示例

5.10 CIC 的意义与应用

第六章 Curry-Howard 同构

6.1 什么是 Curry-Howard 同构？

6.2 核心对应关系

6.3 如何理解"证明即程序"？

逻辑规则：蕴含引入

第一章引言与动机

第四章构造演算 CoC

第五章归纳构造演算 CIC

第七章实践应用与工具