[Prev][Next][Index][Thread]
Interaction Systems 1
Several people has asked to us the first part of our work
on Interaction Systems:
*****************************************************************
Interaction Systems I
The Theory of Optimal Reductions
Andrea Asperti Cosimo Laneve
Department of Mathematics, INRIA - Sophia Antipolis,
University of Bologna, 2004, Route des Lucioles,
Piazza Porta S. Donato 5, B.P.93 - 06902,
40127 Bologna, Italy. Sophia Antipolis, France.
asperti@cs.unibo.it cosimo@garfield.cma.fr
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 still ``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
lambda-calculus to other computational constructs than just
beta-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 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 {\em theoretical} aspect
of optimal reductions (in particular, the notion of {\em
redex-family}).
****************************************************************
The paper is available by anonymous FTP from the area
cma.cma.fr
in the directory
/pub/papers/cosimo
The file, in postscript compressed form, is named
IS1.ps.Z
Cosimo Laneve