delta conversion

delta reduction
delta conversion

   <theory> In {lambda-calculus} extended with constants, delta
   reduction replaces a function applied to the required number
   of arguments (a {redex}) by a result.  E.g. plus 2 3 --> 5.
   In contrast with {beta reduction} (the only kind of reduction
   in the {pure lambda-calculus}) the result is not formed simply
   by textual substitution of arguments into the body of a
   function.  Instead, a delta redex is matched against the left
   hand side of all delta rules and is replaced by the right hand
   side of the (first) matching rule.  There is notionally one
   delta rule for each possible combination of function and
   arguments.  Where this implies an infinite number of rules,
   the result is usually defined by reference to some external
   system such as mathematical addition or the hardware
   operations of some computer.  For other types, all rules can
   be given explicitly, for example {Boolean} negation:

   	not True  = False
   	not False = True

   (1997-02-20)