\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'などと書く

これだけ読むと難しそうだが、プログラマが自明に扱っている様な概念である

α変換では束縛変数の方を置き換えるのはなんでか

β簡約した結果が変わるため

例えば(((\lambda x.(\lambda y.(yx)))y)z)を簡約することを考える

簡約した答えは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が、何らかのα変換で互いに変換可能な場合に、これらはα同値であると言う