Special Issue: Theory and applications of explicit substitutions
Perpetuality in a named lambda calculus with
explicit substitutions
EDUARDO BONELLI a1a2 a1 Laboratoire de Recherche en Informatique, Bât 490, Université de Paris-Sud, 91405,
Orsay Cedex, France. Email: bonelli@lri.fr a2 Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina.
Abstract
We study perpetuality in the calculus of explicit substitutions λx. A reduction is called
perpetual if it preserves the possibility of infinite reduction sequences. We then take a look at
applications of this study: an inductive characterization of the λx-strongly normalizing
terms, two perpetual reduction strategies for λx and finally a proof of strong normalization
of a polymorphic lambda calculus with explicit substitutions Fes. To complete the study of
Fes, the property of subject reduction is shown to hold by extending type assignments of the
typing rules to allow non-pure types (types with possible occurrences of the type substitution
operator).
(Received September 30 1999) (Revised April 15 2000)
