A note on preservation of strong normalisation in the lambda-calculus

Abstract

An auxiliary notion of reduction ρ on the λ-terms preserves strong normalisation if all strongly normalising terms for β are also strongly normalising for β∪ρ.Wegive a sufficient condition for ρ to preserve strong normalisation. As an example of application, we check easily the sufficient condition for Regnier’s σ-reduction rules and the ‘‘assoc’’-reduction rule inspired by calculi with let-expressions. This gives the simplest proof so far that the union of all these rules preserves strong normalisation.