The equivalence of complete reductions
Roger Hindley · Transactions of the American Mathematical Society · 1977
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 ( E + ) : ρ ({{\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 ( E + ) ({{\text {E}}^ + }) . Also ( E + ) ({{\text {E}}^ + }) is proved for the usual extensions of combinatory and λ β \lambda \beta -reduction, and a weak but natural form of ( E + ) ({{\text {E}}^ + }) is proved for λ β η \lambda \beta \eta -reduction.