Deep into Optimality — Complexity and correctness of sharing implementation of bounded logic
Abstract
Sharing graphs are an implementation of both the Lévy-optimal reduction on λ-calculus, and of linear logic proof-nets. Since the proof of inadequacy of Lévy families as a cost model for λ-calculus, studies on the complexity of the shared reduction are far from complete. Indeed, the only comparative result considers the restricted case of bounded logics. Because of their well known complexity, it was possible to provide semantically, via geometry of interaction, a correspondent bounding of their shared implementation.
In a similarly restricted case, where the abstract algorithm is sufficient, we present a complete and stronger comparison between the cost of the cut elimination on proof-nets and the cost of the corresponding shared reduction. Then, for the first time, the expected benefits of sharing and avoiding duplication in the reduction are made explicit. The proof exploits an intermediate graph rewriting system, that permits us to give a precise account of complexity on the former and to establish a simulation of the latter. Such simulation implies the main complexity result of the shared implementation, as well as its correctness.
Our syntactical approach enlightens the connection between the different styles of duplication of the two systems - global in proof-nets, local in sharing graphs. This insight appears a suitable starting point for the two, more general, related complexity problem which are still open: the cost model for the λ-calculus itself, and the cost of its shared implementation.