lambda-calculus

mathematics (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 abstractions (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)