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

DOI10.1145/2603088.2603126MaRDI QIDQ4635635zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

constraint logiclinear logicproof equivalenceproof netsPSPACE-completeness

Mathematics Subject Classification ID

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

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.

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

Cited in

(18)

• Reconfiguration in bounded bandwidth and tree-depth
• Proof diagrams for multiplicative linear logic: syntax and semantics
• Proof equivalence in MLL is PSPACE-complete
• Completeness of MLL proof-nets w.r.t. weak distributivity
• scientific article; zbMATH DE number 5295707 (Why is no real title available?)
• Multiplicative-additive proof equivalence is \textsf{logspace}-complete, via binary decision trees
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• Proof diagrams for multiplicative linear logic
• Proof nets, coends and the Yoneda isomorphism
• A categorical reduction system for linear logic
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Coherence for Frobenius pseudomonoids and the geometry of linear proofs
• Deep inference and expansion trees for second-order multiplicative linear logic
• Weak units, universal cells, and coherence via universality for bicategories
• MALL proof equivalence is logspace-complete, via binary decision diagrams
• Exponentially handsome proof nets and their normalization
• A new conjecture about identity of proofs
• Logic programming with multiplicative structures

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)