Заміна
Зміни, написані Е [V: = R], являють собою процес заміщення всіх вільних входжень змінної V у вираженні Е з обігом R. Підстановка в термінах λ визначається лямбдой обчислення рекурсії за структурою понять наступним чином (примітка: x і y – тільки змінні, а M і N – будь-яке λ-вираз).
x [x: = N] ≡ N
y [x: = N] ≡ y, якщо x ≠ y
(M 1 M 2) [x: = N] ≡ (M 1 [x: = N]) (M 2 [x: = N])
(λ x.M) [x: = N] ≡ λ x.M
(λ y.M) [x: = N] y λ y. (M [x: = N]), якщо x ≠ y, за умови, що y ∉ FV (N).
Для підстановки в лямбда-абстракцію іноді необхідно α-перетворити вираз. Наприклад, невірно, щоб (λ x. Y) [y: = x] призводило до (λ x. X), тому що замещенный x повинен був бути вільним, але в підсумку був пов’язаним. Правильна заміна у цьому випадку (λ z. X) з точністю до α-еквівалентності. Варто звернути увагу, що заміщення визначається однозначно з вірністю до лямбды.
