A Normalisation Result for Higher-Order Calculi with Explicit Substitutions

Explicit substitutions (ES)were introduced as a bridge between the theory of rewrite systems with binders and substitution,such as the λ -calculus,and their implementation.In a seminal paper P.- A.Melliès observed that the dynamical properties of a rewrite system and its ES-based implementation may not coincide:he showed that a strongly normalising term (i.e. one which does not admit in finite derivations)in the λ -calculus may lose this status in its ES-based implementation.This paper studies normalisation for the latter systems in the general setting of higher-order rewriting:Based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the ES-based implementation of any orthogonal pattern higher-order rewrite system.