間違ってるかもしれないけど

ラムダ抽象

f(x)=x+1 -> (λx.(x+1))

カリー化

f(x,y,z)=x+y+z -> (λx.(λy.(λz.(x+y+z))) 多変数の関数を１変数の高階関数として表すこと

α変換

(λx.(x+1)) -> (λy.(y+1)) 束縛変数の交換

β基

(λx.M) NのうちNのこと？

β変換

(λx.(x+1))(λx.(x*2)) -> (λx.(x*2))+1 β基を代入する動作

正規化

β変換を有限回繰り返しβ基を持たないλ項にすること