Standard and normal reductions
Roger Hindley · Transactions of the American Mathematical Society · 1978
Curry and Feys’ original standardization proof for λ β \lambda \beta -reduction is analyzed and generalized to λ β η \lambda \beta \eta -reductions with extra operators. There seem to be two slightly different definitions of ’standard reduction’ in current use, without any awareness that they are different; it is proved that although these definitions turn out to be equivalent for λ β \lambda \beta -reduction, they become different for λ β η \lambda \beta \eta and for reductions involving extra operators, for example the recursion operator. Normal reductions are also studied, and it is shown that the basic normal-reduction theorem stays true when fairly simple operators like Church’s δ \delta and Curry’s iterator Z are added, but fails for more complicated ones like the recursion operator R . Finally, a table is given summarizing the results, and showing how far the main theorems on λ β \lambda \beta -reductions extend to reductions with various extra operators.