lambda calculus

lambda calculus (λ-calculus) 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, λf.λx.f(f(x))

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 (λx.e₁)(e₂)

reduces to e₁ with all free occurrences of x replaced by e₂. For example, (λx.f(λx.x,x))(a)

reduces to f(λx.x,a)

As a second example, involving a functional variable, the expression (λf.f(a))(λx.g)(x,b))

reduces to (λx.g(x,b))(a)

and hence to g(a,b)

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.