Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

TL;DR

This paper generalizes Yeo's theorem for graphs with half-edge colorings to facilitate sequentialization proofs in linear logic proof nets, enabling modular derivation recovery without altering graph structures.

Contribution

It introduces a new graph-theoretic approach based on half-edge colorings to extract sequentiality information from proof nets, extending Yeo's theorem to handle mix-rules and unit-free multiplicative-additive linear logic.

Findings

Provides a modular method for recovering sequent calculus derivations from proof nets.

Generalizes Yeo's theorem to include proof nets with mix-rules.

Simplifies the extraction of sequentiality information without modifying graph structures.

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.