Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
2026-03-03 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors revisit a method for converting proof nets, a way to represent logical proofs, back into traditional step-by-step proofs. They use a new version of a graph theory result called Yeo's theorem, focusing on coloring parts of the graph without changing its structure. This lets them identify special points, called splitting vertices, which help break down the proof net into smaller parts to recover the original proof. Their approach works for different versions of linear logic and unifies several known results in a simpler way.
proof netslinear logicDanos-Regnier correctness criterionYeo's theoremgraph coloringsequent calculussplitting vertexcusp minimizationmix-rulemultiplicative-additive linear logic
Authors
Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, Lionel Vaux Auclair
Abstract
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, which we can impose to be a par-vertex, or a terminal vertex, or a non-axiom vertex, etc., in a modular way. This approach applies in presence of the mix-rules as well as for proof nets of unit-free multiplicative-additive linear logic (through an appropriate further generalization of Yeo's theorem). 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.