Rewriting in Free Hypergraph Categories
Fabio Zanasi
cs.LO

Model independent evaluation of the Wilson coefficient 
 of the Weinberg operator in QCD
    Ryo Nagai
    December 30, 2023
========================================================================================



 We study rewriting for equational theories in the context of symmetric monoidal categories where there is a separable Frobenius monoid on each object. These categories, also called hypergraph categories, are increasingly relevant: Frobenius structures recently appeared in cross-disciplinary applications, including the study of quantum processes, dynamical systems and natural language processing. In this work we give a combinatorial characterisation of arrows of a free hypergraph category as cospans of labelled hypergraphs and establish a precise correspondence between rewriting modulo Frobenius structure on the one hand and double-pushout rewriting of hypergraphs on the other. This interpretation allows to use results on hypergraphs to ensure decidability of confluence for rewriting in a free hypergraph category. Our results generalise previous approaches where only categories generated by a single object (props) were considered.




§ INTRODUCTION


Symmetric monoidal categories (SMCs) are an increasingly popular mathematical framework for the formal analysis of network-style diagrammatic languages that are found across different disciplines. In an SMC arrows have two composition operations, intuitively corresponding to sequential (c  d) and parallel (c  d) combination of compound systems, and there are symmetry arrows sym.pdf, intuitively representing tangles of wires. These constructs are traditionally rendered by the two-dimensional notation of string diagrams, which has the key advantage of absorbing most of the structural equalities prescribed by the definition of SMC. For instance, the two sides of the exchange law (a_1  a_2)  (b_1  b_2) = (a_1  b_1) (a_2  b_2) are encoded by the same string diagram [width=1.5cm]exchangeab. The graphical syntax emphasises connectivity and resource-exchange between components, which makes it particularly effective in the analysis of challenging computational models such as distributed systems (based on threads communication) and quantum processes (powered by a notion of non-separable—entangled—states).

Some applications demand SMCs with a richer structure. In this paper we focus on hypergraph categories, which are SMCs where each object x is equipped with a separable Frobenius monoid. That means, for each x there are operations as on the left, forming a commutative monoid and a commutative comonoid that interact according to the Frobenius  law and the separability law, as on the right.

    multx.pdf    unitx.pdf    comultx.pdf    counitx.pdf            frobxL.pdf =  frobxC.pdf =  frobxR.pdf    sepxL.pdf =  sepxR.pdf

The core intuition is that this extra structure allows dangling wires of a string diagram to fork, be discarded, be moved to the left/right side, resulting in a more flexible manipulation of the interfaces (variables, memory cells) of the represented system. The use of hypergraph categories as an algebraic approach to computation was pioneered by Walters and collaborators <cit.>, under the name of well-supported compact closed categories. Since then separable Frobenius monoids have appeared ubiquitously in diagrammatic calculi across diverse research threads. They notably feature in the ZX-calculus <cit.> (quantum theory), where each Frobenius structure has a precise physical meaning in terms of quantum observables. Frobenius monoids also form the backbone of the calculus of stateless connectors <cit.>, the calculus of signal flow diagrams <cit.>, Baez's network theory <cit.> and Pavlovic's monoidal computer <cit.>. More recently, a particular attention has been devoted to generic constructions of hypergraph categories through abstract notions of span, relation and their duals <cit.>.

Whereas separable Frobenius monoids constitute a common core for the aforementioned approaches, in each application string diagrams are further quotiented by domain-specific equations, instrumental in defining the appropriate notion of behavioural equality of systems. The perspective of this work is to acknowledge the conceptual difference between the symmetric monoidal and Frobenius structure on the one hand, which is a built-in part of any hypergraph category, and the domain-specific equations on the other hand. We shall study the latter as rewriting rules: if the left hand side of such an equation can be found in a larger string diagram, it can be deleted and replaced with its right hand side.

This is coherent with the everyday practice of users of diagrammatic calculi and is the starting point for implementing graphical reasoning in a proof assistant. There is a thorough mathematical theory of rewriting for monoidal categories, which regards rewrite rules as generator 2-cells (variously called computads <cit.> or polygraphs <cit.>) and the possible rewriting trajectories as composite two-cells. However, this abstract perspective does not provide immediate help when it comes to implementing rewriting. The main challenge is a concrete understanding of matching: in order to detect whether a string diagram contains the left-hand side of a rewriting rule, one needs to consider all its possible decompositions according to the structural equations. In an hypergraph category, this amounts to say that rewriting happens modulo the equations of separable Frobenius monoids. For instance, the rewriting rule 

    [width=3.2cm]introRewLc.pdf    [width=2.8cm]introRewRc.pdf

applies in the leftmost string diagram below, module the separable Frobenius structure on objects c, d.

    [width=4.2cm]introRew1c.pdf (<ref>) [width=4.2cm]introRew2c.pdf    [width=4.2cm]introRew3c.pdf

We shall develop a combinatorial characterisation of this rewriting mechanism, in three steps:


  * the first step (Section <ref>) is to give a combinatorial description of the string diagrams in free hypergraph categories. Our choice is a category of cospans of hypergraphs, which is shown to be isomorphic to the free hypergraph category generated by a signature. This data structure encapsulates all the equivalent representations of a string diagram modulo Frobenius into a single object, thus easing the complexity of matching. The idea of the isomorphism is that boxes in a string diagram are represented as hyperedges, and wires as nodes. The use of cospans I_l f G g I_r is essential: the carrier G encodes the string diagram itself, whereas I_l and I_r are discrete hypergraphs (sets of nodes) that indicate through f and g which nodes of G are dangling wires on the left and on the right of the corresponding string diagram.

As the name suggests, the close relationship between hypergraph categories and hypergraph structures was clear to previous authors <cit.>, as well as the use of cospans to mimic interfaces <cit.>. Our characterisation combines existing approaches in a way that best suits the application to rewriting. The main generalisation is characterising hypergraph categories that are freely generated by multi-sorted instead of single-sorted signatures. 


  * The second step (Section <ref>) is to exploit the combinatorial interpretation to realise string diagram rewriting as rewriting of hypergraphs. The fact that cospans of hypergraphs form an adhesive category <cit.> gives an off-the-shelf theory of double-pushout (DPO) rewriting. We show that rewriting modulo Frobenius and DPO rewriting of hypergraphs are essentially the same thing. The problem of matching in an hypergraph category (<ref>) is reduced to finding an hypergraph homomorphism.


  * As last contribution (Section <ref>), we show that confluence for terminating rewriting systems in hypergraph categories is decidable, as it is reducible to a computable critical pair analysis. This well-known property of term rewriting becomes a non-trivial question when dealing with two-dimensional entities. For instance, in the aforementioned polygraph approach <cit.>, where critical pairs are considered in the string diagrammatic syntax rather than in a graph model, even a finite set of rewriting rules may yield infinitely many critical pairs <cit.>. In the context of ordinary DPO graph rewriting decidability also fails <cit.> unless further conditions are imposed, such as requiring that all critical pairs satisfy a syntactic condition called coverability <cit.> or that they are joinable in a stricter sense <cit.>. We establish our decidability result within the framework of recent work <cit.> that studies confluence for DPO hypergraph rewriting with interfaces. Not only this variant enjoys decidability without further restrictions on critical pairs, but is precisely tailored for the interpretation of “syntactic” rewriting from hypergraph categories. We refer to <cit.> for a more extensive discussion of how the interface approach compares to others in the DPO rewriting literature. 



Rewriting modulo Frobenius structure has been studied along the same lines in <cit.>. These recent works by the author and collaborators serve as a roadmap for this paper: the aim here is to verify that such results generalise to multi-sorted algebraic theories, for which the freely generated category has a Frobenius structure on each sort. In light of <cit.>, the way this generalisation unfolds is not particularly surprising, as we are essentially able to lift the same proof techniques from a single to multiple sorts. However, we believe that the redaction of a reference paper for these results is timely. Firstly, it is justified by the renewed interest for hypergraph categories, witnessed by several recent applications, especially to circuit theory <cit.> and to natural language semantics <cit.>: using the theory developed in <cit.> is going to require the full generality of the multi-sorted case. Secondly, another justification comes from axiomatic approaches to various families of systems (concurrent  <cit.>, quantum <cit.>, dynamical <cit.>) in which the equational theory axiomatising system behaviour includes two or more Frobenius algebras. When it comes to rewriting, the approach introduced in <cit.> only allows to absorb one Frobenius structure in the combinatorial model. In this paper, we show how additional Frobenius structures can be also absorbed in the same manner[The fact that multiple Frobenius structures are on the same object (like in the aforementioned theories) or on different objects (like in this work) of a category may be overcome with the addition of `switch' operations from one object to the others, as we are going to show in a paper in preparation.], thus reducing the complexity of the aforementioned axiomatisations and simplifying the task of studying normal forms, confluence and termination.






  
Notation.

In a category  with coproducts, h_1,h_2  X+Y → Z is the copairing of h_1   X → Z and h_2   Y → Z, defined by universal property of +. Also, f  g  a → c is the composition of arrows f  a → b,  g b → c. We sometimes write afb or b f a for f   a → b, or also f and f if object names are immaterial for the context. We write  for the monoidal product in a monoidal category.










§ PROPS AND HYPERGRAPH CATEGORIES







We are going to study hypergraph categories freely generated by a signature of operations. The following is the notion appropriate to the monoidal context.

 A monoidal theory is a tuple (Σ, ) of a signature Σ and a finite set  of colours. Elements of Σ are operations o   w → v with a certain arity w and coarity v, where w, v ∈^⋆.  


Generic theories are typically triples, allowing also for a set of equations on Σ-terms. We do not need that level of generality here: equations will be treated differently, as rewriting rules (unless they are structural, like the equations of symmetric monoidal categories or of hypergraph categories, see below).



Towards hypergraph categories, it is instrumental to describe first the free symmetric monoidal category generated by a theory (Σ,), which is called a -coloured prop <cit.> (pro­duct and permutation category). This works in analogy with the single-sorted case = { c }, in which monoidal theories act as presentations for ({c}-coloured) props <cit.>.

 Let  be a finite set. A -coloured prop is a symmetric monoidal category (SMC) where the set of objects is C^⋆ and the monoidal product  on objects is word concatenation. -coloured props form a category  with morphisms the identity-on-objects symmetric monoidal functors.

Given a monoidal theory (Σ, ), one can freely construct a prop Σ , with arrows the Σ-terms quotiented by the laws of symmetric monoidal categories. Σ-terms are freely obtained by combining operations in Σ, a unit 𝕀 c→ c for each c ∈ and a symmetry σ_c,d cd→ dc for each c,d∈, by sequential (;) and parallel () composition. That means, given terms a  w_1 → w_2, b  w_2→ w_3, a'  v_1→ v_2, one constructs new terms a  b  w_1→ w_3 and a  a'  w_1 v_1 → w_2 v_2.


We shall adopt the graphical notation of string diagrams <cit.> for the arrows of Σ,. An arrow a   w_1 → w_2 is pictured as diagA.pdf. Compositions via  and  are drawn respectively as horizontal and vertical juxtaposition, that means, a  b is drawn [height=.6cm]seqcomp.pdf and a  a' is drawn [height=.8cm]parcomp.pdf. There are specific diagrams for the symmetric monoidal structure, namely idw.pdf for the identity 𝕀_w   w → w and symwu.pdf for the symmetry σ_w,u  wu → uw, for w, u ∈^⋆. These are definable from the basic identities and symmetries for colours in  using the pasting rules for  and .





The initial object in  is the -coloured prop  whose arrows w → v are permutations of w into v (thus arrows exist only when the word v is an anagram of the word w).  is freely generated by the monoidal theory (∅,).


 
For ' ⊆, the -coloured prop ' of separable Frobenius '-monoids is freely generated by the monoidal theory (', ), where ' = { Bmultc.pdf ,  Bunitc.pdf ,  Bcomultc.pdf ,  Bcounitc.pdf| c ∈' }, and quotiented by equations, for each c ∈', stating that Bmultc.pdf and Bunitc.pdf form a commutative monoid (<ref>), that Bcomultc.pdf and Bcounitc.pdf form a commutative comonoid (<ref>), and that these interact according to the Frobenius law and the separability law (<ref>).

    multcommc.pdf = Bmultc.pdf        unitlawc.pdf = idc.pdf        assocLc.pdf = assocRc.pdf
    comultcommc.pdf = Bcomultc.pdf        counitlawc.pdf = idc.pdf        coassocLc.pdf = coassocRc.pdf
    cFrobL.pdf = cFrobC.pdf = cFrobR.pdf        cFrobSepL.pdf = cFrobSepR.pdf


As mentioned, when  is a singleton, -coloured props are just called props, i.e. SMCs with objects the natural numbers where the monoidal product is addition on objects. For later use it is convenient to record the following result about the single-sorted case. It involves the prop  whose arrows n_1 → n_2 are cospans n_1fn_3gn_2 of functions between ordinals n{0,…,n-1}.

 There is an isomorphism of {c}-coloured props between {c} and . It is defined by the following mapping on the {c}-operations.

    Bmultc.pdf  ↦  cspMult.pdf    Bcomultc.pdf  ↦    cspComult.pdf
    Bunitc.pdf  ↦  cspUnit.pdf    Bcounitc.pdf  ↦  cspCounit.pdf



As outlined in the introduction, we are interested in studying non-structural equations as rewriting rules. We now define the appropriate notion of rewriting for arrows in a prop. We call it “syntactic” to emphasise that matching happens when the left-hand side of a rule is a sub-term.

 
A rewriting rule in a -coloured prop  is a pair of morphisms l, r   v_1 → v_2 in , for which we use the notation lr  v_1 → v_2. A rewriting system  is a finite set of rewriting rules. Given a,b   w_1 → w_2 in , we say that a rewrites into b via , notation a  b, if there are a_1 and a_2 yielding the following decompositions in , where lr  v_1 → v_2 is in .

    diagA.pdf = rewl.pdf        diagB.pdf = rewr.pdf
 


We are going to study syntactic rewriting in free hypergraph categories, which we now introduce together with their properties.


 An hypergraph category is an SMC  where each object x ∈ has a separable Frobenius structure, i.e., maps
multx.pdf, unitx.pdf, comultx.pdf and counitx.pdf forming a commutative monoid, a commutative comonoid and satisfying equations as in (<ref>) for each x ∈. Moreover, the Frobenius structure must be compatible with the monoidal product:

    multxtnsy.pdf = multxy.pdf        unitxtnsy.pdf = unitxy.pdf        comultxtnsy.pdf = comultxy.pdf        counitxtnsy.pdf = counitxy.pdf


The free hypergraph category over (Σ, ), notation Σ ,, is the free -coloured prop on (Σ⊎,) quotiented by equations (<ref>), (<ref>) and (<ref>) for each c ∈.

 
 

Observe that the free construction of Σ, indeed creates a Frobenius structure for each object w ∈^⋆ of the category, canonically defined in terms of the one on colours. For instance, for w = c_1 … c_n:

    multw.pdf  multiplemultsc.pdf        unitw.pdf  multipleunitsc.pdf        comultw.pdf  multiplecomultsc.pdf        counitw.pdf  multiplecounitsc.pdf


 

Fix a set  of colours with just two elements, noted  and , and a signature Σ consisting of two “colour switch” operations, gbswitch.pdf → and bgswitch.pdf →. We may construct the free hypergraph category Σ,{,} over (Σ,{,}). Here is an example of a string diagram in this category, where we use the more suggestive convention of colouring wires instead of labelling them with objects  and .

    exbipartite.pdf

We claim that Σ,{,} is the same as the category of finite directed bipartite graphs (with interfaces). This will become clear in Example <ref>, after the characterisation provided by Corollary <ref>.



We now observe that the free hypergraph category Σ, can be seen as a coproduct in . This will be useful in order to separate the component arising from Σ from the built-in Frobenius structure.

 There is an isomorphism Σ ,  + C≅Σ, of -coloured props. It extends to an isomorphism of hypergraph categories: thus Σ ,  + C is the free hypergraph category on (Σ,). 

The first part follows from how coproducts are computed in . As Σ, is presented by (Σ, ) and C by (,) quotiented by (<ref>)-(<ref>), then Σ ,  + C is presented by (Σ⊎, ) quotiented by (<ref>)-(<ref>): this is precisely the definition of Σ,. The second part holds because the isomorphism maps the Frobenius structure on c ∈ in Σ ,  + C to the Frobenius structure on c ∈ in Σ,.


The free hypergraph category has a universal property (of a pushout) in  too. Details are in the proof of Corollary <ref>, which uses this observation. We conclude by recalling that the Frobenius monoids in an hypergraph category defines a canonical compact closed structure. This also justifies the terminology “well-supported compact closed categories” originally used for hypergraph categories <cit.>. 



Hypergraph categories are (self-dual) compact closed.


It is useful to report how the compact closed structure is actually defined. For an object x of an hypergraph category , define
wccL.pdf as wccfrobL.pdf and wccR.pdf as wccfrobR.pdf. The Frobenius equation (<ref>) implies the equation for compact closure:

    snakexL.pdf = idx.pdf = snakexR.pdf.

The dual dualaL.pdf of a morphism diagax.pdf is defined as dualaR.pdf.









§ THE COMBINATORIAL INTERPRETATION


According to Definition <ref>, syntactic rewriting in free hypergraph categories happens modulo Frobenius structure. The goal of this section is to give a combinatorial description of the free hypergraph category, so that a more concrete account of the associated rewriting becomes available.

Fix a monoidal theory (Σ, ). We shall work with finite directed hypergraphs, whose hyperedges are labelled in Σ and nodes are labelled in . We shall visualise hypergraphs as follows: nodec.pdf is a node labeled

.7
with c ∈ and hyperedgeo.pdf is an hyperedge labeled with o ∈Σ, with ordered tentacles attached to the left boundary linking to sources and the ones on the right linking to targets. An example is on the right, with = { c_1, c_2} and Σ = { o_1   c_1 →ϵ , o_2   c_1 c_2 → c_1 c_1 }.

.2


    [width=4cm]exhypergraph.pdf



We now organise these structures into a category. First, consider the SMC  with objects the finite directed (unlabelled) hypergraphs and homomorphisms between them. The monoidal theory (Σ, ) itself can be seen as an object of . For instance, Σ and  as above yield the unlabelled hypergraph on the 

.3

    [width=4cm]signatureunlabeled.pdf


.7
left (where we “call” o_2 the leftmost and o_1 the rightmost hyperedge, and c_2 the leftmost and c_1 the rightmost node). The desired labelling is given formally by working in the slice category ∖ (Σ,), for which we shall use notation Σ,. This definition ensures that a Σ-operation o   w → v labels an hyperedge only when the label of its input (respectively, output) nodes forms the word w (v).


The next step is to add interfaces, formally modelled by cospans. Fix a set {x_i}_i ∈ totally ordered by . Define Σ , as the restriction of the category of cospans in Σ, to objects the discrete hypergraphs (i.e. no hyperedges) whose set of nodes is isomorphic to an initial segment of {x_i}_i ∈. This restriction ensures that Σ , is a -coloured prop. Indeed, an object of Σ , can be identified with a natural number k together with a labelling function {0,…,k-1}→, which is the same as a word in ^*. The notation Σ , stands for “Frobenius termgraphs”, following the terminology introduced for the single-sorted case <cit.>. This name will be justified by the characterisation of Theorem <ref> below.

We now define the two components of the functor that is going to interpret the syntactic definition of an hypergraph category as a combinatorial structure. The key to the approach is the second definition below, which essentially tells that the combinatorial model is able to absorb all the complexity of Frobenius structure simply in terms of nodes.



 We define a -coloured prop morphisms ·  Σ ,  + →Σ, as the copairing of the following functors:


  * · Σ , →Σ, is defined by the following mapping on operations o   c_1c_2… c_m → b_1b_2 … b_m of Σ (where c_i, b_i ∈).

    synTosemL.pdf  ·  synTosemR.pdf

The definition of hypergraph homomorphisms p and q is fixed by colour preservation.

  * · C→Σ, is defined by the following mapping on the -operations.

    Bunitc.pdf  ·  frobTosemUnit.pdf    Bcounitc.pdf  ·  frobTosemCounit.pdf
    Bmultc.pdf  ·  frobTosemMult.pdf    Bcomultc.pdf  ·  frobTosemComult.pdf

Also here the definition of the hypergraph homomorphisms is predetermined.











We now have all the ingredients to state our characterisation theorem.

 · Σ ,  + C→Σ , is an isomorphism of -coloured props. 

The proof of the theorem will be postponed to the end of the section. Let us first observe two interesting consequences.

 Σ , is the free hypergraph category on (Σ, ), i.e. Σ,≅Σ ,. 
 · C→Σ , defines an hypergraph category structure on Σ , and the isomorphism of Theorem <ref> extends to one of hypergraph categories. Then the result follows by Proposition <ref> and Theorem <ref>. 

The next corollary states that there is no `information loss' in passing from the free symmetric monoidal category to the free hypergraph category on (Σ,).
  · Σ , →Σ, is faithful. 

We use that, just as for props <cit.>, coproducts of -coloured props can be computed as certain pushouts in the category  of small SMCs. In particular, Σ ,  + in  arises as

 
    @R=20pt@C=40pt[d]_!_1[r]^-!_2   C[d]^-·
    [r]_-·Σ ,    Σ ,  + ≅Σ,

in , where the maps !_1 and !_2 are given by initiality of  in  (see Example <ref>). Intuitively, in (<ref>) Σ ,  + is built as the “disjoint union” of Σ , and  where one identifies the set of objects ^⋆ and the associated symmetric monoidal structure (the “contribution” of ).

Now, in order to prove that · is faithful, we can use a result <cit.> about amalgamation in  (which transfers to ). As all the functors in (<ref>) are identity-on-objects and !_1, !_2 are faithful, it just requires to show that !_1 and !_2 satisfy the so-called 3-for-2 property: for !_1, this means that, given h= f  g in Σ ,, if any two of f,g,h are in the image of !_1, then so is the third. This trivially holds as every arrow of  is an isomorphism. The argument for !_2 is identical. 



We come back to the free hypergraph category Σ,{,} introduced in Example <ref>. By Corollary <ref>, Σ,{,}≅Σ,{,}. In hypergraphs of Σ,{,}, hyperedges correspond to switches bgswitch.pdf or gbswitch.pdf, thus they are in fact edges (one input and one output node) and we may as well avoid drawing them in the graphical representation. Since they connect any two nodes only when these have a different colour, what we obtain are finite directed bipartite graphs. For instance, reprising (<ref>):

    exbipartite.pdf    ·    exbipartitegraph.pdf

This example shows that Theorem <ref> not only provides a combinatorial representation for algebraic structures, but conversely it is also instrumental in deriving an algebraic presentation for well-known graph-theoretic models.






























We now give a proof of the characterisation theorem.


As a preparatory step, we observe that  itself can be decomposed as a coproduct in , namely Σ_c ∈{c}. Let us suppose for simplicity that = {c,d}, so that = {c} + {d}. It will be apparent how the argument generalises. 

The prop morphism · →Σ, is analogously decomposable as the copairing ·_c,·_d {c} + {d}→Σ, of prop morphisms ·_c {c}→Σ, and ·_d {d}→Σ,, defined by restricting the clauses (<ref>) to the associated colour, either c or d.

We have thus reduced the statement to verify that Σ , satisfies the universal property of the coproduct Σ, + {c} + { d } in . 

    @R=5pt@C=45pt            [dll]_-·_d@/_8pt/[dddll]^<<<<<<β_d{d}
    Σ,[ddrr]_α[rr]^-·      Σ,@.>[dd]^γ
                [ull]_<<<<<<·_c{c}[dll]^β_c

 Given α, β_c, β_d and a -coloured prop  as in (<ref>), we need to show the existence of a unique γ making the diagram commute. Now, because all morphisms in (<ref>) are identity-on-objects, it suffices to show that any arrow of Σ , can be decomposed in an essentially unique way into an expression where all the basic constituents lie in the image of ·, ·_c or ·_d. 
 
To this aim, fix a cospan w f G g v in Σ ,, where G has set of nodes N, set of hyperedges E and labelling functions ψ  N → and χ  E →Σ. We pick an order e_1,…,e_j on the hyperedges in E and one n_1,…,n_k on the nodes in N. Let w̃iẼoṽ be the cospan defined as ⊕_1 ≤ i ≤ jχ(e_i). Intuitively, Ẽ piles up all the hyperdges of G, but disconnected from each other. w̃ and m̃ are the word concatenations of all the inputs, respectively outputs of these hyperedges. 

Similarly, we pile up all the (labeled) nodes in N, by forming the word w_N ∈^⋆ as ⊕_1 ≤ i ≤ kψ(n_i). There are obvious functions from w, v, w̃ and ṽ to w_N, mapping labelled nodes to their occurrence in w_N. All this information is now gathered in the following composition of cospans [We admit a certain degree of sloppiness in writing w_N both for an object of Σ, and for the carrier of a cospan. For w_N = {n_1, …, n_k}, these are isomorphic descriptions of the same data: in the first case it is treated as a word in ^⋆, in the second as a set of nodes with a labelling function χ { n_1, …, n_k }→. ]

    (w f  w_N id, j w_N w̃)   (w_N w̃id  i w_N Ẽid  o w_N ṽ)   (w_N ṽid, p w_N g v)

Copairing maps id, j and id, p are well-defined as  is also a coproduct in Σ,. One can compute that the result of composing (<ref>) (by pushout) is indeed isomorphic to w f g g v.

Towards a definition of γ, we need to check that every component of (<ref>) is in the image of either · or · = ·_c,·_d. The middle cospan is clearly in the image of ·, as it is the monoidal product of the identity cospan w_N id w_N id w_N with cospans in the image of some o ∈Σ. Next, we want to check that the two outmost cospans are in the image of ·_c,·_d. To this aim, we show the following claim.

 Any arrow u_1 h u_3 q u_2 of Σ, with u_1, u_2, u_3 discrete is in the image of ·_c,·_d. 

 First, find permutations π_1   u_1 → c^k d^z, π_2   u_2 → c^m d^n and π_3   u_3 → c^l d^r factorising words u_1, u_2 and u_3 respectively as cs followed by ds. We can then define restrictions of h and of q to the c-segment or the d-segment of their domain: this gives functions h_c   c^k → c^l, h_d   d^z → d^r, q_c   c^m → c^l and q_d   d^n → d^r. Observe that the codomain is restricted too, as h and q are colour-preserving maps. Putting these data together we can decompose u_1 h u_3 q u_2 as follows.

    (u_1 id  w_1 π_1 c^k  d^z)   (c^k  d^z h_c  h_d c^l  d^r q_c  q_d c^m  d^n)   (c^m  d^n π_2 u_2 id u_2)


It is now useful to recall Proposition <ref>. Observe that the bijection given therein between Frobenius structure and cospans in  is defined by the same clauses (<ref>) as · = ·_c,·_d, modulo the labelling of set elements all with c or with d. It follows that the cospan c^k h_c c^l q_c c^m is in the image of ·_c and the cospan d^z h_d d^r q_d d^n is in the image of ·_d. Thus they are both in the image of ·_c,·_d. Concerning the two outermost cospans in (<ref>), they are also in the image of ·_c,·_d, as this is a morphism of -coloured prop and thus preserves and reflects the symmetry structure. Therefore, the whole of (<ref>) is in the image of ·_c,·_d. 

Back to the main proof, thanks to the claim we have shown that the two outmost cospans of (<ref>) are in the image of ·_c,·_d. Therefore γ can be defined on w f G g v by the values of · and ·_c,·_d on its decomposition as in (<ref>). This is a correctly and uniquely defined assignment: in the construction of decompositions (<ref>) and (<ref>), the only variable parts are the different orderings that are picked for labelled nodes and for hyperedges in Ẽ, but these are immaterial since all the involved categories are symmetric monoidal.






As a consequence of the claim enclosed in the proof of Theorem <ref>, it is worth noticing that the Frobenius structure identifies the hypergraphs with no hyperedges, i.e. the sets of -labelled nodes.
 There is an isomorphism of -coloured props ≅∅,. 
As arrows of ∅, are the same thing as cospans in the slice category ∖, this corollary can be seen as a multi-sorted analogue of the well-known result reported in Proposition <ref>.



  
Double-pushout rewriting with interfaces We conclude this section by recalling double-pushout (DPO) rewriting <cit.>, that we will use to compute in Σ,. We will actually use a variation <cit.> of the standard definition: instead of just rewriting an hypergraph G, we shall rewrite an hypergraph homomorphism G  J, standing for “G with interface J”. The intuition is that this form of computation retains the information that J is how G “glues” to a bigger context. This is needed both to match the syntactic notion of rewriting (Definition <ref>) and for ensuring decidability of confluence for terminating system (Section <ref>). We formulate our definition at the level of adhesive categories <cit.>. This is the more abstract setting where DPO rewriting enjoys desirable properties (such as Church-Rosser) and where tools and algorithms for this form of rewriting are generally defined. 

 
Fix an adhesive category . A rule for double-pushout rewriting with interfaces (DPOI rule) is a span L  J  R  in .
A DPOI rewriting system  is a finite set of DPOI rules.

Given morphisms G r I and H p I in , we say that G rewrites into H via  with interface I, notation (G r I)  (H p I), if there exists a DPOI rule L  J  R in  and a cospan
J  C q I such that the following diagram commutes and the two squares are pushouts. We call L → G a match of L in G. 

    25pt@R=10pt@C=20pt
    L [d]       J [d]
    @[dl]|(.8)⌝@[dr]|(.8)⌜[l] [r]      R [d] 
    
     G      C [l] [r]      H 
         I [u]^q [ur]_p  [ul]^r

If  has an initial object 0, one can relax rewriting to act on cospans of the form 0  G r I, seen as objects with interface (G r I). In this case we write (0  G r I)  (0  H p I) for a rewriting step. 



The following makes DPOI rewriting possible in = Σ,, see Ex. <ref> below for an illustration.
 Σ , is an adhesive category. 
 
The category  of finite directed (unlabeled) hypergraphs is a presheaf category and thus adhesive <cit.>. The statement then follows because Σ , is defined as the slice category ∖ (Σ, ) and adhesive categories are closed under slice <cit.>.











§ DPOI IMPLEMENTATION OF REWRITING MODULO FROBENIUS
 

The category Σ, has an initial object 0: the hypergraph with neither nodes nor hyperedges. Therefore, as mentioned in Definition <ref>, we can equivalently think of hypergraphs with interface (G  I) as cospans 0  G  I, and meaningfully define DPOI rewriting on the morphisms with source 0 in Σ,. 

On the other hand, our semantics · maps diagrams of Σ+ to cospans with any source. Thus, in order to interpret syntactic rewriting, we need an intermediate step where we “fold” the two interfaces w_1, w_2 of a string diagram a   w_1 → w_2 into one w_1 w_2. This is formally defined, with the help of the compact closed structure on Σ+ (Proposition <ref>), by an operation ·:


    rewiringA.pdf    rewiringA2.pdf


We are now ready to formulate the correspondence theorem between syntactic rewriting in Σ+ and DPOI rewriting in Σ. 



Let lr be any rewriting rule on Σ,+. Then,

    a ⇒_lr b     iff   alrb .



On the direction from left to right, suppose that a ⇒_lr b. Thus, by definition,

    diagA.pdf = rewl.pdf        diagB.pdf = rewr.pdf.

Using the compact closed structure of Σ,+ we can put a in the following shape

    rewiringA.pdf = rewiringA2.pdf(<ref>)rewiringA3.pdf = rewiringA4.pdf

The dashed line decomposes the rightmost diagram into l  0 → v_1  v_2 followed by a diagram of type v_1 v_2 → w_1 w_2, which we name ã. With analogous reasoning,

    rewiringB.pdf = rewiringB2.pdf     meaning that    a = lã and b = rã.

Next, we introduce cospans giving semantics to the various diagrams:

    l = 0  L  v_1v_2     ã = v_1v_2  C  w_1 w_2     r = 0  R  v_1v_2 
    a = 0  G  w_1 w_2     b = 0  H  w_1 w_2.

Equation (<ref>) tells that the cospan giving semantics to a (respectively, b) is the composite of cospans giving semantics to l (respectively, r) and ã. As composition of cospans is by pushout, we obtain a double-pushout diagram as in (<ref>) with J = v_1v_2 and I = w_1w_2, meaning that alrb.











We now conclude the proof by showing the right to left direction of the statement. Suppose that alrb. Naming cospans a, b, l and r as in (<ref>), this implies by definition the existence of a pushout complement C yielding a DPOI diagram as (<ref>) with J = v_1v_2 and I = w_1w_2. Now, pick â  v_1 v_2 → w_1 w_2 such that â = v_1 v_2  C  w_1 w_2, which exists by fullness of ·. Because composition in Σ, is by pushout, the existence of such a DPOI diagram yields 

    a = (0  G  w_1 w_2) = (0  L  v_1 v_2)(v_1 v_2  C  w_1 w_2) =   lâ
    b = (0  H  w_1 w_2) = (0  R  v_1 v_2)(v_1 v_2  C  w_1 w_2) =   râ.

Because · is faithful, (<ref>) yields decompositions a = lâ and b = râ also on the syntactic side. This allows for a rewriting step a lr b as below, where the dashed lines show how the syntactic matching (cf. the shape (<ref>)) is performed.

    diagA.pdf = secondproof1.pdf = secondproof2.pdflrsecondproof3.pdf = secondproof4.pdf = diagB.pdf


 The syntactic rewriting step (<ref>) takes place in Σ,{c,d} + {c,d} where Σ = { o_1   c → cd, o_2   dd → c}. It maps via Theorem <ref> to the following DPOI rewriting step in Σ,{c,d}. We use numbers 1,2,3 to disambiguate the “folding” of the rule interfaces.

    @C=15pt@R=10ptexGrapRew1.pdf[d]    @[dl]|(.55)⌝exGrapRew2[d]_[l] [r]
    @[dr]|(.55)⌜   exGrapRew3.pdf[d] 
    exGrapRew4.pdf   [l] exGrapRew5.pdf[r]    exGrapRew6.pdf
       [ul] exGrapRew7.pdf[u] [ur]




§ DECIDABILITY OF CONFLUENCE


This section verifies that the form of rewriting crystallised by Theorem <ref> enjoys the Knuth-Bendix property. Echoing the case of term rewriting, we use this terminology to mean that the confluence problem is reducible to critical pair analysis and both are decidable for terminating rewriting systems.

To this aim, we instantiate to our setting the results of <cit.>. There the author and collaborators showed that DPOI rewriting enjoys the aforementioned Knuth-Bendix property. Interfaces play a crucial role here, as Plump showed that for DPO rewriting (without interfaces) confluence is undecidable <cit.>.



Fix an adhesive category and DPOI rules L_1  K_1  R_1 and L_2  K_2  R_2. Consider the following two derivations with common source S.

    @R=15pt
        R_1 [d]    [l] K_1 [d] [r]     L_1 @[dr]|(.8)⌜      @/^5pt/[dr]^f_1      @/_5pt/[dl]_f_2@[dl]|(.8)      ⌝ L_2    [l] K_2 [d] [r]     R_2 [d] 
    
        H_1     [l] C_1 [rr]        S        [ll] C_2  [r]     H_2 
             @/^/[ull] J @[u]|(†)@/_/[urr]

We say that (H_1J)  (S J )  (H_2J) is a critical pair if (i) [f_1,f_2]  L_1 + L_2 → S is epi and (ii) (†) is a pullback. 
It is joinable if there exists (W  J) such that (H_1  J) ^⋆ (W   J) ^⋆  (H_2  J).

Intuitively, condition (i) ensures that a critical pair S is not bigger than L_1+L_2 and condition (ii) says that J is the largest interface that allows both rewriting steps (J is the “intersection” of C_1 and C_2). 


Suppose that  satisfies the following assumptions: (1) it has an epi-mono factorisation system; (2) it has binary coproducts, pushouts and pullbacks; (3) it is adhesive (4) with all the pushouts stable under pullbacks. Then DPOI rewriting in  has the Knuth-Bendix property for computable rewriting systems. 


 In the statement of Proposition <ref>, computability refers to the conditions that (i) pullbacks are computable, (ii) for every pair of DPOI rules L_1  K_1  R_1 and L_2  K_2  R_2 the set of quotients of L_1 + L_2 is finite and computable, and (iii) for all G  J one can compute every H  I such that (G  I)  (H  I). 
In particular, (i)-(ii) ensure that the set of critical pairs is finite and computable, and (iii) ensures that any rewriting step is also computable— see <cit.> for the full technical details. Caveats on computability are intended to single out those structures where it is reasonable to apply the DPOI mechanism, as opposed to e.g. systems with infinitely many critical pairs.


 The one of Definition <ref> is sometimes called a “pre-critical” pair, as no condition ensures that L_1 and L_2 actually overlap in S. This distinction can be formulated abstractly for DPO in adhesive categories when rules are (left- or right-) linear, see <cit.> for an overview. However, Proposition <ref> works with arbitrary (non-linear) rules, cf. <cit.>, whence the more general definition. Non-overlapping pairs can be singled out in our category of interest, Σ,, and discarded for confluence testing as they are always joinable— also, their set is finite, because any DPOI systems is computable in Σ,. 



 DPOI rewriting in Σ, has the Knuth-Bendix property. 


 Given that DPOI rewriting in Σ, is defined in terms of DPOI rewriting in Σ,, it suffices to check the statement in Σ,. We use Proposition <ref>: assumptions (1)-(4) hold in any presheaf category and are closed under slice. Therefore, as Σ, is defined as the slice of a presheaf category (cf. proof of Proposition <ref>), it satisfies (1)-(4). It remains to check that any DPOI rewriting system in Σ, is computable: the relevant observations are that in Σ, (i) pushouts and pushout complements are effectively computable and (ii) for any two rules there are only finitely many hypergraphs that may witness a critical pair as defined in Definition <ref>.










We would now wish to transfer Theorem <ref> to syntactic rewriting in Σ,+. This requires some extra care. In order to determine if a rewriting system  on Σ,+ is confluent, by Theorem <ref> and <ref> it is enough that all the critical pairs in the DPOI system  are joinable. However, for full decidability we also need to make sure that the converse holds: if one critical pair in  is not joinable, then  should not be confluent. To ensure this, we need to verify that all the critical pairs of ℛ lay in the image of ·. This amounts to check that they all have discrete interfaces.



 Consider a critical pair in Σ, as in (<ref>). 
If both K_1 and K_2 are discrete hypergraphs, so is the interface J.




For i=1,2, since K_i is discrete, the hyperedges of C_i are exactly those of G_i that are not in f_i(L_i).
Since [f_1,f_2] L_1+L_2 → S is epi, all the hyperedges of G are either in f_1(L_1) or f_2(L_2). Therefore, J cannot contain any hyperedge.


By definition of ·, for every rule L  K  R in , K is discrete. Therefore we can finally transfer the decidability result to the context of Σ,+.



 Syntactic rewriting in Σ,+ has the Knuth-Bendix property. 



 Since DPOI rewriting in Σ, has the Knuth-Bendix property (Theorem <ref>) and the two forms of rewriting coincide (Theorem <ref>), as discussed above it suffices to check that for a given critical pair in Σ,, say witnessed by (SJ ), there exists a in Σ+, such that a = 0  SJ. As · is full on Σ,, it suffices that J is discrete, which is true by Lemma <ref>.[3]





§ CONCLUSIONS


We described a sound and complete interpretation of string diagram rewriting in hypergraph categories as double-pushout rewriting of hypergraphs, and showed that it enjoys decidability of confluence for terminating rewriting systems. A chief advantage of this approach is that the challenge posed by performing matching modulo Frobenius equations disappears in the combinatorial model. This becomes important when studying axiomatisations with multiple Frobenius monoids: these can now be all seen as structural equations and baked into the combinatorial model, thus confining questions of confluence and termination to the non-Frobenius axioms. This application of our theory, which we plan to explore in future work, was the main reason to generalise the framework of <cit.>, which is only able to absorb a single Frobenius structure. Another promising direction is the algebraic study of bipartite graphs (Example <ref>), which may be relevant for analysing diagrammatic languages, like biological metabolic networks <cit.>, based on these structures.


Acknowledgements Thanks to Filippo Bonchi, Brendan Fong, Fabio Gadducci, Aleks Kissinger, the GAM participants and referees for useful comments and discussion on the topics of this paper.



eptcs



