[L5] ================================================ AMAST Links 02 06

Sharing-Graphs, Sharing-Morphisms, & (Optimal) lambda-Graph Reductions
        by Stefano Guerrini, Dipartimento di Informatica, Pisa

  A _draft version_ of this paper is available via 
URL: http://www.di.unipi.it/~guerrini/guerrini.html

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

  The techniques used to prove the algorithm correct are completely
new and base on the so-called _sharing-morphisms_ via which we
simulate _sharing-nets_ reductions by _unshared-nets_ reductions.

  By such techniques we prove to be sound a set of _propagation
rules_, the $\pi$-rules, more general than any other one in
literature, and among which there is an _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.