アルファ変換

ラムダ計算においては束縛変数の名前は重要でないと考えられる。

たとえば

λx.x

と

λy.y

は同じ関数を表わしているといえる。

ゆえに、あるラムダ式と他のラムダ式との折り合いをつける時などに上記のようにその束縛変数の名前を変更する規則が必要であり、それをアルファ変換という。

基本的には、普通の数式で使われている変数の文字を別の文字に変えるという作業と同じである。

しかし普通の数式の場合にも言えることだが、変数の名前を変更することで式の意味が変わっては困る。

複数のラムダ項で構成されるラムダ式などの場合、変換する変数以外の束縛変数(表記上ラムダの直後に来る変数)の名前や、そのラムダ項に変換する変数以外で元から存在する変数の名前などは使用できない。

この制限は常識的なことではあるが、ラムダ式では直感的にそれを把握することが難しい場合もあるので注意が必要である。