No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete

DOI10.1145/2603088.2603126zbMATH Open1395.03036arXiv1510.06178OpenAlexW2128713292MaRDI QIDQ4635635FDOQ4635635

Authors: Willem Heijltjes, Robin Houston 

Publication date: 23 April 2018

Published 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) (Search for Journal in Brave)

Abstract: MLL proof equivalence is the problem of deciding whether two proofs in multiplicative linear logic are related by a series of inference permutations. It is also known as the word problem for star-autonomous categories. Previous work has shown the problem to be equivalent to a rewiring problem on proof nets, which are not canonical for full MLL due to the presence of the two units. Drawing from recent work on reconfiguration problems, in this paper it is shown that MLL proof equivalence is PSPACE-complete, using a reduction from Nondeterministic Constraint Logic. An important consequence of the result is that the existence of a satisfactory notion of proof nets for MLL with units is ruled out (under current complexity assumptions). The PSPACE-hardness result extends to equivalence of normal forms in MELL without units, where the weakening rule for the exponentials induces a similar rewiring problem.

Full work available at URL: https://arxiv.org/abs/1510.06178

Recommendations

• Proof equivalence in MLL is PSPACE-complete
• MALL proof equivalence is logspace-complete, via binary decision diagrams
• Multiplicative-additive proof equivalence is \textsf{logspace}-complete, via binary decision trees
• Completeness of MLL proof-nets w.r.t. weak distributivity
• Proof nets for unit-free multiplicative-additive linear logic

zbMATH Keywords

linear logicPSPACE-completenessproof netsconstraint logicproof equivalence

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cited In (16)

• Title not available (Why is that?)
• Proof diagrams for multiplicative linear logic
• Deep inference and expansion trees for second-order multiplicative linear logic
• MALL proof equivalence is logspace-complete, via binary decision diagrams
• Title not available (Why is that?)
• A categorical reduction system for linear logic
• Proof diagrams for multiplicative linear logic: syntax and semantics
• Weak units, universal cells, and coherence via universality for bicategories
• Proof equivalence in MLL is PSPACE-complete
• Reconfiguration in bounded bandwidth and tree-depth
• Multiplicative-additive proof equivalence is \textsf{logspace}-complete, via binary decision trees
• Completeness of MLL proof-nets w.r.t. weak distributivity
• Proof nets, coends and the Yoneda isomorphism
• Exponentially handsome proof nets and their normalization
• Title not available (Why is that?)
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem

This page was built for publication: No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635635)