α-перетворення
Альфа-перейменування дозволяють змінювати імена пов’язаних змінних. Наприклад, λ x. х може дати λ у. у. Терміни, які відрізняються тільки альфа-перетворенням, називаються α-еквівалентними. Часто при використанні лямбда-числення α-еквівалентні вважаються взаємними.
Точні правила для альфа-перетворення не зовсім тривіальні. По-перше, при даної абстракції перейменовуються тільки ті змінні, які пов’язані з однією і тією ж системою. Наприклад, альфа-перетворення λ x.λ x. x може призвести до λ y.λ x. х, але це може не призвести до λy.λx.y Останній має інший зміст, ніж оригінал. Це аналогічно поняттю програмування затінення змінних.
По-друге, альфа-перетворення неможливо, якщо воно призведе до захоплення непостійною інший абстракцією. Наприклад, якщо замінити x на y λ x.λ y. x, то можна отримати λ y.λ y. у, що зовсім не те ж саме.
У мовах програмування зі статичною областю видимості альфа-перетворення можна використовувати для спрощення дозволу імен. При цьому стежачи за тим, щоб поняття змінної не маскувало позначення, що містить області.
У нотації індексу Де Брюйна будь-які два альфа-еквівалентних терміна синтаксично ідентичні.
