Lê Thành Dũng Nguyên - Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix

lmcs:5134 - Logical Methods in Computer Science, February 28, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:27)2020
Unique perfect matchings, forbidden transitions and proof nets for linear logic with MixArticle

Authors: Lê Thành Dũng Nguyên

    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. In this journal version, we have added an explanation of Retoré'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).

    Volume: Volume 16, Issue 1
    Published on: February 28, 2020
    Accepted on: February 18, 2020
    Submitted on: January 30, 2019
    Keywords: Computer Science - Logic in Computer Science,03F52, 68R10,F.4.1,G.2.2
      Source : OpenAIRE Graph
    • Expanding Logical Ideas for Complexity Analysis; Funder: French National Research Agency (ANR); Code: ANR-14-CE25-0005

    Consultation statistics

    This page has been seen 1597 times.
    This article's PDF has been downloaded 368 times.