Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix
This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retor\'e (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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5134/pdf |
| _version_ | 1797268581122048000 |
|---|---|
| author | Lê Thành Dũng Nguyên |
| author_facet | Lê Thành Dũng Nguyên |
| author_sort | Lê Thành Dũng Nguyên |
| collection | DOAJ |
| description | This paper establishes a bridge between linear logic and mainstream graph
theory, building on previous work by Retor\'e (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.
In this journal version, we have added an explanation of Retor\'e's
"RB-graphs" in terms of a general construction on graphs with forbidden
transitions. In fact, it is by analyzing RB-graphs that we arrived at this
construction, and thus obtained a polynomial-time algorithm for finding trails
avoiding forbidden transitions; the latter is among the material covered in
another paper by the author focusing on graph theory (arXiv:1901.07028). |
| first_indexed | 2024-04-25T01:34:45Z |
| format | Article |
| id | doaj.art-aaf1e2f0bdc946698f8a1d7920a40935 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:45Z |
| publishDate | 2020-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-aaf1e2f0bdc946698f8a1d7920a409352024-03-08T10:29:27ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-02-01Volume 16, Issue 110.23638/LMCS-16(1:27)20205134Unique perfect matchings, forbidden transitions and proof nets for linear logic with MixLê Thành Dũng NguyênThis paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retor\'e (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. In this journal version, we have added an explanation of Retor\'e's "RB-graphs" in terms of a general construction on graphs with forbidden transitions. In fact, it is by analyzing RB-graphs that we arrived at this construction, and thus obtained a polynomial-time algorithm for finding trails avoiding forbidden transitions; the latter is among the material covered in another paper by the author focusing on graph theory (arXiv:1901.07028).https://lmcs.episciences.org/5134/pdfcomputer science - logic in computer science03f52, 68r10f.4.1g.2.2 |
| spellingShingle | Lê Thành Dũng Nguyên Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix Logical Methods in Computer Science computer science - logic in computer science 03f52, 68r10 f.4.1 g.2.2 |
| title | Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix |
| title_full | Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix |
| title_fullStr | Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix |
| title_full_unstemmed | Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix |
| title_short | Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix |
| title_sort | unique perfect matchings forbidden transitions and proof nets for linear logic with mix |
| topic | computer science - logic in computer science 03f52, 68r10 f.4.1 g.2.2 |
| url | https://lmcs.episciences.org/5134/pdf |
| work_keys_str_mv | AT lethanhdungnguyen uniqueperfectmatchingsforbiddentransitionsandproofnetsforlinearlogicwithmix |