catflap.org Online Dictionary Query

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