A two-coloured flow graph over two signatures V and C with the same sorts is a single-coloured flow graph over V except that:
R |
R |
We can now replay the same proof of soundness and completeness as in the finite products case. In each case, the proof of the theorems is so similar to that in the finite products case that we elide it.
Let Graph(V,C) be the category of acyclic flow graphs over (V,C), viewed up to bisimulation.
Proposition (Flow graphs form a strict symmetric monoidal category).
Define Term(V,C) as the free strict symmetric monoidal category over C which has Term(V) as a sub smc with the same objects.
f,g | ::= | f | |
| | f ; g | ||
| | f g | ||
| | c |
If terms can be proved equal using the axioms for an smc with a sub smc Term(V), we shall write f = g.
Proposition (Soundness). If f = g then [[f]] [[g]].
Proposition (Expressivity). For any graph G, there is a term f such that [[f]] G.
A term is in normal form (ranged over by n) iff it is of the form:
n | ::= | |
| | ||
| | ||
| |
Proposition (Cancellation of permutations). For any:
Proposition (Cancellation of val nodes). For any:
Proposition (Cancellation of central nodes). For any:
Proposition (Completeness). If [[f]] [[g]] then f = g.
Proposition (Initiality). Graph(V,C) is the initial strict symmetric monoidal category over C with Graph(V) as a sub smc with the same objects.