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.
Standard definition
This formal definition was given by
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scien ...
.
Definition
Lambda expressions are composed of
* variables
,
, ...,
, ...
* the abstraction symbols lambda '
' and dot '.'
* parentheses ( )
The set of lambda expressions,
, can be
defined inductively:
#If
is a variable, then
#If
is a variable and
, then
#If
, then
Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications.
Notation
To keep the notation of lambda expressions uncluttered, the following conventions are usually applied.
* Outermost parentheses are dropped:
instead of
* Applications are assumed to be left-associative:
may be written instead of
* The body of an abstraction extends
as far right as possible:
means
and not
* A sequence of abstractions is contracted:
is abbreviated as
[
]
Free and bound variables
The abstraction operator,
, is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of an abstraction are said to be ''bound''. All other variables are called ''free''. For example, in the following expression
is a bound variable and
is free:
. Also note that a variable is bound by its "nearest" abstraction. In the following example the single occurrence of
in the expression is bound by the second lambda:
The set of ''free variables'' of a lambda expression,
, is denoted as
and is defined by recursion on the structure of the terms, as follows:
#
, where
is a variable
#
#
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.
Reduction
The meaning of lambda expressions is defined by how expressions can be reduced.
[ de Queiroz, Ruy J.G.B.]
A Proof-Theoretic Account of Programming and the Role of Reduction Rules.
''Dialectica'' 42(4), pages 265-282, 1988.
There are three kinds of reduction:
* α-conversion: changing bound variables (alpha);
* β-reduction: applying functions to their arguments (beta);
* η-reduction: which captures a notion of extensionality (eta).
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,
is a β-redex in expressing the substitution of
for
in
; if
is not free in
,
is an η-redex. The expression to which a redex reduces is called its reduct; using the previous example, the reducts of these expressions are respectively