Source : Free On-Line Dictionary of Computing
lambda-calculus
(Normally written with a Greek letter lambda).
A branch of mathematical logic developed by {Alonzo Church} in
the late 1930s and early 1940s, dealing with the application
of {functions} to their arguments. The {pure lambda-calculus}
contains no constants - neither numbers nor mathematical
functions such as plus - and is untyped. It consists only of
{lambda abstraction}s (functions), variables and applications
of one function to another. All entities must therefore be
represented as functions. For example, the natural number N
can be represented as the function which applies its first
argument to its second N times ({Church integer} N).
Church invented lambda-calculus in order to set up a
foundational project restricting mathematics to quantities
with "{effective procedures}". Unfortunately, the resulting
system admits {Russell's paradox} in a particularly nasty way;
Church couldn't see any way to get rid of it, and gave the
project up.
Most {functional programming} languages are equivalent to
lambda-calculus extended with constants and types. {Lisp}
uses a variant of lambda notation for defining functions but
only its {purely functional} subset is really equivalent to
lambda-calculus.
See {reduction}.
(1995-04-13)