「どぶらうん」と読む

ラムダ計算で変数名を使わずに変数を参照する方法

引数の出現順番に合わせて、その順番を引数名にする感じ

見づらいが簡素に書けるのが嬉しい

Nicolaas Govert de Bruijnが発明

例

λx.x は λ.0

λxy.yx は λ.λ.1 0

変換手順

示すまでもないが

元のラムダ式の変数名を自然数に順番に変える

λxy.yx → λ0.λ1.01

特殊なα変換をしている

λ にある数値を消す

λ0.λ1.01 → λ.λ.01

自由変数を含む場合

出現する自由変数に予め記号と数値の対応を定義しておく

\Gamma=x\to2,y\to1,z\to0

出現する束縛変数の個数に↑を足して変数を表現する

例

λw.yw は束縛変数は w の一つなので\Gammaに1足して、 y は 2 になるので λ.2 0

λw.λa.x は束縛変数は2つなので、\Gammaに2足して、 x は 4 になるので λ.λ.4

代入操作

indexが1ずれる

ref pp.59-60

関数適用

数値を更新する必要がある

ref pp.60-61

参考