「PFPL」 Judgements and Rules 学习笔记

$$\gdef\Op{\mathcal{O}} \gdef\So{\mathcal{S}} \gdef\X{\mathcal{X}} \gdef\Ast{\mathcal{A}} \gdef\Abt{\mathcal{B}} \gdef\imply{\Rightarrow}$$

本文是 Practical Foundations for Programming Languages 的学习笔记。

抽象语法树（Abstract Syntax Trees）

这里我们直接给出形式化定义：

1. 设$\So$为一有限类型集合。
2. 设$\Op = \{\Op_s\}_{s\in \So}$表示每一个类型$s$拥有的运算符构成集合$\Op_s$，所有的$\Op_s$构成$\{\Op_s\}_{s\in\So}$，称作类型索引的运算符集合族（sort-indexed family of operators）。$n$元运算符$o\in \Op_s$，的元数（计算所需参数个数，arity）记作$ar(o) = (s_1, \ldots, s_n)$，其中$s_1, \ldots, s_n\in\So$，而$o$的运算结果类型为$s$。
3. 类似地，定义$\X = \{\X_s\}_{s\in\So}$表示类型索引的变量集合族。

这样，我们就可以定义 AST 的集合族$\Ast [\X] = \{ \Ast [\X]_s \}_{s\in\So}$为最小非空集合族满足：

1. 一个变量构成一个 AST：$x\in \X_s \imply x\in\Ast[\X]_s$。变量可以理解为类型为$s$的未知 AST。
2. 一个运算符可以构造 AST：对于$o\in\Op_s$，$ar(o) = (s_1, \ldots, s_n)$，若$a_1\in\Ast[\X]_{s_1}, \ldots, a_n\in\Ast[\X]_{s_n}$，那么$o(a_1, \ldots, a_n)\in \Ast[\X]_s$。

$\Ast[\X]_s$可以理解为返回值类型为$s$的表达式。

有了这个定义，那么我们可以有一个类似的归纳推导性质的做法。比如我们要证明性质$P$对所有$a\in \Ast[\X]$成立，就可以按照 AST 的两条构造规则一一证明。

如果上下文里隐含了$x$的类型为$s$，那么我们就记$\X, x$表示把$x$插入到$\X_s$构成的新的变量集合族。

变量的替换：将$x = b$作用于 AST 记作$[b/x]$。也就是说

1. $[b / x] x = b$，$[b/x]y = y\, (y\ne x)$。
2. $[b/x]o(a_1, \ldots, a_n) = o([b/x]a_1, \ldots, [b/x]a_n)$。

显然这个替换的结果是唯一的。

但是我们知道在编程语言中还存在一种现象：某些语法/运算符只能在特定的上下文使用。这催生了作用域（scope）的概念。

举例来说，let x = x * x in x + x 展开之后就会变成 x * x + x * x。通常来说，这里的 let x 中的 x 作用于 x + x，而 x * x 中的 x 只是恰好与其名字相同，实质是另一个变量。类似 C++ 里局部变量和同名全局变量的关系。不过这个东西的行为因语言而异，比如 haskell 是允许循环定义的。

抽象语法限定树（Abstract Binding Trees）

ABT 是 AST 的扩展。它给出了变量作用域的限定方式。比如我们想声明一系列的变量$x_1, \ldots, x_t$只作用于语法树$a$，我们记作$x_1, \ldots, x_t. a$。其中$x_1, \ldots, x_t$类型各异。为了方便，我们记为$\vec{x}.a$。

我们称$\vec{x}$的类型为$\vec{s}$当且仅当对任意$i$有$x_i$的类型是$s_i$。

在 ABT 中，运算符的类型表示为$ar(o) = ((\vec{s_1})s_1, \ldots, (\vec{s_n})s_n)$。$s_i$表示该语法树的类型，而$\vec{s_i}$表示该语法树的作用域下用到的各个变量的类型。

形式化地：

1. 设$\Op$为一个类型索引的运算符集合族。
2. 设$\X$为一个类型索引的变量集合族。
3. 为了处理不同作用域的变量名字相同，对于$\vec{x}$我们定义它的一个重命名（双射）$\pi : \vec{x} \leftrightarrow \vec{x}'$，对于类型为$(\vec{s})s$的语法树$a$，$\pi(a)$的含义就是对所有$j$将$a$中出现的所有$(\vec{x_i})_j$替换为$(\vec{x_i}')_j$。

那么定义关于$\X$的 ABT$\Abt[\X]$为

1. $x\in \X_s \imply x\in \Abt[\X]_s$。
2. 对于$o\in \Op_s$，且$ar(o) = ((\vec{s_1})s_1, \ldots, (\vec{s_n})s_n)$，设$\vec{x_i}$的类型是$\vec{s_i}$。对于$\vec{x_i}$我们定义它的重命名$\pi_i : \vec{x_i} \leftrightarrow \vec{x_i}'$，其中$(\vec{x_i}')_j \notin \X$。则对满足$\pi_i (a_i)\in \Abt[\X, \vec{x_i}']$的$a_i$，有$o(\vec{x_1}.a_1, \ldots, \vec{x_n}.a_n) \in B[\X]_s$。

$\X, \vec{x}$的含义与$\X, x$类似，就是把$\vec{x}$里的变量插入到$\X$对应类型的集合里。

这里的重命名起到的作用其实是与父节点中的参数取消绑定关系（freshness condition on binders）。

于是我们就会发现，在 ABT 中两个参数名字（变量）一样不代表他们真的一样，这得看他们是不是在一个作用域里面。相关判断非常符合经验直觉。如果两个 ABT 本质相同，称作$\alpha$-equivalence，互相称作$\alpha$-variants。它的说法是 fresh renaming（也就是重命名成原来没有的）不影响相等性。

变量的替换：这里要注意如果子树中有同名的参数得停止替换（capture avoidance），即

1. $[b / x] x = b$，$[b/x]y = y\, (y\ne x)$。
2. $[b/x]o(\vec{x_1}.a_1, \ldots,\vec{x_n}.a_n)$的情况，对于$x\in\vec{x_i}$的情况我们设$a_i' = a_i$，否则$a'_i = [b/x]a_i$，这样有$[b/x]o(\vec{x_1}.a_1, \ldots,\vec{x_n}.a_n) = o(\vec{x_1}.a'_1, \ldots, \vec{x_n}.a'_n)$。

但其实还可以换一种定义，就是我们先随便把子树里的参数做 fresh rename，这个时候直接替换$[b/x]$就没有任何问题了，即$[b/x]o(\vec{x_1}.a_1, \ldots,\vec{x_n}.a_n) = o(\vec{x_1'}.[b/x]\pi_1(a_1), \ldots, \vec{x_n'}.[b/x]\pi_n(a_n))$。

归纳（Inductive Definitions）

下面是一点数理逻辑的基础知识。

讲了一堆 Haskell 和 Agda 的东西，想必大家都会。

一个 judgement form 可以理解为 Haskell 里的 type constructor，或者 Agda 里的 data constructor。judgement form 也可以理解为一个函数定义。

规则集合$R$以若干个公理/定理的形式给出，而它代表所有遵循且仅遵循$R$的 judgement 构成的集合。也就是说对于其中的 judgement$J$，它能够从$R$中推导出来（closed under$R$），并且$R$蕴含推导出$J$的必要前提（strongest），如果$J$无法从$R$中推导那它就被视为不成立（vacuously true）。

这其中有一个有意思的叫做 mode specification，是指一个函数对其参数的限定关系。例如

$$R = \left\{ \frac{a \in\mathbb{N}}{\sum(0, a, a)}, \frac{\sum(a, b, c)}{\sum(\text{suc}(a), b, \text{suc}(c))} \right\}$$

这两条规则定义了一个 judgement，$\sum(a, b, c)$指$a + b = c$成立。这时你会发现，对于任意$a, b\in \mathbb{N}$都存在$c$满足它，记作$(\forall, \forall, \exist)$。当然它甚至其实是存在唯一，可以记作$(\forall, \forall, \exists!)$。而$\forall b, c\in \mathbb{N}$，存在至多一个$a$满足它，这个可以记作$(\exists^{\le 1}, \forall, \forall)$。这些被称作 mode specifications。

一般来说，$\forall$对应的是函数的输入，而$\exists$对应函数的输出。这样我们就可以用若干条规则定义函数了。当然为了写出来方便也会直接在上下使用$=$符号来代表函数的输入输出归纳关系。

条件判断（Hypothetical Judgments）

对于一个规则集合$R$，记$J_1, \ldots, J_k \vdash_R K$表示，在假设$J_1, \ldots, J_k$成立（公理）后可以借助$R$中的规则推导得到$K$。常用$\Gamma$或者$\Delta$表示 judgement 集合，记$R[\Gamma]$表示$R$由$\Gamma$拓展得到的规则集合，上式亦可表示为$\Gamma \vdash_R K$，$\Gamma$为空时可省略。$\Gamma \vdash _R \Delta$指$\Delta$中每一个 judgement 都可以由$R[\Gamma]$推导。$\vdash$满足以下性质：

1. 稳定性（stability）：$\Gamma\vdash_R K \imply \Gamma\vdash_{R\cup R'} K$。
2. 自反性（reflexivity）：$\Gamma, J\vdash_R J$。写成$J\vdash_{R[\Gamma]} J$更清楚。
3. 传递性（transitivity）：若$\vdash_{R[\Gamma]}K$且$K\vdash_{R[\Gamma]} J$，则$\vdash_{R[\Gamma]}J$。

另一方面，记$\Gamma \models_R J$表示$\vdash_R\Gamma\imply\; \vdash_R J$。这个的意思是说只要你能用$R$推导出$\Gamma$（其中的全部 judgement），你就可以推导出$J$。

$\models$不稳定。因为你往$R$里面随便加一点公理（记为$R'$），就能使$J$不能被$R'$推导。

举个例子。我们搞两个规则定义自然数：$R = \{\frac{}{\text{zero nat}}, \frac{\text{a nat}}{\text{suc(a) nat}} \}$。那么显然有$\text{suc(a) nat} \models_R \text{a nat}$，这个可以归纳证明。然后我们往$R$里面加一条垃圾公理$\vdash \text{suc(juck) nat}$，记作$R'$。那么如果$\models$稳定，则有$\vdash_{R'}\text{suc(juck) nat} \imply\; \vdash_{R'} \text{junk nat}$，但是这里的$\text{junk}$很可能不是自然数（比如说$-1$），也就是说它没法被$R'$里的规则推导出来，即$\nvdash_{R'}\text{junk nat}$。故$\text{suc(a) nat}\not\models_{R'} \text{a nat}$。

注：这里说$\text{junk nat}$没法被推导其实并不是说非得举出一个$-1$的反例，主要想表达的意思是它没有证据（vacuously true）。

在$\Gamma \vdash_R J$中，$\Gamma$是你推导出$J$的前提之一，$R$是辅助的推导规则集合。因此该命题体现的是在$R$辅助下，$\Gamma$到$J$的可推导性（derivable）。

在$\Gamma\models_R J$（$\vdash_R\Gamma\imply\; \vdash_R J$）中，究竟能不能推导出$J$其实与$\Gamma$无关，与$R$有关。命题的前提$\vdash_R \Gamma$描述的是$R$具有某种性质（使得它能推导出$\Gamma$），而这种性质提供了推导出$J$的充分条件。所以说如果$\Gamma\models J$在$R$下成立，意味着$R$具有这种性质，称作可接受的（admissible）。当然，也可以反客为主，称在$R$下$\Gamma\models J$是可接受的。

$\vdash$明确指出了要推导出$J$的充分前提；而$\models$只是指出，你要推导出$J$需要使得$R$具有某种性质。故也称$\models$是$\vdash$的一个 weaker form。$\models$满足以下性质：

1. 自反性：$J \models_R J$，这个很显然。
2. 传递性：若$\Gamma \models_R K$且$\Gamma, K\models_R J$，那么$\Gamma \models_R J$。

条件归纳（Hypothetical Inductive Definitions）

我们可以用$\vdash$来拓展规则的定义。条件规则（hypothetical rules）的形式如下：

$$\frac{\Gamma\Gamma_1\vdash J_1, \ldots, \Gamma\Gamma_n \vdash J_n}{\Gamma \vdash J}$$

其中$\Gamma$为大前提（global hypotheses）。而$\Gamma_i$为$J_i$的前提假设。

如果一个条件规则不需要大前提，称作一致（uniform）条件规则，可以简写为

$$\frac{\Gamma_1\vdash J_1, \ldots, \Gamma_n \vdash J_n}{J}$$

条件归纳定义为形式可推导的 judgement（formal derivability judgment）$\Gamma\vdash J$，其中$\Gamma$是一个有限的基本 judgement 集合，$J$是一个基本的 judgement。

而条件规则集合$R$代表了一个可从$R$中推导（closed under$R$）的且必须从$R$中推导（strongest）的结构化（structural）的 formal derivability judgment 集合。可推导和必须推导前面已经解释过了。结构化的意思其中的 judgement 满足$\vdash$的三个性质：

1. 自反性：$\dfrac{}{\Gamma, J\vdash J}$。
2. 稳定性：$\dfrac{\Gamma\vdash J}{\Gamma, K\vdash J}$。
3. 传递性：$\dfrac{\Gamma\vdash K\quad \Gamma, K\vdash J}{\Gamma \vdash J}$。

同样地，这里可以用$\Gamma\vdash_R J$表示借用$R$的规则，从$\Gamma$出发可以推导出$J$。

泛化判断（General judgements）

大概就是在 judgement 里引入变量。设$\Gamma, J$分别是含有变量$\vec{x}$的前提集合与目标 judgement，记$\vec{x} \mid \Gamma\vdash_{R}^{\X} J$表示利用包含变量$\X$的规则集合$R$，我们可以从$\Gamma$推导出$J$。这里$\vec{x}\not \subseteq\X$。换句话说对于任何重命名$\pi : \vec{x}\leftrightarrow\vec{x'}$，有$\pi(\Gamma)\vdash_{R}^{\X, \vec{x'}} \pi(J)$。

比如说$\text{x nat}\imply \text{(x + 2) nat}$可以表示为$x \mid \text{x nat}\vdash_{R}^{\X}\text{suc(suc(x)) nat}$。

更准确地说，在$\Gamma\vdash_{R}^{\X} J$中，我们将所有 judgement 视为对 ABT 的判断。这样才能说清楚含有变量的 judgement、重命名、变量替换是什么。刚才的例子里，$\Gamma = \{\text{x nat}\}$中的$x$自己就是一个 ABT。

泛化判断有几个显然的基本性质：

1. 扩张性（Proliferation）：$\vec{x}\mid \Gamma\vdash_R^{\X} J\imply \vec{x}, x\mid \Gamma\vdash_{R}^{\X} J$。
2. 重命名-等价性（Renaming）：$\vec{x}, x\mid \Gamma\vdash_R^{\X} J\imply \vec{x}, x'\mid [x\leftrightarrow x'](\Gamma)\vdash_R^{\X}[x\leftrightarrow x'](J)$，对于任意$x'\notin\X, \vec{x}$。