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