Подстановка

Подстановка терма v вместо всех свободных вхождений переменной x в терм u обозначается

u [ x := v ]

и определяется так:

• x [ x := v ] ≡ v
• y [ x := v ] ≡ y, если x y
• (λy.u) [ x := v ] ≡ λy.(u [ x := v ]), если x y и y ∉ FV(v).
  В противном случае, если x ≡ y, считаем, что подстановка ничего не даёт, т.е. даёт результат, совпадающий с исходным термом.
• (u w) [ x := v ] ≡ (u [ x := v ]) (w [ x := v ])

Если хоть одна переменная в поставляемом терме v должна стать связанной, то мы не имеем права применять подстановку.