delta reduction
<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)
Nearby terms:
Delta-4 « delta conversion « Delta-Prolog « delta
reduction » DELTASE » demand driven » demand
paged
|
