C
Given a strict symmetric monoidal category C: with a full subcategory (not necessarily symmetric monoidal) TC:
C
a partial trace is a natural transformation:
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 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)):
| = | ||||||
| = |
|
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 B
((idX
f);
g)
|
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
|
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))
|
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))
|
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) |
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:
Proposition (Normalization).
For any term f there is a normal form
g such that
f = g.
Proposition (Completeness).
If [[f]] [[g]]
then
f = g.
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:
V.
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.