Logic in Computer Science (LICS 1996)

Paper: Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus (at LICS 1996)

Authors: César A. Munoz

Abstract

Explicit substitutions calculi are formal systems that implement beta-reduction by means of an internal substitution operator. In that calculi it is possible to delay the application of a substitution to a term or to consider terms with partially applied substitutions. The lambda-sigma-calculus of explicit substitutions, proposed by Abadi, Cardelli, Curien and Levy, is a first-order rewriting system that implements substitution and renaming mechanism of lambda-calculus. However, lambda-sigma does not preserve strong normalisation of lambda-calculus and it is not a confluent system. Typed variants of lambda-sigma without composition are strongly normalising but not confluent, while variants with composition are confluent but do not preserve strong normalisation. Neither of them enjoys both properties. In this paper we propose the lambda-zeta-calculus. This is, as far as we know, the first confluent calculus of explicit substitutions that preserves strong normalisation.

BibTeX

  @InProceedings{Munoz-ConfluenceandPreser,
    author = 	 {César A. Munoz},
    title = 	 {Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {440-447},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }