on Global Dynamics of Optimal Graph Reduction

Abstract

Optimal graph reduction technology for the λ-calculus, as developed by Lamping, with modifications by Asperti, Gonthier, Abadl, and Lévy, has a well-understood local dynamics based on a standard menagerie of reduction rules, as well as a global context semantics based on Girard's geometry of interaction. However, the global dynamics of graph reduction has not been subject to careful investigation. In particular, graphs lose their structural resemblance to λ-terms after only a few graph reduction steps, and little is known about graph reduction strategies that maintain efficiency or structure. While the context semantics provides global information about the computation, its use as part of a reduction strategy seems computationally infeasible. We propose a tractable graph reduction strategy that preserves computationally relevant global structure, and allows us to efficiently bound the computational resources needed to implement optimal reduction.A simple canonical representation for graphs is introduced that we call fan-normal form. This normal form allows us to reduce graphs based on efficient identification of β-redexes, rather than being guided by lower-level search for interacting nodes. In addition and perhaps more important, the fan-normal form facilitates a complexity analysis of graph reductions, showing that the number of fan interactions is essentially bounded by a polynomial in the number of unique Lévy labels generated during a labelled reduction. This global analysis of the finitary dynamics of optimal reduction is the first demonstration that a reasonable implementation-independent cost model for the λ-calculus is in fact realized by Lamping's abstract algorithm. It remains to be seen whether similar claims can be made about so-called bookkeeping for fan interactions.