| 释义 |
delta reduction delta reduction (theory)In lambda-calculus extended with constants, deltareduction replaces a function applied to the required numberof arguments (a redex) by a result. E.g. plus 2 3 --> 5.In contrast with beta reduction (the only kind of reductionin the pure lambda-calculus) the result is not formed simplyby textual substitution of arguments into the body of afunction. Instead, a delta redex is matched against the lefthand side of all delta rules and is replaced by the right handside of the (first) matching rule. There is notionally onedelta rule for each possible combination of function andarguments. Where this implies an infinite number of rules,the result is usually defined by reference to some externalsystem such as mathematical addition or the hardwareoperations of some computer. For other types, all rules canbe given explicitly, for example Boolean negation:
not True = Falsenot False = True |