catflap.org Online Dictionary Query

  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 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)