[Prev][Next][Index][Thread]

Paper on lambda calculus optimal graph reductions



A draft version of the paper

                Sharing-Graphs, Sharing-Morphisms, 
            and (Optimal) $\lambda$-Graph Reductions

    by Stefano Guerrini, Dipartimento di Informatica, Pisa

is available via anonymous ftp at 
     ftp.di.unipi.it/pub/Papers/guerrini
files
     SharingGraphs-300dpi.ps.gz           (300 dpi ps version)
     SharingGraphs-600dpi.ps.gz           (600 dpi "     "   )
or WWW URL: 
     http://www.di.unipi.it/~guerrini/guerrini.html

The abstract of the paper is appended to the mail.

============================================================================
    Stefano Guerrini                   Dipartimento di Informatica
        FAX  : ++39 +50 887.226        Universita' di Pisa
        phone: ++39 +50 887.250        Corso Italia, 40
        email: guerrini@di.unipi.it    I-56125 PISA, PI - ITALY
        WWW: http://www.di.unipi.it/~guerrini/guerrini.html
============================================================================


                          * ABSTRACT *

We present a graph implementation of (optimal) $\lambda$-calculus
reductions---here restricted to $\lambda{I}$-calculus---in the
tradition of Lamping [1] and Gonthier {\em et al.\/} [2,3]. But,
differing from the main literature, we unify all the kinds of control
nodes into {\em multiplexer\/} nodes.

The techniques used to prove the algorithm correctness are completely
new and base on the so-called {\em sharing-morphisms\/} via which we
simulate {\em sharing-nets\/} reductions by {\em unshared-nets\/}
reductions.

By such techniques we prove to be sound a set of {\em propagation
rules\/}, the $\pi$-rules, more general than any other one in
literature, and among which there is an {\em absorption rule\/} which
has no equivalent in the previously proposed algorithms. The
$\pi$-rules give a solution to some nasty problems connected with the
so-called ``spurious control nodes'' and allow the internalization of
the read-back into the rewriting system: the $\pi$-normal formal of a
sharing-net being the $\lambda$-tree represented by it.

Finally, by restricting the rewriting system to the shared
$\beta$-rule and to a suitable subset of the $\pi$-rules it is indeed
possible to recover L\'evy optimality.


[1] J. Lamping. An algorithm for optimal lambda calculus reduction. In
Proc. Seventeenth POPL, pp. 16-30, Jan 1990.

[2] G. Gonthier, M. Abadi, and J.-J. L\'evy. The geometry of optimal
lambda reduction. In Proc. Nineteenth POPL, pp. 15--26, Jan 1992.

[3] G. Gonthier, M. Abadi, and J.-J. L\'evy. Linear logic without
boxes. In Proc.\ 7th LICS, pp. 223--234, June 1992.