代入、捕獲、α 同値

自由変数と代入

$\Pi$ と $\lambda$ は変数を束縛し、$\tLam{x}{A}{t}$ において、$t$ の中に現れる $x$ は引数を指す。束縛子のスコープは本体だけであり、注釈 $A$ の中では $x$ は束縛されない。外側の $\Pi$ や $\lambda$ に束縛されていない変数の出現を自由な出現と呼ぶ。

たとえば $\FV(\tLam{x}{P}{f\;x\;y}) = \{P, f, y\}$ であり、$\FV(\tPi{P}{\Sort{0}}{P \to P}) = \emptyset$ である。後者は閉じた項（closed term）である。定数は決して束縛されないので、自由変数には何も寄与しない。

エクスプローラは各束縛変数をその束縛子と同じ色で塗り、自由変数には下線を引き、変数にカーソルを合わせると束縛子が分かる。fun (x : A) => fun (x : A) => x のようなシャドーイングを含む項も試してみてほしい。

$t$ の中の $x$ の自由な出現を $s$ で置き換えた結果を $\subst{t}{x}{s}$ と書くが、束縛子があるときには注意が要る。たとえば $\subst{(\tLam{y}{A}{x})}{x}{y}$ の本体は、「引数を無視して外側の $x$ を返す」という意味である。ところが単純に $x$ を $y$ で置き換えると、自由だった $y$ が束縛子に捕獲され、恒等関数 $\tLam{y}{A}{y}$ になってしまう。意味を保つには、代入する前に束縛子を改名しなければならない。

次の例は束縛子の各場合を一つずつ試すものである。

最後の例では、置き換え項に含まれる自由な $y$ は依然として外側の $y$ を指し、束縛変数（今は $z$）は依然として引数を指す。改名しなければ結果は $\tLam{y}{A}{f\;y\;y}$ となり、引数を二度渡す関数になってしまう。エクスプローラは二通りの代入を並べて実行し、結果に現れる $y$ が、置き換え項由来の自由なものなのか、束縛子に捕獲されたものなのかは、色で区別できる。

文脈における変数の捕獲

C-Ext の側条件 $x \notin \dom(\Gamma)$ を落とし、多くのプログラミング言語と同じように、新しい仮定が古い仮定を単にシャドーイングするようにしたくなるかもしれないが、そうするとカーネルは不健全になる。次の項を考えよう。

変数 $y$ の型は外側の $x$ であり、最も内側の $\lambda$ は引数を無視するので、$t$ の正しい型は次である。

$\Freshen$ のない型検査器は、文脈 $x : \Sort{0},\; y : x,\; x : \Sort{0}$ の中で $y$ を引き、その型である裸の名前 $x$ を返すが、この時点で $x$ は内側の束縛子を指しているため、型検査器が返すのは

となり、これは「任意の型の任意の要素から、あらゆる型の要素を作れる」と言っている。$A : \Sort{0}$ と $a : A$ が与えられれば、項 $t\;A\;a$ の型は $\tPi{B}{\Sort{0}}{B}$、つまり False の証明になる。そのような $A$ と $a$ は空の文脈にも存在する。$A = \tPi{P}{\Sort{0}}{P \to P}$ はそれ自身が命題であり、恒等関数 $a = \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$ がそれを証明するからだ。

$\Freshen$ があれば、最も内側の束縛子は文脈に入る前に $x'$ に改名される。文脈は $x : \Sort{0},\; y : x,\; x' : \Sort{0}$ となり、$y$ を引くと返ってくる $x$ は依然として外側の束縛子を指し、$\Infer$ は上に示した正しい型を返す。導出エクスプローラでこの改名の様子を確認でき、最も内側の T-Lam ノードの注記が改名を報告し、葉の文脈には $x'$ が含まれている。

# カーネルは内側の x を x' に改名し、正しい型を推論する。
# 内側の x が外側の x をシャドーイングすることを許すカーネルは、
# この項を二つ目の文の証明として受け入れてしまう。二つ目の文は偽である。
goal forall (x : Sort 0), forall (y : x), forall (x' : Sort 0), x
exact fun (x : Sort 0) => fun (y : x) => fun (x : Sort 0) => y
qed
goal forall (x : Sort 0), forall (y : x), forall (x' : Sort 0), x'
exact fun (x : Sort 0) => fun (y : x) => fun (x : Sort 0) => y
qed

問題は代入の場合と同じで、名前が、別の意味を持つスコープへ移動してしまう。文脈がリストであれハッシュマップであれ、変数を名前で識別する表現はすべてこの影響を受ける。よく使われる対処法は三つある。

1. シャドーイングを一律に拒否するのが最も単純な選択肢だが、$A \to B$ が使う予約名 _ は例外にして、決して文脈に加えないようにしなければならない。
2. 文脈に入るときに改名する。$\Freshen$ がこれであり、本書の選択でもある。
3. 束縛変数を位置で表す（de Bruijn インデックス [de Bruijn 1972]）か、locally nameless 方式を使う。後者では束縛変数はインデックスで表し、自由変数は一意な識別子を持ち、Lean 4 は後者の方式を採る。

テストスイートには上の $t$ を含め、カーネルがそれを拒否するか、正しい型を割り当てるかを確認すべきである。

α 同値

束縛変数の名前には意味がなく、$\tLam{x}{A}{x}$ と $\tLam{y}{A}{y}$ は同じ関数であり、$\tPi{P}{\Sort{0}}{P \to P}$ と $\tPi{Q}{\Sort{0}}{Q \to Q}$ は同じ命題である。束縛変数の名前だけが異なる項を α 同値（alpha-equivalent）であるという。カーネルは型を単なる構文的な等しさで比較するわけにはいかず、それでは後者の組が拒否されてしまう。

（合同関係（congruence）とは、すべての項構成子で保たれる同値関係である。部分どうしが関係にあれば、全体どうしも関係にある。）この定義は述べるのは簡単だが、どの名前を選ぶべきかを言っていないので、そのままでは実行できない。実装は代わりに両方の項を足並みをそろえてたどり、それぞれの側で、ここまでに通過した束縛子のリストを覚えておく。束縛変数はこうして、名前ではなくどの束縛子を指しているかで識別される。

この走査を記述するために、$E_1; E_2 \vdash s \alphaeq t$ という形の判断を使う。$E_1$ と $E_2$ は名前のリストで、$E_1$ は $s$ を囲む束縛子を外側から内側の順に記録し、$E_2$ は $t$ を囲む束縛子を記録する。この判断は「束縛子 $E_1$ の内側に置かれた $s$ と、束縛子 $E_2$ の内側に置かれた $t$ は、束縛変数の名前を除いて同じ項である」と読む。リストが二つ必要なのは、対応する束縛子に二つの項が異なる名前を使うかもしれないからだ。たとえば $\tLam{x}{A}{\tLam{y}{B}{x}}$ と $\tLam{a}{A}{\tLam{b}{B}{a}}$ の比較では、各側で二つの束縛子を通過して

に到達し、$x$ と $a$ はどちらも二つの束縛子のうち外側を指すので、これは成り立つ。二つの項全体の比較は、空のリスト $\cdot\,;\cdot \vdash s \alphaeq t$ から始まる。

「同じ束縛子」を正確に言うために、$\mathrm{idx}(E, x)$ を、$E$ における $x$ の最後の出現の位置を右から $0$ 始まりで数えたものとし、$x \notin E$ なら未定義とする。上の例では $\mathrm{idx}((x, y), x) = \mathrm{idx}((a, b), a) = 1$ である。最後の出現を取ることでシャドーイングが扱え、$\tLam{x}{A}{\tLam{x}{B}{x}}$ の本体は内側の $x$ を指す。

自由変数は名前で比較し（$\alpha$-Free）、束縛変数は位置で比較し（$\alpha$-Bound）、定数は名前で比較する（$\alpha$-Const）。一方で束縛され他方で自由な変数は何とも等しくならないので、その場合の規則はない。両側は束縛子を一緒に下っていくので、$E_1$ と $E_2$ の長さは常に等しいので、右から数えた位置の比較は左から数えた位置の比較と同じであり、実装は各リストを名前から束縛の深さへの写像として保持してもよい。ただし束縛子を抜けるときには以前の項目を復元する必要がある。名前の代わりに位置をあらゆる場所で使うと de Bruijn 表現になり、そこでは α 同値な項は構文的に同一である。

例

第 6 章の最初の例は、推論した型と宣言された型の比較で終わった。ここで $P \to P$ は $\tPi{\_}{P}{P}$ の略記である。

• $\cdot\,;\cdot \vdash \tPi{P}{\Sort{0}}{\tPi{h}{P}{P}} \alphaeq \tPi{P}{\Sort{0}}{\tPi{\_}{P}{P}}$ $\alpha$-Pi
  • $\cdot\,;\cdot \vdash \Sort{0} \alphaeq \Sort{0}$：成立 $\alpha$-Sort
  • $P;\, P \vdash \tPi{h}{P}{P} \alphaeq \tPi{\_}{P}{P}$ $\alpha$-Pi
    • $P;\, P \vdash P \alphaeq P$：成立。どちらもインデックスは $0$ $\alpha$-Bound
    • $P, h;\; P, \_ \vdash P \alphaeq P$：成立。どちらもインデックスは $1$ $\alpha$-Bound

名前 $h$ と $\_$ は異なるが、どちらも一度も引かれないので問題にならない。第 6 章の誤った証明は、代わりに最後のステップで失敗する。

• $\cdot\,;\cdot \vdash \tPi{P}{\Sort{0}}{\tPi{h}{P}{\Sort{0}}} \alphaeq \tPi{P}{\Sort{0}}{\tPi{\_}{P}{P}}$ $\alpha$-Pi
  • $\cdot\,;\cdot \vdash \Sort{0} \alphaeq \Sort{0}$：成立 $\alpha$-Sort
  • $P;\, P \vdash \tPi{h}{P}{\Sort{0}} \alphaeq \tPi{\_}{P}{P}$ $\alpha$-Pi
    • $P;\, P \vdash P \alphaeq P$：成立 $\alpha$-Bound
    • $P, h;\; P, \_ \vdash \Sort{0} \alphaeq P$：適用できる規則がない

位置は、名前の不注意な比較では混同してしまう項も区別する。$\tLam{x}{A}{\tLam{y}{A}{x}}$ と $\tLam{a}{A}{\tLam{b}{A}{b}}$ は α 同値ではなく、本体の比較は $x, y;\, a, b \vdash x \alphaeq b$ に到達して、$\mathrm{idx}$ は $x$ に $1$、$b$ に $0$ を与える。逆に $\tLam{x}{A}{\tLam{x}{A}{x}}$ と $\tLam{a}{A}{\tLam{b}{A}{b}}$ は α 同値であり、$(x, x)$ における $x$ の最後の出現のインデックスは $0$ で、$(a, b)$ における $b$ と同じである。

図 11.1 の規則は定義 11.3 とは別の定義なので、両者が一致することを確かめなければならない。

証明の要点は、どちらの定義も「$s$ と $t$ が同じ de Bruijn 表現を持つ」と言い換えられることである。アルゴリズムの規則は de Bruijn インデックスと同じ方法で位置を比較しているので、この言い換えはほぼ直接に分かる。一方、定義 11.3 については、束縛変数を改名しても de Bruijn 表現が変わらないことを示す必要がある。完全な証明は 付録 B にある。

演習