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