License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TLCA.2015.60
URN: urn:nbn:de:0030-drops-51558
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5155/
Go to the corresponding LIPIcs Volume Portal

Bagnol, Marc

MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams

pdf-format:
10.pdf (0.6 MB)

Abstract

Proof equivalence in a logic is the problem of deciding whether two proofs are equivalent modulo a set of permutation of rules that reflects the commutative conversions of its cut-elimination procedure. As such, it is related to the question of proofnets: finding canonical representatives of equivalence classes of proofs that have good computational properties. It can also be seen as the word problem for the notion of free category corresponding to the logic.
It has been recently shown that proof equivalence in MLL (the multiplicative with units fragment of linear logic) is Pspace-complete, which rules out any low-complexity notion of proofnet for this particular logic.
Since it is another fragment of linear logic for which attempts to define a fully satisfactory low-complexity notion of proofnet have not been successful so far, we study proof equivalence in MALL- (multiplicative-additive without units fragment of linear logic) and discover a situation that is totally different from the MLL case. Indeed, we show that proof equivalence in MALL- corresponds(under AC_0 reductions)to equivalence of binary decision diagrams, a data structure widely used to represent and analyze Boolean functions efficiently.
We show these two equivalent problems to be Logspace-complete. If this technically leaves open the possibility for a complete solution to the question of proofnets for MALL-, the established relation with binary decision diagrams actually suggests a negative solution to this problem.

BibTeX - Entry

@InProceedings{bagnol:LIPIcs:2015:5155,
  author =	{Marc Bagnol},
  title =	{{MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{60--75},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Thorsten Altenkirch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5155},
  URN =		{urn:nbn:de:0030-drops-51558},
  doi =		{10.4230/LIPIcs.TLCA.2015.60},
  annote =	{Keywords: linear logic, proof equivalence, additive connectives, proofnets, binary decision diagrams, logarithmic space, AC0 reductions}
}

Keywords: linear logic, proof equivalence, additive connectives, proofnets, binary decision diagrams, logarithmic space, AC0 reductions
Collection: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Issue Date: 2015
Date of publication: 15.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI