Standard and normal reductions

Abstract:

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.