Document

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

## File

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

## Cite As

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
• proofnets
• binary decision diagrams
• logarithmic space
• AC0 reductions

## Metrics

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

## 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.
2. Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput., 35(8):677-691, August 1986.
3. Ashok K. Chandra, Larry J. Stockmeyer, and Uzi Vishkin. Constant depth reducibility. SIAM J. Comput., 13(2):423–439, 1984.
4. Kousha Etessami. Counting quantifiers, successor relations, and logarithmic space. Journal of Computer and System Sciences, 54(3):400 - 411, 1997.
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.
6. Jean-Yves Girard. Linear logic. Theoret. Comput. Sci., 50(1):1-101, 1987.
7. Jean-Yves Girard. Proof-nets: The parallel syntax for proof-theory. Logic and Algebra, 180:97-124, May 1996.
8. Stefano Guerrini and Andrea Masini. Parsing MELL Proof Nets. Theoretical Computer Science, 254(1-2):317-335, 2001.
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.
10. Willem Heijltjes and Lutz Straßburger. Proof nets and semi-star-autonomous categories. Mathematical Structures in Computer Science, FirstView:1-40, 11 2014.
11. Dominic J. D. Hughes. Simple multiplicative proof nets with units. Technical report, 2005.
12. Dominic J. D. Hughes. Abstract p-time proof nets for MALL: Conflict nets. arXiv: math.LO/0801.2421v1, 2008.
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.
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.
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.