HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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).
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, May 29, 2006 - 11:46:49 AM
Last modification on : Thursday, February 3, 2022 - 11:18:29 AM
Long-term archiving on: : Friday, May 13, 2011 - 10:23:06 PM


  • HAL Id : inria-00076988, version 1



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



Record views


Files downloads