The equivalence of complete reductions

Abstract:

This paper is about two properties of the $\lambda \beta$-calculus and combinatory reduction, namely (E): all complete reductions $\rho$ and $\sigma$ of the residuals of a set of redexes in a term X have the same end; and $({{\text {E}}^ + }):\rho$ and $\sigma$ leave the same residuals of any other redex in X. Property (E) is deduced from abstract assumptions which do not imply $({{\text {E}}^ + })$. Also $({{\text {E}}^ + })$ is proved for the usual extensions of combinatory and $\lambda \beta$-reduction, and a weak but natural form of $({{\text {E}}^ + })$ is proved for $\lambda \beta \eta$-reduction.