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

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 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 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 ( or $\otimes$), a splitting (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.

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.

The main idea is to follow a path that is an evidence of progression, i.e. a strict partial order $\Rsh$: 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 $\Rsh$ from being an order. First, the concatenation of two cusp-free paths may not be cusp-free. To have $\Rsh$ 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 $\Rsh$ 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 $\Rsh$ a relation $⊲$ which will be our strict partial order. This entails the following:

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

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:

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

• $\mathrm{■}$

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

• $\mathrm{■}$

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

• $\mathrm{■}$

  for a -vertex $v$ of premises $e_1$ and $e_2$ and conclusion $f$, set $\text{c}(e_1,v)=\text{c}(e_2,v)=\text{solid}$ and $\text{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 -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 -vertex.

Observe that, with the local coloring we have fixed, we recover the notions of splitting $\otimes$- or -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:

• $\mathrm{■}$

  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$.

• $\mathrm{■}$

  If $v$ is a -vertex with conclusion labeled $AB$, 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 $AB$. By induction hypothesis, we get two corresponding derivations ${\pi }_1$ and ${\pi }_0$. By adding a () rule to ${\pi }_1$ and substituting the obtained derivation in ${\pi }_0$, we obtain a sequentialization of $\rho$.

• $\mathrm{■}$

  If $v$ is an ax-vertex with conclusions labeled $A^{⟂}$ 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^{⟂}$ 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 $⊲$-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=\mathrm{\varnothing }$, i.e. without vertex. If $\rho$ is empty (no vertex, no edge), it is the desequentialization of the derivation reduced to a (${\text{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 (${\text{mix}}_2$) rules on the sequent calculus side.

Splitting - or $\otimes$-vertices.

Let $P≔\{(v,\alpha )\mid v\text{ is a }\otimes \text{- or -vertex and }\alpha \text{ is a color in }\rho \}$. By Theorem 8, each $⊲$-maximal element $(v,\alpha )\in P$ yields a splitting vertex $v$, which must be a - or $\otimes$-vertex. We reason inductively as before, which leaves only the case $P=\mathrm{\varnothing }$: 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 -vertices (a.k.a. sections) [7].

Let $P$ be the set of all cusp-points: a $⊲$-maximal element of $P$ is $(v,\alpha )$ with $v$ a splitting -vertex by Theorem 8, so we can reason inductively. It remains only to treat the case $P=\mathrm{\varnothing }$ (i.e. no -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\text{ is a }\otimes \text{- or -vertex}\}\cup \{(v,\text{dotted})\mid v\text{ is a }\otimes \text{-vertex}\}$, and let $(v,\alpha )\in P$ be maximal for $⊲$. 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 -vertex (as $e$ can only be one of its premises, and these are the only vertices with premises). Then $(v,\alpha )\stackrel{(v,e,u)}{\Rsh }(u,\text{c}(e,u))$ since $\text{c}(e,v)=\text{dashed}\ne \alpha$. Moreover, we cannot have $(u,\text{c}(e,u))\stackrel{𝑝}{\Rsh }(v,\beta )$ for a color $\beta$ as this would yield a cusp-free cycle $(v,e,u)\cdot p$. We obtain $(v,\alpha )⊲(u,\text{c}(e,u))$, contradicting the maximality of $(v,\alpha )$. So, if $P\ne \mathrm{\varnothing }$, we obtain a splitting terminal $\otimes$- or -vertex. The sequentialization procedure is then the same as before, except that we can focus on terminal vertices all along.

Now having sequentialization for ${\text{MLL}}_{\text{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 $𝒟(\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 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(𝒟(\pi ))=1+\mathrm{\#}{\text{mix}}_2-\mathrm{\#}{\text{mix}}_0$, where $\mathrm{\#}{\text{mix}}_i$ is the number of (${\text{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 𝒟(\pi )$ to obey some constraints on mix-rules, without changing their image by $𝒟$. By Lemma 9, if $\pi$ is a mix-Rétoré normal form, then $\pi$ contains (${\text{mix}}_0$) if and only if $𝒟(\pi )$ is empty, and $\pi$ contains (${\text{mix}}_2$) if and only if $d(𝒟(\pi ))>1$. Combined with Theorem 14, we obtain:

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 -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, 20, 21, 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 -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 $\mathrm{?}$ modality) and promotion – is also easy to deduce from the multiplicative case: contraction is treated as a -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 $⊲$. 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].