型なしλ計算の実装

ISBN:0262162091 の 6章「Nameless Representation of Terms」を読んだ。
この章には、λ式の変数を自然数に置き換えても読みづらいけど
意味は変わらないよねということが書いてあった。

具体的には、

λx.λy. x (y x)

というλ式は、

λ.λ. 1 (0 1)

という式に書き換えられるという話。

ちなみに、De Brujinって人のアイディアなので下の表現を de Brujin termsと言うらしい。
そのまんまの名前ですねorz

この表現式でλ式を扱うとプログラムで扱い易くなるので良い。（らしい）

で、次の7章がMLで型なしλ計算を実装しようという話。
解説はMLでされてるのだが、なんとなくC#（しかも、2.0）で書いてみた。
しかし、Substitutionを実装したあたりで眠くなり中断。（つづく