d

Formal Description Of Lambda Calculus

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:

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:

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.E1)E2 is equivalent to E1[V|E2] if all free variables in E2 are free in E1[V|E2].

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: