[1] To keep the notation of lambda expressions uncluttered, the following conventions are usually applied.
and is defined by recursion on the structure of the terms, as follows: An expression that contains no free variables is said to be closed.
Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.
Alpha-conversion, sometimes known as alpha-renaming,[7] allows bound variable names to be changed.
Frequently in uses of lambda calculus, α-equivalent terms are considered to be equivalent.
Second, alpha-conversion is not possible if it would result in a variable getting captured by a different abstraction.
η-reduction expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments.
A lambda expression that cannot be reduced further, by either β-redex, or η-redex is in normal form.
All normal forms that can be converted into each other by α-conversion are defined to be equal.
See the main article on Beta normal form for details.
The approach is analogous to what a compiler does, but has been adapted to work within the constraints of mathematics.
The execution of a lambda expression proceeds using the following reductions and transformations, where, Execution is performing β-reductions and η-reductions on subexpressions in the canonym of a lambda expression until the result is a lambda function (abstraction) in the normal form.
The set of free variables of a lambda expression, M, is denoted as FV(M).
The set of bound variables of a lambda expression, M, is denoted as BV(M).
[5] Usage; This mathematical definition is structured so that it represents the result, and not the way it gets calculated.
Running or evaluating a lambda expression L is, where Q is a name prefix possibly an empty string and eval is defined by, Then the evaluation strategy may be chosen as either, The result may be different depending on the strategy used.
Eager evaluation will apply all reductions possible, leaving the result in normal form, while lazy evaluation will omit some reductions in parameters, leaving the result in "weak head normal form".
This is the result obtained from applying eager evaluation.
In all other cases, (The definition below is flawed, it is in contradiction with the definition saying that weak head normal form is either head normal form or the term is an abstraction.
This is the result obtained from applying lazy evaluation.
The lambda abstraction operator, λ, takes a formal parameter variable and a body expression.
Also note that a variable is bound by its "nearest" lambda abstraction.
For example the previous rules would have wrongly translated, The new rules block this substitution so that it remains as, The meaning of lambda expressions is defined by how expressions can be transformed or reduced.
Alpha-conversion, sometimes known as alpha-renaming,[7] allows bound variable names to be changed.
Note that the substitution will not recurse into the body of lambda expressions with formal parameter
See example; β-reduction captures the idea of function application (also called a function call), and implements the substitution of the actual parameter expression for the formal parameter variable.
If no variable names are free in the actual parameter and bound in the body, β-reduction may be performed on the lambda abstraction without canonical renaming.
See example; Alpha rename inner, x → a, y → b In this example, η-reduction expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments.
η-reduction may be used without change on lambda expressions that are not canonically renamed.
The problem with using an η-redex when f has free variables is shown in this example, This improper use of η-reduction changes the meaning by leaving x in