Abstract The labeled multigraphs of treewidth at most two can be described using a simple term language over which isomorphism of the denoted graphs can be finitely axiomatized. We formally verify soundness and completeness of such an axiomatization using Coq and the mathematical components library. The completeness proof is based on a normalizing and confluent rewrite system on term-labeled graphs. While for most of the development a dependently typed representation of graphs based on finite types of vertices and edges is most convenient, we switch to a graph representation employing a fixed type of vertices shared among all graphs for establishing confluence of the rewrite system. The completeness result is then obtained by transferring confluence from the fixed-type setting to the dependently typed setting. Introduction In graph theory, the notion of treewidth [6] of a graph measures how close a graph is to a forest. In particular, the graphs of treewidth at most one are just the forests. Among the open problems related to treewidth, there is the question of finding finite axiomatisations of isomorphism for graphs of a given treewidth [5, page 118 ]. This question was recently answered positively for multi-graphs of treewidth at most two [4] , in the following way. A 2pdom-algebra is an algebra over the following signature, subject to eleven equational axioms: Introduction Graphs form an algebra for this signature, and a term u over this signature makes it possible to denote a graph g (u) . For instance, the graphs of (a·b • A first important result is that Σ-terms make it possible to denote precisely the class of connected graphs of treewidth at most two. That the graph of a term is connected and has treewidth at most two is relatively easy; the converse directionÐevery connected graph of treewidth at most two can be represented by a termÐis much harder [4] . This result was recently formalized in Coq [7] , by going through the well-known characterization of treewidth at most two graphs as those excluding K 4 as a minor [11] . We also have that graphs modulo isomorphism form a 2pdom-algebra: the eleven axioms of 2pdom-algebra ( Fig. 1 below) are all valid in the algebra of graphs. While a pen and paper proof is relatively easy, formalizing it in a proof assistant is non-trivial: it requires proper tools for combining graphs (to get the algebra of graphs) and for reasoning about graphs obtained by nested quotients and disjoint unions (to get the laws). This was also formalized in Coq [10] . Introduction As a consequence, for all terms u, v which can be proved equal using the 2pdom-axioms, g(u) and g(v) are isomorphic. The converse implication also holds: 2pdom-axioms are complete w.r.t. graph isomorphisms, so that (connected, treewidth at most two) graphs actually form the free 2pdomalgebra. Formalizing this completeness theorem in Coq is the main contribution of the present paper. Introduction This theorem is difficult because it must translate a rather global notion (an isomorphism between two graphs) into a Introduction x ∥ (y ∥ z) = (x ∥ y) ∥ z Introduction x ∥ y = y ∥ x 1 ∥ 1 = 1 Introduction x · (y · z) = (x · y) · z x · 1 = x Introduction dom(x) · (y ∥ z) = dom(x)·y ∥ z sequence of local reasoning steps (an equational proof from 2pdom-axioms). The result was first proved in [4] . We hoped to formalize this proof in Coq [7] until we realized an alternative proof could be used [8] . The alternative proof is much easier from the graph-theoretical point of view: it does not require a precise analysis of the structure of treewidth at most two graphs. Instead, it relies on a graph rewrite system that is terminating and confluent up to 2pdom-equivalence. By using Newman's lemma to prove confluence via local confluence, the starting global isomorphism is only analyzed locally in the proof. This is the proof we follow in the present formalization [9] ; we give a more precise sketch of it in Section 3. That this proof is simpler does not mean it is easy to formalize in a proof assistant: it involves both local and global operations on graphs, and the local confluence proof, which is already long on paper, requires good abstractions to avoid getting lost in the details. Introduction In order to define the rewrite system and prove most of the required results about it (Sections 4 to 7), we need to slightly generalize the letter-labeled graphs from [7, 10] to allow for a uniform treatment of both letter-labeled graphs (used in the statement) and 2pdom-labeled graphs (used for the rewrite system). However, even the generalized representation turned out to be inappropriate for getting a formal proof of local confluence. We circumvent this difficulty by using a second representation for graphs and rewrite steps for this part of the proof. This second representation makes it possible to prove local confluence in a natural way, as with pen and paper, by organizing case distinctions as most appropriate and using 'without-loss-of-generality' reasoning to factor out similar cases (Section 8). We then establish correspondence between our two representations (Section 9), allowing us to transfer local confluence from the second representation to the first and wrap everything together. 2pdom-Algebras We first recall the definition and basic properties of 2pdomalgebra [4, 16] . We consider the signature from the introduction for terms and algebras. We sometimes omit the · symbol and we assign priorities so that the expression (x · (y • )) ∥ z can be written just as xy • ∥ z. 2pdom-Algebras We deduce from the second equation that α β is a test, and that tests with · and 1 form a commutative monoid. 2pdom-Algebras We fix an alphabet A and let a, b, . . . range over the letters in A. We let u, v . . . range over Σ-terms with variables in A, which we call terms in the sequel. For terms u and v, we write u ≡ v when the equation is derivable from the axioms of 2pdom-algebras (equivalently, when the equation universally holds in all 2pdom-algebras). Terms quotiented by this relation form the free 2pdom-algebra over A. Sketch of Completeness Proof We now sketch the completeness proof from [8] , delegating most of the formal definitions to the subsequent sections. Sketch of Completeness Proof We consider directed multigraphs with two designated vertices respectively called input and output, and edges labeled in A. We just call them graphs. Examples of such graphs were given in Section 1, where inputs and outputs were depicted using unlabeled ingoing and outgoing arrows. Sketch of Completeness Proof Graphs form a 2pdom-algebra by considering the operations in Fig. 2 . The binary operations (·) and ( ∥ ) respectively correspond to series and parallel composition, converse (_ • ) just exchanges input and output, and domain (dom) relocates the output to the input. Proposition 3.1 (Soundness). Graphs form a 2pdom-algebra. Sketch of Completeness Proof By interpreting a letter a ∈ A as the graph a in Fig. 2 , we can associate a graph g(u) to every term u (cf. rest of Fig. 2 ). Sketch of Completeness Proof Note that the parallel composition of a graph with the graph 1 merges the input and output of the former graph. For instance, the graph a ∥ 1 consists of a single vertex with a self-loop labeled with a. We have that a term u is a test if and only if the input and output of g(u) coincide [8, Lemma 10] . Sketch of Completeness Proof By Proposition 3.1, g(u) and g(v) are isomorphic whenever u ≡ v. A formal proof of this soundness result is described in [10] . We slightly generalize it in the present work (Proposition 5.2 below), but our main contribution is a formal proof that the converse implication also holds: the axioms of 2pdom-algebra are complete w.r.t. graph isomorphism: Sketch of Completeness Proof For all terms u, v such that g(u) and g(v) are isomorphic, we have u ≡ v. Sketch of Completeness Proof As explained in the introduction, the key idea in the proof from [8] consists in using a graph rewrite system. This system is not used to obtain canonical normal forms. Instead, it makes it possible to recover various terms denoting a given graph, and its confluence makes it possible to relate those terms via the axioms. Sketch of Completeness Proof The rewrite system works on a generalization of the previous graphs, where vertices are labeled with tests and edges are labeled by terms rather than letters. Its main rules are the following ones: Sketch of Completeness Proof The circular vertices, i.e., those that are removed, must be distinct from input and output and must not have other incident edges.) Its behavior is reminiscent from the stateremoval algorithm used to construct a regular expression from an automaton: vertices and edges are removed until we obtain a small graph, from which we can read back a term. For instance, we have the following sequence of rewrite steps, which witnesses the fact that a·dom(b)·c ∥ d is a term denoting the starting graph. Sketch of Completeness Proof Note that the rewrite system is non-deterministic: one of the most trivial examples is that we could also obtain the term d ∥ a·dom(b)·c from the above graph. It is however confluent modulo a generalized notion of isomorphism where labels are compared using the relation ≡. Proving this property is one of the key steps of the completeness proof. Also note that there are terms which cannot be reached via the rewrite system. Consider for instance, the reduction below, which gives us the term (dom(a)·dom(b))·c for the first graph: Sketch of Completeness Proof A similar reduction would give us (dom(b)·dom(a))·c; but no reduction would give us dom(a)·(dom(b)·c), which is also a term denoting the same graph. To deal with this issue, we use a syntactic normalization function u → u ↓ in order to isolate the tests occurring on both sides of a term. (Normalized terms are not canonical, though: the normalization function is far from equating all provably equal terms.) Sketch of Completeness Proof All in all, the completeness proof is obtained by combining the following three key properties: Sketch of Completeness Proof (i) for all u, u ≡ u ↓ (ii) for all u, g(u) → * g ′ (u ↓ ), where for a normalized term v, g ′ (v) is the small irreducible graph labeled with v. (iii) → is confluent modulo generalized isomorphism The first one is a syntactic property proved by induction on u, whose formalization requires some work but does not raise any problem (induction and equational reasoning have very good support in proof assistants). Sketch of Completeness Proof The second one, reducibility, is also proved by induction on u, but requires much more work: we have to prove that rewrite steps are preserved under the various algebraic operations, and that there are enough rewrite rules to effectively reduce every graph of a term into a small irreducible graph. Sketch of Completeness Proof To prove the third property, we use Newman's lemma to reduce confluence to local confluence. We then have to analyze all critical pairs and show that they can all be joined modulo isomorphism and 2pdom axioms. This is the most delicate step for the formalization: we have to analyze many cases, and in each case we need to produce appropriate rewrite steps and isomorphisms. Sketch of Completeness Proof Once we have proved those three properties, completeness is obtained as follows. Sketch of Completeness Proof Proof of Theorem 3.2. Starting from two terms such that g(u) and g(v) are isomorphic, we know by reducibility (ii) that g(u) → * g ′ (u ↓ ) and g(v) → * g ′ (v ↓ ). Since the graphs g ′ (u ↓ ) and g ′ (v ↓ ) are irreducible, we deduce by confluence (iii) that they are isomorphic (modulo the axioms), from which we deduce u ↓ ≡ v ↓ . We conclude that u ≡ v by transitivity, using (i) twice. □ Packaged Labeled Multigraphs We now describe the formalization of labeled multigraphs. As explained above, we need two kinds of graphs: graphs with unlabeled vertices and edges labeled in A for the overall completeness result, as well as graphs with test-labeled vertices and term-labeled edges as an intermediate data-structure. In order to share code and define the various operations on those two classes of graphs at once, we introduce the following abstraction for labels, which we explain below: Packaged Labeled Multigraphs . A setoid is a pair (X, ≡) of a type X and an equivalence relation ≡ on X . A label structure consists of the following Packaged Labeled Multigraphs • a binary operation ⊗ and an element 1 : Packaged Labeled Multigraphs We usually omit the indices on equivalence relations, if they can be inferred from the context. We use setoids for labels since we want to instantiate these labels with tests and terms, compared modulo the axioms of 2pdom-algebra. Packaged Labeled Multigraphs We require a commutative monoid on vertex labels because one of the most crucial operations in our development is that of forming vertex-quotients of graphs (i.e., collapsing the vertices of a graph with respect to some equivalence relation): collapsed vertices get labeled with the composition in the monoid of their initial labels. Packaged Labeled Multigraphs The last requirement is motivated as follows. In order to express the rewrite system succinctly and to enable more opportunities to reason by symmetry, it is convenient to consider a notion of isomorphism on term-labeled graphs where edges can be flipped, using the converse operation to update the label: an edge from x to y labeled with u can be seen as an edge from y to x labeled with u • . In contrast, such an operation should not be allowed on letter-labeled graphs (there is no converse operation on the alphabet). Packaged Labeled Multigraphs Using the relation ≡ ′ e makes it possible to capture those two cases. We will define isomorphisms such that a u labeled edge from x to y can be mapped to a v labeled edge from y to x provided u ≡ ′ e v. The requirements on this relation ensure that we obtain an equivalence relation on graphs when doing so. The two label structures below capture the two aforementioned cases. Packaged Labeled Multigraphs Definition 4.2 (The alphabet A as a label structure). The trivial monoid (on the single element type unit), together with the discrete setoid on A (i.e., with Leibniz equality), and the empty relation on A for ≡ ′ , form a label structure. Definition 4.3 (2pdom-algebras as label structures). For every 2pdom-algebra X , we have a label structure with X as edge-labels, tests as vertex-labels, and x ≡ ′ e y := x ≡ y • . We fix a label structure L with setoids (L v , ≡) and (L e , ≡) for the rest of this section and the following one. Packaged Labeled Multigraphs the source of the edge e and p true e indicates the target of the edge e • l v : V → L v indicates the label of each vertex • l e : E → L e indicates the label of each edge We write x : G to denote that x is a vertex of G. Packaged Labeled Multigraphs Note that self-loops are allowed, as well as parallel edges with the same label. Representing the source and target functions for edges using a single function allows us to avoid code duplication at several places: this pieces of information are often handled in a uniform way. Packaged Labeled Multigraphs In order to define sequential and parallel composition (cf. Fig. 2 ), we rely, as in [7, 10] , on the following two operations: disjoint union and (vertex-)quotients. Packaged Labeled Multigraphs In order to define quotients on graphs we exploit that finite types are closed under taking quotients. If ≈ : X → X → B is a boolean equivalence relation on some finite type X , the quotient [2] of X with respect to ≈, written X /≈ , is a finite type as well. The type X /≈ comes with functions π : X → X /≈ and π : X /≈ → X such that π (π x) = x for all x : X /≈ and π (π x) ≈ x for all x : X . Packaged Labeled Multigraphs (y:V |π y=x ) l v y gathers in every equivalence class (i.e., every vertex of the new graph) all the vertex labels of the vertices in the class. Packaged Labeled Multigraphs In addition to those global operations for the algebra of graphs, we need the following local operations to define the rewrite system: Definition 4.7. Let G be a graph and let x, y : G, α, β : L v , and u : L e . We write: Packaged Labeled Multigraphs • 1 α for the edge-free graph with one α-labeled vertex. • 2 β α := 1 α + 1 β (a graph with only two vertices). Packaged Labeled Multigraphs α is combined with the existing label of x). Packaged Labeled Multigraphs Note that for all these graph operations (both the local ones and the global ones), working in Coq with a representation of graphs closely following Definition 4.4 is extremely convenient: it is compact, and all basic invariants are nicely enforced via (dependent) types. Moreover, the mathematical components library [18] provides all the required infrastructure for taking disjoint unions and quotients on finite types. Packaged Labeled Multigraphs This allows us to define isomorphisms as follows: Packaged Labeled Multigraphs An isomorphism is a homomorphism where h v and h e are bijections. In this case, the second condition simplifies to Packaged Labeled Multigraphs We denote the type of isomorphisms between graphs F and G by F ≃ G. Packaged Labeled Multigraphs Intuitively, the h d predicate in a homomorphism indicates whether the homomorphism flips a given edge or not. If an edge e is flipped, the vertex component h v should map the source of e to the target of h e e and vice versa, whence the use of a boolean xor operation in the first requirement. Accordingly, the labels of the two edges should be related by ≡ ′ rather than ≡ when an edge is flipped (third requirement). Packaged Labeled Multigraphs Note that the notion of isomorphism depends on the label structure. When the label structure L is the one from Definition 4.2, h d must be the constantly false function (because of the third condition), and the second condition vanishes since all vertices are labeled with the unique value of type unit; therefore, we recover in this case a standard definition of non-edge-flipping isomorphism on edge-labeled multigraphs [7, 10] . We remark that Definition 4.8 formalizes the computational notion of isomorphism rather the property of two graphs being isomorphic. This is crucial for a compositional treatment of isomorphisms. To see this, consider the graph expression F ∔ [x, u, y] and the operation of replacing F with an isomorphic graph G. This requires to also replace the vertices x and y with their respective images under the vertex component of the isomorphism. This approach is thus required in order to state (and prove) the two congruence properties below. (In the following, when an isomorphism h : F ≃ G appears as a function, it is to be taken as the underlying vertex component h v .) Lemma 4.10. Let F, G be graphs and let h : Packaged Labeled Multigraphs Concretely in Coq, formalizing the isomorphisms in such a computational way requires us • to place the definition in Type rather than Prop, Packaged Labeled Multigraphs • to express that functions are bijective using explicit inverses (here we build on a small library where we encapsulate computational bijections between types), • to make sure that whenever we define an isomorphism, we make it either transparent so that its computational content is immediately available, via reduction, or we prove appropriate equations about it before making it opaque for reduction. Like in [10] , we prove the following properties about the global operations of union and quotient: Packaged Labeled Multigraphs relation on G induced through the given isomorphism by a given equivalence relation ≈ on F . Packaged Labeled Multigraphs an equivalence relation on F /≈ , and ≈ ′′ the equivalence relation on F obtained by composing ≈ and ≈ ′ . 7. (F + G) /≈ ≃ F /≈ ′ when G has no edge and all vertices labeled with 1, ≈ is an equivalence relation on F + G, ≈ ′ is its restriction to F , and for all x : G there exists y : F with in r x ≈ in l y. Packaged Labeled Multigraphs These lemmas allow us to extrude quotients out of unions and to simplify quotients [10] . The generalization to vertexlabeled graphs requires us to verify that vertex labels are collected in a consistent way by the quotient operation (Definition 4.6). While we use ssreflect notations for the 'bigops' operation appearing in this definition, we have to reprove various laws since we only have a monoid structure up to a setoid equality. The generalization to edge-flipping isomorphisms is harmless: the concrete isomorphisms (the first, third, and last three items) do not use this opportunity, and the remaining congruence properties just forward this piece of information. Packaged Labeled Multigraphs In addition, we prove a series of basic isomorphisms about interactions between the various operations. We list a few of them below. Together with Lemma 4.11 these properties allow us to reason algebraically and compositionally when we have to prove isomorphisms between graphs. The situation is however not as satisfactory as with standard equational reasoning: the type dependency in congruence lemmas (e.g., Lemma 4.10) prevents us from using standard tools like 'setoid rewriting' so that we generally have to apply these congruence lemmas manually. Packaged Labeled Multigraphs We also prove the following lemma, allowing us to provide an explicit representation for a given quotient graph. We shall see in Section 7 that this makes it possible to prove some concrete isomorphisms by reasoning globally at places where the compositional approach is less convenient. The 2pdom-Algebra of Graphs In order to obtain a Σ-algebra, we need to work with twopointed graphs: The 2pdom-Algebra of Graphs Definition 5.1. A two-pointed graph (or 2p-graph for short) is a structure ⟨G, ι, o⟩ where G is a graph and ι : G and o : G are two vertices called input and output respectively. The 2pdom-Algebra of Graphs The notions of homomorphism and isomorphism are extended accordingly: on 2p-graphs, they should map the input to the input, and likewise for the outputs. We write F ≃ 2 G when two 2p-graphs F and G are isomorphic. The local operations are extended to 2p-graphs in the obvious way, and we overload the notations for these operations. The 2pdom-Algebra of Graphs We can now give a formal definition for the Σ-operations on 2p-graphs ( Fig. 3 , where R eqv is the equivalence closure of a binary relation R). This is the same definition as in [7, 10] except that it is generalized to graphs over an arbitrary label structure; the way vertex labels are handled is completely hidden in the definition of the quotient operation on graphs (Definition 4.6). Accordingly, since we have generalized [10, Lem. 6.6] to L-labeled graphs (Lemma 4.11), the formal proof [10] of Proposition 3.1 smoothly scales into a proof of the following generalization: We finally define the function g interpreting terms into graphs. There are actually two such functions: The 2pdom-Algebra of Graphs • the one from Theorem 3.2, which interprets a term as a letter-labeled graph, i.e., a graph over the label structure from Definition 4.2. This is the unique Σhomomorphism g A such that g A (a) = a * * for all letters a ∈ A, where * : unit is the only allowed vertex-label. The 2pdom-Algebra of Graphs • the one used in the reducibility statement for the rewrite system, which produces a term-labeled graph, i.e., a graph over the label structure from Definition 4.3 applied to the 2pdom-algebra of terms. This is the unique Σ-homomorphism g T such that g T (a) =âˆ1ˆ1 for all letters a ∈ A, where1 is the term 1 seen as a test, andâ is the letter a seen as a term. Since we proved that both algebras of graphs are 2pdomalgebras (Proposition 5.2), we get that u ≡ v entails g(u) ≃ 2 g(v) for both functions. However, the completeness proof we sketched in Section 3 only gives us a proof of completeness with respect to g T . To get completeness with respect to g A , we build on the following lemma: The 2pdom-Algebra of Graphs Proof. Follows from relabelings between two label structures being Σ-homomorphisms and preserving isomorphisms. □ The 2pdom-Algebra of Graphs We only work with g T in the sequel; we abbreviate it as g. Rewrite System We now present the graph rewrite system we use to establish completeness of the axioms in Fig. 1 . The rewrite system rewrites 2p-graphs labeled with elements of an arbitrary 2pdom-algebra X 1 which we fix in this section. Rewrite System An informal description the rules is given in Fig. 4 . A key intuition about these rules, which does not need to be formalized, is the following. First observe that if X is itself an algebra of 'basic' graphs, so that we have graphs labeled with basic graphs, then one can expand a graph into a basic graph by 'replacing' the edges and vertices by their labels. (In fact, the construction of the previous section is a monad in the category of 2pdom-algebras, where multiplication is given by expansion.) The key intuition is that isomorphisms and rewrite rules preserve expansions: if F ≃ 2 G or F → G then the expansions of F and G are isomorphic (as basic graphs) 2 . This is consistent with the analogy given in Section 3 about state-removal procedures for extracting regular expressions out of finite automata: there, the automata are rewritten through local operations that preserve the overall language. Rewrite System It is important here that we work modulo edge-flipping isomorphisms. For instance, the following step is an instance of rule (V2) modulo such isomorphisms: Rewrite System If we were not doing so, we would need two variants of rule (V2) (the one above and the symmetric one), as well as a variant of rule (V1) and a variant of rule (E2). We would thus move from five to nine cases in each case analysis on steps, and from 15 to 45 cases in the local confluence proof. Alternatively, we could add a rule to flip an arbitrary edge. But such a rule is not terminating so that it would prevent us from using Newman's lemma for proving confluence. (All other rules remove either an edge or a vertex, so that the system we use is obviously terminating.) Remark 6.1. Rule (V0) deserves some explanation, as it is not included in [8] . Note that graphs of the shape д(u) are always connected and that the rewrite system never disconnects connected graphs. Consequently, rule (V0) will never apply when starting from the graph of a term. We include the rule because it makes the rewrite system confluent also on possibly disconnected graphs, without changing its behavior on the connected graphs we care about. This allows us to avoid talking about connectivity, at the cost of five easy additional cases in the confluence proof. Rewrite System Unlike for the construction of the 2pdom-algebra of graphs, which mainly uses global operations on graphs, the rewrite system is defined using various local operations. There are at least two fundamentally different ways to formalize this rewrite system: a subtractive version and an additive one. Assume an operation G \ x that removes a vertex x : G (and any incident edges) from the graph G. Then rule (V0) can be expressed as rewriting G to G \ z, provided that z {ι, o} and that z has no incident edges. Alternatively, this rule can be expressed as rewriting G ∔ α to G. Note that the latter formulation does not require any side condition: the fact that the new vertex is isolated and distinct from input and output is implicit in definition of G ∔ α. This makes the additive formulation rather appealing, especially with the graph representation employed so far. Indeed, the subtractive formulation not only requires explicit side conditions, but also an operation for deleting vertices, which is painful to account for with this representation: deleting z : G from G is only possible if z is neither input nor output, so that vertex deletion on 2p-graphs must take a proof of this fact as additional argument. 3 Recall from Section 3 that the two most important properties of the rewrite system are: Rewrite System (ii) Reducibility of g(u) to a small irreducible graph; (iii) Confluence up to isomorphism. It turns out that (ii) can be proved with reasonable effort using an additive formulation of the rewrite system and the packaged representation of graphs. However, as we will argue in Section 8, a subtractive formulation is much more convenient for (iii) and requires us to temporarily use a second representation of graphs. Rewrite System We now give the formal definition of the rewrite system we use to prove the reducibility property. The rules are given in Fig. 5 . Recall that G ∔ α is defined as the disjoint union of G and the single-vertex graph 1 α whose only vertex is * . Hence, its vertices are in l x for x : G and in r * . Rewrite System Note that, by design, the rules to not yield a graph property (i.e., steps are not preserved under isomorphisms). Thus, we need to close under both isomorphism and transitivity in order to obtain a well-behaved rewrite system. We do so through the following inductive definition: Rewrite System Since ≃ 2 is reflexive and transitive, so is ⇒. Rewrite System To obtain reducibility in the following section, we need to show that rewrite steps are preserved by the Σ-operations on 2p-graphs: Figure 5 . Additive presentation of the rewrite system. Rewrite System Since the operations are already known to preserve isomorphisms (part of Proposition 5.2), it suffices by induction on the rewrite sequence to prove the lemma when G → G ′ . The last item is straightforward since converse and domain do not modify the (non-pointed) graph of their argument. It moreover suffices to do only one side of the first two items since parallel composition is commutative, and since we can use converse to swap the arguments of sequential compositions (again, by Proposition 5.2). Rewrite System Since both parallel and sequential composition are defined as a quotient of a disjoint union, we factorize most of the work by proving the following technical lemma: Rewrite System , H be 2p-graphs and let ≈ be an equivalence relation on the vertices of G + H such that vertices of G which are neither input nor output are not equivalent to any other vertex. Let ≈ ′ be the equivalence relation mimicking ≈ on Rewrite System Proof. The lemma intuitively holds because every vertex that can potentially be removed in G by the given rewrite step to G ′ cannot be the input or the output. Since the quotient touches at most the input and output of G, such a vertex can still be removed in ⟨(G + H ) /≈ , π in l ι G , π in r o H ⟩. Rewrite System In practice, this lemma is proved compositionally: after a case analysis on the rule used to derive G → G ′ , we use the commutation properties established between the local operations and the global ones (Lemma 4.12) in order to rewrite ⟨(G + H ) /≈ , π in l ι G , π in r o H ⟩ into an isomorphic graph for which the same rewrite rule syntactically applies, and we prove that the resulting graph is isomorphic to the expected one by using the commutation properties again. □ Note that the use of ⇒ in the lemma above is solely to allow for isomorphism steps around a single proper step; this pattern is occurs at several places in our development Reducibility We work in this section with the 2pdom-algebra of terms over A, and with 2p-graphs labeled using this algebra. Reducibility To get a formal reducibility statement, we need to define the normalization function discussed in Section 3, as well as the function g ′ from normal terms to graphs. Reducibility A normal term is either a test (α), or a triple (α, u, β) where u is intuitively not a test, although we do not need to keep track of this information. We obtain irreducible graphs from normal terms by setting g ′ (α) := 1 α and g ′ (α, u, β) := u β α . We recover a term from a normal term by setting ⌊(α)⌋ := α and ⌊(α, u, β)⌋ := αuβ. Reducibility The role of the normalization function _ ↓ is to recursively compute a term whose shape matches the shape of terms obtained from irreducible graphs. It is defined as the unique Σ-homomorphism such that a ↓ = (1, a, 1) , after having defined the following Σ-algebra on normal terms: Proof. This amounts to proving that the above equations defining the Σ-algebra on normal terms are all derivable from 2pdom axioms after applying ⌊_⌋ on both sides. □ Formalizing reducibility is more challenging: Reducibility Proposition 7.2 (Reducibility). For all terms u, we have g(u) ⇒ g ′ (u ↓ ). Reducibility Proof. We proceed by induction on u. In each case, we obtain reduction sequences by induction, which we can combine using the preservation lemma; then it suffices to do a case analysis on the shape of the normal terms, and to perform a last rewrite step if necessary. Suppose for instance that u = v ∥ w. By induction we get reduction sequences g(v) ⇒ g ′ (v ↓ ) and g(w) ⇒ g ′ (w ↓ ), from which we deduce by Lemma 6.2 that g(u) = g(v) ∥ g(w) ⇒ g ′ (v ↓ ) ∥ g ′ (w ↓ ). Then there are three cases to consider: Reducibility • either both v ↓ and w ↓ are tests, say (α) and (β), so that u ↓ = (α β). In this case it suffices to check that Reducibility , βδ ), and we check that one of them is a test and the other is not, say The last isomorphism comes from the law α βγ (v ′ ∥ 1) ≡ αv ′ β ∥ γ , which is indeed derivable. In those three cases for parallel composition, the first isomorphism we have to provide is between the graph g ′ (v ↓ ) ∥ g ′ (w ↓ ), which is a quotient of a graph with two to four vertices, and a concrete graph with one or two vertices. We could prove those isomorphisms compositionally, but it turned out to be more convenient to prove them using Lemma 4.13, by providing surjective homomorphisms explicitly. one of them is a test and the other is not, say The other Σ-operations are handled similarly, domain and converse of course being simpler. □ Confluence We use Newman's lemma to prove confluence of ⇒ via local confluence of the single step relation →: every strongly normalizing and locally confluent relation is confluent. The rewriting relation is strongly normalizing since the number of vertices plus the number of edges decreases along each step. Since we work modulo isomorphisms and our single step relation is not a graph property, the appropriate local confluence property is the following one: Confluence Thanks to the inductive definition we used for ⇒, we easily formalize the required variant of Newman's lemma to deduce confluence of ⇒. Confluence Formalizing the above local confluence lemma however turns out to be extremely tedious using packaged graphs and our additive definition of the rewrite rules. To see why, consider one of the simplest cases, the interaction of two instances of the (V1) rule. Our assumptions in this case are: Confluence In order to close this pair, we first have to check whether the isomorphism maps in r * to in r * (in which case the two instances are the same). Otherwise, we need to trace the vertex removed on the right through the isomorphism in order to expand F accordingly and vice versa. Moreover, one needs to exhibit an isomorphism between the untouched parts of F and G. This happens in a dependently typed setting and our attempts to carry out these constructions failed due to circular dependencies between the involved statements. Moreover, even if this problem could be solved, it would not lead to a natural proof of local confluence: the vertices of interest each have two names (in F and in G), keeping track of their correspondences rapidly grows out of hands, and we cannot organize case distinctions in the most efficient way. Confluence Instead, we prove local confluence using an alternative representation of both graphs and the step relation. As it comes to graphs, we employ open graphs: graphs where both vertices and edges are just natural numbers. Although such a formal representation is commonplace [1, 13ś15, 17] , we are not aware of any work where a correspondence with a packaged representation was established and exploited. For the step relation, we employ a subtractive characterization such that single steps can be performed independently from the concrete shape of the considered graph. Confluence We let O, U , V . . . range over open pre-graphs. The separation into pre-graphs and well-formedness is crucial here. It allows us to separate the task of proving that a graph has the desired shape from proving that it is actually a graph. Confluence In Coq, we use the finmap library [3] to represent finite sets over the countable types V and E. Moreover, we turn the well-formedness predicate into a class, allowing it to be inferred it automatically in many situations. Confluence We then define operations corresponding to those defined on 2p-graphs. In the case of open graphs, where edges and vertices are external, the operations adding vertices and edges take the edge to be added as additional argument. That is, we have the following operations: Confluence • U \ x denotes U with x and all edges incident to x removed. • U − E denotes U with all the edges in E removed. All these operations are easily defined as operations on pregraphs. They yield graphs under the expected side conditions (e.g., adding an edge requires that the vertices are part of the graph and deleting a vertex requires that the deleted vertex is distinct from input and output). In particular, vertex deletion, which we will use extensively below, is a benign operation on open graphs. In contrast, the quotient and disjoint union operations we extensively used in the previous sections would be painful to deal with on open graphs. Confluence We have the following notion of strong equivalence: two pre-graphs are strongly equivalent if they only differ by their labels, up to the setoid relations on L v and L e . Confluence In other words, strong equivalences correspond to nonedge flipping isomorphisms which are the identity on both vertices and edges. This relation enjoys a number of useful properties, of which we list only a few: Confluence Note that most of these equivalences hold irrespective of whether the graph G is well-formed or not. A notable exception is (6) , where the addition of x to a graph that is not well-formed could turn a formerly łdanglingž edge into one that is incident to x and would therefore be removed by the deletion of x. That the last two items hold is extremely convenient as it allows us to use 'setoid rewriting', something we cannot use for isomorphisms on packaged graphs due to the dependency between the replaced graphs and their vertices (cf. Lemma 4.10). Confluence We now turn to the definition of the step relation. We want steps to be preserved under isomorphism so that the local confluence property can be stated using a single graph as a left-hand side of two reduction steps. This forces us to handle the edge-flipping behavior in the definition of the rules. To this end, we define a predicate expressing whether an edge can, up to reversal, be seen as a given edge, and then use this predicate in the definition of the step relation. Confluence arc U e x u y := e ∈ E U ∧ ∃b. p U b e = x ∧ p U (¬b) e = y ∧ l e U e ≡ [b] u We moreover write I G (x) for the set of edges incident to x in G. The rules of our subtractive variant of the step relation are given in Fig. 6 . We use a max operation on edges (natural numbers) in rules (V2) and (E2): by doing so, the name of the edge which is kept depends only on the edges being removed and not on the order in which the edges are matched. This is convenient in that it allows us to close localconfluence critical pairs using strong equivalences rather than isomorphisms. Confluence We define the multi-step rewrite relation ⇒ as the least transitive relation containing strong equivalence, single steps, but also the relation that flips a single edge in a graph. This is fine since we reason modulo edge-flipping isomorphisms on packaged graphs; doing so makes it possible to use symmetry reasoning in the analysis of the critical pairs. Now we have everything in place to prove local confluence Confluence Since ⇒ is closed under strong equivalence, the statement is equivalent to the one where U ′ is syntactically equal to V ′ . We prefer this formulation because it matches the way we prove the lemma. Confluence Proof. The proof boils down to a case distinction between all the possible pairs of rules that could have been applied to obtain U ← O → V . We can reduce the number of cases by assuming, without loss of generality, that the rule applied on the left has a lower index (with respect to the textual order in Fig. 6 ). In Coq, this is realized by defining the relation → as a relation in Type and defining a function numbering the rules. There are still fifteen cases left, and each of them comes with its own case distinctions. We discuss only some illustrative cases below. Confluence • Consider an interaction of the rule (V1) with arc O e x u z and rule (V2) with arc O e 1 x ′ u ′ z ′ and arc O e 2 z ′ v ′ y ′ . We have z z ′ due to the different number of incident edges. If z {x ′ , y ′ } the instances are independent, so assume z ∈ {x ′ , y ′ }. Without loss of generality, we can assume z = x ′ , for otherwise we exchange the roles of x ′ and y ′ as well as e 1 and e 2 , setting u ′ := v ′• and v ′ := u ′• and flipping the edge introduced through the application of (V2). Hence, e 2 = e, z ′ = x, and v ′ = u, exhibiting the situation below: Confluence After applying rule (V1) on both sides and using the equivalences from Lemma 8.4, it suffices to show dom(uαvβ) ≡ dom(uαdom(vβ)). Confluence • Rules (V2) and (E2) can interact as follows: Confluence This pair can be joined by applying rule (E1) in the left and rule (V1) on the right, yielding the derivable Confluence This pair can be joined by applying Rule (V0) on both sides, not requiring any equation. □ Note that we need to allow edge-flips in the definition of ⇒ in order to factor the proof by reasoning without loss of generality in the first case discussed in the proof. This is important: we use this pattern thirteen times in the full proof, which is 500 lines long. We remark that the last case mentioned above does not arise in [8] where the graphs are assumed to be connected. Transferring Local Confluence Proposition 8.5 proves local confluence, but not using the representation employed in the rest of the formalization. In this section, we outline what is needed in order to transfer this result and obtain a proof of Proposition 8.1. Transferring Local Confluence We first need translation functions between the two representations of graphs. We start with the translation from open graphs to packaged graphs. Definition 9.1 (Packing). Let U be an open graph. We define the packing of U , written pack U , to be the 2p-graph whose finite type of vertices is the finite type of elements of V U (also denoted by V U 4 ) and likewise for edges. The remaining components are obtained by casting the components of U to the appropriate types (e.g., p : B → E U → V U for the endpoints of edges). Transferring Local Confluence Since finite sets over countable types coerce to finite types in Coq, this packing operation is easy to define. Transferring Local Confluence For the converse translation, from packaged graphs to open graphs, the main issue is in embedding the finite types of edges and vertices of a given packaged graph into the generic vertex and edge types. For these, we employ two generic injections Transferring Local Confluence Both of these come only with partial inverses in general, since T may be empty. This is never the case for the vertex type of 2p-graphs however, which must contain input and output, so that we get: Transferring Local Confluence The functions are defined such that proj v (inj v v) = v whenever v is a vertex (of some 2p-graph) and proj e (inj e e) = Some e whenever e is an edge. The operation of opening a packaged graph can then be defined as follows Transferring Local Confluence • l e ′ e := if proj e e is Some e ′ then l e e ′ else 1 At this point, we can prove: In order to relate the two variants of the step relation, we need a proper notion of isomorphism on open graphs. This is obtained by reusing isomorphisms on packaged graphs via the packing operation. Note that we define isomorphism as a relation between pre-graphs; this relation is a partial equivalence relation (PER) rather than an equivalence relation due to the wellformedness requirement. Transferring Local Confluence As expected, strong equivalences give rise to isomorphisms. Transferring Local Confluence Note that, given O ≡ U , well-formedness of O implies well-formedness of U , allowing us to have only one wellformedness assumption. This is convenient when showing that a complex graph expression is isomorphic to an expression known to be well-formed. Now that we have a proper notion of isomorphisms on open graphs, we can show that the open step relation commutes with them. Transferring Local Confluence This property is relatively easy to prove because it deals exclusively with open graphs. All we need to do is establish a number of lemmas showing that incidence of edges and the arc predicate are preserved under isomorphisms. As with isomorphisms of packaged graphs, this requires viewing isomorphisms as functions from vertices to vertices. Transferring Local Confluence We then need to prove that (additive) packaged steps and (subtractive) open steps actually match. To prove that packaged steps give rise to open steps we first establish a number of commutation properties about the opening operation: Transferring Local Confluence By Lemma 9.6, we can also make isomorphism steps before making an actual step. We pick a fresh vertex z and a fresh edge e and then use Fact 9.7 to push the opening operation down to the graph G. Thus (1) reduces to showing: Transferring Local Confluence The side conditions of rule (V1) are then easily established. Applying the rule (V1) determines U ′ to be Transferring Local Confluence For the converse direction (reflecting open steps with packaged steps), we need to be able to trace vertices through the packing operation. For this, we define a function Transferring Local Confluence Recall that the vertex type of pack U is
{'paper_id': '207823347', 'title': 'Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq', 's2_url': 'https://api.semanticscholar.org/CorpusID:207823347', 'source': 'S2ORC'}