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 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).
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014 |
| Place of Publication | New York |
| Publisher | Association for Computing Machinery |
| Number of pages | 10 |
| ISBN (Print) | 9781450328869 |
| DOIs | |
| Publication status | Published - 2014 |
| Event | Joint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014 - Vienna , Austria Duration: 14 Jul 2014 → 18 Jul 2014 |
Conference
| Conference | Joint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014 |
|---|---|
| Country/Territory | Austria |
| City | Vienna |
| Period | 14/07/14 → 18/07/14 |