# 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

► To cite this version:

Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, Lionel Vaux Auclair. Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic. 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), Jul 2025, Birmingham, United Kingdom. 10.4230/LIPIcs.FSCD.2025.16 . hal-05149336

HAL Id: hal-05149336

https://hal.science/hal-05149336v1

Submitted on 25 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

Rémi Di Guardia ☐

Université Paris Cité, CNRS, IRIF, Paris, France

Olivier Laurent ☐

CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France

Lorenzo Tortora de Falco ☐

Università Roma Tre, Dipartimento di Matematica e Fisica, Rome, Italy

GNSAGA, Istituto Nazionale di Alta Matematica, Rome, Italy

Lionel Vaux Auclair ☐

Aix Marseille Univ, CNRS, I2M, Marseille, France

## 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 $\mathcal{N}$-vertex, on a splitting $\otimes$-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.

**2012 ACM Subject Classification** Mathematics of computing → Graph coloring; Theory of computation → Linear logic

**Keywords and phrases** Linear Logic, Proof Net, Sequentialization, Graph Theory, Yeo's Theorem

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2025.16

**Funding** Rémi Di Guardia: Partially funded by the French PEPR integrated project EPIQ (ANR-22-PETQ-0007).

Olivier Laurent: Partially funded by French ANR project ReCiProg (ANR-21-CE48-0019).

Lionel Vaux Auclair: Partially funded by French ANR projects PPS (ANR-19-CE48-0014), Lambda-Comb (ANR-21-CE48-0017), and ReCiProg (ANR-21-CE48-0019).

## 1 Introduction

Proof nets are a major contribution from linear logic [14]. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof nets represent proofs as general graphs respecting some *correctness criterion* [7], which imposes the absence of a particular kind of cycle. Proof nets identify derivations of the sequent calculus up to rule commutations and, as a consequence of this canonicity, results like cut elimination become easier to prove in this formalism. A key theorem in this approach is the fact that each proof net is indeed the

<figure><img src="image_2.png" /></figure>

© Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, and Lionel Vaux Auclair; licensed under Creative Commons License CC-BY 4.0

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025).

Editor: Maribel Fernández; Article No. 16; pp. 16:1–16:18

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
16:2 Yeo's Theorem for Locally Colored Graphs: The Path to Sequentialization in LL

graph representation of a derivation of sequent calculus: the process of recovering such a
derivation tree is called sequentialization. Many proofs of this result can be found in the
literature [14, 7, 16, 18, 5, etc.], but proving sequentialization is still considered as not easy.

Not only many proofs but more generally many equivalent correctness criteria have been
introduced in the last 40 years, based on the existence or absence of particular paths in an
associated graph (long trips, switching cycles, alternating-elementary-cycles) [14, 7, 34], on
the success of a rewriting procedure (contractibility, parsing) [6, 26, 21, 8], on homological [30]
or topological [29] properties, etc. They all describe the same set of valid graphs (those
which are the image of a sequent calculus derivation) but through very different statements
of properties characterizing the appropriate structure. The diversity of these approaches
reflects both the central nature of the concept of proof net in linear logic, and the variety
of motivations in the design of correctness criteria: some ensure tight complexity bounds
(especially those based on contractibility), some weave connexions with other fields (e.g.,
topology or graph theory), some are more naturally generalized to other logical systems, etc.

On the other hand, when it comes to the study of the theory of proof nets (confluence,
normalization, reduction strategies, etc.) most of those approaches are hardly usable in
practice. This gives the Danos-Regnier criterion [7] a special status: the absence of switching
cycles is of direct use for proving results about proof nets. For instance, it forbids the
occurrence of axiom-cut cycles along cut elimination [17]; it ensures the confluence of
reduction in multiplicative-exponential linear logic [33]; it provides the existence of so-called
closed cuts [27], which play a crucial rôle in geometry of interaction [15]; it allows for the
definition of a parallel procedure of cut elimination for multiplicative-exponential linear
logic [20]; etc. This means in particular that, based on this criterion, it becomes possible
to develop the theory of proof nets without referring to the sequent calculus anymore. For
this reason, we are interested in a better understanding of this precise criterion and its links
with the sequential structure of tree derivations, via sequentialization. Following previous
lines of work on relating graph theory and proof net theory [34, 10, 32], we looked for a
direct link between graph properties and the sequential structure of proof nets: splitting
vertices. Indeed the key step for extracting a sequent calculus derivation from a proof net is
to inductively decompose it into sub-graphs themselves satisfying the correctness condition.

In graph theory, it is common to have several (equivalent) characterizations for a same class
of graphs, and an inductive characterization may allow for simpler proofs – see e.g., cographs,
$k$-trees or graphs with a unique perfect matching. Such an inductive characterization may be
deduced from the existence of a vertex or an edge separating the graph in a “nice” manner
(e.g. a bridge [3]). Five theorems yielding such a vertex or edge have been shown equivalent
by Szeider [38], meaning they can be deduced from each other using an encoding of the graph
under consideration. Among those five are Yeo’s theorem on colored graphs [39], Kotzig’s
theorem on unique perfect matchings [25], but also Shoesmith and Smiley’s theorem on
turning vertices [37] – interestingly the approach of the latter bears striking resemblance
with our own work, that we discuss more in detail in the last part of the paper.

On the proof net side, Rétoré remarked that perfect matchings provided an alternative
presentation of proof nets [34]: in this context, he recovered sequentialization proofs based on
different notions of splitting vertex, in the spirit of Kotzig’s theorem. Remarkably, Nguyễn
later established that Kotzig’s theorem is in fact equivalent to the sequentialization theorem
of unit-free multiplicative proof nets with *mix* [32], again through graph encodings.

In the present paper, we focus on Yeo's theorem [39] instead, which is about *edge-colored* undirected graphs. Our goal is to obtain the existence of splitting vertices in proof nets by a direct application of a Yeo-style statement to an edge-coloring of the proof net (with no
<figure><img src="image_4.png" /><figcaption>Figure 1 Example of Yeo's theorem with a filled splitting vertex and dotted connected components.</figcaption></figure>

modification of the graph structure at all). In an edge-colored graph, a cycle is *alternating* when all its consecutive edges have different colors. Yeo's theorem states that an edge-colored graph $G$ with no alternating cycle has a *splitting vertex* $v$, i.e. such that no connected component of $G-v$ (the removal of $v$) is joined to $v$ with edges of more than one color – see Figure 1. This decomposition can be carried on, so as to give an inductive representation of graphs with no alternating cycle. This important structural result on edge-colored graphs has been used extensively in the literature (see e.g. the book [3] or papers such as [1, 12]).

To allow a direct application to proof nets, we generalize Yeo's theorem in two directions. First, we consider a more general notion of edge-coloring, that we called *local coloring*: it associates a color with each endpoint of each edge (this is equivalent to coloring half-edges, but we avoid to introduce half-edges formally, just to stick to more basic graph-theoretic notions). Second, we introduce a parameter (a set of *vertex-color pairs*, i.e. a set of vertices labeled with colors) which gives us finer control over the obtained splitting vertex.

Our proof of this new result is elementary and based on a key lemma we call *cusp minimization*, as well as on the definition of an ordering on vertex-color pairs induced by local coloring. Formally, a cusp in a path of a locally colored graph is a pair of two successive edges, such that the color associated with the middle vertex is the same for both edges. The ordering on vertex-color pairs is induced by particular cusp-free paths. Moreover, given a cycle $\omega$ containing a cusp, and a non-cusp vertex $v$ of $\omega$, satisfying some additional technical conditions, our cusp minimization result (Lemma 6) yields either a cusp-free cycle, or another cycle with strictly less cusps than $\omega$, but also having $v$ as a non-cusp vertex. In a locally colored graph without cusp-free cycle, our generalization of Yeo's theorem then follows easily by considering a maximal vertex-color pair among those in the parameter.

Cusp minimization also provides a proof of the original version of Yeo's theorem, as simple as known short proofs from the literature [28, 31]. While the generalization to local colorings gives a statement that we prove equivalent to Yeo's theorem, it seems difficult to reduce the parametrized version to the non-parametrized one. We moreover show how the local and parametrized generalization of Yeo's theorem allows to deduce each of the statements considered in [38] (as well as [13, Theorem 2]), simply by choosing appropriate colorings, without modifying the sets of vertices and edges of the graph under consideration.

Back to linear logic and the theory of proof nets, it is possible to derive the existence of a splitting vertex (in the sense of sequentialization) from the generalization of Yeo's theorem, and we are even able to modularly focus on a particular kind of splitting vertex: an arbitrary splitting vertex, a splitting multiplicative vertex ($\mathcal{N}$ or $\otimes$), a splitting $\mathcal{N}$ (a.k.a. section [7]), a terminal splitting multiplicative vertex, etc. From any of these choices, a sequentialization procedure is easy to deduce. Notably, this proof of the sequentialization theorem applies directly in the presence of the *mix* rules, and the *mix*-free case can be easily deduced.

Putting everything together, we get a direct simple proof of sequentialization for the Danos-Regnier criterion, assuming no prerequisite in graph theory. The path to sequentialization in linear logic that we propose starts from cusp minimization then goes to the generalization of Yeo's theorem and concludes with the extraction of an inductive decomposition of proof nets.
16:4 Yeo's Theorem for Locally Colored Graphs: The Path to Sequentialization in LL

**Outline.** This paper is organized into three parts: first a purely graph-theoretical part leading to our generalization of Yeo's theorem; then two independent segments leveraging this result, one about proof nets of linear logic and sequentialization, and another on graph theory comparing our generalization to other graph statements. We start by recalling usual notions (graphs, paths, ...) and with our definition of local coloring (Section 2). Then we state and prove our generalization of Yeo's theorem (Theorem 8), through the cusp minimization lemma (Section 3). Next comes the part about logic, with a definition of unit-free multiplicative linear logic with the *mix* rules and the associated notion of proof net (Section 4). We then give various proofs of the sequentialization theorem for these proof nets, leveraging our generalization of Yeo's theorem (Section 5). Last, we go back to graph theory and show the parameter-free version of our Yeo-style result is equivalent to the original one, and how to use it to deduce, in a straightforward way by only defining an appropriate coloring, the four other equivalent theorems from [38] as well as a generalization of Yeo's theorem to *H*-colored graphs [13, Theorem 2] (Section 6).

2 Graphs and Cusps

2.1 Partial Undirected Graphs and Paths

As we take interest in proof nets and Yeo's theorem in this paper, we study undirected paths
in finite undirected partial multigraphs. We recall here quickly some basic notions from
graph theory, for more details we refer the reader to [2].

A (finite undirected multi) **partial graph** (without loop) is a triple $(\mathcal{V}, \mathcal{E}, \psi)$ where $\mathcal{V}$ (**vertices**) and $\mathcal{E}$ (**edges**) are finite sets and $\psi$ (**the incidence function**) associates to each edge a set of at most two vertices. An edge $e$ is **total** when $\psi(e)$ is of cardinal two, and a **total graph** (or simply a **graph**) is one whose edges are total. Many notions lift immediately from total graphs to partial graphs, e.g. isomorphisms – that we denote $\simeq$. An edge $e$ is **incident** to a vertex $v$ if $v \in \psi(e)$, in which case $v$ is an **endpoint** of $e$.

A path $p$ is a finite alternating sequence of vertices and edges ($v_0, e_1, v_1, e_2, v_2, \dots, e_n, v_n$)
such that for all $i \in \{1; \dots; n\}$, the endpoints of $e_i$ are exactly $v_{i-1}$ and $v_i$ (which are distinct).
A path always has at least one vertex, but it can have no edge and be reduced to a single
vertex ($v_0$), in which case it is called an **empty path**. With the notation above, $v_0$ is the
**source** of $p$, $v_n$ is its **target** and both make the **endpoints** of $p$. Since a given vertex may
occur more than once in a path, we may have to talk about **occurrences of vertices in a
path** to distinguish these equal values. We use the following notations:

- the **concatenation** of two paths $p_1 = (v_0, e_1, \dots, e_k, v_k)$ and $p_2 = (v_k, e_{k+1}, \dots, e_n, v_n)$
  is the path $p_1 \cdot p_2 = (v_0, e_1, \dots, e_k, v_k, e_{k+1}, \dots, e_n, v_n)$;

- the **reverse** of a path $p = (v_0, e_1, v_1, \dots, e_k, v_k)$ is $\bar{p} = (v_k, e_k, v_{k-1}, \dots, e_1, v_0)$;

- if $v$ and $u$ are two (occurrences of) vertices of a path $p$, with $v$ occurring before $u$, $p_{(v,u)}$ is the unique **sub-path** (i.e. sub-sequence that is a path) of $p$ with source $v$ and target $u$.

A path is **simple** if its edges are pairwise distinct and its vertices are pairwise distinct except possibly its endpoints which may be equal. A path is **closed** if it has equal endpoints, otherwise it is **open**. A **cycle** is a non-empty simple closed path.

Given a partial graph $G = (\mathcal{V}, \mathcal{E}, \psi)$, a **sub-graph** of $G$ is a partial graph $G' = (\mathcal{V}', \mathcal{E}', \psi')$
such that $\mathcal{V}' \subseteq \mathcal{V}$, $\mathcal{E}' \subseteq \mathcal{E}$ and $\psi'$ is the restriction of $\psi$ to $\mathcal{E}'$ in its domain and sets of $\mathcal{V}'$
in its codomain. Connectedness is not immediate to define in partial graphs because paths
go from vertices to vertices. Two vertices $v$ and $u$ are **connected** when there exists a path
with endpoints $v$ and $u$. Two edges are **connected** if they are incident to two connected
vertices. An edge *e* and a vertex *v* are **connected** if *e* is incident to a vertex connected to *v*. A partial graph *G* is **connected** when any two different vertices or edges of *G* are connected. A **connected component** is a non-empty connected sub-graph maximal for the inclusion.

## 2.2 Local Coloring and Cusps

Let $G$ be a (partial) graph. A **local coloring** of $G$ is a function $c$ taking as arguments an edge $e$ and one of its endpoints $v$. By convention, the elements $c(e, v)$ are called **colors**. The intuition is that given an edge $e$ and one of its endpoints $v$, $c(e, v)$ is the color of $e$ according to $v$. A local coloring can also be seen as a coloring of half-edges, i.e. $c(e, v)$ is the color of the half of $e$ near $v$. When drawing a graph, we therefore represent $c(e, v)$ by coloring the part of $e$ touching $v$, with colors also given by the shape of the edges (solid, dashed, ... ). We recover the standard notion of **edge-coloring**, which maps edges to colors, when for every edge $e$, $c(e, \_\_)$ has the same value for all endpoints of $e$. An example of locally colored graph is given on Figure 2, where $c(e, v) = \text{solid}$, $c(e, u) = \text{solid}$, $c(f, u) = \text{solid}$, $c(f, w) = \text{dashed}$, $c(g, v) = \text{dashed}$, $c(g, w) = \text{solid}$ and $c(h, v) = \text{dotted}$.

A **cusp** at $v$ of color $\alpha$ is a triple $(e, v, f)$ where $e$ and $f$ are distinct edges such that $v$ is an endpoint of both of these edges and $c(e, v) = \alpha = c(f, v)$. In this case, $v$ is called the **vertex of the cusp**, $\alpha$ the **color of the cusp** and $(v, \alpha)$ is called a **cusp-point**. More generally, we will consider in this paper **vertex-color pairs** which are pairs made of a vertex and a color, and a cusp-point is a particular instance of a vertex-color pair. The locally colored graph in Figure 2 has two cusps, $(e, u, f)$ and $(f, u, e)$, both of vertex $u$ and color **solid**, so that $(u, \text{solid})$ is the only cusp-point of this graph.

A **cusp of a path** $p$ is a cusp made by a sub-sequence $(e, v, f)$ of this path or, in case $p$ is closed, a cusp $(e_n, v_0, e_1)$ made by its last edge $e_n$, its source (and target) $v_0$ and its first edge $e_1$. Remark that the reverse of a path contains the same number of cusps as this path. A **cusp-free path**, also called an **alternating path**, is one without cusp. Given a **non-empty** path $p$, whose source is $v_0$ and first edge is $e_1$, its **starting color** is $c(e_1, v_0)$. Similarly, if its target is $v_n$ and its last edge is $e_n$, then the **ending color** of $p$ is $c(e_n, v_n)$. Remark the starting (resp. ending) color of $\bar{p}$ is the ending (resp. starting) color of $p$. For instance, in the graph depicted on Figure 2 the path $(v, e, u, f, w)$ has one cusp at $u$ of color **solid**, its starting color is **solid** and its ending one is **dashed**.

**Fact 1.** Let $\omega$ be a cycle with no cusp at its source, and $\alpha$ a color. Then $\alpha$ is not the starting color of $\omega$ or $\alpha$ is not the starting color of $\bar{\omega}$.

We call **splitting** a vertex $v$ such that any cycle containing it has a cusp at $v$. We will show in Section 6.1 that this fits the notion at play in the conclusion of Yeo's theorem [39].

**Remark 2.** We invented this “local coloring”, which is not standard in the literature, and the name “cusp”. When used only through the notions of cusps and splitting vertices, that a given color is used on different vertices has no impact. Hence, we could use different sets of colors depending on each vertex, or not use more colors than the maximal degree of the graph. Equivalently, a local coloring is an equivalence relation on the edges incident to $v$, for each vertex $v$. We keep the idea of local coloring as it is a direct generalization of edge-coloring.

# 3 A Generalization of Yeo's Theorem

We prove a version of Yeo's theorem [39] for locally colored partial graphs, which is moreover parametrized by the choice of a set of vertex-color pairs (subject to a technical condition): Theorem 8. We first fix a partial graph $G$ with a local coloring $c$.
<figure><img src="image_5.png" /><figcaption>Figure 2 Example of locally colored graph.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 3 Illustration of Lemma 6.</figcaption></figure>

The main idea is to follow a path that is an evidence of progression, i.e. a strict partial order $\uparrow$: a vertex is smaller than another when there is a path from the first to the second, and we will prove that a maximal vertex is splitting. As the hypothesis of the theorem is about cusp-free cycles, it makes sense to consider cusp-free paths in this ordering. However, two issues prevent $\uparrow$ from being an order. First, the concatenation of two cusp-free paths may not be cusp-free. To have $\uparrow$ transitive, we impose a condition on the starting and ending colors of the cusp-free path – which is why we consider vertex-color pairs and not simply vertices. Second, there is no reason for this relation $\uparrow$ of “being linked by a cusp-free path” to not loop. Hence, we add a condition on the path that there is no way to go back on it, yielding from $\uparrow$ a relation $\triangleleft$ which will be our strict partial order. This entails the following:

**Definition 3.** Given vertices $v$ and $u$, and colors $\alpha$ and $\beta$, we write $(v, \alpha) \uparrow^p (u, \beta)$ if $p$ is a simple open cusp-free path from $v$ to $u$ with starting color not $\alpha$ and with ending color $\beta$. We note $(v, \alpha) \triangleleft^p (u, \beta)$ when $(v, \alpha) \uparrow^p (u, \beta)$ and for all vertex $w$, color $\tau$ and path $q$ such that $(u, \beta) \uparrow^q (w, \tau)$, $w$ is not in $p$. We simply write $(v, \alpha) \triangleleft (u, \beta)$ when such a path exists.

**Lemma 4.** Let $v$, $u$ and $w$ be vertices, $\alpha$, $\beta$ and $\tau$ be colors, and $p$ and $q$ be paths. If $(v, \alpha) \triangleleft^p (u, \beta)$ and $(u, \beta) \uparrow^q (w, \tau)$ then $(v, \alpha) \uparrow^{p \cdot q} (w, \tau)$.

**Lemma 5.** The relation $\triangleleft$ is a strict partial order on vertex-color pairs.

The key ingredient for proving our Yeo-style theorem is showing that for any pair $(v, \alpha)$ maximal for the strict partial order $\triangleleft$, $v$ is splitting. It is a consequence of the following:

**Lemma 6 (Cusp Minimization).** Fix a partial graph $G$ with a local coloring. Assume $\omega$ is a cycle starting from a vertex $v$, with no cusp at $v$ but containing a cusp of vertex $u$ and color $\alpha$. If $(u, \alpha) \uparrow^q (w, \beta)$ with $w$ a vertex of $\omega$, then either there exists a cusp-free cycle or there exists a cycle $\omega'$ starting from $v$, with no cusp at $v$ and strictly less cusps than $\omega$.

**Proof.** Use Figure 3 as a reference for notations. W.l.o.g. $q$ has no vertex in common with $\omega$ other than its endpoints $u$ and $w$. We use the notation $v_1$ for the occurrence of $v$ at the source of $\omega$, and $v_2$ for its occurrence at the target of $\omega$.

By symmetry (considering the reverse of $\omega$ if necessary), we can assume that $w$ is in $\omega_{(u,v_2)}$ and if $w = v_2$ then $\beta$ is not the starting color of $\omega$. Indeed, if $w \notin \omega_{(u,v_2)}$, we reverse $\omega$. Otherwise and if $w = v_2$, we apply Fact 1 to $\omega$ and $\beta$ to get that $\omega$ or $\bar{\omega}$ respects our assumption.

Consider the cycles $\omega' = \omega_{(v_1,u)} \cdot q \cdot \omega_{(w,v_2)}$ and $d = q \cdot \bar{\omega}_{(w,u)}$ (see Figure 3). We count the cusps in $\omega$, $\omega'$ and $d$. Recall that $u$ is a cusp of $\omega$ of color $\alpha$, $q$ is cusp-free and its starting color is not $\alpha$, and that $\omega'$ has no cusp at $v$ (by our symmetry argument above). Thus, there are $n_1 + 1 + n_2 + b_w^\omega + n_3$ cusps in $\omega$, $n_1 + b_w^{\omega'} + n_3$ in $\omega'$, and $b_w^d + n_2$ in $d$, where:
n$_1$ (resp. n$_2$, n$_3$) is the number of cusps of $\omega_{(v_1,u)}$ (resp. $\omega_{(u,w)}$, $\omega_{(w,v_2)}$);

$b_w^\omega$ (resp. $b_w^{\omega'}$, $b_w^d$) is 1 if $\omega$ (resp. $\omega'$, $d$) has a cusp at $w$ and 0 otherwise.

If $\omega'$ has strictly less cusps than $\omega$ we are done, otherwise $b_w^{\omega'} \ge 1 + n_2 + b_w^\omega$. Hence, $n_2 = 0$, $b_w^\omega = 0$ and $b_w^{\omega'} = 1$. But the latter two imply $b_w^d = 0$, so that $d$ is a cusp-free cycle. ◀

**Proposition 7.** Let $v$ be a non-splitting vertex of a locally colored partial graph which has no cusp-free cycle. For any color $\alpha$ there exists a cusp-point $(u, \beta)$ such that $(v, \alpha) \triangleleft (u, \beta)$.

**Proof.** Since $v$ is not splitting, it is the source (and target) of a cycle $\omega$ which has no cusp at $v$. W.l.o.g. $\omega$ has a minimal number of cusps among all such cycles, and has not $\alpha$ as a starting color (thanks to Fact 1 and as reversing a path preserves the number and vertices of cusps). For $\omega$ cannot be cusp-free, it contains at least one cusp: denote by $u$ the vertex of the first cusp of $\omega$, and by $\beta$ its color. We have $(v, \alpha) \xrightarrow{\omega_{(v,u)}} (u, \beta)$, and conclude $(v, \alpha) \triangleleft (u, \beta)$ by Lemma 6, the minimal number of cusps of $\omega$ and the absence of cusp-free cycles. ◀

A set $P$ of vertex-color pairs **dominates** cusp-points if for any cusp-point $(v, \alpha)$, either $(v, \alpha) \in P$ or there is $(u, \beta) \in P$ with $(v, \alpha) \triangleleft (u, \beta)$. Our main result follows by Proposition 7.

**Theorem 8 (Parametrized Local Yeo).** Take $G$ a partial graph with a local coloring and pose $P$ a set of vertex-color pairs which dominates cusp-points. If $G$ has no cusp-free cycle, the vertex of any $\triangleleft$-maximal element of $P$ is splitting.

# 4 Multiplicative Proof Nets

## 4.1 Unit-Free Multiplicative Linear Logic with Mix

We focus on unit-free multiplicative linear logic whose formulas are given by:

$$A ::= X \mid X^{\perp} \mid A \otimes A \mid A \not\otimes A$$

The **dual** operator ($\_\perp$) is extended to an involution on all formulas by De Morgan duality: $(X^\perp)^\perp = X$, $(A \otimes B)^\perp = A^\perp \not\otimes B^\perp$ and $(A \not\otimes B)^\perp = A^\perp \otimes B^\perp$. We consider the deduction system $\text{MLL}_{\text{hyp}}^{0,2}$ of *open* derivations in cut-free multiplicative linear logic with *mix* rules:

$$\frac{\vdash A, \Gamma \quad \vdash B, \Delta}{\vdash A^\perp, A} \quad (ax) \quad \frac{\vdash A, B, \Gamma}{\vdash A \otimes B, \Gamma, \Delta} \quad (\otimes) \quad \frac{\vdash A, B, \Gamma}{\vdash A \not\otimes B, \Gamma} \quad (\not\otimes) \quad \frac{\vdash \Gamma \quad \vdash \Delta}{\vdash \Gamma, \Delta} \quad (\text{mix}_2) \quad \frac{\vdash (\text{mix}_0)}{\vdash A} \quad (\text{hyp})$$

The (*hyp*) rule introduces an **hypothesis** $A$ in a derivation, with $A$ a single formula. We restrict ourselves to a single formula not because we consider the (*mix*$_2$) rule but because substitution of proof structures along more than one edge is much more complex. In this restricted setting, it is clear that all hypotheses formulas of a proof belong to distinct sequents and that we only need substitution of one hypothesis at a time. If $\pi$ is a derivation with hypotheses $\vdash A_1, \dots, \vdash A_n$ and conclusion $\vdash B_1, \dots, B_k$, we call $\pi$ a **derivation of** $A_1, \dots, A_n \vdash B_1, \dots, B_k$. If $\pi_1$ is a derivation of $\Sigma \vdash \Gamma$, $A$ and $\pi_2$ is a derivation of $A, \Theta \vdash \Delta$, the **substitution** of $\pi_1$ in $\pi_2$ is a derivation of $\Sigma, \Theta \vdash \Gamma, \Delta$: it is obtained from $\pi_2$ by replacing the (*hyp*) rule on $\vdash A$ with $\pi_1$ (this adds $\Gamma$ to all sequents of $\pi_2$ below $\vdash A$).

To be formal, we should be more precise on how we handle occurrences of formulas (e.g. considering sequents as lists and having an explicit exchange rule) but we keep this implicit.
<figure><img src="image_7.png" /><figcaption>Figure 4 Example of proof structure.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Figure 5 Locally colored proof structure.</figcaption></figure>

We also consider the following rewriting of derivations which we call **mix-Rétoré reduction** (due to its similarity to Rétoré's reduction on the exponential connective $\vdash$ [6, page 77], with contraction and weakening forming a monoid):

$$ \frac{\vdash \Gamma \quad \vdash^{(\text{mix}_0)}} \quad \vdash^{(\text{mix}_2)}}}{\vdash \Gamma} \rightsquigarrow \vdash \Gamma $$

$$ \frac{\vdash^{(\text{mix}_0)}} \quad \vdash \Gamma}{\vdash \Gamma} \rightsquigarrow \vdash^{(\text{mix}_2)} \rightsquigarrow \vdash \Gamma $$

It defines a confluent and strongly normalizing rewriting system on derivations.

**Lemma 9 (Mix-Rétoré Normal Forms).** If $\pi$ is a derivation in mix-Rétoré normal form, either it is $\vdash^{(\text{mix}_0)}$, or it does not contain the $(\text{mix}_0)$ rule and it proves a non-empty sequent.

## 4.2 Proof Structures

A **proof structure** is a partial graph with labeled vertices and edges. Edges are labeled with formulas, and vertices with names of the three following rules: $ax$, $\otimes$ or $\mathcal{Y}$. Vertices are named according to their label: $ax$-vertices, $\otimes$-vertices and $\mathcal{Y}$-vertices. Some additional local constraints are required depending on the label of vertices, also pictured below:

<figure><img src="image_9.png" /></figure>

- each $ax$-vertex has two incident edges, called its **conclusions**, labeled with dual formulas;

- each $\otimes$-vertex has three incident edges, labeled by $A$, $B$ and $A \otimes B$ for some formulas $A$ and $B$; the first two edges are its **premises**, the last one is its **conclusion**;

- each $\mathcal{Y}$-vertex has three incident edges, labeled by $A$, $B$ and $A \mathcal{Y} B$ for some formulas $A$ and $B$; the first two edges are its **premises**, the last one is its **conclusion**;

- an edge is the premise of at most one vertex and the conclusion of at most one vertex.

An example of proof structure is given on Figure 4. A vertex is **terminal** when all its conclusions have exactly one endpoint (or equivalently, are not premises). An edge that is the premise of no vertex is a **conclusion** of the proof structure. An edge that is the conclusion of no vertex is an **hypothesis** of the proof structure.

**Remark 10.** There are many ways to define proof structures. In the typed multiplicative case considered here, it is easy to check our definition is equivalent to others in the literature (e.g. [14, 32]). To strictly recover the usual notion of proof structure, and to distinguish for example the two proof structures with two conclusions typed $X^{\perp} \mathcal{Y} X^{\perp}$ and $X \otimes X$, we should impose an order on the premises of vertices, as well as on the hypotheses and conclusions: we do not do so since this has no impact on correctness nor on (proofs of) sequentialization.
To identify proof structures corresponding to proofs, and create a distinction between ⊗- and ℧-vertices, it is usual to ask for a proof structure to respect a correctness criterion. As explained in the introduction, we use one due to Danos and Regnier [7]. A path in a proof structure is called **switching** when it does not contain the two premises of any ℧-vertex. A proof structure is **DR-correct** (and is called a **proof net**) if it has no switching cycle.

**Remark 11.** The original definition of the acyclicity condition in the Danos-Regnier correctness criterion [7] (extended to (*mix*₂) in [11]) is in fact slightly different. They consider **correctness graphs**: graphs obtained by removing one of the two premises of each ℧-vertex. A proof structure is correct when all its correctness graphs are acyclic (and connected in the original work without the *mix* rules). This condition is equivalent to the fact that any cycle in the proof structure must contain the two premises of some ℧-vertex (i.e. no cycle is *feasible* in the sense of [11]). This is also equivalent to the apparently weaker condition that any cycle in the proof structure must go through the two premises of some ℧-vertex consecutively:

**Lemma 12 (Local-Global Principle).** A simple path that never goes through the two premises of a ℧-vertex consecutively (including as last and first edges for a cycle) is a switching path.

## 4.3 Desequentialization

We define, by induction on a derivation $\pi$ of $A_1, \dots, A_n \vdash B_1, \dots, B_k$, its **desequentialization** $\mathcal{D}(\pi)$ which is a DR-correct proof structure with hypotheses labeled $A_1, \dots, A_n$ and conclusions labeled $B_1, \dots, B_k$.

- If $\pi$ is reduced to an ($ax$) rule with conclusion $\vdash A^{\perp}, A$, then $\mathcal{D}(\pi)$ is the proof structure with one $ax$-vertex $v$ and two edges labeled $A^{\perp}$ and $A$, both with unique endpoint $v$.

$$ \overline{\vdash A^{\perp}, A}^{(ax)} \mapsto A \underbrace{\vdash ax}_{\mathcal{D}(\pi)} A $$

- If the last rule of $\pi$ is a ($\otimes$) rule applied to two derivations $\pi_1$ and $\pi_2$ then $\mathcal{D}(\pi)$ is obtained from the disjoint union of $\mathcal{D}(\pi_1)$ and $\mathcal{D}(\pi_2)$ by adding a new ⊗-vertex $v$. The conclusions of $\mathcal{D}(\pi_1)$ and $\mathcal{D}(\pi_2)$ labeled by the principal formulas $A$ and $B$ of the ($\otimes$) rule now have $v$ as an additional endpoint, and we add a new edge, labeled $A \otimes B$, with $v$ as unique endpoint.

<figure><img src="image_10.png" /></figure>

- If the last rule of $\pi$ is a ($\aleph$) rule applied to a derivation $\pi_1$ then $\mathcal{D}(\pi)$ is obtained from $\mathcal{D}(\pi_1)$ by adding a new ℧-vertex $v$. The conclusions of $\mathcal{D}(\pi_1)$ labeled by the principal formulas $A$ and $B$ of the ($\aleph$) rule now have $v$ as an additional endpoint, and we add a new edge, labeled $A \aleph B$, whose unique endpoint is $v$.

<figure><img src="image_11.png" /></figure>
16:10 Yeo's Theorem for Locally Colored Graphs: The Path to Sequentialization in LL

■ If the last rule of $\pi$ is a $(mix_2)$ rule applied to two derivations $\pi_1$ and $\pi_2$ then $\mathcal{D}(\pi)$ is the disjoint union of $\mathcal{D}(\pi_1)$ and $\mathcal{D}(\pi_2)$.

$$ \frac{\begin{array}{c} \pi_1 \\ \vdash \Gamma \\ \vdash \Delta \end{array} \quad \begin{array}{c} \pi_2 \\ \vdash \Gamma, \Delta \end{array}}{(mix_2)} \quad \mapsto \left( \begin{array}{c} \mathcal{D}(\pi_1) \\ \vdots \\ \mathcal{D}(\pi_2) \end{array} \right) $$

■ If $\pi$ is reduced to a $(mix_0)$ rule, $\mathcal{D}(\pi)$ is the empty proof structure (no vertex, no edge).

$$ \vdash \begin{array}{c} (mix_0) \\ \bar{\quad} \end{array} \quad \mapsto \quad \vdash \begin{array}{c} (hyp) \\ \bar{\quad} \end{array} $$

■ If $\pi$ is reduced to a $(hyp)$ rule on $\vdash A$, then $\mathcal{D}(\pi)$ is the proof structure with no vertex and a single edge with no endpoint, labeled A.

$$ \vdash \begin{array}{c} A \end{array} \quad \mapsto \quad \left| \begin{array}{c} A \end{array} \right. $$

There is a bijection between the $(ax)$, $(\otimes)$ and $(\mathcal{Y})$ rules of $\pi$ and the vertices of $\mathcal{D}(\pi)$. Moreover, if $\pi_2$ is obtained from $\pi_1$ by a mix-Rétoré reduction then $\mathcal{D}(\pi_1) \simeq \mathcal{D}(\pi_2)$.

**► Lemma 13 (Desequentialization of a substitution).** If $\pi$ is the substitution of a derivation $\pi_1$ for a hypothesis A in a derivation $\pi_2$, then $\mathcal{D}(\pi)$ is obtained from the disjoint union of $\mathcal{D}(\pi_1)$ and $\mathcal{D}(\pi_2)$ by identifying the conclusion e of $\mathcal{D}(\pi_1)$ labeled A with the hypothesis e' of $\mathcal{D}(\pi_2)$ labeled A. The obtained edge has label A and endpoints the union of those of e and e'.

5 Sequentialization from Parametrized Local Yeo

This section is dedicated to show how sequentialization results (see [14, 7, 6, 11] for example) can be deduced from Theorem 8. We provide several proofs of the known statement:

**► Theorem 14 (Sequentialization [14, 7, 6, 11]).** Given a DR-correct proof structure $\rho$, there exists a derivation $\pi$ in MLL$_{hyp}^{0,2}$ such that $\rho \simeq \mathcal{D}(\pi)$; $\pi$ is called a **sequentialization** of $\rho$.

The first step is to define the following local coloring c (see Figure 5 for an example):

■ for an $ax$-vertex $v$ of conclusions $e_1$ and $e_2$, set $c(e_1, v) = \text{solid}$ and $c(e_2, v) = \text{dashed}$;

■ for a $\otimes$-vertex $v$ of premises $e_1$ and $e_2$ and conclusion $f$, set $c(e_1, v) = \text{solid}$, $c(e_2, v) = \text{dotted}$ and $c(f, v) = \text{dashed}$;

■ for a $\mathcal{Y}$-vertex $v$ of premises $e_1$ and $e_2$ and conclusion $f$, set $c(e_1, v) = c(e_2, v) = \text{solid}$ and $c(f, v) = \text{dashed}$.

Note the cusp-points of a colored proof structure are exactly the pairs $(v, \text{solid})$ where $v$ is a $\mathcal{Y}$-vertex – which is in fact the only condition we need and requires a local coloring (see the left $ax$ in Figure 5). In all this section, we assume proof structures to be colored this way. Then, the absence of switching cycles means there is no cusp-free cycle. Theorem 8 gives a splitting vertex for any set $P$ dominating cusp-points – i.e. pairs $(v, \text{solid})$ with $v$ a $\mathcal{Y}$-vertex.

Observe that, with the local coloring we have fixed, we recover the notions of splitting $\otimes$- or $\mathcal{Y}$-vertex which play a crucial rôle in most of the sequentialization results for DR-correct proof structures: finding such a vertex allows to decompose a proof net in smaller components, and to deduce sequentialization inductively. Indeed, for $v$ a splitting vertex:

■ If $v$ is a $\otimes$-vertex with conclusion labeled $A \otimes B$, its premises and conclusion are not connected, except through $v$. By removing $v$, we obtain three disjoint proof structures: $\rho_1$ with a conclusion A, $\rho_2$ with a conclusion B, and $\rho_0$ with a hypothesis $A \otimes B$. By induction hypothesis, we get corresponding derivations $\pi_1, \pi_2$ and $\pi_0$. By adding a $(\otimes)$ rule to $\pi_1$ and $\pi_2$, and substituting the obtained derivation in $\pi_0$, we get a sequentialization of $\rho$.
- If $v$ is a $\mathcal{N}$-vertex with conclusion labeled $A \mathcal{N} B$, its premises are not connected to its conclusion, except through $v$. By removing $v$ from $\rho$, we obtain two disjoint proof structures: $\rho_1$ with conclusions $A$ and $B$, and $\rho_0$ with a hypothesis $A \mathcal{N} B$. By induction hypothesis, we get two corresponding derivations $\pi_1$ and $\pi_0$. By adding a ($\mathcal{N}$) rule to $\pi_1$ and substituting the obtained derivation in $\pi_0$, we obtain a sequentialization of $\rho$.

- If $v$ is an $ax$-vertex with conclusions labeled $A^{\perp}$ and $A$, its conclusions are not connected, except through $v$. By removing $v$ from $\rho$, we obtain two disjoint proof structures: $\rho_1$ with a hypothesis $A^{\perp}$ and $\rho_2$ with a hypothesis $A$. By induction hypothesis, we get two corresponding derivations $\pi_1$ and $\pi_2$. By first substituting a derivation reduced to a single ($ax$) rule into $\pi_1$, and then substituting the result in $\pi_2$, we get a sequentialization of $\rho$.

We fix a DR-correct proof structure $\rho$: $\rho$ has no cusp-free cycle. We review how natural choices for the parameter $P$ in Theorem 8 yield various proofs of Theorem 14, differing only in the order in which splitting vertices are selected along the sequentialization procedure. Each of these choices satisfies the hypothesis of Theorem 8 trivially: $P$ contains all cusp-points.

**General splitting vertices.** Take $P$ the set of all vertex-color pairs. By Theorem 8, for each $\triangleleft$-maximal element $(v, \alpha) \in P$, the vertex $v$ is splitting. As described above, $v$ allows to decompose $\rho$ and to go on by induction. It remains only to treat the case $P = \emptyset$, i.e. without vertex. If $\rho$ is empty (no vertex, no edge), it is the desequentialization of the derivation reduced to a $(mix_0)$ rule. If $\rho$ is a single edge (with no endpoint), it is the desequentialization of a derivation reduced to a ($hyp$) rule. Else, decomposing $\rho$ into connected components corresponds to applying $(mix_2)$ rules on the sequent calculus side.

**Splitting $\mathcal{N}$- or $\otimes$-vertices.** Let $P := \{(v, \alpha) \mid v$ is a $\otimes$- or $\mathcal{N}$-vertex and $\alpha$ is a color in $\rho\}$. By Theorem 8, each $\triangleleft$-maximal element $(v, \alpha) \in P$ yields a splitting vertex $v$, which must be a $\mathcal{N}$- or $\otimes$-vertex. We reason inductively as before, which leaves only the case $P = \emptyset$: all vertices must be $ax$-vertices and we reason as above, splitting along connected components that can be an $ax$-vertex with its two conclusions or an edge without endpoint.

**Splitting $\mathcal{N}$-vertices (a.k.a. sections) [7].** Let $P$ be the set of all cusp-points: a $\triangleleft$-maximal element of $P$ is $(v, \alpha)$ with $v$ a splitting $\mathcal{N}$-vertex by Theorem 8, so we can reason inductively. It remains only to treat the case $P = \emptyset$ (i.e. no $\mathcal{N}$-vertex, hence no cusp in $\rho$): by DR-correctness, $\rho$ is cycle-free, and all the remaining vertices are splitting.

**Splitting terminal vertices [14].** Let $P := \{(v, \text{solid}) \mid v$ is a $\otimes$- or $\mathcal{N}$-vertex$\} \cup \{(v, \text{dotted}) \mid v$ is a $\otimes$-vertex$\}$, and let $(v, \alpha) \in P$ be maximal for $\triangleleft$. Then $v$ is not only splitting by Theorem 8, but it is also terminal. Indeed, otherwise its conclusion $e$ has another endpoint $u$. This $u$ must be a $\otimes$- or $\mathcal{N}$-vertex (as $e$ can only be one of its premises, and these are the only vertices with premises). Then $(v, \alpha) \overset{(v,e,u)}{\rhd} (u, c(e, u))$ since $c(e, v) = \text{dashed} \neq \alpha$. Moreover, we cannot have $(u, c(e, u)) \overset{p}{\rhd} (v, \beta)$ for a color $\beta$ as this would yield a cusp-free cycle $(v, e, u) \cdot p$. We obtain $(v, \alpha) \triangleleft (u, c(e, u))$, contradicting the maximality of $(v, \alpha)$. So, if $P \neq \emptyset$, we obtain a splitting terminal $\otimes$- or $\mathcal{N}$-vertex. The sequentialization procedure is then the same as before, except that we can focus on terminal vertices all along.

Now having sequentialization for MLL$_{hyp}^{0,2}$, we consider some restrictions and characterize sub-systems of the sequent calculus by means of properties of their image in proof structures.

**Hypothesis-free derivations.** A derivation $\pi$ contains no ($hyp$) rule if and only if $D(\pi)$ is hypothesis-free (i.e. each edge is the conclusion of some vertex). We thus recover the usual sequentialization result of (hypothesis-free) proof nets into (($hyp$)-free) derivations. Note that following the *splitting terminal vertices* procedure above, we never need to consider ($hyp$) rules nor hypotheses in proof structures. Indeed, if $\rho$ is hypothesis-free
16:12 Yeo's Theorem for Locally Colored Graphs: The Path to Sequentialization in LL

and $v$ is a splitting terminal vertex: the components associated with the premises of $v$ are also hypothesis-free; and those associated with its conclusions are reduced to a single hypothesis edge, so there is no need to perform a substitution.

**Connected proof structures.** Another important sub-system is obtained by removing the *mix* rules, which is captured by a connectedness property of DR-correct proof structures. Given some DR-correct proof structure $\rho$, the **DR-connectedness degree** $d(\rho)$ is the number of connected components of any its correctness graphs (see Remark 11). Note that, thanks to acyclicity, $d(\rho)$ does not depend on the choice of the correctness graph. We say $\rho$ is **DR-connected** if $d(\rho) = 1$ (in particular it is not empty). Given a derivation $\pi$, one can check that $d(D(\pi)) = 1 + \#mix_2 - \#mix_0$, where $\#mix_i$ is the number of $(mix_i)$ rules in $\pi$. In particular, derivations without *mix* have a DR-connected desequentialization. Conversely, depending on $d(\rho)$, we can transform the derivations $\pi$ such that $\rho \simeq D(\pi)$ to obey some constraints on *mix*-rules, without changing their image by $D$. By Lemma 9, if $\pi$ is a mix-Rétoré normal form, then $\pi$ contains $(mix_0)$ if and only if $D(\pi)$ is empty, and $\pi$ contains $(mix_2)$ if and only if $d(D(\pi)) > 1$. Combined with Theorem 14, we obtain:

**Theorem 15 (Connected sequentialization).** *Given a DR-connected and DR-correct proof structure $\rho$ (i.e. $d(\rho) = 1$), there exists a mix-free derivation $\pi$ such that $\rho \simeq D(\pi)$.*

# 6 Comparison of our Generalized Yeo's Theorem with the Literature

## 6.1 Local and Global Colorings

First, remark our parametrized version implies a simpler one, closer to Yeo's theorem.

**Theorem 16 (Local Yeo).** *Take $G$ a partial graph equipped with a local coloring and with at least one vertex. If $G$ has no cusp-free cycle, then there exists a splitting vertex in $G$.*

**Proof.** The set $P$ of all vertex-color pairs of $G$ is finite and non-empty (if we only consider colors used in $G$, plus a dummy one if there is no such color), and thus contains a maximal element $(v, \alpha)$ with respect to $\triangleleft$ (Lemma 5). The vertex $v$ is splitting (Theorem 8). ◀

As an example, the graph depicted on Figure 2 has no cusp-free cycle, and $u$ is its only splitting vertex. We now bridge the gap with the terminology from Yeo's theorem [39] and prove it is a direct consequence of our local version. For $G$ a partial graph and $v$ a vertex of $G$, the partial graph $G \setminus v$ is the sub-graph obtained by removing $v$ from the vertices of $G$ (same edges with possibly less endpoints). This gives an alternative characterization of splitting vertices: a vertex $v$ is splitting if and only if any two edges with endpoint $v$ and connected in $G \setminus v$ have the same color on $v$. Let us move to the terminology for total graphs:

- As $G \setminus v$ leads in general to a partial graph, it has to be replaced with the operation $G - v$ on total graphs, which removes not only $v$ but also all its incident edges. Connectedness on partial graphs gives the standard notion when restricted to total graphs.

- Recall the standard notion of **edge-coloring** that maps edges to colors. An **alternating cycle** for an edge-coloring is the restriction of the same notion for a local coloring: a cycle whose consecutive edges are of different colors, including its last and first edges.

**Theorem 17 (Yeo's Theorem).** *If $G$ is a non-empty edge-colored (total) graph with no alternating cycle, then there exists a vertex $v$ of $G$ such that no connected component of $G - v$ is joined to $v$ with edges of more than one color.*
<figure><img src="image_12.png" /><figcaption>■ **Figure 6** Example of encoding of local coloring as edge-coloring, where filled vertices are splitting ones and square vertices represent added ones.</figcaption></figure>

**Proof.** Call $c$ the edge-coloring of $G$, we set a local coloring $c'$ by $c'(e, v) = c(e)$. Alternating cycles with respect to $c'$ are those with respect to $c$. Theorem 16 yields a splitting vertex $v$, so no connected component of $G-v$ is joined to $v$ with edges of more than one color. ◀

While Theorem 16 seems more general than Theorem 17, we deduce the first from the second by a graph encoding. Partial edges play no role, so we consider only total graphs. Take $G$ a graph with local coloring $c$, we associate with it a graph $\bar{G}$ with an edge-coloring $\bar{c}$:

- all vertices of $G$ are considered as vertices of $\bar{G}$ (and some are going to be added);

- with each edge $e$ of $G$ of endpoints $v$ and $u$ such that $c(e, v) = c(e, u)$, we associate one edge $f$ in $\bar{G}$ with the same endpoints as $e$ and $\bar{c}(f) = c(e, v)$;

<figure><img src="image_13.png" /></figure>

- with each edge $e$ of $G$ of endpoints $v$ and $u$ such that $c(e, v) \neq c(e, u)$ and $e$ is in a cycle, we associate two edges $f_1$ and $f_2$ and a new vertex $w$, the endpoints of $f_1$ being $v$ and $w$, and the endpoints of $f_2$ being $w$ and $u$, with $\bar{c}(f_1) = c(e, v)$ and $\bar{c}(f_2) = c(e, u)$;

<figure><img src="image_14.png" /></figure>

- with each edge $e$ of $G$ of endpoints $v$ and $u$ such that $c(e, v) \neq c(e, u)$ and $e$ is not in a cycle (i.e. $e$ is a bridge), we associate one edge $f$ in $\bar{G}$ with the same endpoints as $e$ and an arbitrary color $\bar{c}(f)$.

<figure><img src="image_15.png" /></figure>

An example of this encoding is on Figure 6. The key properties of this encoding are that:

- alternating cycles in the obtained graph $\bar{G}$ correspond to those of $G$;

- a vertex of $G$ is splitting in $G$ if and only if the corresponding one is splitting in $\bar{G}$;

- no added vertex is splitting in $\bar{G}$.

Using these properties, one easily deduces Theorem 16 for a graph $G$ with a local coloring $c$ from Theorem 17 applied to $\bar{G}$ and $\bar{c}$.

► **Remark 18.** The encoding (___) is not stable by sub-graph, e.g. after removing the leftmost splitting (filled) vertex in the graph on Figure 6, the unique solid-dashed edge should not be encoded with a vertex in its middle anymore, because it is no longer in a cycle. An encoding stable by sub-graph seems hard to come by. In particular, an idea that cannot work is adding a same “gadget” graph in the middle of each edge (or of each “bicolored” edge) so as to
<figure><img src="image_16.png" /><figcaption>Figure 7 No edge-coloring for Theorem 20.</figcaption></figure>

<figure><img src="image_17.png" /><figcaption>Figure 8 No edge-coloring for Theorem 22.</figcaption></figure>

duplicate each edge and color them correspondingly – whether this gadget is simply a single vertex or a more complex graph. Indeed, the gadget to add must not have any cusp-free cycle so as to be able to apply Theorem 17, nor should it have any splitting vertex as one wants to find a splitting vertex in the original graph. Such a graph cannot exist by Theorem 17 itself!

## 6.2 Variants of Yeo's Theorem

It is known that Yeo's theorem is equivalent to various other graph-theoretical results. In particular, Szeider [38] exhibited four such alternative statements. One of them is Kotzig's theorem, proved equivalent to the sequentialization of unit-free multiplicative proof nets with *mix* [32]. We will also consider the generalization of Yeo's theorem to *H*-coloring from [13].

In [38] are given non-trivial encodings of graphs into graphs such that applying one theorem on an encoding allows to prove another theorem on the initial graph. We show here that Theorem 8 provides a natural unifying principle subsuming all these results (Theorems 17, 19–22, and 25). Indeed, we prove each of these results by applying Theorem 8 to a well-chosen local coloring of the graph with no modification of its structure (vertices and edges), giving somehow “encoding-less” proofs. Besides, this implies that our proof of Theorem 8 *via* cusp minimization is also a proof of each of these results, just by adapting the definition of a cusp.

A **perfect matching** (or 1-factor) of an undirected total graph $G$ is a set of edges $F$ such that every vertex has a unique edge in $F$ incident to it. It is well known that a perfect matching $F$ in a graph $G$ is unique if and only if $G$ contains no **F-alternating cycle**, which is a cycle whose edges are alternatively in and out of $F$, including the last and first ones (it is e.g. a simple variant of [4, Theorem 1] which considers $F$-alternating open paths). A **bridge** is an edge whose removal increases the number of connected components of the graph.

**Theorem 19 (Kotzig [25]).** If a graph $G$ has a unique perfect matching $F$, then $G$ has a bridge which belongs to $F$.

*Proof.* It suffices to define an edge-coloring $c$ of $G$ into $\{0,1\}$ by $c(e) = 1$ iff $e \in F$. Then $F$-alternating cycles are exactly cusp-free cycles, so by Theorem 16 (here even Theorem 17 would suffice) there is a splitting vertex $v$. The unique edge of $F$ incident to $v$ is a bridge. ◀

**Theorem 20 ([35]).** Take a graph $G$ and a function $\phi$ from its vertices to its edges such that $\phi(v)$ is incident to $v$ for all vertex $v$. If $G$ has no cycle $\omega$ satisfying $\phi(v) \in \omega$ for every $v \in \omega$, then there exists a vertex $u$ such that $\phi(u)$ is a bridge.

*Proof.* Set a local coloring into $\{0,1\}$ by $c(e, v) = 1$ iff $e = \phi(v)$. With this local coloring, $G$ has no cusp-free cycle, so Theorem 16 gives a splitting vertex $v$: $\phi(v)$ is a bridge. ◀

Note that an edge-coloring $c$ cannot prove Theorem 20 without changing the structure of the graph: consider the graph drawn on Figure 7. For the cycle $\omega = (u, f, w, e, v, \phi(u), u)$ to have exactly cusps corresponding to vertices $z$ such that $\phi(z) \notin \omega$, we need $c(f) = c(e)$ (at $w$), $c(e) = c(\phi(u))$ (at $v$) and $c(\phi(u)) \neq c(f)$ (at $u$), absurd.
**Theorem 21 ([19]).** Any 2-edge-colored graph has a splitting vertex or an alternating cycle.

**Proof.** This is just the particular case of Theorem 17 restricted to two colors. ◀

The next theorem considers *undirected paths* in *directed graphs*. A **directed graph** is the same as a graph defined in this paper, except the incidence function $\psi$ yields an ordered pair $(v, u)$ given a directed edge $a$: $v$ is the **source** of $a$, while $u$ is its **target**. An **undirected path** is a path in the underlying graph where one forgets the orientation of the edges. (See [2] for more details.) In a directed graph, a vertex $v$ of a cycle $\omega$ is a **turning vertex** of $\omega$ if all directed edges incident to $v$ in $\omega$ are either all of source $v$ or all of target $v$.

**Theorem 22 (Shoesmith and Smiley [37]).** If a non-empty set $S$ of vertices of a directed graph $G$ contains a turning vertex of each undirected cycle of $G$, then $S$ contains a vertex which is a turning vertex of every undirected cycle it belongs to.

**Proof.** Forget the orientation of the graph, but let $c(e, v) = 0$ if $v \in S$ is the source of $e$, $c(e, v) = 1$ if $v \in S$ is the target of $e$ and $c(e, v) = e \notin \{0; 1\}$ otherwise. Cycles with no turning vertex in $S$ are exactly cusp-free cycles, so Theorem 8 with $P := \{(v, \alpha) \mid v \in S, \alpha \in \{0; 1\}\}$ yields a splitting vertex $v \in S$, which is a turning vertex of every cycle it belongs to. ◀

We need the parametrized version of our result to deal in a simple way with the parameter $S$. Here again, an edge-coloring $c$ is not enough for proving Theorem 22 without changing the structure of the graph: look at Figure 8 with all vertices in $S$. To have the equivalence between cycles without turning vertex and cusp-free cycles, one needs $c(f) = c(g) \neq c(e) = c(f)$.

**Remark 23.** Shoesmith and Smiley's stated and proved Theorem 22 to handle a particular kind of proofs represented as graphs [36], sharing striking similarities with proof nets of multiplicative linear logic (notably, forbidding some classes of cycles).<fnref n="1" /> Moreover, Theorem 22 can be used directly to obtain a splitting $\mathcal{Y}$ in a proof net by instantiating $S$ as the set of all $\mathcal{Y}$-vertices. Furthermore, Shoesmith and Smiley's proof of this theorem is quite similar to our proof by cusp minimization: the key idea of both proofs is to look at cycles with a minimal number of cusps (or turning vertices). Still, there are important differences: we construct an explicit order relation on vertex-color pairs, while their proof builds an infinite path to reach a contradiction; besides, the association of colors with vertices in our parameter makes our result more modular. This is particularly relevant for proof nets: Theorem 22 seems limited to giving a splitting $\mathcal{Y}$, without the unifying character of Theorem 8 seen in Section 5.

Theorem 16 implies another generalization of Yeo's theorem [13]. An *H-coloring* is an edge-coloring with colors the vertices of a graph *H*. An *H-cycle* is a cycle where the colors of consecutive edges (including the last and first ones) are linked by an edge in *H*. When *H* is a complete graph, we recover the standard edge-coloring and *H*-cycles correspond to alternating cycles. A **complete multipartite** graph *R* has vertices $S_1 \cup \dots \cup S_k$ (disjoint union) where each $S_i$ is an independent set of vertices (no edge in *R* between vertices of $S_i$) and if $v \in S_i$ and $u \in S_j$ (with $i \neq j$) then there is exactly one edge between them in *R*.

**Definition 24.** Given a graph $G$ with an $H$-coloring $c$, and $v$ a vertex of $G$, $G_v$ is the graph with vertices the edges of $G$ incident to $v$, and one edge between $e$ and $f$ if and only if their colors $c(e)$ and $c(f)$ are linked by an edge in $H$.

<footnote n="1">¹ We were not aware of this work during the research leading to the present paper: it only came to our attention via Szeider's equivalence results [38]. As far as we know, 46 years after the publication of [36] and 37 years after the publication of [14], the first line of work has been ignored by the linear logic community: it would certainly be of interest to investigate further connexions with proof nets.</footnote>
**Theorem 25** ([13, Theorem 2]). *Take H a graph and G a non-empty H-colored graph. Assume G has no H-cycle and that, for every vertex v of G, $G_v$ is a complete multipartite graph. Then there exists a vertex v of G such that every connected component D of G-v satisfies that the set of edges of G between v and vertices of D is an independent set in $G_v$.*

**Proof.** Define a local coloring $c$ by $c(e, v)$ is the independent set in $G_v$ to which $e$ belongs. For $G$ has no $H$-cycle, it has no cusp-free cycle for $c$, and the result follows by Theorem 16. ◀

As far as we know, this theorem was not known to be equivalent to Yeo's theorem before.

## 7 Conclusion

We gave a new simple proof of sequentialization, as a corollary of a generalization of Yeo's theorem (Theorem 8), by defining an appropriate coloring. This new theorem is very modular: it can give a splitting terminal vertex, a splitting $\mathcal{Y}$-vertex, or a general splitting vertex. This generalization has a simple proof, that can be reformulated as a proof of sequentialization just by defining what is a cusp in proof structures. It also allows to deduce theorems known to be equivalent (Theorems 17, 19–22, and 25), again just by defining a coloring. Thus, our simple proof can also be adapted as one of any of these results by defining what is a cusp.

Focusing on proof nets, this approach can be extended to richer systems than cut-free MLL. As usual, dealing with cuts is easy once we know how to deal with $(\otimes)$ rules. Dealing with multiplicative units is also straightforward, as long as we allow for *mix*-rules and forget about DR-connectedness [11]: those just amount to the introduction of premise-free vertices, without any particular treatment. Our approach is also successful without the *mix*-rules, in a framework with a jump edge for each $\perp$-vertex (linking it with another vertex) [18, 23, 22]. One should only take care that cusps are exactly made by the non-jump premises of $\mathcal{Y}$-vertices; this can be done *e.g.* by giving a new color to each jump edge.

Similarly, sequentialization in presence of exponentials – with structural rules (weakening, contraction, dereliction for the ? modality) and promotion – is also easy to deduce from the multiplicative case: contraction is treated as a $\mathcal{Y}$-vertex, and promotion boxes allow to sequentialize inductively. Again, this works both with the *mix*-rules or with jump edges [18].

Dealing with additive connectives in the spirit of the unit-free multiplicative-additive proof nets from Hughes and van Glabbeek [24] requires more work, but our approach can be adapted, yielding a proof of sequentialization in a much more involved context. The main price to pay is establishing a further generalization of Theorem 8 allowing some cusp-free cycles – whose proof also reposes on the cusp minimization lemma. The argumentation for the additives then follows the same idea as the one for MLL: a non-splitting vertex cannot be maximal for $\langle\Delta\rangle$. As in MLL, the approach is robust enough to also enable sequentialization through terminal vertices, as opposed to what is done in [24]. Nevertheless, the technical details are a bit more involved, making this result out of scope for the present paper.

More details about the results presented in this paper and in particular regarding the extension to the additive connectives can be found in [9, Part II].

## References

1. A. Abouelaoualim, K.Ch. Das, L. Faria, Y. Manoussakis, C. Martinhon, and R. Saad. Paths and trails in edge-colored graphs. *Theoretical Computer Science*, 409(3):497–510, 2008. doi:10.1016/j.tcs.2008.09.021.

2. Adrian Bondy and U. S. R. Murty. *Graph Theory*. Number 1 in Graduate Texts in Mathematics. Springer London, 2008. URL: https://link.springer.com/book/9781846289699.
3 Jørgen Bang-Jensen and Gregory Z Gutin. *Digraphs: theory, algorithms and applications.* Springer Science & Business Media, 2008.

4 Claude Berge. Two theorems in graph theory. *Proceedings of the National Academy of Sciences of the United States of America*, 43(9):842-844, September 1957. URL: https://www.jstor.org/stable/89875.

5 Pierre-Louis Curien. Introduction to linear logic and ludics, part II. lecture notes cs/0501039, arXiv, 2005. URL: https://arxiv.org/abs/cs/0501039.

6 Vincent Danos. *La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du λ-calcul).* Thèse de doctorat, Université Paris VII, 1990.

7 Vincent Danos and Laurent Regnier. The structure of multiplicatives. *Archive for Mathematical Logic*, 28:181-203, 1989. doi:10.1007/BF01622878.

8 Paulin Jacobé de Naurois and Virgile Mogbil. Correctness of linear logic proof structures is NL-complete. *Theoretical Computer Science*, 412(20):1941-1957, 2011. doi:10.1016/j.tcs.2010.12.020.

9 Rémi Di Guardia. *Identity of Proofs and Formulas using Proof-Nets in Multiplicative-Additive Linear Logic*. Thèse de doctorat, École Normale Supérieure de Lyon, September 2024.

10 Thomas Ehrhard. A new correctness criterion for MLL proof nets. In Thomas A. Henzinger and Dale Miller, editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 38:1-38:10. ACM, 2014. doi:10.1145/2603088.2603125.

11 Arnaud Fleury and Christian Retoré. The mix rule. *Mathematical Structures in Computer Science*, 4(2):273-285, 1994. doi:10.1017/S0960129500000451.

12 Shinya Fujita, Ruonan Li, and Shenggui Zhang. Color degree and monochromatic degree conditions for short properly colored cycles in edge-colored graphs. *Journal of Graph Theory*, 87(3):362-373, 2018. doi:10.1002/jgt.22163.

13 Hortensia Galeana-Sánchez, Rocío Rojas-Monroy, Rocío Sánchez-López, and Juana Imelda Villareal-Valdés. H-cycles in H-colored multigraphs. *Graphs and Combinatorics*, 38:62, 2022. doi:10.1007/s00373-022-02464-4.

14 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1-102, 1987. doi:10.1016/0304-3975(87)90045-4.

15 Jean-Yves Girard. Geometry of interaction I: an interpretation of system *F*. In Ferro, Bonotto, Valentini, and Zanardo, editors, *Logic Colloquium '88*. North-Holland, 1988.

16 Jean-Yves Girard. Quantifiers in linear logic II. In Corsi and Sambin, editors, *Nuovi problemi della logica e della filosofia della scienza*, pages 79-90, Bologna, 1991. CLUEB.

17 Jean-Yves Girard. Linear logic: its syntax and semantics. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, *Advances in Linear Logic*, volume 222 of *London Mathematical Society Lecture Note Series*, pages 1-42. Cambridge University Press, 1995.

18 Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. In Aldo Ursini and Paolo Agliano, editors, *Logic and Algebra*, volume 180 of *Lecture Notes in Pure and Applied Mathematics*, pages 97-124, New York, 1996. Marcel Dekker.

19 Jerrold W. Grossman and Roland Häggkvist. Alternating cycles in edge-partitioned graphs. *Journal of Combinatorial Theory, Series B*, 34(1):77-81, 1983. doi:10.1016/0095-8956(83)90008-4.

20 Giulio Guerrieri, Giulia Manara, Lorenzo Tortora de Falco, and Lionel Vaux Auclair. Confluence for proof-nets via parallel cut elimination. In Nikolaj S. Bjørner, Marijn Heule, and Andrei Voronkov, editors, *LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024*, volume 100 of *EPiC Series in Computing*, pages 464-483. EasyChair, 2024. doi:10.29007/VKFN.

21 Stefano Guerrini. Correctness of multiplicative proof nets is linear. In *Proceedings of the fourteenth annual symposium on Logic in Computer Science*, pages 454-463, Trento, July 1999. IEEE, IEEE Computer Society Press. doi:10.1109/LICS.1999.782640.

22 Dominic Hughes. Simple multiplicative proof nets with units, 2005. arXiv:math/0507003.
16:18 Yeo's Theorem for Locally Colored Graphs: The Path to Sequentialization in LL

23 Dominic Hughes. Simple free star-autonomous categories and full coherence. *Journal of Pure and Applied Algebra*, 216(11):2386-2410, 2012. doi:10.1016/j.jpaa.2012.03.020.

24 Dominic Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. *ACM Transactions on Computational Logic*, 6(4):784-842, 2005. doi:10.1145/1094622.1094629.

25 Anton Kotzig. On the theory of finite graphs with a linear factor II. *Matematicko-Fyzikálny Časopis*, 09(3):136-159, 1959. In Slovak, with as original title Z teórie konečných grafov s lineárnym faktorom II. URL: https://eudml.org/doc/29908.

26 Yves Lafont. From proof nets to interaction nets. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, *Advances in Linear Logic*, volume 222 of London Mathematical Society Lecture Note Series, pages 225-247. Cambridge University Press, 1995.

27 Olivier Laurent. Polynomial time in untyped elementary linear logic. *Theoretical Computer Science*, 813:117-142, 2020. doi:10.1016/J.TCS.2019.10.002.

28 Ruonan Li and Bo Ning. A revisit to Bang-Jensen-Gutin conjecture and Yeo's theorem. preprint, 2022. doi:10.48550/arXiv.2207.03793.

29 Paul-André Melliès. A topological correctness criterion for multiplicative non-commutative logic. In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Philip J. Scott, editors, *Linear Logic in Computer Science*, volume 316 of London Mathematical Society Lecture Note Series, pages 283-322. Cambridge University Press, November 2004.

30 François Métayer. Homology of proof-nets. *Archive for Mathematical Logic*, 33(3):169-188, 1994. doi:10.1007/bf01203031.

31 Gleb Nenashev. A short proof of Kotzig's theorem. preprint, 2014. doi:10.48550/arXiv.1402.0949.

32 Lê Thành Dũng Nguyễn. Unique perfect matchings, forbidden transitions and proof nets for linear logic with mix. *Logical Methods in Computer Science*, 16(1), February 2020. doi:10.23638/LMCS-16(1:27)2020.

33 Michele Pagani and Lorenzo Tortora de Falco. Strong normalization property for second order linear logic. *Theoretical Computer Science*, 411(2):410-444, 2010. doi:10.1016/J.TCS.2009.07.053.

34 Christian Retoré. Handsome proof-nets: perfect matchings and cographs. *Theoretical Computer Science*, 294(3):473-488, 2003. doi:10.1016/S0304-3975(01)00175-X.

35 Paul D. Seymour. Sums of circuits. *Graph Theory and Related Topics*, pages 341-355, 1978.

36 D. J. Shoesmith and T. J. Smiley. *Multiple-Conclusion Logic*. Cambridge University Press, 1978.

37 D. J. Shoesmith and T. J. Smiley. Theorem on directed graphs, applicable to logic. *Journal of Graph Theory*, 3(4):401-406, 1979. doi:10.1002/jgt.3190030412.

38 Stefan Szeider. On theorems equivalent with Kotzig's result on graphs with unique 1-factors. *Ars Combinatoria*, 73:53-64, 2004. URL: https://www.ac.tuwien.ac.at/files/pub/szeider-AC-2004.pdf.

39 Anders Yeo. A note on alternating cycles in edge-coloured graphs. *Journal of Combinatorial Theory, Series B*, 69(2):222-225, 1997. doi:10.1006/jctb.1997.1728.