2026-07-23T03:28:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23631 2025-10-27T10:30:25Z ddc:004 open_access

Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic Di Guardia, Rémi Laurent, Olivier Tortora de Falco, Lorenzo Vaux Auclair, Lionel Linear Logic Proof Net Sequentialization Graph Theory Yeo’s Theorem We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo’s theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting ⅋-vertex, on a splitting ⊗-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo’s theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Rémi Di Guardia and Olivier Laurent and Lorenzo Tortora de Falco and Lionel Vaux Auclair 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.16 urn:nbn:de:0030-drops-236317 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.16 eng https://creativecommons.org/licenses/by/4.0/legalcode