Interaction systems I : the theory of optimal reductions

Andrea Asperti 1 Cosimo Laneve 1
1 PARA - Parallélisme
Inria Paris-Rocquencourt
Abstract : A new class of higher order rewriting systems, called interaction systems is introduced. From one side, interaction systems provide the intuitionistic generalization of Lafont's interaction nets (recall that interaction nets are linear). In particular, we keep the idea of binary interaction and the syntactical bipartition of operators into constructors and destructors. From the other side, interaction systems are the subsystem of Klop's combinatory reduction systems where the Curry-Howard analogy stoll "makes sense". This means that we can associate with every IS a suitable logical (intuitionistic) system ; constructors and destructors respectively correspond to right and left introduction rules, interaction is cut and computation is cut-elimination. Interaction systems have been primarily motivated by the necessity of extending Lamping's optimal graph reduction technique for the l-calculus to other computational constructs than just -reduction. This implementation style can be smootly generalized to arbitrary IS's providing in this way a uniform description of essential rules such as conditionals and recursion The optimal implementation of IS's will be only sketched here (it will eventually be the subject of the forthcoming Part II). The main aim of this paper is to introduce this new class of systems, to discuss the motivations behind its definition and to investigate the theoretical aspect of optimal reductions (in particular, the notion of redex-family).
Type de document :
Rapport
[Research Report] RR-1748, INRIA. 1992
Liste complète des métadonnées

https://hal.inria.fr/inria-00076988
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 11:46:49
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : vendredi 13 mai 2011 - 22:23:06

Fichiers

Identifiants

  • HAL Id : inria-00076988, version 1

Collections

Citation

Andrea Asperti, Cosimo Laneve. Interaction systems I : the theory of optimal reductions. [Research Report] RR-1748, INRIA. 1992. 〈inria-00076988〉

Partager

Métriques

Consultations de la notice

129

Téléchargements de fichiers

77