[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.