lambda.arc

某所で上手いと話題になっていた lambda.arc 読んでみました。最初何が上手いのかわかりませんでしたけど、たぶん代入で変数捕捉回避するところのことですね。

 (\lambda x. M)[y := N] = \lambda u. (M[x := u][y := N])

と。ついでに同時代入にしてます。

このあたりの定義は本によっていくらか差があると思うんですが、手元のテキストだと捕捉が起きないときはそのまま代入、起きるときは上のようなやり方(逐次代入)という定義になってました。原理的にはこの場合分けはなくても何の問題もありませんが、わざわざそんなことを書くのは「変数捕捉を回避するための名前換えだから、捕捉が起きないとわかっているときは必要ないんだよ」という著者のメッセージなのでしょうかね。