Lambda calculus is a formal mathematical system based on lambda abstraction and function application. Two definitions of the language are given here: a standard definition, and a definition using mathematical formulas.
This formal definition was given by Alonzo Church.
Lambda expressions are composed of
v1
v2
vn
λ
The set of lambda expressions,
Λ
x
x\inΛ
x
M\inΛ
(λx.M)\inΛ
M,N\inΛ
(M N)\inΛ
To keep the notation of lambda expressions uncluttered, the following conventions are usually applied.
M N
(M N)
M N P
((M N) P)
λx.M N
λx.(M N)
(λx.M) N
λx.λy.λz.N
λxyz.N
The abstraction operator,
λ
y
x
λy.x x y
x
λx.y(λx.z x)
The set of free variables of a lambda expression,
M
\operatorname{FV}(M)
\operatorname{FV}(x)=\{x\}
x
\operatorname{FV}(λx.M)=\operatorname{FV}(M)\backslash\{x\}
\operatorname{FV}(M N)=\operatorname{FV}(M)\cup\operatorname{FV}(N)
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.
The meaning of lambda expressions is defined by how expressions can be reduced.[4]
There are three kinds of reduction:
We also speak of the resulting equivalences: two expressions are β-equivalent, if they can be β-converted into the same expression, and α/η-equivalence are defined similarly.
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example,
(λx.M) N
N
x
M
x
M
λx.M x
M[x:=N]
M
Alpha-conversion, sometimes known as alpha-renaming, allows bound variable names to be changed. For example, alpha-conversion of
λx.x
λy.y
The precise rules for alpha-conversion are not completely trivial. First, when alpha-converting an abstraction, the only variable occurrences that are renamed are those that are bound by the same abstraction. For example, an alpha-conversion of
λx.λx.x
λy.λx.x
λy.λx.y
Second, alpha-conversion is not possible if it would result in a variable getting captured by a different abstraction. For example, if we replace
x
y
λx.λy.x
λy.λy.y
In programming languages with static scope, alpha-conversion can be used to make name resolution simpler by ensuring that no variable name masks a name in a containing scope (see alpha renaming to make name resolution trivial).
Substitution, written
E[V:=R]
V
E
R
\begin{align} x[x:=N]&\equivN\\ y[x:=N]&\equivy,ifx ≠ y \end{align}
\begin{align} (M1 M2)[x:=N]&\equiv(M1[x:=N]) (M2[x:=N])\\ (λx.M)[x:=N]&\equivλx.M\\ (λy.M)[x:=N]&\equivλy.(M[x:=N]),ifx ≠ y,providedy\notinFV(N) \end{align}
To substitute into a lambda abstraction, it is sometimes necessary to α-convert the expression. For example, it is not correct for
(λx.y)[y:=x]
(λx.x)
x
(λz.x)
β-reduction captures the idea of function application. β-reduction is defined in terms of substitution: the β-reduction of
((λV.E) E')
E[V:=E']
For example, assuming some encoding of
2,7, x
((λn. n x 2) 7) → 7 x 2
η-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 converts between
λx.(fx)
f
x
f
See main article: Beta normal form. The purpose of β-reduction is to calculate a value. A value in lambda calculus is a function. So β-reduction continues until the expression looks like a function abstraction.
A lambda expression that cannot be reduced further, by either β-redex, or η-redex is in normal form. Note that alpha-conversion may convert functions. 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.
| Normal Form Type | Definition. | |
|---|---|---|
| Normal Form | No β- or η-reductions are possible. | |
| Head Normal Form | In the form of a lambda abstraction whose body is not reducible. | |
| Weak Head Normal Form | In the form of a lambda abstraction. |
Lambda Calculus has a simple syntax. A lambda calculus program has the syntax of an expression where,
| Name | BNF | Description | |
|---|---|---|---|
| Abstraction | Anonymous function definition. | ||
| Application term | |||
| Application | A function call. | ||
| Item | |||
| Variable | E.g. x, y, fact, sum, ... | ||
| Grouping | Bracketed expression. |
The variable list is defined as,
A variable as used by computer scientists has the syntax,
A lambda abstraction has a lower precedence than an application, so;
λx.y z=λx.(y z)
Applications are left associative;
x y z=(x y) z
An abstraction with multiple parameters is equivalent to multiple abstractions of one parameter.
λx.y.z=λx.λy.z
The problem of how variables may be renamed is difficult. This definition avoids the problem by substituting all names with canonical names, which are constructed based on the position of the definition of the name in the expression. 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,
\operatorname{alpha-conv}(a)\to\operatorname{canonym}[A,P]=\operatorname{canonym}[a[A],P]
\operatorname{beta-redex}[λp.b v]=b[p:=v]
x\not\in\operatorname{FV}(f)\to\operatorname{eta-redex}[λx.(f x)]=f
b[p:=v]
p
v
b
\operatorname{FV}(f)
f
All α-conversions of a λ-expression are considered to be equivalent.
Canonym is a function that takes a lambda expression and renames all names canonically, based on their positions in the expression. This might be implemented as,
\begin{align} \operatorname{canonym}[L,Q]&=\operatorname{canonym}[L,O,Q]\\ \operatorname{canonym}[λp.b,M,Q]&=λ\operatorname{name}(Q).\operatorname{canonym}[b,M[p:=Q],Q+N]\\ \operatorname{canonym}[X Y,x,Q]&=\operatorname{canonym}[X,x,Q+F] \operatorname{canonym}[Y,x,E+S]\\ \operatorname{canonym}[x,M,Q]&=\operatorname{name}(M[x])\end{align}
Where, N is the string "N", F is the string "F", S is the string "S", + is concatenation, and "name" converts a string into a name
Map from one value to another if the value is in the map. O is the empty map.
O[x]=x
M[x:=y][x]=y
x\nez\toM[x:=y][z]=M[z]
If L is a lambda expression, x is a name, and y is a lambda expression;
L[x:=y]
(λp.b)[x:=y]=λp.b[x:=y]
(XY)[x:=y]=X[x:=y]Y[x:=y]
z=x\to(z)[x:=y]=y
z\nex\to(z)[x:=y]=z
Note that rule 1 must be modified if it is to be used on non canonically renamed lambda expressions. See Changes to the substitution operator.
The set of free variables of a lambda expression, M, is denoted as FV(M). This is the set of variable names that have instances not bound (used) in a lambda abstraction, within the lambda expression. They are the variable names that may be bound to formal parameter variables from outside the lambda expression.
The set of bound variables of a lambda expression, M, is denoted as BV(M). This is the set of variable names that have instances bound (used) in a lambda abstraction, within the lambda expression.
The rules for the two sets are given below.
FV(M) | Comment | BV(M) | Comment | |
|---|---|---|---|---|
FV(x)=\{x\} | where x is a variable | BV(x)=\emptyset | where x is a variable | |
FV(λx.M)=FV(M)\setminus\{x\} | Free variables of M excluding x | BV(λx.M)=BV(M)\cup\{x\} | Bound variables of M plus x. | |
FV(M N)=FV(M)\cupFV(N) | Combine the free variables from the function and the parameter | BV(M N)=BV(M)\cupBV(N) | Combine the bound variables from the function and the parameter |
Usage;
This mathematical definition is structured so that it represents the result, and not the way it gets calculated. However the result may be different between lazy and eager evaluation. This difference is described in the evaluation formulas.
The definitions given here assume that the first definition that matches the lambda expression will be used. This convention is used to make the definition more readable. Otherwise some if conditions would be required to make the definition precise.
Running or evaluating a lambda expression L is,
\operatorname{eval}[\operatorname{canonym}[L,Q]]
where Q is a name prefix possibly an empty string and eval is defined by,
\begin{align} \operatorname{eval}[x y]&=\operatorname{eval}[\operatorname{apply}[\operatorname{eval}[x] \operatorname{strategy}[y]]]\\ \operatorname{apply}[(λx.y) z]&=\operatorname{canonym}[\operatorname{beta-redex}[(λx.y) z],x]\\ \operatorname{apply}[x]&=xifxdoesmatchtheabove.\\ \operatorname{eval}[λx.(f x)]&=\operatorname{eval}[\operatorname{eta-redex}[λx.(f x)]]\\ \operatorname{eval}[L]&=L\\ \operatorname{lazy}[X]&=X\\ \operatorname{eager}[X]&=\operatorname{eval}[X]\end{align}
Then the evaluation strategy may be chosen as either,
\begin{align} \operatorname{strategy}&=\operatorname{lazy}\\ \operatorname{strategy}&=\operatorname{eager}\end{align}
All reductions that can be applied have been applied. This is the result obtained from applying eager evaluation.
\begin{align} \operatorname{normal}[(λx.y) z]&=\operatorname{false}\\ \operatorname{normal}[λx.(f x)]&=\operatorname{false}\\ \operatorname{normal}[x y]&=\operatorname{normal}[x]\land\operatorname{normal}[y]\end{align}
\operatorname{normal}[x]=\operatorname{true}
(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.[5] The notion has been introduced by Simon Peyton Jones.[6])
Reductions to the function (the head) have been applied, but not all reductions to the parameter have been applied. This is the result obtained from applying lazy evaluation.
\begin{align} \operatorname{whnf}[(λx.y) z]&=\operatorname{false}\\ \operatorname{whnf}[λx.(f x)]&=\operatorname{false}\\ \operatorname{whnf}[x y]&=\operatorname{whnf}[x]\end{align}
\operatorname{whnf}[x]=\operatorname{true}
The standard definition of lambda calculus uses some definitions which may be considered as theorems, which can be proved based on the definition as mathematical formulas.
The canonical naming definition deals with the problem of variable identity by constructing a unique name for each variable based on the position of the lambda abstraction for the variable name in the expression.
This definition introduces the rules used in the standard definition and relates explains them in terms of the canonical renaming definition.
The lambda abstraction operator, λ, takes a formal parameter variable and a body expression. When evaluated the formal parameter variable is identified with the value of the actual parameter.
Variables in a lambda expression may either be "bound" or "free". Bound variables are variable names that are already attached to formal parameter variables in the expression.
The formal parameter variable is said to bind the variable name wherever it occurs free in the body. Variable (names) that have already been matched to formal parameter variable are said to be bound. All other variables in the expression are called free.
For example, in the following expression y is a bound variable and x is free:
λy.x x y
λx.y (λx.z x)
In the definition of the Substitution Operator the rule,
(λp.b)[x:=y]=λp.b[x:=y]
(λx.b)[x:=y]=λx.b
z\nex \to(λz.b)[x:=y]=λz.b[x:=y]
This is to stop bound variables with the same name being substituted. This would not have occurred in a canonically renamed lambda expression.
For example the previous rules would have wrongly translated,
(λx.x z)[x:=y]=(λx.y z)
The new rules block this substitution so that it remains as,
(λx.x z)[x:=y]=(λx.x z)
The meaning of lambda expressions is defined by how expressions can be transformed or reduced.[4]
There are three kinds of transformation:
We also speak of the resulting equivalences: two expressions are β-equivalent, if they can be β-converted into the same expression, and α/η-equivalence are defined similarly.
The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules.
Alpha-conversion, sometimes known as alpha-renaming, allows bound variable names to be changed. For example, alpha-conversion of
λx.x
λy.y
In an α-conversion, names may be substituted for new names if the new name is not free in the body, as this would lead to the capture of free variables.
(y\not\inFV(b)\landa(λx.b)=λy.b[x:=y])\to\operatorname{alpha-con}(a)
Note that the substitution will not recurse into the body of lambda expressions with formal parameter
x
See example;
| α-conversion | λ-expression | Canonically named | Comment | |
|---|---|---|---|---|
λz.λy.(z y) | λ\operatorname{P}.λ\operatorname{PN}.(\operatorname{P}\operatorname{PN}) | Original expressions. | ||
| correctly rename y to k, (because k is not used in the body) | λz.λk.(z k) | λ\operatorname{P}.λ\operatorname{PN}.(\operatorname{P}\operatorname{PN}) | No change to canonical renamed expression. | |
| naively rename y to z, (wrong because z free in λy.(z y) | λz.λz.(z z) | λ\operatorname{P}.λ\operatorname{PN}.({\color{Red}\operatorname{PN}}\operatorname{PN}) | z |
β-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. β-reduction is defined in terms of substitution.
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.
(\forallz:z\not\inFV(y)\lorz\not\inBV(b))\to\operatorname{beta-redex}[λx.b y]=b[x:=y]
Alpha renaming may be used on
b
y
b
See example;
| β-reduction | λ-expression | Canonically named | Comment | ||||||
|---|---|---|---|---|---|---|---|---|---|
(λx.λy.(λz.(λx.z x)(λy.z y))(x y)) | (λ\operatorname{P}.λ\operatorname{PN}.(λ\operatorname{PNF}.(λ\operatorname{PNFNF}.\operatorname{PNF}\operatorname{PNFNF})(λ\operatorname{PNFNS}.\operatorname{PNF}\operatorname{PNFNS}))(\operatorname{P}\operatorname{PN})) | Original expressions. | |||||||
| Naive beta 1, | (λx.λy.((λx.(x y)x)(λy.(x y)y))) |
| x (P) and y (PN) have been captured in the substitution. | ||||||
| Alpha rename inner,x → a, y → b | (λx.λy.(λz.(λa.z a)(λb.z b))(x y)) | (λ\operatorname{P}.λ\operatorname{PN}.(λ\operatorname{PNF}.(λ\operatorname{PNFNF}.\operatorname{PNF}\operatorname{PNFNF})(λ\operatorname{PNFNS}.\operatorname{PNF}\operatorname{PNFNS}))(\operatorname{P}\operatorname{PN})) | |||||||
| Beta 2, | (λx.λy.((λa.(x y)a)(λb.(x y)b))) |
| x and y not captured. |
\begin{array}{r} ((λx.z x)(λy.z y))[z:=(x y)]\\ ((λa.z a)(λb.z b))[z:=(x y)]\end{array}
In this example,
\operatorname{FV}(x y)=\{x,y\}
\operatorname{BV}((λx.z x)(λy.z y))=\{x,y\}
\operatorname{FV}(x y)=\{x,y\}
\operatorname{BV}((λa.z a)(λb.z b))=\{a,b\}
η-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.
x\not\inFV(f)\toη-redex[λx.(fx)]=f
The problem with using an η-redex when f has free variables is shown in this example,
| Reduction | Lambda expression | β-reduction | |
|---|---|---|---|
(λx.(λy.yx)x)a | λa.aa | ||
| Naive η-reduction | (λy.yx)a | λa.ax |
This improper use of η-reduction changes the meaning by leaving in
λy.yx