http://en.wikipedia.org/wiki/De_Bruijn_index 簡約時のα変換不要にするラムダ式の変数表現法 λx.λy.x → λ λ 2 λu.λv.((λx.λy.x) u v) → λλ((λλ2) 2 1) => λλ((λ3) 1) => λλ2 その式の内側から数えたλのインデックスで変数名を表現する。β変換では 適用する…