s'authentifier
version française rss feed

inria-00073929, version 1

Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus

César Augusto Munoz Hurtado 1

N° RR-2762 (1995)

Résumé : Explicit substitutions calculi are formal systems that implement $\beta$-reduction by means of an internal substitution operator. Thus, in that calculi it is possible to delay the application of a substitution to a term or to consider terms with partially applied substitutions. This feature is useful, for instance, to represent incomplete proofs in type based proof systems. The $\lambda_{\sigma}$-calculus of explicit substitutions proposed by Abadi, Cardelli, Curien and Lévy gives an elegant way to deal with management of variable names and substitutions of $\lambda$-calculus. However, $\lambda_{\si- gma}$ 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 an we present the full proofs of its main properties. This is, as far as we know, the first confluent calculus of explicit substitutions that preserves strong normalisation.

  • Domaine : Informatique/Autre
  • Mots-clés : EXPLICIT SUBSTITUTIONS / CONFLUENCE / PRESERVATION OF STRONG NORMALISATION / $\LAMBDA$-CALCULUS
  • Référence interne : RR-2762
  • Commentaire : Projet COQ
 
  • inria-00073929, version 1
  • oai:hal.inria.fr:inria-00073929
  • Contributeur : 
  • Soumis le : Mercredi 24 Mai 2006, 14:06:36
  • Dernière modification le : Mercredi 9 Mai 2007, 09:45:07
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
  翻译: