用户: Trebor/综合 Tait 可计算性

注 0.1. 本篇已经废弃. 读者可以在此找到文章的内容. 它经过了重新组织, 并且有更充足的上下文.

注 0.2. 这篇是英文, 但是写的更好懂一点.

1简单类型 $\lambda$ 算术

假定读者已经大致了解简单类型 $\lambda$ 算术是什么. 我们规定有一个基本类型 $\mathsf{Ans}$, 含有两个元素 $\mathsf{yes},\mathsf{no}$.¹ 我们也要求函数和乘积类型. 典范性说的是任何一个表达式 $⊢M:\mathsf{Ans}$ 都等于 $\mathsf{yes},\mathsf{no}$ 其中之一 (并且这两种可能是互斥的). 这里的等价关系即 $\beta \eta$-等价. 而可正规性指的是任何一个表达式 $\Gamma ⊢M:\sigma$ 都有一个 $\beta \eta$-等价的表达式是正规的. 我们互相递归地定义正规表达式和中性表达式:

定义 1.1. 正规表达式要么是类型为 $\mathsf{Ans}$ 的中性表达式, 要么是 $\mathsf{yes},\mathsf{no}$ 之一, 要么形如 $\lambda x.M$, 其中 $M$ 是正规表达式.

中性表达式要么是变量, 要么形如 $M(N)$, 其中 $M$ 是中性表达式, $N$ 是正规表达式.

一些读者可能之前接触的正规表达式的定义和这里不同, 是先定义 $\beta ,\eta$-规约, 再定义正规表达式为 “不可以再进行规约的表达式”. 我引用 Jonathan Sterling 在他的博士论文中的论述:

正规化对不同的人来说含义不同; 其中常见的一种观点是, 可正规性是某种重写系统的性质, 此时它通常有强/弱两个版本. 重写系统的强可正规性说的是一切可能的规约策略最终都必然会停止. 当然, 在这种解读下, 可正规性就不再是类型论的性质, 而是类型论的其中一种呈现方式的性质. [...]

不幸的是, 当代的类型论难以使用重写系统的技术; 一部分原因是重写系统目前看来非常不适合处理外延性和唯一性. 为此, 越来越多的类型论学者开始使用无重写的方式研究可正规性, 如求值正规化 (normalization by evaluation) 等.

无论是证明典范性还是可正规性都需要不少功夫, 因为简单地直接归纳是行不通的. 我们需要先通过归纳法证明一个更强的命题.² 有很多这样的方案, 大致思路是在每个类型 $\sigma$ 上定义一个谓词 $R_{\sigma }$, 并归纳证明其性质. (因为集合 $X$ 上的谓词 $P$ 等价于它的子集 $\{x\in X\mid P(x)\}$, 所以这两者可以交换使用.) 如$$R_{\sigma \to \tau }=\left\{(\Gamma ,f)|\begin{array}{rl}\Gamma ⊢& f:\sigma \to \tau ,\\ \forall (\Delta ,s)\in R_{\sigma },\Gamma \subseteq \Delta & ⟹(\Delta ,f(s))\in R_{\tau }\end{array}\right\}.$$这比较不直观, 而且很难想到. 利用范畴语言, 可以给出更加系统的表述, 其中这些略微复杂的构造其实都是自然而唯一的.

为此, 我们首先需要将简单类型 $\lambda$ 算术的语法做成范畴语言. 我们令所有的上下文 $\Gamma$ 为范畴 $\mathcal{T}$ 中的对象, 而 $\Gamma$ 到 $\Delta$ 的态射就是在 $\Gamma$ 上下文中的一列表达式, 其中第 $n$ 个表达式的类型恰好是 $\Delta$ 中的第 $n$ 个类型. 换言之, 这一列表达式给出了从 $\Delta$ 到 $\Gamma$ 的替换 (substitution). 并且我们认为 $\beta \eta$-相等的项给出相同的替换.

实际上由于简单类型 $\lambda$ 算术自身的性质, 我们可以等价地让对象为所有的类型, 而态射为这些类型间的函数. 因为$${\sigma }_1,\dots ,{\sigma }_n⊢{\tau }_1,\dots ,{\tau }_m$$可以表述为$$⊢{\sigma }_1\times \cdots \times {\sigma }_n\to {\tau }_1\times \cdots \times {\tau }_n.$$但是用上下文的方法更具普适性. 此后为了行文简洁, 我们会混淆这两个方法.

我们实际上有非常好的方式刻画这个范畴.

定理 1.2. $\mathcal{T}$ 是由图表 $1\rightrightarrows \mathsf{Ans}$ 生成的自由 Descartes 闭范畴.

“自由生成” 在这里的含义或许需要阐明. 我们定义这样一种数学结构, 其中包含一个 Descartes 闭范畴以及选定一个对象 $A$ 和两个态射 $1\rightrightarrows A$. 这些数学结构之间可以定义一些同态, 即保持选定的对象和态射的 Descartes 闭函子. 那么这就构成了一个范畴 (其实是 2-范畴), 姑且称作 ${\mathsf{CartClosedCat}}_{1\rightrightarrows \mathsf{Ans}}$. 那么其中的始对象就是我们所说的被自由生成的范畴.

证明. 把这个定理展开, 就可以发现它整齐地打包了很多预备的引理. 在这里我们只提到重要的引理, 其余部分都是直接展开定义即可.

首先我们需要证明 $\mathcal{T}$ 构成范畴, 需要验证结合律. 这就是替换引理. (很不幸的是这个词可以指代两个不同的引理.) 这可以通过对表达式的结构做归纳得到.

其次我们需要证明 $\mathcal{T}$ Descartes 闭. 这实际上就是简单类型 $\lambda$ 算术的语法决定的, 而其中那些自然同构的等式则是由 $\beta ,\eta$ 规则保证.

接下来需要证明任意给定一个这样的范畴 $\mathcal{C}$, 都能找到保持选定的对象和态射的 Descartes 闭函子 $F:\mathcal{T}\to \mathcal{C}$. 这之中需要证明的是替换与 $\beta \eta$ 规约是可交换的. 而这函子 (在唯一的自然同构意义下) 的唯一性来源于其所有类型都是用 $\mathsf{Ans},\times ,\to$ 三者生成的.

$\square$

2范畴模型

在研究逻辑学的时候, 经常可以通过构造模型来研究形式理论. 这实际上在通常的数学中就很常见, 如一个具体的群就是群的公理所构成的形式理论的一个模型; 或者 Cauchy 实数就是实数公理的一个模型.³

不同的理论的 “模型” 定义也不同. 基于一阶逻辑的公理理论的模型比较熟知, 但是研究其他理论时 (如类型论) 就不能用了. 为此产生了许多不同的模型定义. 在范畴论中, 可以将这些定义全部统一. 一个范畴模型就是从语法范畴出发的保持语法结构的函子. 在我们这里, 简单类型 $\lambda$ 理论的模型就是从 $\mathcal{T}$ 出发的保持 $\mathsf{Ans},\mathsf{yes},\mathsf{no}$ 的 Descartes 闭函子.

如果你回顾上文, 就会发现我们刚刚已经证明的定理 1.2 可以表述成 “$\mathcal{T}$ 是简单类型 $\lambda$ 算术的范畴模型构成的 2-范畴中的始对象”. 特别地, 语法范畴本身也是模型之一.

我们现在就可以迅速证明 $\mathsf{yes}\ne \mathsf{no}$. 考虑所有集合的范畴 $\mathsf{Set}$, 它是 Descartes 闭的. 我们再选择 $1\rightrightarrows A$ 为 $1=\{\varnothing \}$ 到 $2=\{\varnothing ,\{\varnothing \}\}$ 的两个态射即可. 如果 $\mathsf{yes}=\mathsf{no}$, 那么说明定理 1.2 产生的函子 $\mathrm{s}:\mathcal{T}\to \mathsf{Set}$ 满足 $\mathrm{s}(\mathsf{yes})=\mathrm{s}(\mathsf{no})$, 进一步得到 $2$ 的两个元素相等, 矛盾. 但是注意这个模型仍然无法证明典范性, 因为 $\mathrm{s}$ 仍然有可能把不相等的表达式 $M,N\in {\mathrm{Hom}}_{\mathcal{T}}(1,\mathsf{Ans})$ 映射到相等的函数.

题外话: $\mathsf{Ans}$ 与语法

有些读者或许会疑惑: 既然 $\mathsf{Ans}$ 不像 $\mathsf{Bool}$ 那样有消去子, 那么为什么可以说 $\mathsf{yes}\ne \mathsf{no}$ 呢? 这个涉及到语言和元语言之间的混淆.

在一般的依值类型论中, 可以在语言内部证明 $\mathsf{true}\ne \mathsf{false}$. 但是无法证明 $\mathsf{yes}\ne \mathsf{no}$. 因为有一些模型中的确有 $\mathsf{yes}=\mathsf{no}$. 但是在语法范畴中这两者是不相等的, 也就是说不存在一系列 $\beta \eta$-规约连接这两者. 这其实类似于研究环的时候, $3=1+1+1$ 和 $1$ 不一定是不相等的, 但是从环的公理出发是肯定无法证明这两者相等的. 换句话说, 自由环 $\mathbb{Z}$ 中 $1\ne 3$. 因此, 我们研究的典范性, 实际上是在始对象 (自由对象) 中涌现的性质. 由于在语言内部能够证明的事物, 肯定在一切模型中都成立, 因此典范性必然是元语言的性质.

3典范性

为了研究典范性, 我们需要先找出类型论中的闭元素, 即不包含自由变量的表达式. 这很容易, 我们只需要要求上下文为空即可. 因此我们考虑 $\mathbf{\Gamma }(X)={\mathrm{Hom}}_{\mathcal{T}}(1,X)$. 这是一个 $\mathcal{T}\to \mathsf{Set}$ 的函子.

如上文所述, 我们一般的思路是为每一个类型赋予一个谓词. 在范畴论中, 我们经常使用一个 $f:Y\to X$ 的态射作为 $X$ 上的 “谓词”. 大致来说, 我们认为如果 $f^{-1}(x)$ 非空, 那么这个谓词就取值为真, 否则为假. (当然这个大致说法只在集合范畴里成立, 其他范畴中只能起启发作用.)⁴ 因此, 我们考虑这样一个范畴 $\mathcal{G}$, 它的对象是形如 $f:{\Sigma }^{\prime }\to \mathbf{\Gamma }(\Sigma )$ 的态射, (准确地说, 是一个三元组 $({\Sigma }^{\prime },f,\Sigma )$.) 其中 $\Sigma$ 是 $\mathcal{T}$ 中的对象, ${\Sigma }^{\prime }$ 是集合. 这个范畴里的态射是这样的交换图:$${\Sigma }^{\prime }{\Delta }^{\prime }\mathbf{\Gamma }(\Sigma )\mathbf{\Gamma }(\Delta ){\sigma }^{\prime }\mathbf{\Gamma }(\sigma )$$其中 $\sigma$ 是 $\Sigma ⊢\Delta$ 的一个替代, ${\sigma }^{\prime }$ 是某个函数.

如果读者熟悉范畴论, 就应该知道这是逗号范畴的特例:$$\mathcal{G}={\mathrm{Id}}_{\mathsf{Set}}\downarrow \mathbf{\Gamma }.$$它也可以看成是下面这个拉回:$$\mathcal{G}{\mathsf{Set}}^{\to }\mathcal{T}\mathsf{Set}\mathrm{gl}┘\mathrm{cod}\mathbf{\Gamma }$$

注意这时候我们自动有了一个函子 $\mathrm{gl}$, 它把 $\mathcal{G}$ 中的对象 ${\Sigma }^{\prime }\stackrel{f}{\to }\mathbf{\Gamma }(\Sigma )$ 映射到 $\Sigma$.

我们希望能够取 $\mathcal{G}$ 为一个模型. 回顾模型的定义, 我们的第一步当然是要证明:

引理 3.1. $\mathcal{G}$ 是 Descartes 闭范畴, 并且 $\mathrm{gl}$ 是 Descartes 闭函子.

这个证明实际上对应的就是通常的证明中在类型上递归定义谓词. 但是注意这个命题本身已经完全限制了构造的可能性, 因此无需任何创意, 仅仅是机械地展开定义即可. 留给读者作为练习.

接下来, 我们只需要在 $\mathcal{G}$ 中选择一个对象 $A$ 和两个态射 $1\rightrightarrows A$. 选择了之后, 根据定理 1.2 我们立刻得知有唯一的保持这个对象和态射的函子 $\mathrm{s}:\mathcal{T}\to \mathcal{G}$. 如果 $\mathrm{gl}$ 也保持这个对象和态射的话, 那么这两个函子都在 ${\mathsf{CartClosedCat}}_{1\rightrightarrows \mathsf{Ans}}$ 中. 根据始对象的性质, $\mathrm{gl}\circ \mathrm{s}:\mathcal{T}\to \mathcal{T}$ 必然等于恒等函子 ${\mathrm{Id}}_{\mathcal{T}}$. 知道了这个, 我们自然要选择合适的对象. 这也不难, 如图构造即可:$$1\{\mathsf{yes},\mathsf{no}\}1\mathbf{\Gamma }(1)\mathbf{\Gamma }(\mathsf{Ans})\mathbf{\Gamma }(1)\mathsf{yes}\mathsf{no}\mathbf{\Gamma }(\mathsf{yes})\mathbf{\Gamma }(\mathsf{no})$$注意整个交换图都在 $\mathsf{Set}$ 中.

现在 $\mathrm{gl}\circ \mathrm{s}$ 等于恒等函子. 我们需要证明的是任何一个表达式 $M\in \mathbf{\Gamma }(\mathsf{Ans})={\mathrm{Hom}}_{\mathcal{T}}(1,\mathsf{Ans})$ 都一定恰好是 $\mathsf{yes},\mathsf{no}$ 其中之一. 因此我们考虑 $\mathrm{s}(M)\in {\mathrm{Hom}}_{\mathcal{G}}(\mathrm{s}(1),\mathrm{s}(\mathsf{Ans}))$, 根据 $\mathcal{G}$ 中态射的定义, 这对应一个交换图:$$1\{\mathsf{yes},\mathsf{no}\}\mathbf{\Gamma }(1)\mathbf{\Gamma }(\mathsf{Ans})M^{\prime }\mathbf{\Gamma }(M)$$其中左侧是 $1\to \mathbf{\Gamma }(1)$, 因为 $\mathrm{s}$ 是 Descartes 闭函子, 因此在同构意义下保持始对象. 右侧则是因为 $\mathrm{s}$ 按照定义需要保持范畴中选定的 $A$ 对象. 那么虚线表示的映射就选出了 $\mathsf{yes},\mathsf{no}$ 的其中一个. 无论是哪种, $\mathrm{gl}$ 必然保持这个映射. 又因为 $\mathrm{gl}(\mathrm{s}(M))=M$, 我们可以得出结论, $M$ 必然是 $\mathsf{yes},\mathsf{no}$ 其中之一.⁵

4可正规性

从可正规性开始就略微复杂了, 因为可正规性要求考虑所有的表达式, 包括那些有自由变量的表达式 $M\in \mathrm{Hom}(\Gamma ,\Delta )$. 然而我们之前使用了 $\mathbf{\Gamma }(X)=\mathrm{Hom}(1,X)$ 作为构造逗号范畴的函子, 只考虑了空上下文 $1$ 的情况. 但是如果不使用 $1$, 我们也不能使用某个固定的上下文, 因为在 $\lambda$-抽象中, 上下文是会改变的, 因此就走不通了. 我们需要同时考虑所有的上下文. 换句话说, 我们需要考虑上下文构成的范畴 $\mathcal{T}$.

与此同时, 注意到一般的替代并不明显保持可正规性, 如果已知 $M$ 是可正规的, $M[x/N]$ 的可正规性似乎和 $M$ 没有任何关系. 但是如果我们限制这些替代只能替代变量的话, 问题就解决了: 如果 $M$ 可正规, 那么 $M[x/y]$ 显然也是可正规的. 这对多变量的替代也成立. 这种特殊的替代称为重命名. 因此, 我们应该考虑 $\mathcal{T}$ 中由重命名作为态射的子范畴 $\mathcal{C}$.⁶

设 $\rho :\mathcal{C}\hookrightarrow \mathcal{T}$ 是含入函子. 我们需要考虑所有的可能有自由变量的式子, 因此应该考虑$${\mathrm{N}}_{\rho }(X)={\mathrm{Hom}}_{\mathcal{T}}(\rho (-),X).$$注意 ${\mathrm{N}}_{\rho }(X)$ 是范畴 $\mathrm{Pr}(\mathcal{C})$ 的对象, 其中 $\mathrm{Pr}(\mathcal{C})={\mathcal{C}}^{\mathrm{op}}\to \mathsf{Set}$. 这个范畴称为 $\mathcal{C}$ 上的预层范畴,⁷ 它和集合范畴 $\mathsf{Set}=\mathrm{Pr}(1)$ 有许多相似的性质, 这在后面会讲到.

仿照之前的做法, 我们应该在每个 ${\mathrm{N}}_{\rho }(X)$ 上找一些谓词, 也就是形如 $f:X^{\prime }\to {\mathrm{N}}_{\rho }(X)$ 的态射. 注意这里 $X^{\prime }$ 也是 $\mathrm{Pr}(\mathcal{C})$ 的对象. 因此同理我们构造范畴 $\mathcal{G}={\mathrm{Id}}_{\mathrm{Pr}(\mathcal{C})}\downarrow {\mathrm{N}}_{\rho }$. 注意到如果把 $\mathcal{C}$ 改成范畴 $1$, 那么就退化到上一节中的 $\mathcal{G}$.

但是我们仍然需要证明 $\mathcal{G}$ 是 Descartes 闭的. 我们在下一节会讲述大幅简化论证的方法. 这里为了完整性继续用朴素的方法构造.

$$\mathsf{Se}{\mathsf{t}}_{\mathsf{G}}\mathrm{Pr}(\mathcal{C}{)}^{\to }\mathrm{Pr}(\mathcal{T})\mathrm{Pr}(\mathcal{C})\mathrm{gl}┘\mathrm{cod}{\rho }^{\ast }$$

5合成语言

6Tait 瑜伽

脚注

1.	或许有读者会说:“为什么不叫 $\mathsf{Bool}$ 类型呢?” 实际上这并不是 $\mathsf{Bool}$ 类型, 因为没有配备消去子 (eliminator), 因此不满足其泛性质.
2.	对于简单类型来说有一些纯组合的手段, 但是这些方法是无法推广到更复杂的类型系统的.
3.	满足实数公理的模型都是同构的, 因此它具有范畴性 (categoricity). 不过注意这个名词和范畴论没有关系, “categorical” 本身具有 “明确的; 绝对的” 的含义.
4.	有些读者可能会认为, 我们需要让 $f$ 为单射, 即 $f^{-1}(x)$ 要么是空集要么是单点集. 在这里这个要求可有可无. 没有这个要求时行文更简洁.
5.	直接观察交换图, 并且对 $\mathbf{\Gamma }$ 做一些分析, 可以绕过 $\mathrm{gl}\circ \mathrm{s}=\mathrm{Id}$ 直接说明这一点, 不过使用 $\mathrm{gl}$ 说理在后面更加干净.
6.	这里实际上有一些细微的问题. 其一是如何用纯范畴语言定义重命名; 其二是重命名是否允许引入 (1) 重复的变量 (2) 变量顺序交换 (3) 若不许交换顺序, 那么两个出现的变量之间是否可以夹一个不出现的变量. 在我们这个例子中, 最好的定义是所有的类型 (作为一个集合) 自由生成的有限乘积范畴. 对于依值类型论来说, 也有一个优雅的泛性质决定.
7.	这个名称来源于几何, 不必太担心具体是为什么.