α 等价算法的正确性

对 $s$ 归纳，同时对所有 $t$、$E_1$ 和 $E_2$。对 $s$ 的每种形状，图 11.1 中恰有一条规则能得出该判断，而其前提与 $\db{\cdot}{}$ 的等式一一对应。

若 $s = \Sort{u}$，由规则 $\alpha$-Sort 和宇宙的等式，两边都恰当 $t = \Sort{u}$ 时成立。

若 $s = x$，无名形式只有在 $t$ 是变量 $y$ 时才可能相等，因为无名变量（数字或名字）永远不等于 $\Pi$、$\lambda$、应用或宇宙。若 $x \in E_1$，则 $\db{x}{E_1} = \#\mathrm{idx}(E_1, x)$，相等恰当 $y \in E_2$ 且 $\mathrm{idx}(E_2, y) = \mathrm{idx}(E_1, x)$ 时成立，这正是 $\alpha$-Bound 的前提。若 $x \notin E_1$，则 $\db{x}{E_1} = x$，相等恰当 $y \notin E_2$ 且 $y = x$ 时成立，这正是 $\alpha$-Free 的前提。数字永远不等于名字，这对应于：对于只在一侧被绑定的变量，没有任何规则适用。

若 $s = \tPi{x}{A}{B}$，相等恰当 $t = \tPi{y}{A'}{B'}$ 且 $\db{A}{E_1} = \db{A'}{E_2}$、$\db{B}{E_1, x} = \db{B'}{E_2, y}$ 时成立。对 $A$ 和 $B$ 分别应用归纳假设，这两个等式正是 $\alpha$-Pi 的前提。$\lambda$ 和应用的情形相同，分别用 $\alpha$-Lam 和 $\alpha$-App。

对 $t$ 归纳，同时对所有 $E_1$ 和 $E_2$。变量情形正是假设本身：自由变量 $v$ 在两边变成同一个数字，或保持同一个名字。宇宙不受 $E$ 影响；应用由两个部分的归纳假设得出。

在绑定子 $x$ 之下，列表 $E_1, x$ 和 $E_2, x$ 在体的自由变量上仍然相合：变量 $x$ 在两边的位置都是 $0$，而体的其他任何自由变量 $v$ 都是 $t$ 的自由变量，由假设，它在 $E_1$ 和 $E_2$ 中的位置相同；追加 $x$ 使这个位置在两边各加一，或者在两边都保持无定义。于是对体可用归纳假设；注记部分则用原列表的归纳假设处理。

对 $B$ 的大小归纳，同时对所有 $E$ 和 $E'$。记 $L_x = E, x, E'$ 和 $L_y = E, y, E'$；它们恰有一个条目不同，且位于同一位置。

若 $B = x$，则 $\subst{B}{x}{y} = y$。由于 $x, y \notin E'$，$x$ 在 $L_x$ 中的最后一次出现和 $y$ 在 $L_y$ 中的最后一次出现都是那个特殊条目，所以 $\mathrm{idx}(L_x, x)$ 和 $\mathrm{idx}(L_y, y)$ 都等于 $E'$ 的长度，两个无名形式是同一个数字。

若 $B = v$ 且 $v \neq x$，则因 $y \notin \FV(B)$ 有 $v \neq y$，并且 $\subst{B}{x}{y} = v$。$v$ 在 $L_x$ 和 $L_y$ 中的位置相同，因为 $v$ 不是那两个不同条目中的任何一个；或者它在两边都无定义。

宇宙和应用由定义和归纳假设直接得出。

设 $B = \tPi{w}{C}{D}$；$\lambda$ 的情形相同。下面每种情形中注记 $C$ 都由归纳假设处理，所以只考虑体。按照第 11 章替换的定义，分三种情形。

情形 $w = x$. 绑定子遮蔽了 $x$，所以 $\subst{B}{x}{y} = \tPi{x}{\subst{C}{x}{y}}{D}$，我们需要 $\db{D}{L_x, x} = \db{D}{L_y, x}$，为此应用引理 B.2：变量 $x$ 在两个列表中的位置都是 $0$，因为它刚被追加；其他任何 $v \in \FV(D)$ 都不同于 $y$，因为 $y \notin \FV(B)$，所以它在两个列表中的位置相同，或在两边都无定义。

情形 $w \notin \{x, y\}$. 不需要改名，$\subst{B}{x}{y} = \tPi{w}{\subst{C}{x}{y}}{\subst{D}{x}{y}}$。对 $D$ 用归纳假设，并把 $E'$ 扩展为加上 $w$（这是允许的，因为 $w$ 既不是 $x$ 也不是 $y$），得 $\db{D}{L_x, w} = \db{\subst{D}{x}{y}}{L_y, w}$，这正是体所需要的。

情形 $w = y$. 绑定子会捕获 $y$，所以替换把它改名为新鲜的 $z \notin \FV(D) \cup \{x, y\}$：

我们需要 $\db{D}{L_x, y} = \db{\subst{(\subst{D}{y}{z})}{x}{y}}{L_y, z}$，分两步到达。第一步，对 $D$ 用归纳假设，把它最后一个绑定子 $y$ 改名为 $z$（取 $E$ 为 $L_x$，$E'$ 为空；前提成立，因为 $z \neq y$，$z \notin \FV(D)$，且绑定子之后的列表为空），得 $\db{D}{L_x, y} = \db{\subst{D}{y}{z}}{L_x, z}$。第二步，对 $\subst{D}{y}{z}$ 用归纳假设，它的大小与 $D$ 相同且不含自由的 $y$，把 $E'$ 扩展为加上 $z$，得 $\db{\subst{D}{y}{z}}{L_x, z} = \db{\subst{(\subst{D}{y}{z})}{x}{y}}{L_y, z}$。把两个等式串起来即得结论。

第一部分. 令 $s \sim t$ 表示对每个 $E$ 都有 $\db{s}{E} = \db{t}{E}$。这个关系是等价关系，因为相等是。它是同余关系，因为 $\db{\cdot}{}$ 是逐构造子定义的：如果两个项的各部分在相应列表下的无名形式相等，那么这两个项的无名形式也相等。最后，$\sim$ 包含 $\alphaeq$ 的定义等式：若 $y \notin \FV(B)$，则

而两个体由引理 B.3（取 $E'$ 为空）相等；$y = x$ 的情形平凡，因为此时两个项完全相同。$\lambda$ 的情形同理。由于 $\alphaeq$ 是包含该等式的最小同余关系，而 $\sim$ 是包含它的一个同余关系，所以 $s \alphaeq t$ 蕴涵 $s \sim t$。

第二部分. 对 $s$ 的大小归纳，同时对所有 $t$ 和 $E$，假设 $\db{s}{E} = \db{t}{E}$。

若 $s$ 是变量，则 $t$ 也是，因为其他形状的无名形式绝不会是数字或名字。若两个无名形式都是数字 $\#i$，则两个变量都是 $E$ 中位置 $i$ 处的条目，所以 $s = t$。若两个都是名字，则直接有 $s = t$。无论哪种情形，由自反性得 $s \alphaeq t$。

宇宙直接相等。对于应用，两部分的无名形式各自相等，于是归纳假设给出每部分的 $\alphaeq$，再由 $\alphaeq$ 的同余性质得到整体的结论。

设 $s = \tPi{x}{A}{B}$，于是 $t = \tPi{y}{A'}{B'}$，且 $\db{A}{E} = \db{A'}{E}$、$\db{B}{E, x} = \db{B'}{E, y}$。归纳假设给出 $A \alphaeq A'$。对于体，选取 $z \notin \FV(B) \cup \FV(B') \cup \{x, y\}$。引理 B.3（取 $E'$ 为空）给出 $\db{B}{E, x} = \db{\subst{B}{x}{z}}{E, z}$ 和 $\db{B'}{E, y} = \db{\subst{B'}{y}{z}}{E, z}$，所以

由于 $\subst{B}{x}{z}$ 的大小与 $B$ 相同，小于 $s$ 的大小，归纳假设给出 $\subst{B}{x}{z} \alphaeq \subst{B'}{y}{z}$。于是

三步分别依据定义等式（因 $z \notin \FV(B)$ 而成立）、同余性，以及反向读的定义等式（因 $z \notin \FV(B')$ 而成立）。$\lambda$ 的情形相同。

若 $s \alphaeq t$，则由引理 B.4 的第一部分（取 $E$ 为空）得 $\db{s}{\cdot} = \db{t}{\cdot}$，再由引理 B.1 得 $\cdot\,;\cdot \vdash s \alphaeq t$。

反之，若 $\cdot\,;\cdot \vdash s \alphaeq t$，则由引理 B.1 得 $\db{s}{\cdot} = \db{t}{\cdot}$，再由引理 B.4 的第二部分得 $s \alphaeq t$。