Skip to main content

Pure Type System

#类型系统

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（命题宇宙）， 对应 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$ 。 这是构造证明项或程序的基本方式。一个类型为$\Pi x:A. B$的证明，就是一个函数 $\lambda x:A. t$;
  • $t\ u$ 是abstraction，函数调用，$u$是参数。

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

  • 当它被赋予一个类型时，它是一个程序或证明。
  • 当它被用作其他项的类型时，它是一个类型或命题。
  • 当它被用作类型的类型时，它是一个种类 (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}$$ 这条规则说：如果 $A$ 属于宇宙 $s_1$，并且在假设 $x:A$ 下 $B$ 属于宇宙 $s_2$，那么依赖乘积类型 $\Pi x:A. B$ 就属于宇宙 $s_3$。
  5. 抽象规则 (Abstraction / $\lambda$-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)}$$
  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}$ 规则集来区分。 !200

  • 图片展示了这些系统如何通过允许不同“维度”的依赖关系（项依赖项、类型依赖项、项依赖类型、类型依赖类型）来扩展简单类型 λ 演算。

  • Calculus of Constructions (CoC) 是 λ-Cube 右上角的那个系统，其规则集 $\mathcal{R}$ 最丰富，允许所有形式的依赖。它的 $\mathcal{R} = {(,,*), (\square, *, ), (, \square, \square), (\square, \square, \square)}$。

    • $(*, *, *)$: 允许形成命题间的蕴含（$Prop \to Prop$）；
    • $(\square, *, *)$: 允许形成从类型到命题的量化（$\forall (x:Type), P(x)$，即多态命题）；
    • $(*, \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 这样复杂的系统提供一个简洁、形式化的基础定义。