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

  1. Внешние скобки не пишутся.
  2. λx1...xn.u ≡ (λx1.(λx2. ...(λxn.(u)) ...)
    - λ "действует" до конца выражения или до закрывающий скобки.
  3. u v1 ... vn ≡ (...((u v1) v2) ... vn)
    - левая ассоциативность аппликации.
  4. Будем использовать буквы из конца латинского алфавита:
  5. Знак ≡ означает конгруэнтность - синтаксическое равенство или "по определению" (с точностью до соглашений 1-4 выше).