Lambda-calculus

from The Free On-line Dictionary of Computing (8 July 2008)
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)
    

[email protected]