Marc Bagnol - 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 - https://doi.org/10.23638/LMCS-13(4:20)2017
Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision TreesArticle

Authors: Marc Bagnol

    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.


    Volume: Volume 13, Issue 4
    Published on: November 30, 2017
    Accepted on: November 30, 2017
    Submitted on: November 30, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1580 times.
    This article's PDF has been downloaded 405 times.