A formalism for representing functions and ways of combining functions, invented around 1930 by the logician Alonzo Church. The following are examples of λ-expressions:
λx.x denotes the identity function, which simply returns its argument;
λx.c denotes the constant function, which always returns the constant c regardless of its argument;
λx.f(f(x)) denotes the composition of the function f with itself, i.e. the function that, for any argument x, returns f(f(x)).
Much of the power of the notation derives from the ability to represent higher-order functions. For example,
denotes the (higher-order) function that, when applied to a function
f, returns the function obtained by composing
f with itself.
As well as a notation, the λ-calculus comprises rules for reducing λ-expressions to equivalent ones. The most important is the rule of β-reduction, by which an expression of the form
reduces to
e1 with all free occurrences of
x replaced by
e2. For example:
reduces to
As a second example, involving a functional variable, the expression
reduces to
and hence to
In theoretical terms, the formalism of λ-calculus can be shown to be equivalent in expressive power to that of Turing machines. It has a special role in the study of programming languages: one can point to its influence on the design of functional languages such as J. McCarthy’s Lisp; to P. Landin’s reduction of Algol 60 to λ-calculus, and to D. Scott’s construction of a set-theory meaning for the full unrestricted λ-calculus—a construction that ushered in the theory of domains in the denotational semantics of programming languages.