项的语言

五种项

核心语言是一个小型依赖类型论，它的项由如下文法生成

其中 $u$ 是自然数，$x$ 是变量名。每种形式各有角色。

• $\Sort{u}$ 是宇宙（universe）：一种元素本身也是类型的类型，数 $u$ 是它的层级，而 $\Sort{0}$ 是命题的宇宙。第 13 章解释为什么需要整个层级结构，而不是单个宇宙。
• $x$ 是变量，它的含义来自所在的上下文：要么是包围它的某个 $\lambda$ 或 $\Pi$ 绑定子，要么是类型上下文中的一条假设。
• $\tPi{x}{A}{B}$ 是 $\Pi$ 类型，即第 1 章的依赖函数类型，也就是这样一类函数的类型：接收一个 $x : A$，返回类型为 $B$ 的东西，而 $B$ 可以提到 $x$。
• $\tLam{x}{A}{t}$ 是 $\lambda$ 抽象，即接收类型为 $A$ 的参数 $x$ 并返回 $t$ 的函数。
• $t\;s$ 是 $t$ 对 $s$ 的应用。

文法不区分类型和项，命题 $\tPi{P}{\Sort{0}}{P \to P}$ 和它的证明 $\tLam{P}{\Sort{0}}{\tLam{p}{P}{p}}$ 都是由同样五种构造子搭建的项：

把这两个项画成树，共用的文法就一目了然。每个节点都是五种构造子之一；$\Pi$ 或 $\lambda$ 节点上的名字是它绑定的变量。点击节点可以查看它代表的子项，也可以输入另一个项。

一个项是否为合法的类型，不是语法性质，而是由类型检查器判定的：一个项是类型，当且仅当它自己的类型是一个宇宙（第 5 章）。

约定

本书始终如一地使用以下字母。

三个缩写让项保持可读。

->。当 $B$ 不提到 $x$ 时，我们把 $\tPi{x}{A}{B}$ 写作 $A \to B$。于是普通函数类型是依赖函数类型的特例，蕴含是全称量化的特例。在实现中，-> 的绑定子是保留名 _。

结合性。应用向左结合，-> 向右结合：

柯里化。两个参数的函数，就是接收第一个参数后返回一个等待第二个参数的函数。例如，$\tLam{a}{A}{\tLam{b}{B}{a}}$ 的类型是 $A \to B \to A$，把它应用于 $x : A$ 和 $y : B$ 写作

两条结合性约定是配套设计的：类型为 $A \to B \to C$ 的柯里化函数以 $f\;a\;b$ 的形式应用时，两边都不需要括号。

绑定与作用域

在 $\tLam{x}{A}{t}$ 和 $\tPi{x}{A}{B}$ 中，变量 $x$ 是约束的（bound），它的作用域是函数体 $t$ 或 $B$。标注 $A$ 在作用域之外：在 $\tLam{x}{x}{x}$ 中，标注里的 $x$ 指向项外部的某个东西，而函数体里的 $x$ 指向参数。不处于任何对应绑定子作用域内的变量出现称为自由的（free）。例如，在 $\tLam{x}{P}{f\;x\;y}$ 中，变量 $P$、$f$ 和 $y$ 是自由的，$x$ 是约束的。

关于约束变量有两个事实贯穿全书，两者都在第 11 章中形式化。

1. 约束变量的名字没有意义：$\tLam{x}{A}{x}$ 和 $\tLam{y}{A}{y}$ 是同一个函数。仅在约束变量名上有差异的项称为 α 等价的，内核必须把它们视为相等。
2. 用项替换变量（类型规则和计算都需要这一操作）时，绝不能意外地把自由变量带进同名绑定子之下。把这件事做对就叫避免捕获的替换。

这两个事实都容易陈述，也都在真实的证明检查器中造成过真实的错误，所以它们有专门的一章。

代码中

同一文件还提供了一些小的构造函数，使得写项时不必嵌套 Box::new 调用：var("x")、const_term("Nat")、app(f, a)、pi("x", a, b)、lam("x", a, b)，以及构造 pi("_", a, b) 的 arrow(a, b)。三个辅助函数直接编码了本章的约定。

/// f a_1 ... a_n   （左结合的应用）
pub fn apps(f: Term, args: impl IntoIterator<Item = Term>) -> Term {
    args.into_iter().fold(f, app)
}

/// Pi (x_1 : A_1) ... Pi (x_k : A_k). tail   （由绑定子组成的 telescope）
pub fn telescope(binders: &[(String, Term)], tail: Term) -> Term {
    binders.iter().rev().fold(tail, |body, (name, ty)| pi(name, ty.clone(), body))
}

/// 把 t 分解为它的脊（spine）：一个不是应用的头部，以及它的参数。
/// f a b  变成  (f, [a, b])；非应用的项变成  (t, [])。
pub fn spine(t: &Term) -> (Term, Vec<Term>) {
    match t {
        Term::App(f, a) => {
            let (head, mut args) = spine(f);
            args.push((**a).clone());
            (head, args)
        }
        _ => (t.clone(), vec![]),
    }
}

apps 和 spine 互为逆操作：apps(h, args) 构造左嵌套的应用 $h\;a_1 \cdots a_n$，spine 再把它拆开。脊（spine）视角是第 12 章的归约引擎看待项的方式，所以现在就熟悉它。嵌套项 $((f\;a)\;b)\;c$ 的头部是 $f$，参数是 $[a, b, c]$；沿每个应用的函数一侧向下走就到达头部，沿途收集的参数由内向外读，顺序正好。

本书通篇使用的 .leanmini 脚本的表层语法把同样的项写成 Sort 0、forall (x : A), B、A -> B、fun (x : A) => b，应用则用并置表示。附录 E给出完整文法。

练习

goal forall (P : Sort 0), forall (Q : Sort 0), P -> Q -> P
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (p : P) => fun (q : Q) => p
qed