Overview

lambda calculus


Show Summary Details

Quick Reference

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, λfx.f(f(x) denotes the (higher-order) function that, when applied to a function f, returns the function obtained by composing f with itself.

λfx.f(f(x)

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.e1)(e2) reduces to e1 with all free occurrences of x replaced by e2. For example, (λx.fx.x,x)(a) reduces to fx.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)

x.e1)(e2)

x.fx.x,x)(a)

fx.x,a)

f.f(a)(λx.g)(x,b)

x.g(x,b)(a)

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.

Subjects: Computing.


Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.