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

Author Marc Bagnol



PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.60.pdf
  • Filesize: 0.6 MB
  • 16 pages

Document Identifiers

Author Details

Marc Bagnol

Cite AsGet BibTex

Marc Bagnol. MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 60-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TLCA.2015.60

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.
Keywords
  • linear logic
  • proof equivalence
  • additive connectives
  • proofnets
  • binary decision diagrams
  • logarithmic space
  • AC0 reductions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. David A. Barrington. Bounded-width polynomial-size branching programs recognize exactly those languages in NC1. Journal of Computer and System Sciences, 38(1):150 - 164, 1989. Google Scholar
  2. Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput., 35(8):677-691, August 1986. Google Scholar
  3. Ashok K. Chandra, Larry J. Stockmeyer, and Uzi Vishkin. Constant depth reducibility. SIAM J. Comput., 13(2):423–439, 1984. Google Scholar
  4. Kousha Etessami. Counting quantifiers, successor relations, and logarithmic space. Journal of Computer and System Sciences, 54(3):400 - 411, 1997. Google Scholar
  5. Jean Gallier. On the correspondence between proofs and lambda-terms. In Philippe de Groote, editor, The Curry-Howard isomorphism, Cahiers du Centre de Logique, pages 55-138. Academia, 1995. Google Scholar
  6. Jean-Yves Girard. Linear logic. Theoret. Comput. Sci., 50(1):1-101, 1987. Google Scholar
  7. Jean-Yves Girard. Proof-nets: The parallel syntax for proof-theory. Logic and Algebra, 180:97-124, May 1996. Google Scholar
  8. Stefano Guerrini and Andrea Masini. Parsing MELL Proof Nets. Theoretical Computer Science, 254(1-2):317-335, 2001. Google Scholar
  9. Willem Heijltjes and Robin Houston. No Proof Nets for MLL with Units: Proof Equivalence in MLL is PSPACE-complete. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pages 50:1-50:10, New York, NY, USA, 2014. ACM. Google Scholar
  10. Willem Heijltjes and Lutz Straßburger. Proof nets and semi-star-autonomous categories. Mathematical Structures in Computer Science, FirstView:1-40, 11 2014. Google Scholar
  11. Dominic J. D. Hughes. Simple multiplicative proof nets with units. Technical report, 2005. Google Scholar
  12. Dominic J. D. Hughes. Abstract p-time proof nets for MALL: Conflict nets. arXiv: math.LO/0801.2421v1, 2008. Google Scholar
  13. Dominic J. D. Hughes and Rob J. van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. ACM Trans. Comput. Log., 6(4):784-842, 2005. Google Scholar
  14. Dominic J. D. Hughes and Rob J. van Glabbeek. MALL proof nets identify proofs modulo rule commutation. http://boole.stanford.edu/~dominic/MALL-equiv.pdf, to appear, 2015.
  15. Donald E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams. Addison-Wesley Professional, 12th edition, 2009. Google Scholar
  16. Olivier Laurent and Roberto Maieli. Cut elimination for monomial MALL proof nets. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 486-497, 2008. Google Scholar