The Lambda Calculus was developed by Alonzo Church in the 1930s and published in 1941 as ‘The Calculi Of Lambda Conversion’. It became important, along with Turing machines, in the development of computation theory, and is the theoretical basis of all functional programming languages, such as Lisp, Haskell and ML.
Functions in lambda calculus are very different from those in imperative programming languages (such as Java and C). In an imperative programming language the evaluation of a function can have side effects, affecting future evaluations of that function or other functions. In lambda calculus a function does not ‘return’ a result based on its parameters — instead the function and its parameters are ‘reduced’ to give an answer, which mathematically is equivalent to the question.
The following paragraphs give an informal description of lambda calculus — a formal description of lambda calculus is also available.
A function in lambda calculus is wriiten in the form λx.E, where x is the function’s parameter and E is a lambda expression constituting the function body. A lambda expression is either a variable (like the x in the above expression), a function in the form above, or an application E1E2.
In the expression λx.E, any occurance of x in E is ‘bound’, while any other variable is ‘free’ (unless bound by another lambda expression, like the y in λx.λy.xy). A ‘pure’ lambda expression has no free variables.
Three things can be done with lambda expressions:
- α conversion
- Alpha conversion renames a bound variable — λx.x can be alpha converted to λy.y.
- β reduction
- Beta reduction allows applications to be reduced — (λx.E1)E2 can be beta reduced to E1 with all occurances of x replaced with E2. If there are name clashes (for example in (λx.λy.xy)y), alpha conversion may be required first.
- η conversion
- Eta conversion allows us to say that f and λx.fx are equivalent.
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:
- λx1... ...xn.E means λx1... ...λxn.E
- fab means (fa)b