K正規化とα変換のよくわかっていないメモ

自分はあたまがそれほど良くないのでスパイラル的に何度も見て覚えるしかないなぁと思ってます。
なんとなくわかってるんだけど、詳細がよくわからない。
作って見ればいいのかもしれないけど、作れる自信がない。

結局うわべだけなめて、細かいところまで見てないからなんだろうなぁ。
ということで、細かく読んでみてます。

K正規化は式を単純なものに置き換える処理です。
なので、K正規化された式はネストしている部分が少なくなります。
最初にその恩恵を受けるのがα変換です。

α変換でやっていることはletを受け取って
変数xにxdashという新しい名前を付けて、新しい名前が入っている環境を次の式以降に渡して変換を
続けるということです。

		case Let((x, t), e1, e2) => // letのα変換 (caml2html: alpha_let)
			val xdash = Id.genid(x);// 新しい名前を作成
			Let((xdash, t), g(env, e1), g(env + (x -> xdash), e2))

で、さらにlet recとかは同じことを複雑にしたものらしいので今回はスルーします。

K正規化のKはletを挿入する処理に渡す関数のことみたいです。
新しい環境は書き換え不能なMapに値を１つだけ追加したものとして env + (x -> xdash)って書けるので
非常にうれしいかんじです。