Term syntax

Just as in mathematics an incredible number of fields — calculus, complex analysis, and so on — rest on a handful of axioms taken on faith, in the λ-calculus just three constructs form the foundation. The entire language is built from the variable, the abstraction, and the application; everything else — numbers, logic, data structures, and recursion — appears on top of them.

Λ  ::\displaystyle \Lambda \;:: =  x    (λx.M)    (MN)\displaystyle =\; x \;\mid\; (\lambda x.\,M) \;\mid\; (M\,N)
(1.1)

where xx is a variable; (λx.M)(\lambda x.\,M) is an abstraction: an anonymous function with parameter xx and body MM; (MN)(M\,N) is an application: the function MM applied to the argument NN. Here NN may be any term: a variable xx, another application (PQ)(P\,Q), or a whole abstraction (λy.y)(\lambda y.\,y). For example: MxM\,x, M(PQ)M\,(P\,Q), M(λy.y)M\,(\lambda y.\,y).

A few important remarks: application is left-associative: MNPM\,N\,P ((MN)P)\equiv ((M\,N)\,P); the body of an abstraction extends as far to the right as possible: λx.MN\lambda x.\,M\,N λx.(MN)\equiv \lambda x.\,(M\,N); a chain of abstractions is abbreviated: λxyz.M\lambda x\,y\,z.\,M λx.λy.λz.M\equiv \lambda x.\,\lambda y.\,\lambda z.\,M.

A term is a tree: the leaves are variables, the inner nodes are abstractions and applications. It is worth training yourself to see a term as a tree rather than as a string.