Perpetuality in a Lambda Calculus with Explicit Substitutions and Composition

Abstract

We study perpetual rewrite strategies (strategies that preserve the possibility of in finite derivations) in the λws-calculus, a lambda calculus with explicit substitutions allowing the composition of substitutions. Since current literature on perpetuality is not applicable to λws we exploit a proof technique for proving preservation of strong normalization of calculi of explicit substitutions. We de fine a perpetual rewrite strategy for λws and formulate an inductive characterization of the set of strongly λws-normalizing terms.