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

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)

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

(16)

• scientific article; zbMATH DE number 7089066 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• 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
• Reconfiguration in bounded bandwidth and tree-depth
• Proof equivalence in MLL is PSPACE-complete
• 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
• scientific article; zbMATH DE number 5295707 (Why is no real title available?)
• 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)