Unique perfect matchings, edge-colored graphs and proof nets for linear logic with Mix
share
This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms. Alternating cycles in perfect matchings serve as witnesses of non-uniqueness, and in this significantly expanded journal version, we discuss connections with other kinds of constrained cycles known to be equivalent: semicycles in directed graphs, trails avoiding forbidden transitions, and properly colored cycles in edge-colored graphs. While the second one provides an explanation and generalization of Retoré's "R&B-graphs", the latter leads us to prove the coNP-hardness of Pagani's visible acyclicity criterion for MELL proof nets. We also connect Lamarche's essential nets to R&B-graphs.
READ FULL TEXT