Enric Cosme-Llópez
email: enric.cosme-llopez@ens-lyon.fr

Damien Pous
email: damien.pous@ens-lyon.fr

K 4 -free Graphs as a Free Algebra *

Graphs of treewidth at most two are the ones excluding the clique with four vertices (K4) as a minor, or equivalently, the graphs whose biconnected components are series-parallel.

We turn those graphs into a finitely presented free algebra, answering positively a question by Courcelle and Engelfriet, in the case of treewidth two.

First we propose a syntax for denoting these graphs: in addition to parallel composition and series composition, it suffices to consider the neutral elements of those operations and a unary transpose operation. Then we give a finite equational presentation and we prove it complete: two terms from the syntax are congruent if and only if they denote the same graph. * This paper is an extended version of the one with the same title, published in Proc. MFCS'17 [7]; it contains all proofs, and some typos are fixed.

form the free algebra over the signature , • , where is an associative-commutative binary operation (parallel composition), and • is an associative binary operation (series composition). For instance, the terms ((a•(b c))•d) e and e (a•((c b)•d)) both denote the graph below, and they are equal up to associativity of • and commutativity of .

I. INTRODUCTION

The notion of treewidth is a cornerstone in (algorithmic) graph theory [START_REF] Diestel | Graph Theory[END_REF]. It measures how close a graph is from a forest, and classes of graphs of bounded treewidth often enjoy good computational properties. For instance, graph homomorphism (and thus k-colouring) becomes polynomialtime [START_REF] Grohe | The complexity of homomorphism and constraint satisfaction problems seen from the other side[END_REF], so does model-checking of Monadic Second Order (MSO) formulae, and satisfiability of MSO formulae becomes decidable, even linear. (See the monograph of Courcelle and Engelfriet about monadic second order logic on graphs [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF].)

Here we focus on graphs of treewidth at most two. They coincide with the partial 2-trees, with the K 4 -free graphs (those that exclude the clique with four vertices (K 4 ) as a minor), and with the graphs whose biconnected components are series-parallel [START_REF] Duffin | Topology of series-parallel networks[END_REF], [START_REF] Bodlaender | A partial k-arboretum of graphs with bounded treewidth[END_REF].

For reasons to become apparent later on, we consider the set Gph of directed graphs with edges labelled with letters a, b, . . . in some alphabet Σ, and with two distinguished vertices, called the input and the output. We represent such graphs as usual, using an unlabelled ingoing (resp. outgoing) arrow to denote the input (resp. output).

Such graphs can be composed:

• in parallel by putting them side by side, merging their inputs, and merging their outputs; • in series by putting them one after the other and merging the output of the first one with the input of the second. Every letter of the alphabet can be represented by the graph consisting of two vertices (the input and the output), and a single edge from the input to the output, labelled with the given letter.

If we allow only those operations, we obtain precisely the series-parallel graphs, and it is easy to see that these (Note that parallel composition is not idempotent: (a•b) (a•b) and a•b denote distinct graphs.) However, we cannot denote all graphs of treewidth at most two in such a way.

First the notion of treewidth does not depend on the orientation of the edges. For instance, the following graph has treewidth two, yet it is not the image of a term in the previous syntax. To this end, we add a unary operation • • to our signature, which we interpret in graphs as the exchange of input and output. Doing so, the terms (a•b • ) c and (b•a • ) • c denote the above graph, and series-parallel graphs with converse become a free algebra when we ask that • • is an involution that distributes over and satisfies (a•b) • = b • •a • . Second, the treewidth of a graph does not depend on selfloops, so that the following graph actually has treewidth one (it is a tree once we remove the self-loop). There it suffices to add a constant, 1, interpreted as the graph with a single vertex (both input and output), and no edge. Doing so, the above graph is denoted by a•(1 b)•c. While the constant 1 is clearly a neutral element for series composition (•), axiomatising its interactions with parallel composition is much harder, and is actually one of the key contributions of the present work. For instance, the equation (1 a)•(1 b) = 1 a b should belong to the theory as both sides denote the graph below:

a b G • H G H 1 G H G H G • G a a Figure 1
. The 2p-algebra of graphs and the graph of a letter Up-to this point, we have recovered the syntax of allegories [START_REF] Freyd | Categories, Allegories[END_REF], and the graphs associated to the terms are precisely the ones Freyd and Scedrov use to obtain that the theory of representable allegories is decidable, yet not finitely presentable [17, page 210].

But we still miss some graphs, like the one below:

a b c
One can also remark that we only obtain connected graphs using the above operations. Instead, treewidth allows disconnected graphs: a graph has a given treedwidth if and only if all of its connected components do. Surprisingly, it suffices to add a second constant, , interpreted as the disconnected graph with no edges and two distinct vertices (the input and the output). This allows us to obtain disconnected graphs, but also to get a term for the above connected graph, namely, a•((b• ) c). Again while it is clear that this constant is a neutral element for parallel composition ( ), capturing its interactions with the other operations is non-trivial. To sum up, the set Gph of graphs forms an algebra for the signature • 2 , 2 , • • 1 , 1 0 , 0 . The various operations of this algebra are depicted in Figure 1.

Write Trm for the set of terms over the alphabet Σ and TW 2 for the set of graphs of treewidth at most two when an extra edge is added between input and output. (See Section IV for this additional condition.) One easily proves that the latter set actually forms a subalgebra of the algebra of graphs. Therefore, the function interpreting each term as a graph actually gives a function g : Trm → TW 2 .

We first prove that this function has a right-inverse: we define a function t :

TW 2 → Trm such that for all graph G ∈ TW 2 , g(t(G)) is isomorphic to G: Trm TW 2 g t g(t(G)) G (1)
By doing so, we get that the graphs of treewidth at most two are exactly the ones that can be expressed using the syntax.

Our key contribution then consists in giving a finite equational axiomatisation of graph isomorphism over this syntax. Note that the choice of the syntax is important. Various finite syntaxes have already been proposed [START_REF] Courcelle | Graph grammars, monadic second-order logic and the theory of graph minors[END_REF], [START_REF] Diestel | Graph Theory[END_REF], [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF] to capture graphs of treewidth at most k, for a given k. However, some choices prevent finite presentations. For instance, while the converse operation we use could be eliminated by pushing it to the leaves, doing so would turn some of our axioms into infinite equational schemes. (See also Remark 28.)

u (v w) ≡ (u v) w (A1) u v ≡ v u (A2) u ≡ u (A3) u•(v•w) ≡ (u•v)•w (A4) u•1 ≡ u (A5) u •• ≡ u (A6) (u v) • ≡ u • v • (A7) (u•v) • ≡ v • •u • (A8) 1 1 ≡ 1 (A9) 1 u•v ≡ 1 (u v • )• (A10) u• ≡ (1 u• )• (A11) (1 u)•v ≡ (1 u)• v (A12)
As explained above, a few laws are rather natural like associativity of the two compositions, commutativity of , or the facts that 1 and are neutral elements and that • • is an involution. Those are the first eight laws in Figure 2. Surprisingly, the four subsequent axioms suffice to obtain a complete axiomatisation: for all terms u, v, u and v are provably equal using the axioms from Figure 2 if and only if g(u) and g(v) are isomorphic:

u ≡ v ⇔ g(u) g(v) (2)
In other words, calling a 2p-algebra an algebra satisfying the axioms from Figure 2, TW 2 is the free 2p-algebra. All axioms but (A3) are independent. (See Appendix C; Axiom (A3) follows from (A9) and (A12) but we keep it for the sake of clarity.) . Correctness, i.e., the left-to-right implication from [START_REF] Arnborg | An algebraic theory of graph reduction[END_REF], is easy to establish. Indeed, it suffices to compute and compare the graphs of each equation, and to prove that valid equations are stable under graph substitution. The converse implication, completeness, is much harder. This is because there is no canonical way of extracting a term out of a graph. In particular, the function t we define to this end has to make choices based on the concrete representation of the input graph, so that isomorphic graphs do not always map to syntactically equal terms.

We proceed in the following way to obtain completeness. First we prove that the function t maps isomorphic graphs to congruent terms:

G H ⇒ t(G) ≡ t(H) (3)
Then we prove that this function is an homomorphism (up to the axioms), which allows us to deduce that for all term u, t(g(u)) is provably equal to u:

t(g(u)) ≡ u (4)
In a sense, by interpreting a term u into a graph and then reading it back, we obtain a term t(g(u)) which plays the role of a normal form even if it is not canonical (which would typically be the case in rewriting theory, or in normalisation by evaluation [START_REF] Berger | An inverse of the evaluation functional for typed lambda-calculus[END_REF]). Defining a function t satisfying (1) could be done rather easily by relying on the notion of tree decomposition. However, doing so makes it extremely difficult to obtain properties (3) and ( 4): the notion of tree decomposition, despite its inductive nature, does not provide enough structure. Instead, we use the fact that treewidth at most two graphs are K 4 -free, and we exhibit stronger graph invariants that allow us to extract terms from graphs in a much more structured way.

For instance, when the graph is connected and when its input and output are distinct, one can compute its checkpoints: those vertices which all paths from the input to the output must visit. Those checkpoints are linearly ordered so that the graph necessarily has the following shape

• • •
If there is at least one checkpoint then the graph should be interpreted as a series composition. Otherwise, by the absence of K 4 as a minor, one can show that the graph necessarily is a non-trivial parallel composition.

The aforementioned step is already there in the standard result that the biconnected components of a K 4 -free graph are series-parallel. More challenging is the case when the input and output coincide. In this case, we consider the checkpoints of all pairs of neighbours of the input, and we show that they form a tree which is a minor of the starting graph. This tree is a key invariant of the isomorphism class of the graph and we show that one can extract a term for each choice of a node in this tree. This is where our function t has to rely on the concrete representation of the graph: although all choices of a node in the tree result in provably equal terms, they do not yield syntactically equal terms. A similar situation happens with components which are disconnected from the input and the output: we handle those recursively by taking any vertex as a new choice of input and output.

II. RELATED WORK

Except for the presence of , the algebra of graphs we work with has been proposed independently by Freyd and Scedrov [17,page 207], and by Andréka and Bredikhin [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF]. They used it to characterise the equational theory of binary relations over the considered signature. Indeed for every set S, the set P (S × S) of binary relations over S forms an algebra for the signature we consider in this paper: • is relational composition, is set-theoretic intersection (thus it is written ∩ in [START_REF] Freyd | Categories, Allegories[END_REF], [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF]), • • is transposition (converse), 1 is the identity relation and is the full relation. Writing Rel u ≤ v for the containments that hold in all such algebras of relations, and G H if there exists a graph homomorphism from H to G, we have the following equivalence.

Rel u ≤ v ⇔ g(u) g(v)
This characterisation immediately gives decidability: existence of a graph homomorphism is an NP-complete problem. Thanks to the present observation that graphs of terms have bounded treewidth, the complexity is actually polynomial [START_REF] Grohe | The complexity of homomorphism and constraint satisfaction problems seen from the other side[END_REF].

Freyd and Scedrov also use this characterisation to prove that this theory is not finitely presentable [START_REF] Freyd | Categories, Allegories[END_REF]: every complete equational axiomatisation must contain axioms corresponding to homomorphisms equating arbitrarily many vertices at a time, and thus must be infinite. Andréka and Bredikhin go even further and show that it is not even a variety [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF].

In this work we focus on isomorphism rather than on homomorphism, and this is why we do obtain a finite equational axiomatisation. Although all algebras of relations validate our axioms, these algebras cannot be free models. For instance, their parallel composition (intersection) is always idempotent.

Freyd and Scedrov remark that certain graphs cannot be the image of a term [17, page 207]; similarly, Andréka and Bredikhin use a weak form of the K 4 exclusion property [1, Lemma 7]. However, they cannot obtain a characterisation result since they do not consider , which is necessary to reach all graphs of treewidth at most two.

Our work is also really close to that of Dougherty and Gutiérrez [START_REF] Dougherty | Normal forms for binary relations[END_REF], who proposed an axiomatisation of graph isomorphism for a slightly different syntax: instead of the constant , they use a unary operation dom(•), called domain. This operation can be defined using : we have dom(u) = 1 (u• ); at the graphical level, it consists in relocating the output of a graph on its input. (Note that cannot be defined in terms of dom(•) and the other operations.)

Choosing this domain operation has the advantage of keeping connected graphs, and the disadvantage of being less general: disconnected graphs cannot be expressed. More importantly, the operation being more primitive than dom(•), we can obtain a shorter axiomatisation: while we share with [START_REF] Dougherty | Normal forms for binary relations[END_REF] the nine natural axioms from Figure 2 that do not mention , the four remaining ones in this figure have to be replaced by nine axioms when using dom(•): three about 1 and , and six about dom(•).

To prove completeness, Dougherty and Gutiérrez compute normal forms for terms using rewriting techniques. Like in the present work, their normal forms are not canonical and some additional work is needed. In a second part of the paper, they characterise graphs of terms using a minor exclusion theorem which corresponds precisely to what we obtain in the connected case (see Remark 28).

There are however several typos or gaps in their paper which we were not able to fix-see the Appendix B for more details.

Bauderon and Courcelle gave a syntax and a complete axiomatisation for arbitrary graphs [START_REF] Bauderon | Graph expressions and graph rewritings[END_REF]. While the overall statement is similar to ours, their syntax can hardly be related to the present one (it is infinitary, for instance), and the present results are not corollaries of their work. Although we need to present them differently for the sake of our completeness proof, the structural invariants we exhibit for treewidth at most two graphs are reminiscent of the general decomposition results of Tutte [START_REF] Tutte | Graph Theory[END_REF], which Courcelle later studied in the context of MSO [START_REF] Courcelle | The monadic second-order logic of graphs XI: Hierarchical decompositions of connected graphs[END_REF].

III. 2P-ALGEBRA

We consider the signature • 2 , 2 , • • 1 , 1 0 , 0 and we let u, v, w range over terms over a set Σ of variables.

u, v, w ::= u•v | u v | u • | 1 | | a (a ∈ Σ)
We usually omit the • symbol and we assign priorities so that the term (a • (b • )) c can be written just as ab • c. A 2p-algebra is an algebra over this signature satisfying the axioms from Figure 2. We write u ≡ v when two terms u and v are congruent modulo those axioms, or equivalently, when the equation holds in all 2p-algebras.

Following notations from Kleene algebra with tests (KAT) [START_REF] Kozen | Kleene algebra with tests[END_REF], we let α, β range over tests, those terms that are congruent to some term of the shape 1 u. (Equivalently by axiom A9, u is a test if u ≡ 1 u.) The graphs of tests are precisely those whose input and output coincide.

We shall use the derived operation mentioned in Section II, domain, as well as its dual, codomain:

dom(u) 1 u cod(u) 1 u

Domain and codomain terms are tests by definition.

As is standard for involutive monoids, the first eight axioms from Figure 2 entail 1 • ≡ 1, • ≡ , and 1u ≡ u. We will use such laws freely in the sequel. We recall the four remaining axioms below, using the above notations.

1 1 ≡ 1 (A9) 1 uv ≡ dom(u v • ) (A10) u ≡ dom(u) (A11) αv ≡ α v (A12)
Thanks to converse being an involution, there is a notion of duality in 2p-algebras: one obtains a valid law when swapping the arguments of all products and exchanging domains with codomains in a valid law. (We have cod(u) ≡ dom(u • ).) Proposition 1. The following equations hold in all 2palgebras.

α • ≡ α (5) αβ ≡ α β (6) α(v w) ≡ αv w (7) (v w)α ≡ vα w (8) dom(uv w) ≡ dom(u wv • ) (9) u • ≡ u (10) u w ≡ u w (11) u v w ≡ u w v (12) (u v )w ≡ uw v (13)
Proof. To prove [START_REF] Bodlaender | A partial k-arboretum of graphs with bounded treewidth[END_REF] we can assume that α = 1 u; by using axiom A10 twice, we get

α • ≡ 1 1u • ≡ dom(1 u •• ) ≡ dom(u 1 • ) ≡ 1 u1 ≡ α
Equation ( 6) follows from ( 7) by taking v = 1 and w = β. For ( 7), we use axiom A12 twice:

α(v w) ≡ α v w ≡ αv w
Equation ( 8) is the dual of [START_REF] Cosme-Llópez | k 4 -free graphs as a free algebra[END_REF]. For ( 9), we use axiom A10 twice:

dom(uv w) ≡ (1 uvw • ) ≡ dom(u wv • )
We use ( 5) as well as axiom A11 and its dual for [START_REF] Courcelle | Graph grammars, monadic second-order logic and the theory of graph minors[END_REF]:

u • ≡ dom(u • ) ≡ cod(u) ≡ u
Thanks to axiom A11 and its dual, it suffices to prove the laws [START_REF] Courcelle | The monadic second-order logic of graphs XI: Hierarchical decompositions of connected graphs[END_REF] and [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF] in the case where u, v and w are tests. The law α β ≡ α β is the instance of axiom A12 where v = β. For the second one, we have

α β γ ≡ α β γ (by A12) ≡ α β γ (by dual of A12) ≡ α γ β (by (11))
For the last law, we use axioms A12 and A11 twice:

(u v )w ≡ (u dom( v))w ≡ dom( v)uw ≡ uw dom( v) ≡ uw v IV. GRAPHS
As explained in the introduction, we consider labelled directed graphs with two designated vertices. We just call them graphs in the sequel. Note that we allow multiple edges between two vertices, as well as self-loops. Definition 2. A graph is a tuple G = V, E, s, t, l, ι, o , where V is a finite set of vertices, E is a finite set of edges, s, t : E → V are maps indicating the source and target of each edge, l : E → Σ is map indicating the label of each edge, and ι, o ∈ V are the designated vertices, respectively called input and output.

We write G[x; y] for the graph G with input set to x and output set to y; we abbreviate G

[x; x] to G[x]. Definition 3. A (graph) homomorphism from G = V, E, s, t, l, ι, o to G = V , E , s , t , l , ι , o is a pair h = f, g of functions f : V → V and g : E → E that respect the various components: s • g = f • s, t • g = f • t, l = l • g, ι = f (ι), and o = f (o).
A (graph) isomorphism is an homomorphism whose two components are bijective functions. We write G G when there exists an isomorphism between graphs G and G . Proposition 4. Graphs up to isomorphism form a 2p-algebra.

Proof. The operations of the signature on graphs have been described in the Introduction and in Figure 1. Providing an isomorphism for each law from Figure 2 is routine. E,s,t,l,ι, o be a graph. A tree decomposition of G is a tree T where each node t is labelled with a set V t ⊆ V of vertices, such that: (T1) for every vertex x ∈ V , the set of nodes t such that

Definition 5. Let G = V,
x ∈ V t is non-empty and connected in T (i.e., forms a sub-tree); (T2) for every edge e ∈ E, there exists a node t such that {s(e), t(e)} ⊆ V t ; (T3) there exists a node t such that {ι, o} ⊆ V t .

The width of a tree decomposition is the size of the largest set V t minus one; the treewidth of a graph is the minimal width of a tree decomposition for this graph. We write TW 2 for the set of graphs of treewidth at most two.

The first two conditions in the definition of tree decomposition are standard; the third one is related to the presence of distinguished nodes: it requires them to lie together in some node of the tree. This condition ensures that the following graph is excluded from TW 2 whatever the orientation and labelling of its edges, even though it has treewidth two when forgetting about input and output.

(M 3 )
Indeed, such a graph cannot be represented in the syntax we consider. (Something already observed by Freyd and Scedrov [START_REF] Freyd | Categories, Allegories[END_REF]-the addition of to the syntax does not help.) Lemma 6. Let G, H be two graphs with an homomorphism h from G to H. Suppose we have a tree decomposition of G such that for all vertices x, y such that h(x) = h(y), there is a node containing both x and y. Then this tree decomposition can be renamed by h into a tree decomposition of h(G) of width smaller or equal. Proposition 7. Graphs of treewidth at most two (TW 2 ) form a subalgebra of the algebra of graphs.

Proof. Graphs 1 and actually have treewidth 0 and 1, respectively. A tree decomposition for a graph G remains a tree decomposition for the graph G • .

For a series composition

G 1 •G 2 , we have two graph ho- momorphisms h i from G i to G 1 •G 2 such that h 1 (o 1 ) = h 2 (ι 2 ).
Those homomorphisms are injective (on both vertices and edges), and

h 1 (G 1 ) h 2 (G 2 ) ⊆ P {h 1 (ι 1 ), h 1 (o 1 ), h 2 (o 2 )}.
Take tree decompositions of G 1 and G 2 and rename them using h 1 and h 2 . By (T3), the former has a node t 1 containing h 1 (ι 1 ) and h 1 (o 1 ), and the latter has a node t 2 containing h 2 (ι 2 ) and h 2 (o 2 ). A tree decomposition of G 1 •G 2 is obtained by joining t 1 and t 2 through a new node labelled P .

For a parallel composition G 1 G 2 , we also have two graph homomorphisms

h i from G i to G 1 G 2 such that h 1 (ι 1 ) = h 2 (ι 2 ) and h 1 (o 1 ) = h 2 (o 2
). Those homomorphisms are not necessarily injective on vertices (e.g., when ι 1 = o 1 and ι 2 = o 2 ). Nevertheless, they identify at most the input and the output, and those are related in some node in any tree decomposition, by (T3). Thus Lemma 6 applies: we can take tree decompositions of G 1 and G 2 and rename them according to the two homomorphisms. A tree decomposition of G 1 G 2 is obtained by adding an edge between the nodes given by (T3) in each decomposition.

The graphs we associate to each letter (Figure 1) also belong to this subalgebra, so that we obtain an homomorphism g : Trm → TW 2 associating a graph of treewidth at most two to each syntactic term. When taking quotients under term congruence and graph isomorphism, this function becomes a 2p-algebra homomorphism g : Trm /≡ → TW 2/ . Our key result is that g actually is an isomorphism of 2p-algebras (Corollary 41).

V. K 4 -FREENESS

In this section we establish preliminary technical results about unlabelled undirected graphs with at most one edge between two vertices and without self-loops; we call those simple graphs. We use standard notation and terminology from graph theory [START_REF] Diestel | Graph Theory[END_REF]. In particular, we denote by xy a potential edge between two vertices x and y; an xy-path is a (possibly trivial) path whose ends are x and y; G + xy is the simple graph obtained from G by adding the edge xy if x and y were not already adjacent; G\x is the simple graph obtained from G by removing the vertex x and its incident edges. Definition 8. A minor of a simple graph G is a simple graph obtained up to isomorphism by performing a sequence of the following operations on G: delete an edge or a vertex, contract an edge.

A cornerstone result of graph theory, Robertson and Seymour's graph minor theorem [START_REF] Robertson | Graph minors. XX. Wagner's conjecture[END_REF], states that (simple) graphs are well-quasi-ordered by the minor relation. As a consequence, the classes of graphs of bounded treewidth, which are closed under taking minors, can be characterised by finite sets of excluded minors. Two simple and standard instances are the following ones: the graphs of treewidth at most one (the forests) are precisely those excluding the cycle with three vertices (C 3 ); those of treewidth at most two are those excluding the complete graph with four vertices (K 4 ) [START_REF] Duffin | Topology of series-parallel networks[END_REF]. We eventually reprove the latter one here.

(C 3 ) (K 4 )
We fix a connected simple graph G in the remainder of this section.

Definition 9. The checkpoints between two vertices x, y are the vertices which any xy-path must visit.

cp(x, y) {z | every xy-path crosses z}

Note that for all vertices x, y, we have cp(x, x) = {x} and {x, y} ⊆ cp(x, y) = cp(y, x). Two vertices x, y are linked, written x♦y, when x = y and cp(x, y) = {x, y}, i.e., when there are no proper checkpoints between x and y. The link graph of G is the graph of linked vertices.

The graph G is a subgraph of its link graph: if xy is an edge in G then x♦y. We also have the following properties.

Lemma 10. Every irredundant cycle in the link graph is a clique.

Proof. Let x, y ∈ CP(U ) be two distinct vertices on the cycle, and let π 1 , π 2 be the two corresponding xy-paths in CP(U ). We have to show x♦y. Let p = x, y be a vertex in G. Chose π ∈ {π 1 , π 2 } such that π does not cross p. Each edge zt in π can be replaced by a zt-path in G not crossing p. Doing so, we obtain an xy-path in G excluding p. Thus p cannot be a checkpoint.

Lemma 11. If xyz is a triangle in the link graph and ι is a vertex not in G, then the graph G + ιx + ιy + ιz admits K 4 as a minor.

Proof. Let π by an irredundant xy-path avoiding z. Let π be a path not crossing π, from z to a neighbour z of some elements from π.

• If z has at least two neighbours in π, say x and y such that x appears before y in π. Then we can get K 4 in the enriched graph by contracting the xx and yy subpaths of π as well as the zz subpath of π into vertices, contracting the x y subpath into an edge, and deleting irrelevant vertices. • If z has only one neighbour in π, say n, we can assume w.l.o.g. that n = x. Take an irredundant xz-path avoiding n. Since π and π are disjoint, there must be a sub-path π of it whose ends m and z are respectively in π and π but whose inner vertices (if any) avoid those sets. We have m = n by assumption, so that K 4 can be obtained in a way similar to the previous case. Now fix a set U of vertices; we extend the notion of checkpoints as follows.

Definition 12. The checkpoints of U , CP(U ), is the set of vertices which are checkpoints of some pair in U .

CP(U )

x,y∈U cp(x, y)

The checkpoint graph of U is the subgraph of the link graph induced by this set. We also denote this graph by CP(U ).

Lemma 13. CP(•) is a closure operator on the set of vertices. In particular, for all checkpoints x, y ∈ CP(U ), cp(x, y) ⊆ CP(U ).

Proof. Since x ∈ cp(x, x), the operator is extensive. It is increasing by definition. For idempotency, take vertices z 1 ∈ cp(x 1 , y 1 ) and z 2 ∈ cp(x 2 , y 2 ) for vertices x 1 , y 1 , x 2 , y 2 in U . We need to prove that every vertex t ∈ cp(z 1 , z 2 ) is a check point between elements in U . Let π 1 and π 2 be, respectively, two irredundant paths of the form x 1 y 1 and x 2 y 2 . We distinguish four cases.

• if t neither appears in π 1 nor in π 2 , then t ∈ cp(x 1 , x 2 ).
Assume this is not the case, then we can find an x 1 x 2path π x not crossing t. The concatenation of the z 1 x 1subpath of π 1 , the path π x , and the x 2 z 2 -subpath of π 2 give us a z 1 z 2 -path avoiding t, which contradicts t being a check point in cp(z 1 , z 2 ). • If t appears in one of them, say π 1 , but not in the other (π 2 ), then either t appears before z 1 , and we prove t ∈ cp(y 1 , y 2 ), or t appears after z 1 , and we prove t ∈ cp(x 1 , x 2 ). The proofs are done as in the first case, by exhibiting a z 1 z 2 -path avoiding t. • If where t belongs to both π 1 and π 2 , we distinguish four subcases according to whether t appears before or after z 1 in π 1 and before or after z 2 in π 2 .

Lemma 14. For every path in G between two checkpoints x, y ∈ CP(U ), the sequence obtained by keeping only the elements in CP(U ) is an xy-path in CP(U ).

Proof. This follows from Lemma 13: we cannot miss intermediate checkpoints when we select only the elements in CP(U ).

Since G is assumed to be connected, it follows that so is CP(U ). A key instance of a checkpoint graph is when U only contains two vertices, presumably the input and output of some graph: the checkpoint graph is a line in this case, and it allows us to decompose the considered graph into a sequence of series compositions.

Lemma 15. If U = {x, y} for some vertices x, y, then CP(U ) is a line graph whose ends are x and y.

Proof. For vertices z 1 and z 2 in cp(x, y), we say that z 1 z 2 if every xy-path in G crosses z 1 before z 2 . The relation is a total order on cp(x, y).

The following two lemmas are helpful in Proposition 21 below, to prove that the checkpoint graph is a tree under certain circumstances.

Lemma 16. If xy is an edge in CP(U ), then there exists x , y ∈ U such that x and y belong to cp(x , y ). Lemma 17. If xyz is a triangle in CP(U ), then there exists x , y , z ∈ U such that x and y (resp. x and z, y and z) belong to cp(x , y ) (resp. cp(x , z ), cp(y , z )).

As explained above we use the checkpoint graphs to decompose graphs. The following notions of intervals and bags are the basic blocks of those decompositions. Definition 18. Let x, y be two vertices. The strict interval x; y is the following set of vertices.

x; y {p | there is an xp-path avoiding y and a py-path avoiding x}

The interval x; y is obtained by adding x and y to that set. We abuse notation and write x; y for the subgraph of G induced by the set x; y .

Note that while the intervals do not depend on the set U , they will mostly be used under the assumption that xy is an edge in a checkpoint graph.

Definition 19. The bag of a checkpoint x ∈ CP(U ) is the set of vertices that need to cross x in order to reach the other checkpoints.

x U {p | ∀y ∈ CP(U ), any py-path crosses x} .

As before, we also write x U for the induced subgraph of G.

Note that x U depends on U and differs from x; x (which is always the singleton {x}). Proposition 20. If CP(U ) is a tree, then the following set V is a partition of the vertices of G such that any edge of G appears in exactly one graph of the set E.

V { x U | x ∈ CP(U )} ∪ { x; y | xy edge in CP(U )} E { x U | x ∈ CP(U )} ∪ { x; y | xy edge in CP(U )}
Graphically, this means G can be decomposed as in the picture below; only the vertices of CP(U ) are depicted, the green blocks correspond to edges in CP(U ), the yellow blocks correspond to the graphs x U . The leaves of CP(U ) are elements of U ; the converse does not always hold.

Proof. Let p be a vertex. Let N be the set of checkpoints x ∈ CP(U ) for which there exists a px-path avoiding all checkpoints except x. N is non-empty since G is connected. One can show that N is a clique in CP(U ) using Lemma 14, whence |N | ≤ 2 since CP(U ) is assumed to be a tree. If N is a singleton {x}, then p ∈ x U and p cannot appear anywhere else in V by definition of N . If N is a pair {x, y}, then p ∈ x; y ; p cannot be in one of the z U by definition of N , and if it were to belong to some other interval x ; y with x y an edge in CP(U ) then one could exhibit a cycle in CP(U ).

Note that the above argument shows that when p ∈ x; y then p lies on an xy-path where the only checkpoints are x and y, and any path from p to a checkpoint must cross either x or y ( †).

For the second part of the statement, let pq be an edge of G. If p and q belong to the same element of V then the edge belongs to the corresponding element in E. Otherwise,

• either p ∈ x U and q ∈ y U for some distinct checkpoints x, y. Then necessarily p = x and q = y (by considering a py-path going through q and a qx-path going through p). The edge pq thus belongs to the graph x; y in E. • Or p ∈ x U and q ∈ y; z for some edge yz in CP(U ).

Then there exists a qx-path going through p, so that x must be either y or z by ( †). Say x = y. There exists a pz-path (throug q) enforcing p = x, so that the edge pq belongs to the graph y; z . • Or p ∈ x; y and q ∈ x ; y for some distinct edges xy and x y in CP(U ). Assume w.l.o.g. that x = x . By ( †), y and x cannot be equal. There is moreover an xxpath and a yx -path (both taking the edge pq) witnessing the fact that xx and yx are adjacent in CP(U ). This contradicts CP(U ) being a tree.

As a consequence, when CP(U ) is a tree, it is also a minor of G: contract all subgraphs of the form x U to the vertex x and every subgraph of the form x; y to an edge xy.

The following proposition is a key element in the developments to come. It makes it possible to extract a term out of a graph whose input and output coincide, by providing ways to chose an element where to relocate the output and resort to the easier case when input and output differ.

Proposition 21. Assume G = H\ι, for some K 4 -free simple graph H and some vertex ι. Further assume that U is the set of neighbours of ι in H and that this set is not empty.

(i) CP(U ) is a tree, (ii) for every edge xy in CP(U ), the graph x; y + xy is K 4 -free, (iii) for every vertex x in CP(U ), the graph H +ιx is K 4 -free.

(Note that G is still assumed to be connected.)

Proof. Assume by contradiction that CP(U ) contains a cycle, and thus a triangle xyz by Lemma 10. Let x , y , z be the elements of U given by Lemma 17. By Proposition 20 applied to the line graph CP({x , y }), one can decompose G as follows:

x x y y • • • • • • z z . . .
One obtains two symmetrical decompositions by using Proposition 20 on the line graphs CP({y , z }) and CP({x , z }). By combining those three decompositions, we get the following decomposition of G:

V {X, Y, Z, T } E {X , Y , Z , T } where • X x; x ∪ x U ∪
x U and X is the corresponding induced subgraph;

• similarly for Y, Y , Z, and Z ; • T

x; y ∩ y; z ∩ z; x and T is the subgraph induced by T ∪ {x, y, z}. Adding back the vertex ι and the corresponding edges, the graph H looks as follows:

x y z x y z
Other edges could be incident to ι, delete them and contract the blocks X, Y , and Z to obtain a minor H of H. By Lemma 11, H admits K 4 as a minor. This contradicts H being K 4 -free.

Thus CP(U ) is a tree (i), and by Proposition 20, the graph H looks as follows:

x ι Item (ii) follows: for any edge xy in CP(U ), x; y + xy can be seen to be a minor of H; thus it cannot contain K 4 as a minor.

The last point (iii) is more delicate. If x ∈ U , then H + ιx = H is K 4 -free by assumption. Otherwise, x must be an inner node of the tree CP(U ), say with n neighbours. We can weaken the previous decomposition of the graph H to get n+1 components: one for x U and one for each neighbour of x (the blue ones in the picture below). The latter are adjacent to ι in G while the former is not.

x ι x Consider a minoring process evolving H + ιx into K 4 . The case where the edge ιx is deleted is trivial. If it is contracted, then K 4 is necessarily obtained using only one of the n + 1 components; since n ≥ 2, one can always contract one blue component to achieve the effect of contracting ιx. If ιx is kept to justify an edge in K 4 , then name the vertices of K 4 ι, x, y, z and consider the connected components of H giving rise to y and z. Those connected components cannot contain ι nor x, and they must be adjacent to justify the yz-edge in K 4 . Thus both of them are contained in one of the n + 1 components. As previously one can contract one blue component to achieve the effect of keeping ιx.

As a consequence of the above proposition, we have the following one, which makes it posible to decompose graphs with distinct input and output into a parallel composition when they cannot be a series composition.

Proposition 22. Let ι, o be two distinct vertices such that G + ιo is K 4 -free. We have that:

VI. EXTRACTING TERMS

Now we have enough preliminary material and we can look for a right inverse to the function g : Trm → TW 2 . As explained in the Introduction, we use K 4 -freeness to extract terms from graphs in a more structured way than using tree decompositions directly. Definition 23. The skeleton of a graph G is the simple graph S obtained from G by forgetting input, output, labelling, edge directions, edge multiplicities, and self-loops. The strong skeleton of G is S + ιo if ι = o, and S otherwise.

As an example, the strong skeleton of any instance of the graph (M 3 ) from Section IV is K 4 . More generally, a graph belongs to TW 2 if and only if its strong skeleton has treewidth at most two in the standard sense (i.e., for simple graphs, without taking input and output into account).

Proposition 24. The strong skeleton of every graph in TW 2 is K 4 -free.

Proof. The operations used to obtain a minor do not increase the treewidth, and K 4 has treewidth three.

Given a graph G and two vertices x, y, we write G x; y for the subgraph of G induced by the set x; y (computed in the skeleton of G), with input and output respectively set to x and y, and with self-loops on x and y removed. The strong skeleton of G x; y is x; y + xy.

Similarly, given a graph G, a set U of vertices and vertex x, we write G x U for the subgraph of G induced by the set x U (computed in the skeleton of G), with both input and output set to x. Doing so, the skeleton and strong skeleton of G x U are both x U . We shall omit the subscript when it is clear from the context. Definition 25. The term t(G) of a graph G whose strong skeleton is K 4 -free is defined by induction on the number of edges in G1 . When G is connected there are two mains cases depending on whether the input and output coincide (a) or not (b). We deal with the general case (c) by decomposing the graph into connected components.

a) Connected, distinct input and output: consider the line graph (Lemma 15) obtained by taking the checkpoint graph of U = {ι, o} in the skeleton of G. Write it as x 0 . . . x n+1 with ι = x 0 and o = x n+1 . According to Proposition 20, G looks as follows.

ι x 1 x 2 xn o • • • We set t(G) t(G x 0 )•t(G x 0 ; x 1 )•t(G x 1 )• . . . •t(G x n )•t(G x n ; x n+1 )•t(G x n+1 )
The (strong) skeleton of each graph G x i is just x i , which is necessarily K 4 -free, as a subgraph of that of G. Proposition 22(ii) moreover ensures that so are the strong skeletons of all graphs G x i ; x i+1 .

The above recursive calls occur on smaller graphs unless n = 0 and the graphs G ι and G o are reduced to the trivial graph with one vertex and no edge (i.e., the graph 1). In such a situation,

• either ι and o are adjacent in G. Then let G be the graph obtained by removing from G all edges between ι and o and let u = a 1 . . . a i b • 1 . . . b • j be a term corresponding to those edges. We set t(G) t(G ) u

• Or they are not, and Proposition 22(i) applies so that we can decompose G into parallel components:

G = G 1 . . . G m with m ≥ 2. Accordingly, we set t(G) t(G 1 ) . . . t(G m )
b) Connected, input equals output: if there are self-loops on ι, let u = a 1 . . . a n be a term corresponding to those edges, let G be the graph obtained by removing them, and recursively set t(G) t(G ) u.

Otherwise let H be the skeleton of G. Decompose H\ι into connected components H 1 \ι, . . . , H m \ι such that H H 1 ∪ • • • ∪ H m . The graph thus looks as follows.

ι If m = 0, then set t(G) = 1. If m > 1, set t(G) i≤m t(G i ) ,
where G i is the subgraph of G induced by H i . It remains to cover the case where m = 1. Let U be the set of neighbours of the input and compute the checkpoint graph CP(U ) in H\ι. Pick an arbitrary node x ∈ CP(U ). By Proposition 21(iii), the strong skeleton of G

[ι; x] is K 4 -free. Set t(G) dom(t(G[ι; x]))
(Remember that dom(•) relocates the output to the input.) c) General case: decompose the graph G into connected components G 1 , . . . , G n . For all i ≤ n, pick an arbitrary vertex x i in the component G i . There are two cases:

• either input and output belong to the same component, say G j ; then set

t(G) t(G j ) i =j •t(G i [x i ])• ι o
• or they belong to two distinct components, say ι in G j and o in G k , in which case we set

t(G) t(G j [ι])• •t(G k [o]) i =j,k •t(G i [x i ])• ι o
In both cases, it is easy to check that the recursive calls occur on graphs whose (strong) skeletons are subgraphs of the strong skeleton of G, and thus K 4 -free.

The definition of the extraction function t ends here. Note that this function is defined on "concrete" graphs: we need to choose some vertices in cases (b) and (c), and we can only do so by relying on the concrete identity of those vertices (e.g., choosing the smallest one, assuming they are numbers). We shall see in the following section that all those potential choices, nevertheless, always lead to congruent terms (Theorem 34).

We obtain the following theorem by construction.

Theorem 26. For every graph G ∈ TW 2 , g(t(G)) G.

Corollary 27. The following are equivalent for all graph G:

(i) G has treewidth at most two;

(ii) the strong skeleton of G is K 4 -free;

(iii) G is (isomorphic to) the graph of a term.

Remark 28. When G is connected, t(G) does not contain occurrences of other than those that are implicit in our uses of the domain operation (case (b)). Thus we obtain an alternative proof of Dougherty and Gutiérrez' characterisation [15, Section 4, Theorem 31] (their minor exclusion property is easily proved equivalent to ours-they do not mention treewidth).

Also note that we can easily avoid using 1 (but not dom(•)) when the graph does not contain self-loops and is not reduced to the trivial graph 1. When the graph does not contain selfloops and has distinct input and output, the construction can be modifed to produce terms without both 1 and dom(•); the resulting construction becomes, however, less local, and we do not know how to use it to axiomatise the 1-free reduct of 2p-algebra.

VII. COMPLETENESS OF THE AXIOMS

Our goal is now to prove that the axioms of 2p-algebras are complete w.r.t. graphs: they suffice to equate all terms denoting the same graph up to isomorphism.

We first prove that t maps isomorphic graphs to congruent terms (Theorem 34 below). We need for that the following lemmas and propositions.

Lemma 29. Let G ∈ TW 2 . If ι = o, then t(G) is a test.
Proof. By a simple case analysis.

Lemma 30. For every graph G ∈ TW 2 , t(G • ) ≡ t(G) • .

Proof. Follows by a simple induction, using Lemma 29 and Equation [START_REF] Bodlaender | A partial k-arboretum of graphs with bounded treewidth[END_REF].

Proposition 31. Let G ∈ TW 2 be a graph with ι = o, without self-loops on ι. Let S be its skeleton, and assume that S\ι is connected. Let U be the neighbours of ι in G and consider the checkpoint graph of U in the skeleton of S\ι. For all checkpoints x, y, we have dom(t(G[ι, x])) ≡ dom(t(G[ι, y])).

Proof. The checkpoint graph is connected, so that it suffices to prove the statement when xy is an edge in the checkpoint graph. We depict the generic situation below. dom((aαb c)γ) ≡ dom(aαb cγ) (by ( 8)) ≡ dom(aα cγb • ) (by ( 9)) ≡ dom((a cγb • )α)

(by ( 8))

Lemma 32. Let G ∈ TW 2 be a connected graph with ι = o. For all neighbour x of ι, we have t(G) ≡ t(G[ι, x]) .

Proof. The graph might have self-loops on ι and might be disconnected when removing ι. Let G be the maximal subgraph without self-loops on ι that contains x and remains connected when removing ι. Let G be the subgraph of G induced by {ι} ∪ (G\G ). The situation is depicted below: In other words, the extraction function t yields a function t : TW 2/ → Trm /≡ between 2p-algebras.

x ι G G Let α = t(G ) and u = t(G [ι, x]
Proof. By induction following the computation of t(G) and t(H). The interesting cases are the following ones.

• Case (b) when m = 1. Modulo the axioms, the extracted terms do not depend on the chosen checkpoints, thanks to Proposition 31. • Case (c). The only difficulties occur in the connected components that contain neither the input nor the output:

we arbitrarily pick a vertex which becomes both input and output. Proposition 33 shows that such a choice is inocuous modulo the axioms.

We finally prove that t is an homomorphism, and, in fact, an isomorphism.

Lemma 35. Let G, H ∈ TW 2 be two graphs whose input and output coincide. We have

t(G•H) ≡ t(G H) ≡ t(G) t(H) ≡ t(G)•t(H) • Proof.
The first equation follows from Theorem 34: G•H and G H are isomorphic. The second one is obtained using associativity and commutativity of , and axiom A9. The third one is an instance of ( 6) by Lemma 29.

Lemma 36. Let G, H ∈ TW 2 , we have t(G•H) ≡ t(G)•t(H).
Proof. If G (resp. H) has components disconnected from both input and output, we use (13) (resp. its dual) to extrude the corresponding terms (of shape b ) at toplevel. Then we reason by cases.

• G and H are connected. We use associativity of • and Lemma 35 on the last test in t(G) and the first test in t(H).

• Both G and H have exactly two connected components and their input and output are not connected. We use Lemma 35 as previously, and (12).

• H is in the latter situation, and G is connected. If the input and output of G coincide, then we just use Lemma 35. Otherwise, we proceed by induction on the size of G.

if there is a proper checkpoint between ι and o (in G), then decompose the graph into smaller graphs using this checkpoint: (by definition)

G G 1 •G 2 . We have t(G•H) ≡ t(G 1 •G 2 •H) (by Theorem 34) ≡ t(G 1 )t(G 2 •H) (by induction on G 1 ) ≡ t(G 1 )t(G 2 )t(H) (by induction on G 2 ) ≡ t(G)
• The case where one graph is disconnected and the other has equal input and output is routine, using the same laws as above.

• The only remaining case is when one graph is connected, say G, and the other (H) has equal input and output. We proceed by induction on the number of vertices of G. It suffices to prove the statement when H = 1: indeed, we have Proof. The cases for converse, series composition, and parallel composition are given by Lemmas 30, 36, and 37; those for constants 1 and are straightforward.

t(G H) ≡ t(G 1
Theorem 39. For every term u, we have t(g(u)) ≡ u.

Proof. By structural induction on u, using Proposition 38 and the observation that t(g(a)) ≡ a for every letter a.

Corollary 40. For all terms u and v, we have u ≡ v if and only if g(u) g(v).

Proof. The direct implication amounts to Proposition 4. Conversely, if g(u) g(v) then t(g(u)) ≡ t(g(v)) by Theorem 34, and thus u ≡ v by Theorem 39.

Corollary 41. Graphs of treewidth at most two form the free 2p-algebra, as witnessed by the following diagram.

Trm /≡ TW 2/ g t (14)
VIII. FUTURE WORK What is the free idempotent 2p-algebra? (Where parallel composition is idempotent.) One could be tempted to switch to simple directed graphs, where there is at most one edge with a given label from one vertex to another. This is however not an option: the graphs of ab ab and ab are not isomorphic. One could also consider equivalences on graphs that are weaker than isomorphism. The notion of (two-way) bisimilarity [START_REF] Park | Concurrency and automata on infinite sequences[END_REF], [START_REF] Milner | Communication and Concurrency[END_REF] that come to mind does not work either: such an equivalence relation on graphs certainly validates idempotency of parallel composition, but it also introduces new laws, e.g.,

(1 aa) = (1 a) , which are not even true in algebras of binary a a ∼ a Courcelle used the algebraic theory he defined with Bauderon for arbitrary graphs [START_REF] Bauderon | Graph expressions and graph rewritings[END_REF] to propose a notion of graph recognisability [START_REF] Courcelle | The monadic second-order logic of graphs. I: Recognizable sets of finite graphs[END_REF], based on the generic framework by Mezei and Wright [START_REF] Mezei | Algebraic automata and context-free sets[END_REF]. He proved that sets of graphs definable in MSO are recognisable. The converse does not hold in general. He later proved it for graphs of treewidth at most two [START_REF] Courcelle | The monadic second-order logic of graphs V: on closing the gap between definability and recognizability[END_REF] with a counting variant of MSO, conjecturing that it would be so for classes of graphs of bounded treewidth. This conjecture was proved only last year, by Bojańczyk and Pilipczuk [START_REF] Bojańczyk | Definability equals recognizability for graphs of bounded treewidth[END_REF].

The present work makes it possible to propose an alternative notion of recognisability for treewidth at most two, 2p-recognisability: recognisability by a finite 2p-algebra. We conjecture that this notion coincides with recognisability. That recognisability entails 2p-recognisability is easy. The converse is harder; it amounts to proving that any finite congruence with respect to substitutions in treewidth at most two graphs can be refined into a finite congruence with respect to substitutions in arbitrary graphs. We see two ways of attaining this implication:

1) prove that 2p-recognisability entails MSO-definability, which could possibly be done along the lines of [START_REF] Courcelle | The monadic second-order logic of graphs V: on closing the gap between definability and recognizability[END_REF], by showing that our term extraction procedure is MSOdefinable. 2) or use a slight generalisation of the result by Courcelle and Lagergren [START_REF] Courcelle | Equivalent definitions of recognizability for sets of graphs of bounded tree-width[END_REF], relating recognisability to krecognisability for graphs of treewidth at most k. Indeed, 2p-recognisability is really close to 2-recognisability.

Unfortunately, Courcelle and Lagergren's result is established only for unlabelled, undirected graphs, without sources, while we need labelled directed graphs with two sources. One can easily extend our syntax to cover graphs of treewidth at most k, with k sources, for a given k (see, e.g., [START_REF] Courcelle | Graph grammars, monadic second-order logic and the theory of graph minors[END_REF], [START_REF] Arnborg | An algebraic theory of graph reduction[END_REF]). However, we do not know how to generate finite axiomatisations in a systematic way, for every such k. Moreover, our proof strategy heavily depends on the fact that when k = 2, K 4 is the only excluded minor. We would need another strategy to deal with the general case since the excluded minors are not known for k ≥ 4.

  For instance, •a• •b• and •b• •a• both denote the graph below, and should thus be equated. a b

Figure 2 .

 2 Figure 2. Twelve axioms for 2p-algebras

  (i) if ι and o are not adjacent in G, ι♦o, and ι {ι,o} = {ι} then the graph induced by ι; o has at least two connected components. (ii) for every edge xy in CP({ι, o}), the graph x; y + xy is K 4 -free, Proof. (i) Let H = G + ιo and G = H\ι. The neighbours U of ι in H are the neighbours of ι in G, plus o. By Proposition 21, CP(U ) (for G ) is a tree. If o is a leaf in that tree then its unique neighbour must be a proper checkpoint between ι and o, contradicting the hypothesis cp(ι, o) = {ι, o}. Otherwise its neighbours make it possible to partition ι; o into at least two connected components, thanks to Proposition 20. (ii) By Lemma 15 and Proposition 20, x; y + xy can be obtained as a minor of G + ιo; thus it cannot contain K 4 as a minor.

b

  In such a case, we have t(G[ι; y]) = dom((aαb c)γ) for some terms a, b, c and tests α, γ (up to associativity of • and associativity and commutativity of ), and t(G[ι; x]) ≡ dom((a cγb )α) for some term b such that b ≡ b • by Lemma 30. We conclude as follows.

  ). By definition of the extraction function, we have t(G) ≡ α t(G ) and t(G[ι, x]) ≡ αu. By Proposition 31, we moreover have t(G ) ≡ dom(u). We conclude: Proposition 33. Let G ∈ TW 2 be a connected graph. For all vertices x, y, we have t(G[x]) ≡ t(G[y]) .Proof. Since G is connected, it suffices to prove the property for every edge xy in G. For each of these, we have

	t(G) ≡ (α dom(u))
	≡ αdom(u)	(by (6))
	≡ αu	(by axiom A11)
	≡ t(G[ι, x])
	t(G[x]) ≡ t(G[x, y])	(by Lemma 32)
	≡ t(G[y, x]) •	(by Lemma 30)
	≡ t(G[y, x])	(by (10))
	≡ t(G[y])	(by Lemma 32)
	Theorem 34. Let G, H ∈ TW 2 be two graphs. If G	H
	then t(G) ≡ t(H).

  t(H) (by the connected case) if there is no checkpoint between ι and o, then let αuβ = t(G) and γ δ = t(H). By Proposition 31, t(G•H) ≡ (α dom(u(β γ))) δ. (Indeed, o belongs to the appropriate checkpoint graph: either ι and o are adjacent, or this is a consequence of Proposition 22 (i).) We have The last case is symmetric and can be handled using Lemma 30 to get back to the previous case. Proof. If G or H have components disconnected from both input and output, we use associativity and commutativity of to reorganise them. Then we reason by cases.

	t(G)•t(H) = αuβγ δ
	≡ αdom(uβγ) δ (by axiom A11)
	≡ (α dom(u(β γ))) δ	(by (6))
	≡ t(G•H)
	Lemma 37. For all graphs G, H ∈ TW 2 , we have t(G H) ≡
	t(G) t(H).

• • If both G and H have distinct input and output, then let αuβ = t(G) and α vβ = t(H). (With u and/or v possibly equal to , if G and/or H are disconnected.) We have t(G) t(H) = αuβ αuβ ≡ αα (u v)ββ (by (7,8) twice) ≡ (α α )(u v)(β β ) (by (6) twice) ≡ t(G H) .

  We can further assume that ι = o in G (otherwise Lemma 35 applies), and that there are no self-loops on ι and o (otherwise decompose G intoG ι •G •G o with G satisfying the above property; we have G 1 G 1 G ι G o , use the fact that αuβ 1 ≡ (u 1) α β).-If there is a proper checkpoint between ι and o, write t(G) = uβv using this checkpoint. We havet(G 1) ≡ dom((u v • )β) (by Proposition 31) -Otherwise, G is a (non-trivial) parallel composition G 1 G 2 . We have t(G 1) ≡ t(G 1 G 2 1) ≡ t(G 1 ) t(G21) (by induction on G 1 ) ≡ t(G 1 ) t(G 2 ) 1 (by induction on G 2 )

	≡ dom(uβ v • )	(by (8))
	≡ 1 uβv	(by axiom A10)
	≡ t(G) 1
		H)	(by Theorem 34)
		≡ t(G 1) t(H)	(by Lemma 35)
		≡ t(G) 1 t(H)	(by the proof below)
		≡ t(G) t(H)	(by Lemma 29)

≡ t(G) 1

(by the first case)

Proposition 38. The function t : TW 2/ → Trm /≡ is an homomorphism of 2p-algebras.

More precisely, on the lexicographic product of the number of edges and the textual precedence of the three considered cases.

ACKNOWLEDGMENTS

We would like to thank Nicolas Trotignon for the reasonably short proof he gave us for Lemma 11, and Christian Doczkal for the typos and slight mistakes he found that are fixed in this extended version.

The authors were supported by the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157).

This work was also supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

APPENDIX A OMMITTED PROOFS

Proof of Lemma 16. There exists elements x 1 , x 2 , y 1 , y 2 in U for which x ∈ cp(x 1 , x 2 ) and y ∈ cp(y 1 , y 2 ). We can assume without loss of generality that y ∈ cp(x 1 , x 2 ) and x ∈ cp(y 1 , y 2 ), otherwise the statement will follow immediately. Let π x and π y be, respectively, two irredundant paths of the form x 1 x 2 and y 1 y 2 avoiding, respectively, y and x. Assume x ∈ cp(x 1 , y 1 ) and x ∈ cp(x 2 , y 2 ), then we can find paths π 1 and π 2 of the form x 1 y 1 and y 2 x 2 avoiding x, but then we find a contradiction, since the concatenation of the paths π 1 , π y , and π 2 give us a x 1 x 2 -path avoiding x. Consequently, x ∈ cp(x 1 , y 1 ) or x ∈ cp(x 2 , y 2 ). We have, by a similar argument, the same statement on y.

Assume, without loss of generality, that x ∈ cp(x 1 , y 1 ) but y ∈ cp(x 1 , y 1 ), then necessarily, y ∈ cp(x 2 , y 2 ). Assume that x ∈ cp(x 2 , y 2 ) and consider a y 2 x 2 -path γ x avoiding x. We claim that x, y ∈ cp(x 1 , y 2 ). Assume towards a contradiction the existence of a x 1 y 2 -path δ x avoiding x. Then the concatenation of the paths δ x and γ x give us a x 1 x 2path avoiding x, and, thus, a contradiction. Similarly, if we assume the existence of a y 2 x 1 -path δ y avoiding y. Then the concatenation of the paths δ y and π 1 give us y 2 x 2 -path avoiding y, and, thus, a contradiction. Consequently, x and y must belong to cp(x 1 , y 2 ).

Proof of Lemma 17. Since we have an edge xy in CP(U ), Lemma 16 give us elements x and y in U for which x and y are vertices in cp(x , y ). We claim that z cannot be an element in cp(x , y ), otherwise, we would have three checkpoints in sequence, and, since xyz is a triangle, a path from the first to the third check point avoiding the vertex in the middle. This configuration contradicts the fact that the vertex in the middle is a check point in cp(x , y ).

Fix an irredundant x y -path π avoiding z. Assume, without loss of generality, that x appears before y in this path. There exists elements z 1 and z 2 in U for which z ∈ cp(z 1 , z 2 ). Assume that z is neither an element in cp(x , z 1 ) nor in cp(y , z 2 ), then we can find π 1 and π 2 , respectively z 1 x and y z 2 paths, avoiding z. The concatenation of the paths π 1 , π, and π 2 give us a z 1 z 2 -path avoiding z, and, thus, a contradiction. Consequently, either z ∈ cp(x , z 1 ) or z ∈ cp(y , z 2 ).

Consider the first configuration. We claim that z = z 1 satisfies the conditions on the statement. Assume the existence of a x z-path γ 1 avoiding x. Since zy is an edge in CP(U ), we can find a zy-path γ 2 avoiding x. The concatenation of the paths γ 1 , γ 2 and the yy -subpath of π give us a x y path avoiding x, which is a contradiction. Consequently, x ∈ cp(x , z). Moreover, since z ∈ cp(x , z ) we conclude that x ∈ cp(x , z ). By the same argument as before, the three elements x, y, and z cannot be at the same time check points of two single elements in U . Consequently, we can find an irredundant x z -path γ avoiding y. Assume the existence of a z y -path δ y avoiding y. The concatenation of the paths γ and δ y give us a x y -path avoiding y, which is a contradiction. Consequently, y ∈ cp(y , z ). Similarly, if we assume the existence of a y z -path δ z avoiding z, the concatenation of the paths π and δ z gives an x z -path avoiding z, which is a contradiction. Consequently, z ∈ cp(y , z ).

Finally, for the second configuration take z = z 2 .

APPENDIX B PROBLEMS WITH [START_REF] Dougherty | Normal forms for binary relations[END_REF] Parallel composition ( ) is written as an intersection (∩) in [START_REF] Dougherty | Normal forms for binary relations[END_REF]; we switch to this convention in this appendix.

A. Completeness of the axiomatisation

The authors define a taxonomy allowing to characterise certain terms as standard forms. They also define a rewriting system which they prove to be terminating and such that the irreducible terms belong to the taxonomy (Proposition 14).

However:

• The irreducible term dom(a ∩ b) does not belong to the taxonomy. One certainly wants to rewrite this term into 1 ∩ ab • using Equation ( 16) from Table 3. But doing so requires us to interpret the rewriting system modulo the neutral element 1.

If we do so in a systematic way, then it is no longer terminating: we get a loop between (1 ∩ (1 ∩ 1)) and

(1 ∩ 1) ∩ (1 ∩ 1) using Equations ( 9) and ( 10). All in all, it is unclear to us how to interpret the rewriting system and its termination proof. Moreover, the presented taxonomy is not strong enough for the final induction to go through (in Theorem 15). Indeed, take terms dom(d(ab ∩ c)) and dom(d(a ∩ cb • )), which are irreducible and belong to the taxonomy; they denote the same graph so that they should be proved congruent. The main induction in the proof of Theorem 15 however asks us to prove recursively that the subterms ab ∩ c and a ∩ cb • are congruent, which is false (lines 8,9 in the proof).

B. Minor exclusion theorem

On pages 240-241, a function unfold is defined and it is claimed that it should satisfy P 1 ∩ unfold(P ).

According to the definition, unfold(dom(a)) is 1 ∩ aa • , but the graphs of dom(a) and 1 ∩ aa • are not isomorphic.

This function is later used to extract terms from graphs whose input and output coincide. We could not understand how this works. (Cf. the end of the proof of Theorem 31.)

APPENDIX C INDEPENDENCE OF THE 2P-ALGEBRA AXIOMS

The following finite and commutative algebras, where we set x • = x, prove the independence of the last four axioms of 2p-algebras (Figure 2). In each case, we automatically checked that they form a model of the remaining axioms using the Coq proof assistant. See the web appendix of this work available at http://perso.ens-lyon.fr/damien.pous/tw2/. Except for (A3), the other axioms are also independent; their finite counter-models are provided on the aforementioned page.

Counter-model for axiom A9

Counter-model for axiom A10 (Take a = b = 2.)