A draft version of this paper is available.
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.