Pure Type System (PTS) 详解

Pure Type System (PTS) 详解

Pure Type System 是一种用于定义依赖类型 λ 演算的通用框架。它之所以被称为"Pure"，是因为其语法和推导规则非常简洁统一：所有东西（项、类型、种类、命题）都是"项"（term），而类型关系仅由少数几条抽象和应用规则来定义。

1. 核心定义

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

• $\mathcal{S}$ (Sorts)：一组特殊的常量，称为"universe"或"sort"。它们是类型的类型，构成了类型的层级。例如，在 CoC 中，$\mathcal{S} = {,\ \square}$，其中 $$ 通常代表命题宇宙 Prop，$\square$ 代表类型宇宙 Type。
• $\mathcal{A}$ (Axioms)：一组形如 $s_1 : s_2$ 的公理，其中 $s_1, s_2 \in \mathcal{S}$。它规定了 universe 之间的层级关系。例如，${* : \square}$ 表示"命题是一种类型"。
• $\mathcal{R}$ (Rules)：一组形如 $(s_1, s_2, s_3)$ 的规则，其中 $s_1, s_2, s_3 \in \mathcal{S}$。它规定了在哪个宇宙中可以形成依赖乘积类型（Dependent Product Type），以及这个乘积类型本身属于哪个 universe。

2. 语法

在 PTS 中，所有东西——无论是变量、函数、类型，还是类型本身的类型（Sort）——都是用同一种语法定义的，统称为 项 (Term)。这种统一性是 PTS 被称为"Pure"的原因之一。PTS 的项（Terms）$\mathcal{T}$ 语法极其精简：

$$ \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{V}$ 是变量集合，代表未知的项；
• $\mathcal{S}$ 是种类集合（Sorts），代表类型的类型，是所有其他类型构造的起点。在 CoC 中，$*$ 对应 Prop（命题宇宙），$\square$ 对应 Type（类型宇宙）。在 CIC 中，有无限层级：Prop, Type₀, Type₁, ...。
• $\Pi x:A. B$ 是依赖乘积类型。返回的类型 B 依赖于输入值 $x$。如果 $x$ 不在 $B$ 中自由出现，则退化为简单函数类型 $A \to B$。在逻辑系统中 $\Pi x:A. B(x)$ 对应 $\forall x\in A, B(x)$。
• $\lambda x:A. t$ 是抽象（函数），引入参数 $x$ 及其类型 $A$，并给出函数体 $t$。如果 $t$ 在假设 $x:A$ 下具有类型 $B$，那么 $\lambda x:A. t$ 就具有类型 $\Pi x:A. B$。这是构造证明项或程序的基本方式。
• $t\ u$ 是函数调用，$u$ 是参数。

关键点：在 PTS 中，类型本身也是项。我们通过判断（Judgement）来声明一个项的类型：

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

这种统一性使得 PTS 成为一个极其简洁而强大的框架。通过仅仅五种语法构造（变量、抽象、应用、Π 类型、种类）和几条推导规则，它就能定义出从简单类型到全依赖类型的整个谱系。

3. 推导规则

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

1. 排序公理 (Axiom)：如果 $(s_1, s_2) \in \mathcal{A}$，那么： $$\frac{}{\vdash s_1 : s_2}$$

2. 变量声明 (Start)：如果 $x$ 不在 $\Gamma$ 中： $$\frac{\Gamma \vdash A : s}{\Gamma, x:A \vdash x : A}$$

3. 弱化规则 (Weakening)：确保上下文扩展有效。

4. 乘积形成规则 (Product / $\Pi$-formation)：这是 PTS 的核心。如果 $(s_1, s_2, s_3) \in \mathcal{R}$，那么： $$\frac{\Gamma \vdash A : s_1 \quad \Gamma, x:A \vdash B : s_2}{\Gamma \vdash (\Pi x:A. B) : s_3}$$

5. 抽象规则 (Abstraction)： $$\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)}$$

6. 应用规则 (Application)： $$\frac{\Gamma \vdash t : (\Pi x:A. B) \quad \Gamma \vdash u : A}{\Gamma \vdash t\ u : B[x := u]}$$

7. 转换规则 (Conversion)：如果两个项在 $\beta$-规约下等价，则它们的类型可以互换： $$\frac{\Gamma \vdash t : A \quad \Gamma \vdash B : s \quad A =_\beta B}{\Gamma \vdash t : B}$$

4. 与 λ-Cube 和 CoC/CIC 的关系

λ-Cube 是 8 个特定的 PTS，它们共享 $\mathcal{S} = {,\ \square}$ 和 $\mathcal{A} = { : \square}$，但通过不同的 $\mathcal{R}$ 规则集来区分。

Calculus of Constructions (CoC) 是 λ-Cube 右上角（最顶点）的系统，规则集 $\mathcal{R}$ 最丰富，允许所有形式的依赖：

• $(*, *, *)$：允许形成命题间的蕴含（$Prop \to Prop$）；
• $(\square, *, *)$：允许形成从类型到命题的量化（多态命题）；
• $(*, \square, \square)$：允许形成从命题到类型的函数（依赖命题的类型）；
• $(\square, \square, \square)$：允许形成类型构造子（高阶类型）。

Calculus of Inductive Constructions (CIC) 在 CoC 的基础上，增加了定义归纳类型（Inductive Types）的原语和推导规则。这是 Coq/Lean 等证明助理的核心。归纳类型使得我们可以自然地定义自然数、链表等数据结构，并对其进行归纳证明。

5. 总结：PTS 的意义

PTS 提供了一个模块化、可扩展的框架来研究类型系统。通过选择不同的 $(\mathcal{S}, \mathcal{A}, \mathcal{R})$，我们可以：

• 实例化出从简单类型系统到全依赖类型系统的各种演算；
• 清晰地分析一个类型系统的表达能力（它能表达哪种依赖？）；
• 为像 CoC/CIC 这样复杂的系统提供一个简洁、形式化的基础定义。