Preservation of Strong Normalisation for Explicit Substitution

摘要

The authors introduce a calculus of explicit substitutions and prove that termsthat are strongly normalizing with respect to Beta-reduction are also strongly normalizing with respect to explicit substitution reduction. The authors show by means of a counterexample that an extension of lambda exp with certain interaction between substitutions does not preserve strong normalization. In appendix A, the authors use a more common notation trying to determine the borderline between preservation of strong normalization and interaction of substitutions.