The following paragraphs give a formal description of lambda calculus — an informal introduction to lambda calculus is also available.
Given a countably infinite set of variable names, a lambda expression <expr> matches one of the following BNF productions:
- <expr> = <variable>
- <expr> = (λ<identifier>.<expr>)
- <expr> = (<expr><expr>)
The brackets in the second and third production are usually omitted if there is no ambiguity given that lambdas bind to the entire following expression and that application is left associative.
Bound and free variables are defined by induction on the productions above:
- In V (where V is a variable name), V is free
- In (λV.E) the free variables are those in E that are not V — occurances of V in E are bound by the preceding lambda
- In (E_{1}E_{2}) the free variables are those free in either E_{1} or E_{2}
If V and W are variables and E is a lambda expression, E[V|W] means E with every free occurance of V replaced by W. Alpha conversion states that λV.E is equivalent to λW.E[V|W] if W does not occur freely in E and is not bound by a lambda wherever it replaces V.
Beta reduction states that (λV.E_{1})E_{2} is equivalent to E_{1}[V|E_{2}] if all free variables in E_{2} are free in E_{1}[V|E_{2}s].
Eta conversion states that λV.EV and E are equivalent if V doesn’t occur in E.
A lambda expression is in normal form if no sub-expression can be reduced. A lambda expression is in head normal form if the outermost application cannot be reduced. Some expressions do not have a normal form as reduction never terminates. Lambda calculus has the Church-Rosser property, so that if two methods of reduction lead to two normal forms, they can differ only by alpha conversion.
Two lambda expressions are equivalent if they can be beta reduced to the same expresion, subject to alpha conversion. Two lambda expressions are extensionally equivalent if they can be beta reduced and eta converted to the same expression, subject to alpha conversion.
Two shorthand notations are used:
- λx_{1}… …x_{n}.E means λx_{1}… …λx_{n}.E
- fab means (fa)b