Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, Lionel Vaux Auclair

TL;DR

The novelty of this Yeo-style theorem is that it can be derived in a straightforward way, just by defining a dedicated coloring, without any modification of the underlying graph structure (vertices and edges) -- similar results from the literature required more involved encodings.

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.

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

TL;DR

The novelty of this Yeo-style theorem is that it can be derived in a straightforward way, just by defining a dedicated coloring, without any modification of the underlying graph structure (vertices and edges) -- similar results from the literature required more involved encodings.

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.
Paper Structure (37 sections, 71 theorems, 22 equations, 29 figures)

This paper contains 37 sections, 71 theorems, 22 equations, 29 figures.

Table of Contents

  1. Introduction
  2. Graphs and Cusps
  3. Partial Undirected Graphs and Paths
  4. Local Coloring and Cusps
  5. Cusp Minimization
  6. A Generalization of Yeo's Theorem
  7. Parametrized Local Yeo
  8. Terminality
  9. Comparison of our Generalized Yeo's Theorem with the Literature
  10. Local and Global Colorings
  11. Variants of Yeo's Theorem
  12. Multiplicative Proof Nets
  13. Unit-Free Multiplicative Linear Logic with Mix
  14. Proof Structures
  15. Desequentialization
  16. ...and 22 more sections

Key Result

Lemma 2.1

If $p_1$ and $p_2$ are two simple open paths and their unique common vertices are the target of $p_1$ and the source of $p_2$, and possibly the target of $p_2$ and the source of $p_1$, and if the last edge of $p_1$ is different from the first edge of $p_2$, then $p_1\cdot p_2$ is simple.

Figures (29)

  • Figure 1: Example of Yeo's theorem with a filled splitting vertex and dotted connected components
  • Figure 2: Example of locally colored partial graph
  • Figure 3: Illustration of \ref{['lem:bjumping_Yeo_base']}
  • Figure 4: Illustration of \ref{['lem:bjumping_gen']}
  • Figure 5: Illustration of the relation $\lhd$ (\ref{['def:orderyeo']})
  • ...and 24 more figures

Theorems & Definitions (159)

  • Lemma 2.1: Concatenation of Simple Paths
  • Lemma 2.2: Concatenation of Disjoint Simple Paths
  • Remark 2.4
  • Lemma 2.5: Cusp Minimization
  • proof
  • Remark 2.6
  • Corollary 2.7: Cusp Cycling
  • proof
  • Corollary 2.8: Cusp Minimization 2
  • proof
  • ...and 149 more