Синтаксис термов

Как в математике невероятное количество направлений — анализ, ТФКП и т. д. — держится на нескольких аксиомах, которые принимаются на веру, так и в λ-исчислении всего три конструкции являются основой. Весь язык строится из переменной, абстракции и аппликации; всё остальное — числа, логика, структуры данных и рекурсия — появляется уже поверх них.

Λ  ::=  x  ∣  (λx. M)  ∣  (M N)\Lambda \;\mathrel{\text{::=}}\; x \;\mid\; (\lambda x.\,M) \;\mid\; (M\,N)
(1.1)

где xx — переменная; (λx. M)(\lambda x.\,M) — абстракция: анонимная функция с параметром xx и телом MM; (M N)(M\,N) — аппликация: применение функции MM к аргументу NN. При этом NN может быть любым термом: переменной xx, другой аппликацией (P Q)(P\,Q) или целой абстракцией (λy. y)(\lambda y.\,y). Например: M xM\,x, M (P Q)M\,(P\,Q), M (λy. y)M\,(\lambda y.\,y).

Несколько важных замечаний: аппликация лево-ассоциативна: M N PM\,N\,P​≡((M N) P){} \equiv ((M\,N)\,P); тело абстракции простирается максимально вправо: λx. M N\lambda x.\,M\,N​≡λx. (M N){} \equiv \lambda x.\,(M\,N); цепочка абстракций сокращается: λx y z. M\lambda x\,y\,z.\,M​≡λx. λy. λz. M{} \equiv \lambda x.\,\lambda y.\,\lambda z.\,M.

Терм — это дерево: листья — переменные, внутренние узлы — абстракции и аппликации. Полезно приучить себя видеть терм как дерево, а не как строку.