variable)という。ある変数の出現が自由出現であるかどうかは、より正確には以下のように帰納的に定義されている。以外のものが自由出現である。ラムダに束縛されたという。自由出現の和が自由出現である。書くことにする)は、直感的には、2つのラムダ式が同じ関数を表していることである。この同値関係は以下で述べるα-変換とβ-簡約によって定義される。第3の規則としてη-変換と呼ばれる規則が導入されることもある。α-変換編集アルファ変換の基本的なアイデアは、束縛変数の名前は重要ではない、ということにある。同じ関数を表している。ことはそう単純ではない。ある束縛変数の名前を置換してもよいかどうかには、いくつかの規則が絡んでくる。なるが、これは最初の式とはまったく異なるものを表すことになる。W]と書くことにする。束縛されることがないときに限る。変換されることがわかる。β-簡約編集ベータ簡約(ベータ変換とも)の基本的なアイデアは、関数の適用である。ベータ簡約は以下の変換である。中の自由変数が新たに束縛されることがないときに限る。上の2つの規則を含む最小の同値関係(同値閉包)である。ベータ簡約は、(同値関係ではなく)左辺から右辺への一方的な変換であると見ることもできる。form)であるという。上に挙げた2つの規則の他に、第3の規則としてイータ変換が導入されることがある。イータ変換の基本的なアイデアは、関数の外延性である。ここでいう外延性とは、2つの関数が全ての引数に対して常に同じ値を返すようなとき、互いに同値であるとみなすという概念である。イータ変換は以下の変換である。自由出現しないときに限る。この同値性は関数の外延性という概念によって以下のように示される。