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)