Is the Optimal Implementation Inefficient? Elementarily Not

[bcdarwin]

http://drops.dagstuhl.de/opus/volltexte/2017/7733/pdf/LIPIcs-FSCD-2017-17.pdf

Abstract

Sharing graphs are a local and asynchronous implementation of lambda-calculus beta-reduction
(or linear logic proof-net cut-elimination) that avoids useless duplications. Empirical benchmarks
suggest that they are one of the most efficient machineries, when one wants to fully exploit
the higher-order features of lambda-calculus. However, we still lack confirming grounds with
theoretical solidity to dispel uncertainties about the adoption of sharing graphs. Aiming at
analysing in detail the worst-case overhead cost of sharing operators, we restrict to the case
of elementary and light linear logic, two subsystems with bounded computational complexity
of multiplicative exponential linear logic. In these two cases, the bookkeeping component is
unnecessary, and sharing graphs are simplified to the so-called “abstract algorithm”. By a modular
cost comparison over a syntactical simulation, we prove that the overhead of shared reductions is
quadratically bounded to cost of the naive implementation, i.e. proof-net reduction. This result
generalises and strengthens a previous complexity result, and implies that the price of sharing
is negligible, if compared to the obtainable benefits on reductions requiring a large amount of
duplication.