An abstract factorization theorem for explicit substitutions

Beniamino Accattoli 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We study a simple form of standardization, here called factorization, for explicit substitutions calculi, i.e. lambda-calculi where beta-reduction is decomposed in various rules. These calculi, despite being non-terminating and non-orthogonal, have a key feature: each rule terminates when considered separately. It is well-known that the study of rewriting properties simplifies in presence of termination (e.g. confluence reduces to local confluence). This remark is exploited to develop an abstract theorem deducing factorization from some axioms on local diagrams. The axioms are simple and easy to check, in particular they do not mention residuals. The abstract theorem is then applied to some explicit substitution calculi related to Proof-Nets. We show how to recover standardization by levels, we model both call-by-name and call-by-value calculi and we characterize linear head reduction via a factorization theorem for a linear calculus of substitutions.
Type de document :
Communication dans un congrès
23rd International Conference on Rewriting Techniques and Applications (RTA'12), May 2012, Nagoya, Japan. 2012
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger
Contributeur : Beniamino Accattoli <>
Soumis le : mercredi 23 janvier 2013 - 17:24:38
Dernière modification le : jeudi 10 mai 2018 - 02:06:53
Document(s) archivé(s) le : samedi 1 avril 2017 - 08:54:14


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00780344, version 1



Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. 23rd International Conference on Rewriting Techniques and Applications (RTA'12), May 2012, Nagoya, Japan. 2012. 〈hal-00780344〉



Consultations de la notice


Téléchargements de fichiers