α-конверсия и α-конгруэнтные термы

λx.uα λy.u [ x := y]
где y ∉ FV(u) ∪ BV(u), т.е. y не является ни свободной, ни связанной в u.
(α-конверсия)

α-конверсия позволяет переименовывать связанные переменные. Полученные с её помощью термы называется α-конгруэнтными.

Примеры

β-конверсия

x.u) vβ u [ x := v ] (β-конверсия)

Как следует из определения подстановки, β-конверсию нельзя применять без оговорок, поскольку при постановке в терм u терма v свободная переменная в v может оказаться связанной. Такая ситуация называется

Для преодоления этого конфликта