α変換
alpha-conversion
$ \lambda x.xと$ \lambda z.zは同じだよね、
このような変換のことを$ \alpha変換という
つまり、束縛変数を別のものに入れ替えて全く同じ意味のラムダ抽象を作成する操作 名前の衝突を回避するときに使う
$ \lambda x.(y\lambda y.yx)のように、同じyでも、自由変数と束縛変数が混在していて読みづらい α変換を施し、別の文字を使った同値の式にする
例えば$ \lambda x.(y\lambda z.zx)
このとき$ \lambda x.(z\lambda y.yx)のように自由変数の方を置き換えない。
α変換では束縛変数の方を置き換える
定義
ラムダ式$ \lambda x.Mの部分項$ Mの自由変数$ xを、
$ Mの中に部分項として現れない変数$ yに置き換えて$ M'が得られたとき
$ \lambda x.Mと$ \lambda y.M'を同一視し、
$ \lambda x.N \equiv_\alpha \lambda y.N'などと書く
これだけ読むと難しそうだが、プログラマが自明に扱っている様な概念であるmrsekut.icon
α変換では束縛変数の方を置き換えるのはなんでか
例えば$ (((\lambda x.(\lambda y.(yx)))y)z)を簡約することを考える
簡約した答えは$ zyだが、
$ ((\lambda x.(\lambda y.(yx)))y)z\equiv_\alpha((\lambda x.(\lambda w.wx))y)z\to_\beta (\lambda w.wy)z\to_\beta zy
自由変数の方を置き換えると$ wyとかになってしまう
$ wは$ x,y,z以外の任意の変数
$ \alpha変数ではない変換
$ \lambda x.xzの
$ xを$ zに変えて、$ \lambda z.zzとする
$ \lambda x.xz\not\equiv_\alpha\lambda z.zzなのでα変換ではない
ラムダ抽象$ M,Nが、何らかのα変換で互いに変換可能な場合に、これらはα同値であると言う