Abstract
Sharing graphs are a local and asynchronous implementation of lambdacalculus betareduction (or linear logic proofnet cutelimination) that avoids useless duplications. Empirical benchmarks suggest that they are one of the most efficient machineries, when one wants to fully exploit the higherorder features of lambdacalculus. However, we still lack confirming grounds with theoretical solidity to dispel uncertainties about the adoption of sharing graphs.
Aiming at analysing in detail the worstcase 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 socalled "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. proofnet 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.
BibTeX  Entry
@InProceedings{guerrini_et_al:LIPIcs:2017:7733,
author = {Stefano Guerrini and Marco Solieri},
title = {{Is the Optimal Implementation Inefficientl Elementarily Not}},
booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
pages = {17:117:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770477},
ISSN = {18688969},
year = {2017},
volume = {84},
editor = {Dale Miller},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7733},
URN = {urn:nbn:de:0030drops77337},
doi = {10.4230/LIPIcs.FSCD.2017.17},
annote = {Keywords: optimality, sharing graphs, lambdacalculus, complexity, linear logic, proof nets}
}
Keywords: 

optimality, sharing graphs, lambdacalculus, complexity, linear logic, proof nets 
Seminar: 

2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) 
Issue Date: 

2017 
Date of publication: 

21.08.2017 