Bagnol, Marc - Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees

lmcs:4111 - Logical Methods in Computer Science, November 30, 2017, Volume 13, Issue 4
Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees

Authors: Bagnol, Marc

Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics, ie any categorical interpretation of the logic compatible with its cut-elimination procedure. This notion can usually be captured syntactically by a set of rule permutations. Very generally, proofnets can be defined as combinatorial objects which provide canonical representatives of equivalence classes of proofs. In particular, the existence of proof nets for a logic provides a solution to the equivalence problem of this logic. In certain fragments of linear logic, it is possible to give a notion of proofnet with good computational properties, making it a suitable representation of proofs for studying the cut-elimination procedure, among other things. It has recently been proved that there cannot be such a notion of proofnets for the multiplicative (with units) fragment of linear logic, due to the equivalence problem for this logic being Pspace-complete. We investigate the multiplicative-additive (without unit) fragment of linear logic and show it is closely related to binary decision trees: we build a representation of proofs based on binary decision trees, reducing proof equivalence to decision tree equivalence, and give a converse encoding of binary decision trees as proofs. We get as our main result that the complexity of the proof equivalence problem of the studied fragment is Logspace-complete.

Source :
DOI : 10.23638/LMCS-13(4:20)2017
Volume: Volume 13, Issue 4
Published on: November 30, 2017
Submitted on: November 30, 2017
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 142 times.
This article's PDF has been downloaded 102 times.