6. Nameless Representation of Terms

5章 The Untyped Lambda-Calculusで束縛変数の名前は自由に書き換えてよいという話をしたけれど、さてそれをどうすれば実現できるか？　という話。人間がこれに取り組むのであれば直感によって新たな名前を考案すればよいが、もちろんここの手順を厳密に定義したい。

いろいろ方法は挙げられているけれど、この章では、項から変数の名前を取り去った形に項を正規化することで、そもそも名前の書き換えを不要にする、という方法を採る。

6.1 Terms and Contexts

De Brujin の方法では、束縛変数がそれから外側に数えて何番目のλによって導入されたか、という番号で表す（\(λ.λ.1 (0 1)\) など）。そうして表され名前なしとなった項を De Brujin Term、番号を De Brujin Index と呼ぶ。

自由変数を扱えるようにするために、naming context \(\Gamma\) というものを導入する。これは変数名から de Brujin index への対応である。

Ex. 6.1.5

項を無名化する \(removenames\) と名前なし項に名前をつける \(restorenames\) を定義する。例によって工夫がいるのはラムダ抽象のパート。restorenames を定義するには、ラムダ抽象で束縛される変数名を作り出す操作が必要になる。ここではあり得る変数名の集合が順序付けられていて、\(\Gamma\) 中の変数名が互いに異なる［この条件が何に効くのかよくわからない］と仮定して、\(\Gamma\) の定義域に含まれていない変数名を選び出す、という操作が可能だということにしてよい。

removenames

\[\begin{eqnarray} removenames_\Gamma (x) \; &=& \Gamma(x) \\ removenames_\Gamma (t_1 \; t_2) \; &=& removenames_\Gamma(t_1) \; removenames_\Gamma(t_2) \\ removenames_\Gamma (λx.t) \; &=& λ.removenames_{\Gamma'}(t) \\ && \; \mathrm{where} \; \Gamma' = \{ x \mapsto 0, \Gamma(0) \mapsto 1, \dots \} \end{eqnarray}\]

restorenames

\[\begin{eqnarray} restorenames_\Gamma (n) \; &=& \Gamma^{-1} (n) \\ restorenames_\Gamma (n \; m) \; &=& restorenames_\Gamma(n) \; restorenames_\Gamma(m) \\ restorenames_\Gamma (λ.t) \; &=& λx.restorenames_{\Gamma'}(t) \\ & & \mathrm{where} \; x \not \in \mathrm{dom}(\Gamma) \\ && \Gamma' = \{ x \mapsto 0, \Gamma(0) \mapsto 1, \dots \} \end{eqnarray}\]

6.2 Shifting and Substitution

次は書き換え \([k \mapsto s] t\) を名前なし項において定義する。書き換えがラムダ抽象の中に及ぶときには、書き換え先の項を包むλの数が1だけ増えるので、自由変数のインデックスにも1を加えてやる（1だけシフトする）必要がある。例えば、\([1 \mapsto s](λ. 2)\) （\([x \mapsto s](λy.x)\)）では、書き換え後の \(s\) はそれを包むλの数が1だけ多い。

ただし束縛変数のことを考えると、無条件にインデックスをシフトさせることはできない。例えば、\(s = 2 \; (λ.0)\) （\(s = z \; (λw.w)\)）のうち 2 をシフトするのはよいが 0 をシフトするとおかしい。

結局シフト関数 \(↑^d_c(-)\) は「インデックスにいくつだけ加えるか」と「いくつ未満のインデックスはシフトしないか」の2つのパラメータを持つことになる。

Ex. 6.2.8

名前なし項における書き換えの定義は、名前ありの項における書き換えの定義と一致していなければいけない。(1) そのために示されるべき定理はなにか？ (2) 証明せよ。

ある書き換えを行ってから無名化した時と、無名化してから書き換えをおこなった時とで同じ結果が得られること。
省略。

6.3 Evaluation

名前なし項の評価をおこなえるようにするにはベータ簡約のルールを新たに決めればよい。今回は簡約後にλの数が減るので、インデックスを減らす必要がある。先ほどのシフト関数が \(↑^{-1}\) という形でそのまま利用できる。

\((λ.1 \; 0 \; 2) \; (λ.0)\) は \(0 \; (λ.0) \; 1\) に簡約される。\(1\; (λ.0) \; 2\) でないことに注意。