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

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

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

Примеры

λx.x z →_α λy.y z, но λx.x z _α λz.z z
- замена связанной переменной x на y.
λx.x (λx.x) →_α λy.y (λx.x) →_α λy.y (λz.z)

β-конверсия

(λx.u) v →_β u [ x := v ]

(β-конверсия)

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

терм v не свободен для подстановки в u вместо х,
смешение локальных и глобальных переменных (программирование).

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

либо свободные переменные в v должны отличаться от переменных, встречающихся в u,
либо делается переименование связанных переменных в u, так чтобы они отличались от свободных переменных в v (α-конверсия).