de Bruijn indexについての備忘録
型システム入門で，de Bruijn indexの話で少しつまづいたのでメモ．型なしラムダ計算を前提とします．
de Bruijn index
de Bruijn index（ど・ぶらん・いんでっくす）とは，変数名として文字列ではなく，番号を振ってやることで表現を簡潔にしたものであり，ある場所に出現する変数が，どれほど外側で束縛されているかを表す数のこと．
言葉では分かりづらいので，次の図で．
- 青い矢印
- 対応する項
- 赤い矢印
- 束縛している場所
要点は，
- いくつ外側のλで束縛された変数かを意味するため，出現する場所により同じだった変数でもindexが変わる．
- 囲まれたλの個数以上のindexは，自由変数を表す．
- つまり，相対的な表記法である．（代入操作において重要）
あと，型システム入門p.57に，
この方法による実装が間違っている場合、微妙に失敗するのではなく壊滅的に失敗する傾向がある
とあることも，de Bruijn項を使用する利点と思われる．
代入操作
ある項tのあるindex jを，他の項sで置き換える操作（[ j ↦ s ] t）は，関数の適用の時に用いられる．
しかし，ある一つのラムダ抽象の外部と内部では，indexが1ほど変化するため，sの中のindexを付け替える作業が必要となる．
ただ，考えなしにsに出現するindexをすべて置き換えるわけにはいかない．sの中で束縛されているものを付け替えるとおかしくなる．よってsの自由変数に限ってindexを付け替える．
付け替え自体は簡単で，根元からたどっていき，出現したラムダ抽象の数と同じ以上のindexが出現した際に，1を足せば良い．これをシフト操作と呼ぶ．
シフト操作をもうすこしパラメタライズすると，dをシフトする数（負の数もあり得る），cを根元から見て出現したラムダ抽象の数，転じて，ある数以上のインデックスをシフトさせるかを表す指標となる．
代入操作自体は再帰的に記述できる．ラムダ抽象に入るとき，sをシフトすることを忘れないでおけばよい．もちろん，合致するインデックスが現れた時には置換するが，そこでは単純に置き換えれば良いようだ．
関数適用
疲れてきた．つまり，E-AppAbsを適用する時（(λ. t) v の評価）は，
- vをラムダ抽象の中に放り込むので，1だけシフトする．
- tの中の，index 0にvを代入する．
- すると，ラムダ抽象の内部にあったtを無理矢理引っ張りだしたことになっているため，置き換えた結果を-1だけシフトする．
という流れになる．
まとめ
- indexは相対的なので注意すること
- シフト操作は案外簡単に書ける
- 技術ブログを書きたかった
