# Completeness proof: partial traced cartesian categories

Given a strict symmetric monoidal category C: with a full subcategory (not necessarily symmetric monoidal) TC:

U : TC C

a partial trace is a natural transformation:

TrX Y A : C[X U(A), Y U(A)] C[X, Y]

satisfying certain axioms (given below, since they are much simpler to present graphically than equationally).

As an example, let TCpo be the full subcategory of Cpo where all of the objects have a least element. Then TCpo Cpo has a partial trace given by fixed points.

As another example, given a signature V where a subset of the sorts are define a cyclic single-coloured flow graph to be traceable iff any cyclic path goes through at least one edge labelled with a traceable sort. Taking C to be the category of traceable graphs up to bisimulation, and TC to be the full subcategory where the objects are traceable sorts, we have a partial trace given by forming a feedback loop:

Note that in order to allow `black holes':

we have to relax the condition that all edges have a unique source, and allow traceable edges to have at most one source. Then the above black hole is a graph with one outgoing edge with no source.

We shall provide a different axiomatization of traces than that provided by Joyal, Street and Verity, but we shall show below that in the case when C and TC are the same category, we recover their definition. Note that these axioms are all graph isomorphisms, and indeed are a complete axiomatization for graph isomorphism.

Naturality in X (for f : X X and g : X U(A) Y U(A) in C):

| = |
f; TrX Y A (g) | = | TrX Y A (f idU(A); g)

Naturality in Y (for f : Y Y and g : X U(A) Y U(A) in C):

| = |
TrX Y A (g); f | = | TrX Y A (g; f idU(A))

Yanking:

| = |
TrU(A) U(A) A (symmU(A) U(A)) | = | idU(A)

Symmetry sliding (for f : X U(A) U(B) Y U(B) U(A)):

| = |
TrX Y A (Tr(X U(A)) (Y U(A)) B
(f; (idY symmU(B) U(A)))
| = |
TrX Y B (Tr(X U(B)) (Y U(B)) A
((idX symmU(B) U(A)); f)

Strength (for f : V W and g : X U(A) Y U(A) in C):

| = |
f TrX Y A (g) | = | Tr(V X) (W Y) A (f g)

For those readers familiar with Joyal, Street and Verity's axiomatization of a trace, the above axioms are obviously derivable from theirs. Moreover, the following lemmas show that we can derive their axiomatization, so in the case where TC and C coincide, our axiomatization is the same as theirs.

Proposition (Parameterized dinaturality) (for f : Z U(B) U(A) and g : X U(A) Y U(B) in C):

| = |
Tr(X Z) Y A ((idX symmZ U(A));
(g idZ); (idY (symmU(B) Z); f)))
| = | Tr(X Z) Y B ((idX f); g)

Proof.

Corollary (Dinaturality) (for f : U(B) U(A) and g : X U(A) Y U(B) in C):

| = |
TrX Y A (g; (idY f)) | = | TrX Y B ((idX f); g)

Proof. Let Z be I in the above.

Proposition (Trace respects unit) (for f : I U(A) and g : X U(A) Y in C):

| = |
TrX Y A (g; idY f) | = | (idX f); g

Proof.

Proposition (Trace respects tensor) (for f : U(B) U(C) U(A) and g : X U(A) Y U(B) U(C) in C):

| = |
TrX Y A (g; idY f) | = | TrX Y C (TrX Y B ((idX f); g))

Proof.

Proposition (Trace respects double symmetry) (for f : V W and g : X U(A) Y U(A) in C):

| = |
TrX Y A (g) f | = | Tr(X V) (Y W) A ((idX symmV U(A)); (g f); (idY symmU(A) W))

Proof.

We show below that the axioms for a partially traced monoidal category are complete for graphs up to graph isomorphism. But as we discussed before, graph isomorphism is not a sound model for categories with finite products, and we chose bisimulation as the appropriate equivalence on graphs. In order to provide a complete axiomatization for cyclic graphs up to bisimulation, we need an additional property. In a partially traced monoidal category where the monoid is product, the trace is uniform wrt shuffles iff, for any shuffle s:
If: =
then: =
A partially traced cartesian category is a partially traced monoidal category where the monoid is product and the trace is uniform wrt shuffles. We shall show below that the axioms for a partially traced cartesian category are sound and complete for traceable cyclic graphs up to bisimulation.

We can now replay the same proof of soundness and completeness as in the finite products case. In some cases, the proof of the theorems is so similar to that in the finite products case that we elide it.

Let CGraph(V) be the category of traceable cyclic single-coloured flow graphs over V viewed up to bisimulation.

Proposition (Bisimulation is a congruence). Bisimulation is a congruence wrt the graph operations.

Proposition (Flow graphs form a partially traced cartesian category). CGraph(V) is a partially traced cartesian category.

Define CTerm(V) as the free partially traced cartesian category with finite products over V.

f,g | ::= | ...as for Term...
| | | TrX(f) |

If terms can be proved equal using the axioms for a partially traced cartesian category, we shall write f = g.

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

Proposition (Expressivity). For any traceable 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:

where f is acyclic, and the only traceable edges in f are the incoming and outgoing edges.

Proposition (Normalization). For any term f there is a normal form g such that f = g.

Proof.

We can then prove completeness, essentially by converting any bisimulation between cyclic graphs into a shuffle, then using uniformity.

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

Proof.

Proposition (Initiality). CGraph(V) is the initial partially traced cartesian category over V.

We can extend this result to include embedding single-coloured cyclic graphs into two- or three-coloured graphs. Let CGraph(V,C) and CGraph(V,V,P) be the categories of cyclic two- and three-coloured graphs such that:

- Any cyclic path goes through at least one edge labelled with a traceable sort.

- Any nodes on a cycle are labelled in V.

Proposition (Initiality). CGraph(V,C) is the initial symmetric monoidal category over C with Graph(V) as a sub smc with the same objects. CGraph(V,C,P) is the initial symmetric premonoidal category over P with CGraph(V,C) as centre.

Previous | Next