Willem Heijltjes ; Robin Houston - Proof equivalence in MLL is PSPACE-complete

lmcs:1625 - Logical Methods in Computer Science, March 2, 2016, Volume 12, Issue 1 - https://doi.org/10.2168/LMCS-12(1:2)2016
Proof equivalence in MLL is PSPACE-completeArticle

Authors: Willem Heijltjes ORCID; Robin Houston

    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.

    Volume: Volume 12, Issue 1
    Published on: March 2, 2016
    Submitted on: February 2, 2015
    Keywords: Computer Science - Logic in Computer Science

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1364 times.
    This article's PDF has been downloaded 432 times.