Lambdacalculus

1 definition found

From The Free On-line Dictionary of Computing (27 SEP 03) [foldoc]:

  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)