Соглашения и обозначения

1. Внешние скобки не пишутся.
2. λx₁...x_n.u ≡ (λx₁.(λx₂. ...(λx_n.(u)) ...)
   - λ действует до конца выражения или до закрывающий скобки.
3. u v₁ ... v_n ≡ (...((u v₁) v₂) ... v_n)
   - левая ассоциативность аппликации.
4. Будем использовать буквы из конца латинского алфавита:
   • курсивные u, v, w, t₁, t₂ - произвольные λ-термы,
   • курсивные x, y, z, иногда с индексами - произвольные переменные,
   • прямым шрифтом x, y, z - конкретные переменные в примерах.
5. Знак ≡ означает конгруэнтность - синтаксическое равенство или по определению (с точностью до соглашений 1-4 выше).