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 ∗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 PSPACEcomplete, 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 PSPACEhardness result extends to equivalence of normal forms in MELL without units, where the weakening rule for the exponentials induces a similar rewiring problem.
Original language  English 

Pages (fromto)  134 
Number of pages  34 
Journal  Logical Methods in Computer Science 
Volume  12 
Issue number  1 
Early online date  2 Mar 2016 
DOIs  
Publication status  Published  31 Dec 2016 
Fingerprint
Dive into the research topics of 'Proof equivalence in MLL is PSPACEcomplete'. Together they form a unique fingerprint.Profiles

Willem Heijltjes
 Department of Computer Science  Senior Lecturer
 Mathematical Foundations of Computation
Person: Research & Teaching