{'fraction_non_alphanumeric': 0.0446269037692504, 'fraction_numerical': 0.004254232961796988, 'mean_word_length': 4.093607800650054, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Encoding !-tensors as !-graphs with neighbourhood orders

Diagrammatic reasoning using string diagrams provides an intuitive language for reasoning about morphisms in a symmetric monoidal category. To allow working with infinite families of string diagrams, !-graphs were introduced as a method to mark repeated structure inside a diagram. This led to !-graphs being implemented in the diagrammatic proof assistant Quantomatic. Having a partially automated program for rewriting diagrams has proven very useful, but being based on !-graphs, only commutative theories are allowed. An enriched abstract tensor notation, called !-tensors, has been used to formalise the notion of !-boxes in non-commutative structures. This work-in-progress paper presents a method to encode !-tensors as !-graphs with some additional structure. This will allow us to leverage the existing code from Quantomatic and quickly provide various tools for non-commutative diagrammatic reasoning.


Motivation
Reasoning using diagrams can often be simpler and more intuitive than using a term-based mathematical syntax [7]. There has recently been a shift toward using graphical calculi in a number of different fields. The String graph formalism is one which has far-reaching applications in areas including categorical quantum mechanics [4,3,5], computational linguistics [8] and control theory [2,1]. String graphs are a formalism for typed directed graphs, with the idea of edges replaced by (directed) wires. Unlike edges, wires do not need to have vertices at the ends. Those without starting vertices can be considered inputs and those without end vertices can be considered outputs. Wires also allow for identity edges (neither end connected to a node) or loops (a wire connected to itself). String graphs achieve this by having wirevertices along a wire, so that a loop for example could be two wire-vertices a and b with edges a → b and b → a. String graphs can be combined by plugging outputs from one in to inputs of another.
A diagrammatic theory is a set of equations between string diagrams on some set of generating morphisms. For example, a (commutative) associative multiplication operation with a unit can be described by the string diagram equations: = , = An equation, G = H, between string graphs can be used in a form of rewriting where a subgraph matching G can be replaced by H.

= = ⇒
Many theories allow for nodes to have variable arity edges. For example, the multiplication and unit above can be replaced by a single operation taking the product of an arbitrary number of inputs (order unimportant), along with two diagram equations.

=
This extension, while powerful, loses the mathematical rigour from the previous formalism (as can be seen from the use of ellipses). To return to a rigorous semantics, !-boxes (pronounced bang-boxes) were introduced in [6] to designate (by enclosing in a blue box) parts of a diagram which are allowed to be repeated. Adding !-boxes to string graphs results in the notion of a !-graph. This was formalised in [10,15] and has many applications, particularly in categorical quantum mechanics. Note that a !-graph represents a family of string graphs which can be recovered by two !-box operations, Kill B and Exp B . Kill B is the operation removing the !-box B and all contents from a !-graph. Exp B is the operation which creates a new copy of the contents of B attached to the same nodes. Equations between !-graphs have the restriction that the !-graphs have the same !-boxes with the same nesting (!-boxes can contain other !-boxes). Hence the ellipsis equation in our example theory describes the following set: As !-graphs get applied to more complicated systems, rewriting by hand becomes difficult. This problem was solved by the introduction of Quantomatic [11], an automated theorem prover which allows rewriting of !-graphs using substitution. Quantomatic encompasses many tools for automated reasoning with string diagrams and has the ability to output graphical derivations directly to LaTeX.

Figure 1: Example derivation in Quantomatic
One major drawback of both !-graphs and Quantomatic is that they are only designed to allow theories in which all nodes are commutative on inputs and outputs. This not only restricts the types of theory we can work with but more subtly, it rules out the option to definitionally extend a theory. i.e. defining new nodes (possibly inductively) as diagrams of other nodes. This is important if we want to rigorously replace finite arity nodes with their more intuitive arbitrary arity counterparts.
Since graphs inherently lack any notion of order on the edges surrounding a node, a more logical choice for representing non-commutative systems is a tensor notation in which edges are listed (in order) in a subscript. This tensor syntax was suggested in [9] and then extended in [12] to !-tensors which use an enriched version of Penrose's abstract tensor notation [16] allowing non-commutative nodes and !-boxes. Here nodes are of the form φ e where φ is the type and e is called the edgeterm (describes order of edges). Nodes are enclosed in [_] B to represent that they are inside a !-box named B. Edgeterms contain edges outâ and edges inb where a and b are the names of the edges. Ifâ andǎ appear in a !-tensor it represents an edge between their nodes. In the edgeterms anything inside [_ B is an edge entering B which should be expanded clockwise during Exp B and _] B represents edges with anticlockwise expansion.
While it would be possible to write new automation tools based on term rewriting in the !-tensor formalism, this would require rebuilding the features already present in [11] from scratch. Instead we wish to leverage this pre-existing code but extend it to work with the logic of non-commutative theories as formalised in [13], by adding edgeterms to !-graphs. This paper shows work in progress demonstrating how we can fully encode !-tensors as !-graphs with added data. For the remainder of this section we recall the definitions of string graphs and !-graphs as defined in [15].

String graphs as typed graphs
The standard definition of a graph in mathematics is not powerful enough for our purposes. As can be seen from the string graphs in Section 1.1 our vertices need to be labelled (as generator types or wirevertices). There should also be some restrictions as to which vertex types edges can connect. We achieve this using a typegraph, where every vertex gets mapped to a type. Definition 1.1. A graph G along with a graph morphism τ : G → G is said to be a G -typed graph. We refer to the set O as the objects, the set M as the morphisms and dom and cod assign the domain and codomain of each morphism allowing edges to be tagged as single (•) or variable (∞) arity.
• one ∞-edge from X to f for each (X, ∞) in dom( f ), and • one ∞-edge from f to X for each (X, ∞) in cod( f ).
For example, the compressed monoidal signature T with the two morphisms f : If a graph G is G T -typed then we write W (G) for the wire-vertices (those mapped into O) and N(G) for the node-vertices (those mapped into M). •-tagged edges represent edges of fixed (single) arity whereas ∞-tagged edges represent edges of variable arity.
is called a string graph if τ is arity-matching (a bijection between the •-edge neighbourhoods of N and τ(N), for each N ∈ N(G)) and each wire-vertex in G has at most one incoming edge and at most one outgoing edge.
The notion of a string graph requires node vertices to be connected by chains of wire vertices which we refer to as wires. Wire points with no incoming edge represent an input to the graph and wire points with no outgoing edge represent outputs. We refer to the input vertices and output vertices together as the boundary. The set of wire-vertices in a wire are referred to as the interior of the wire.
Remark 1.5. The edges around a node-vertex in a string graph are either •-tagged, which means they are single arity; or they are ∞-tagged meaning there could be many copies made. This is important when we transition to !-graphs where we need to be careful not to copy single arity edges.

!-Graphs
!-boxes denote subsections of a graph which can be repeated many times. We represent a !-box B as a node (of the new type !) with an edge to each vertex contained in B. Definition 1.6. A subgraph O of a string graph G is said to be open if it is not adjacent to any wirevertices or incident to any fixed-arity edges.
Openness (as described in [15]) encapsulates the property of being able to repeat that part of a graph an arbitrary number of times. It ensures adjacent edges are copied with nodes; fixed arity edges are not copied without the adjacent node; and that wires cannot be partially inside a !-box (to avoid wire splitting). Definition 1.7. Given a compressed monoidal signature T , the derived compressed !-typegraph G T ! is G T with the addition of a vertex ! along with edges from ! to every vertex (including itself).
Our previous example of the compressed monoidal signature T with morphisms f : for the box-vertices in G (those mapped to !) and U(G) for the full subgraph of G with all vertices except !(G). Given B ∈!(G) let C(B) be the full subgraph of G with nodes which have edges from B. So C(B) represents the contents of a !-box B. We use this notation in the !-graph conditions to ensure !-boxes are well-behaved under !-box operations.
As an example, the theory described in Section 1.1 has !-typegraph and !-graph rules as follows:

!-Graphs with simple overlap and ordered neighbourhoods
Given a compact closed signature Σ we wish to encode the !-tensors of T Σ as !-graphs with some additional data. However, !-graphs allow for two or more non-nested !-boxes to share nodes, which is not permitted with !-tensors. In this section we define a restricted set of !-graphs and the additional structure recording non-commutativity.

Simple overlap
We must now add the restriction to rule out !-graphs with overlap on nodes, we do this by introducing the idea of simple overlap of !-boxes.
Definition 2.1. Given a pair of non-nested !-boxes B and B , we say they overlap simply if C(B) ∩C(B ) consists of only the interior of zero or more wires, where at least one endpoint is a node-vertex and any node-vertex endpoints are in either C(B) or C(B ).
Definition 2.2. A !-graph where any two non-nested !-boxes overlap simply is called a !-graph with simple overlap.
Compare this definition to !-graphs with trivial overlap (BGTO) which were first defined in [14] where it was shown that they can be encoded using a context-free grammar. The difference here is that we allow non-nested overlap at a boundary rather than just between two node-vertices.
The first two !-graphs have only simple overlap (though the second is non-trivial) the final two have non-simple overlap.

Adding orders to neighbourhoods
We now only need to describe the additional data to keep track of edge orders. For this we need the notion of an edgeterm which was originally described in [12]. Edgeterms list, in clockwise order, the edges (inǎ or outâ) around a node grouping those which expand clockwise under !-box B inside [_ B and those which expand anticlockwise inside _] B . For examples see (1) and [12]. Definition 2.3. The set of edgeterms T E over the edge names E and !-box names B is defined inductively as follows: Two edgeterms are equivalent if one can be transformed into the other by: Definition 2.4. Given a !-graph with simple overlap G, a neighbourhood order on G is a function nhd : • nhd(N) is an edgeterm with input edge names {w ∈ W (G) : w → N} and output edge names {w ∈ W (G) : N → w}, • The !-boxes with edges to a ∈ nhd(N) but not to N are precisely those containing a in nhd(N) (ordered by nesting order).
We define three !-box operations: Kill B removes B and its contents; Drop B removes B leaving its contents; and Copy B add a new copy of B and its contents. The operation Exp B can be applied using Copy B and then dropping the new !-box. Definition 2.5. For Op B any !-box operation, Op B (G, nhd) := (Op B (G), Op B • nhd). Where our three !-box operations are applied to !-graphs by: • Copy B (G) is defined by a pushout of inclusions: and Op B is applied to an edgeterm in the following trivial cases: Recall the definition of a !-tensor expression and equivalence of !-tensors from [12]. Definition 3.2. The set of all !-tensor expressions T Σ for a signature Σ is defined recursively as: Where E is a set of possible edge names and B is a set of possible !-box names. Subject to the conditions (F1)ǎ andâ must occur at most once for each edge name a and (F2) [. . .] A must occur at most once for each !-box name A, as well as some consistency conditions (C1)-(C3) for !-boxes [12]. Definition 3.3. Two !-tensor expressions G and H are considered equivalent, G ≡ H, if one can be obtained from the other by replacing bound names and/or applying one or more of the following enforced identities: where for the last two identitiesb andb are free in G and H respectively. Note Ins is inserting the identity wires inside the appropriate !-box B such that the edge b is well defined. The !-tensor formalism avoids the need to name nodes, but we will need to assign them with unique names if we want to convert to !-graphs. We do this using an indexing set. Say G is a !-tensor and let J be a set indexing the nodes (subexpressions of the form φ e , 1bǎ or 1) of G, write N j for the node corresponding to j ∈ J. In converting to a !-graph, the node N j can be labelled j.
We can define a function I taking !-tensors to what we will prove to be !-graphs with simple overlap and neighbourhood orders: Definition 3.5. I taking !-tensor expressions to !-graphs with neighbourhood orders is defined recursively: • So, for example, from the tensor expression if we index the nodes from left to right using {1, 2, 3, 4} then we get the following after I : Going through the recursive definition these combine to the !-graph we would expect:

I is Well-Behaved
We now check I behaves as desired so we can use this mapping to encode !-tensors in Quantomatic.
Theorem 3.6. Given G ∈ T Σ , I (G) is a G I (Σ)! -typed !-graph with simple overlap and a neighbourhood order.
Proof. Let J index the nodes in G. Hence it is reflexive, transitive and antisymmetric (ensuring 'child of' is cycle-free). BG3. Take B ∈!(G) and write X for U(C(B)), so we need to show that X is an open subgraph of U(G). We first show that any wire-vertex adjacent to a vertex in X is in X. From the definition of I , the only time an edge is added from a box-vertex to a node-vertex j, there are also edges added to each neighbour of j. Any two adjacent wire-vertices must come from Incident edges can only come from node-vertices not in X with adjacent wire-vertices in X. Hence, the wire comes from a directed edge with B in its edge context which means it is ∞-tagged in the typegraph. • Next we check that any overlap of non-nested !-boxes B, B is simple. Suppose j is a node-vertex such that B → j and B → j. From the definition of I we see that B and B must appear in the node context of N j and so one is nested inside the other. This contradiction proves that C(B) ∩C(B ) contains only wire vertices Suppose a is a wire-vertex such that B → a and B → a. If a is adjacent to another wire-vertex b then this edge must have come from 1bǎ or 1âb so a and b are nested inside the same !-boxes. Hence the intersection C(B) ∩C(B ) contains only the interiors of zero or more wires.
Suppose both endpoints are wire-vertices. Hence the edges have come from identity wires 1bǎ which must have B and B in their node context which would require them to be nested.
Suppose a wire-vertex a ∈ C(B) ∩C(B ) is adjacent to the node-vertex j. If j was not in C(B) nor C(B ) then both B and B must occur in the edge context of a and hence would be nested. We conclude that j must occur in exactly one of C(B) or C(B ).
• Finally we wish to check that nhd is a neighbourhood order on I (G). For j ∈ N(I (G)) the incoming edges a to j come from inputsǎ and the outgoing edges b come from outputsb as required. Also, for the node N j = φ e , !-boxes with edges to a ∈ ectx e but not to j are exactly those which appear in ectx e (a) = ectx nhd(φ ) (a).
Hence I takes a !-tensor expression and returns a correctly typed !-graph with a neighbourhood order. By the following theorem, the definition of I can be lifted from specific !-tensor expressions to !-tensors (equivalence classes of !-tensor expressions). Proof. We prove first that all !-tensor equivalences from Definitions 2.3 and 3.3 are preserved through I . In both formalisms bound variables can be renamed freely, so we will not worry about names here.
• Since edgeterms are copied directly from !-tensors to !-graphs, the edgeterm equivalences are still preserved. The associativity, commutativity and identity equivalences on !-tensor expressions have no affect on the graphical formalism so these are also preserved. The only thing left to check are the two equivalences involving inserting identity wires 1bǎ. These two conditions come down to wire homeomorphism in the !-graph framework. First we are given thatb exists in G and (for some !-box B) we look at Ins B 1bǎ (G) under I . This becomes a graph with edges a → b → x for some x and since a and b are both wire-vertices this is wire homeomorphic to G[b →ǎ]. The other case is similar but with arrows reversed.
• For the other direction suppose I (G) and I (H) differ only by a single wire homeomorphism, so there exist wire-vertices a, b and a vertex c in I (G) with a → b → c, and I (H) is I (G) but with a → b → c replaced with a → c. From the definition of I we see that there exists some G and !-box B such that G = Ins B 1bǎ (G ) (this is the only way two wire vertices can be connected) and alsob must exist in G. H must be the same as G except the edgeb is replaced by the edgeǎ.
We have shown I is injective on !-tensors and hence is a bijection onto its image. We can hence take any !-tensor G and work with it in Quantomatic in the form of I (G). To work as an encoding we would hope that !-box operations are equivalent in each formalism. Applying the !-box operation Op B to I (G) and then returning to the !-tensor formalism should result in a !-tensor equivalent to Op B (G). By the previous theorem we need only check that Op B •I = I • Op B and it then follows that • X is a G I (Σ)! -typed !-graph • X has simple overlap • nhd is a neighbourhood order on X Related to this, we would like to explore the differences between simple overlap and the stricter property of trivial overlap of !-boxes [14].
Matching (finding occurrences of one !-graph inside another) and substitution (replacing matches with equivalent graphs) are the key parts of diagrammatic reasoning with !-graphs. Matching a string graph G with a string graph K means finding a monomorphism from G in to K showing that G is isomorphic to a subgraph of K. For example, in a commutative theory the following is a string graph matching: This may not be the case if we are working with non-commutative nodes. If the top node-vertex in G has edges ordered ab and the top node-vertex in K has edges ordered yx then we can not find a matching. This can be seen from their !-tensor equivalents: b Hence we hope to define a matching from (G, nhd G ) to (K, nhd K ) to be a !-graph matching i : G → K satisfying i(nhd G (x)) = nhd K (i(x)) ∀x ∈ N(G). This is currently being looked into by the author, along with checking that substitution works without any changes. Once matching and substitution are formalised we can start comparing the differences between rewriting using substitution in !-graphs with neighbourhood orders and !-logic as defined in [13]. Ideally we would like to demonstrate that any case of proof by substitution of !-graphs (with neighbourhood order) can be shown in !-logic for !-tensors and conversely that each rule in !-logic can be implemented using substitution.

Implementation
The key contribution of this paper is to demonstrate that !-tensors could be quickly implemented in a program such as Quantomatic by adding neighbourhood order data to node vertices. Hence an obvious piece of further work would be to actually implement this in Quantomatic. There are three key areas to work on here. First is to code the new neighbourhood data on the !-graph datatype. Secondly we should update the matching and substitution algorithms to respect neighbourhood orders. Finally the user needs to be able to interact with !-graphs in a new way allowing neighbourhood orders to be chosen.
We add neighbourhood orders by recursively defining an edgeterm datatype (using the set of edge and !-box names) and then adding a node-vertex indexed table of edgeterms to the !-graph datatype. Code can be written to enforce the restrictions of Definition 2.4 whenever a !-graph is updated. The functions acting on !-graphs can then be extended to also work on the individual edgeterms. For example !-box operations should be defined to act on edgeterms as described in Definition 2.5.
Once the theory has been checked, the matching and substitution algorithms can be updated to test orders on neighbourhoods are preserved. A naive approach to matching would be to look for all matches ignoring edgeterms and then to filter out those in which edgeterms do not match up. This would be easy to implement but not very efficient. More work is needed to find a better method, checking edgeterms as the matching algorithm searches. As for substitution, the requirement that two !-tensors in a !-tensor equation have compatible boundaries should make sure that substitution does not create any issues.
We present a planned graphical user interface for !-tensors in Quantomatic in Appendix A.
Since non-commutativity is added to each node-vertex individually it may be possible for Quantomatic to have commutative and non-commutative nodes interacting in one diagram. This is something which needs to be explored further.

A Graphical user interface
Implementing the gui could require a large amount of work. The current method for drawing edges simply draws a line directly between nodes. This will need to be changed for non-commutative nodes where it becomes important where edges enter/leave a node. New edges will need to be curves defined by their source and target nodes and angles. We will add handles to each edge controlling which direction the edge should go. Figure 2 demonstrates what this may look like. We envisage Quantomatic choosing the angles initially and only letting the user drag one edge handle over another edge to reorder them. If the user wished to have more control, double clicking the handle would allow them to control the angle exactly. The user should also be able to choose the angle of the tick.  Figure 3 demonstrates the second major interface modification. We need to draw and let the user interact with arcs over edges entering a !-box. Whenever the user draws an edge between a noncommutative node and a !-box, Quantomatic will automatically add an arc over the edge (grouping multiple edges if possible). To change the arcs the user should be able to click on any part of an arc and drag. This would start a new arc containing every edge the user drags over in the direction of dragging. Hence arcs over multiple edges can be split apart by drawing each single arc in its required direction. Split/order arc Add an edge Swap edges