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は相対的なので注意すること
- シフト操作は案外簡単に書ける
- 技術ブログを書きたかった