The graphs we consider in this paper are finite edge-labelled, node labelled graphs where the incoming and outgoing edges to each node are ordered. We also impose a type discipline to ensure that the edge and node labels match.

A generator for such a graph is:

• A set of sorts (ranged over by X, Y, Z).

• A set of constructors (ranged over by c, d).

• For each constructor, a source and target list of sorts, written c : X₁,...,X_m Y₁,...,Y_n.

This is the usual notion of a generator for a term algebra, except that we are allowing constructors to have multiple result sorts, since we will be generating syntax graphs rather than syntax trees.

A flow graph G for a given generator is:

• A finite set of edges (ranged over by E).

• A finite set of nodes (ranged over by N).

• A list of incoming edges and a list of outgoing edges, written G : E₁,...,E_m E'₁,...,E'_n.

• For each edge, a label sort, written E : X.

• For each node, a label constructor, written N : c.

• For each node, a list of incoming edges and a list of outgoing edges, written N : E₁,...,E_m E'₁,...,E'_n, such that E_i : X_i, E'_i : X'_i, N : c and c : X₁,...,X_m X'₁,...,X'_n.

• Each edge occurs exactly once either as an incoming edge of the graph, or an outgoing edge of a node.
• Each edge occurs exactly once either as an outgoing edge of the graph, or an incoming edge of a node.

A morphism F between flow graphs G and G' is:

• A map from the edges of G to the edges of G'.

• A map from the nodes of G to the nodes of G'.

• The maps respect labels, incoming edges and outgoing edges.

Acyclic flow graphs over a given generator form a category where:

• Objects are lists of sorts X₁,...,X_n.

• Morphisms from X₁,...,X_m to Y₁,...,Y_n are acyclic graphs G : E₁,...,E_m E'₁,...,E'_n such that E_i : X_i, and E'_i : X'_i. We view graphs up to graph isomorphism.

(If we wanted to be completely formal here, we would define this to be a bicategory, and make the use of isomorphisms explicit, however we leave such a construction to the interested reader.)

We have already seen how such graphs form a symmetric monoidal category. We shall now show that this is the free symmetric monoidal category over a set of generators, by showing that the smc axioms are sound and complete for acyclic flow graphs.

We can construct the term algebra for the free smc over a generator as having vectors of sorts for objects, and morphisms given by the grammar (together with the familiar graphical interpretation):

f,g	::=	idX
	|	f ; g
	|	f g
	|	symmX Y
	|	c

together with the obvious typings. We shall write f = g if f and g are provably equal using the smc axioms. We shall write [[f]] for the interpretation of f as an acyclic flow graph.

We can now show that acyclic flow graphs are the free smc over a generator, by showing that the smc axioms are sound and complete for the graph semantics of a term. As usual, soundness is routine, but completeness requires a normal form result.

Proposition (Soundness). If f = g then [[f]] = [[g]].

Proof. Inspection of each of the smc axioms shows that they are all graph isomorphisms.

We can now lead up to the definition of the normal form. We shall first show completeness for terms without constructors, which we shall call permutations, ranged over by p.

Proposition (Normalization of permutations). For any permutation p : X₁,X,X₂ Y we can find Y₁,X,Y₂ = Y and q : X₁,X₂ Y₁,Y₂ such that:

=

Proof.

From this we can show completeness of the proof system for permutations.

Proposition (Completeness for permutations). If [[p]] = [[q]] then p = q.

Proof. An induction on the type of p and q.

• If p, q : Y then show by induction on p that p = id, similarly for q, and so p = q.

• If p, q : X,X Y then by the above we can normalize p: = and similarly for q. Since [[p]] = [[q]], we have [[p1]] = [[q1]] so by induction p1 = q1 and hence p = q.

For any term f such that [[f]] = [[p ; g]] we can find f' such that f = p ; f' and [[f']] = [[g]].

Proof.

A vine is a term of the form:

Proposition. For any term f there is a vine g such that f = g.

Proof. An induction on f.

Proposition (Cancellation of nodes). For any term f such that [[f]] = [[c id ; g]] we can find f' such that f = c id ; f' and [[f']] = [[g]].

Proof.

Proposition (Completeness). If [[f]] = [[g]] then f = g.

Proof. Find the vine equal to g, and then cancel permutations and nodes iteratively to prove f = g.