Characterising explicit substitutions which preserve termination

Abstract

Contrary to all expectations, the λ σ calculus, the canonical simply-typed lambda-calculus with explicit substitutions, is not strongly normalising. This result has led to a proliferation of calculi with explicit substitutions. This paper shows that the reducibility method provides a general criterion when a calculus of explicit substitution is strongly normalising for all untyped lambda-terms that are strongly normalising. This result is general enough to imply preservation of strong normalisation of the calculi considered in the literature. We also propose a version of the λ σ calculus with explicit substitutions which is strongly normalising for strongly normalising λterms.