[Prev][Next][Index][Thread]
Two papers on MELL shared reductions and sharing graphs
These two full papers are available
(the abstracts are enclosed at the end of the mail):
---------------
Coherence for sharing proof-nets
Stefano Guerrini, Simone Martini, Andrea Masini
ftp://ftp.cis.upenn.edu/pub/papers/guerrini/CoherenceFull.ps.gz
---------------
A general theory of sharing graphs
Stefano Guerrini
ftp://ftp.cis.upenn.edu/pub/papers/guerrini/GeneralTheory.ps.gz
---------------
They will be avaible as TR of IRCS (soon):
http://www.cis.upenn.edu/~ircs/tech-reps.html
Hardcopies can be requested at IRCS:
Technical Report Information
Institute for Research in Cognitive Science
3401 Walnut Street, Suite 400A
Philadelphia, PA 19104-6228
or contact:
sdeysher@central.cis.upenn.edu
---------------------------------------------------------------------------
Coherence for sharing proof-nets
Stefano Guerrini
IRCS- University of Pennsylvania,
3401 Walnut Street, Suite 400A - Philadelphia, PA, 19104-6228
mailto:stefanog@saul.cis.upenn.edu
Simone Martini
Dip. di Matematica e Informatica, Univ. di Udine
Via delle Scienze, 206 - I-33100, Udine, Italy
mailto:martini@dimi.uniud.it
Andrea Masini
Dipartimento di Informatica, Univ. di Pisa
Corso Italia, 40 - I-56100, Pisa, Italy
mailto:masini@di.unipi.it
Abstract
Sharing graphs are an implementation of linear logic proof-nets
in such a way that their reduction never duplicate a redex.
In their usual formulations, proof-nets present a problem of coherence:
if the proof-net $N$ reduces by standard cut-elimination to $N'$,
then, by reducing the sharing graph of $N$ we do {\em not\/} obtain
the sharing graph of $N'$. We solve this problem by changing the
way the information is coded into sharing graphs and introducing a
new reduction rule ({\em absorption\/}). The rewriting system is
confluent and terminating. The proof of this fact exploits an
algebraic semantics for sharing graphs.
---------------------------------------------------------------------------
A general theory of sharing graphs
Stefano Guerrini
IRCS- University of Pennsylvania,
3401 Walnut Street, Suite 400A - Philadelphia, PA, 19104-6228
mailto:stefanog@saul.cis.upenn.edu
Sharing graphs are the structures introduced by Lamping to implement
optimal reductions of lambda calculus. Gonthier's reformulation of
Lamping's technique inside Geometry of Interaction, and Asperti and
Laneve's work on Interaction Systems have shown that sharing graphs
can be used to implement a wide class of calculi. Here, we give a
general characterization of sharing graphs independent from the
calculus to be implemented. Such a characterization rests on an
\emph{algebraic semantics} of sharing graphs exploiting the methods
of Geometry of Interaction. By this semantics we can define an
unfolding partial order between proper sharing graphs, whose minimal
elements are unshared graphs. The \emph{least-shared-instance} of a
sharing graph is the unique unshared graph that the unfolding
partial order associates to it. The algebraic semantics allows to
prove that we can associate a semantical \emph{read-back} to each
unshared graph and that such a read-back can be computed via
suitable \emph{read-back reductions}. The result is then lifted to
sharing graphs proving that any read-back (or unfolding) reduction
of them can be simulated on their least-shared-instances. The
sharing graphs defined in this way allow to implement in a
distributed and local way any calculus with a global reduction rule
in the style of the beta rule of lambda calculus. Also in this case
the proof technique is to prove that sharing reductions can be
simulated on least-shared-instances. The result is proved under the
only assumption that the structures of the calculus have a \emph{box
nesting property}, that is, that two beta redexes may not
partially overlap. As a result, we get a \emph{sharing graph
machine} that seems to be the most natural low-level computational
model for functional languages. The paper concludes showing that
optimality is a by-product of this technique: optimal reductions are
lazy reductions of the sharing graph machine. We stress the proof
strategy followed in the paper: it is based on an amazing interplay
between standard rewriting system properties (strong normalization,
confluence, and unique normal form) and algebraic properties
definable via the techniques of Geometry of Interaction.