α 同値アルゴリズムの正しさ

$s$ に関する帰納法により、すべての $t$、$E_1$、$E_2$ について示す。$s$ の各形について、判断を結論できる図 11.1 の規則はちょうど一つであり、その前提は $\db{\cdot}{}$ の等式と対応する。

$s = \Sort{u}$ のとき、規則 $\alpha$-Sort と宇宙の等式により、両側とも $t = \Sort{u}$ のときにちょうど成り立つ。

$s = x$ のとき、名前なしの変数（数または名前）は $\Pi$、$\lambda$、適用、宇宙と決して等しくならないので、名前なし形が等しくなるのは $t$ が変数 $y$ のときに限る。$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'$ なので、$L_x$ における $x$ の最後の出現と $L_y$ における $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$ は異なる二つの要素のどちらでもないので、$v$ の位置は $L_x$ と $L_y$ で同じであるか、両方で未定義である。

宇宙と適用は、定義と帰納法の仮定から直ちに従う。

$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 \notin \FV(B)$ より $y$ とは異なるので、その位置は両方のリストで同じか、両方で未定義である。

ケース $w \notin \{x, y\}$. 改名は不要であり、$\subst{B}{x}{y} = \tPi{w}{\subst{C}{x}{y}}{\subst{D}{x}{y}}$ である。$E'$ を $w$ で拡張して（$w$ は $x$ でも $y$ でもないので許される）$D$ に帰納法の仮定を適用すると、$\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)$ ならば

であり、本体は $E'$ を空とした補題 B.3 により等しい。$y = x$ の場合は二つの項が同一なので自明であり、$\lambda$ についても同じである。$\alphaeq$ はこの等式を含む最小の合同関係であり、$\sim$ はこの等式を含む合同関係なので、$s \alphaeq t$ ならば $s \sim t$ である。

後半. $\db{s}{E} = \db{t}{E}$ を仮定し、$s$ のサイズに関する帰納法により、すべての $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\}$ を選ぶと、$E'$ を空とした補題 B.3 から $\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$ である。