Partial trace

Syntax

Given three signatures _V, _C and _P with the same sorts, where a subset of the sorts are tagged as traceable, define RecExp(_V,_C,_P) as extending Exp(_V,_C,_P) with:

D	::=	...as before...
	\|	local rec x; D	(Local recursive declaration)

Add new judgements T traceable, which for this section just inherits the tags from the signatures. Then the type rule for local recursive declarations is:

		T traceable
, x : T		D : (₁, x : T, ₂) in val

		(local rec x; D) : (₁, ₂) in val

Note that recursive declarations are only allowed in val: this restriction is based on the motivating denotational model, where non-trivial fixed points only exist in Cpo, not in Cpo. The restriction to traceable types is also based on this example: Cpo does not have fixed points for all objects, only those with least elements. So in this motivating example, V is Cpo, P is Cpo, and the traceable objects are those with least elements.

Graphical semantics

Previously, all of the graphs we have described have been acyclic. In order to give the semantics for recursive declarations, we allow cyclic graphs:

[[local rec x; D in val]]

For example, the fixed point of f is (when f has a traceable result):

This is an indexed fixed point becase:


=		(Naturality of copy)
=		(Naturality of Tr)
=		(Indexed dinaturality of Tr)

However, not all cyclic graphs can be expressed as a program. In particular:

We have restricted local rec declarations to traceable types, so any cyclic path must go through at least one traceable edge.
We have restricted local rec declarations to val declarations, so any nodes in a cycle are val nodes.

Traces were initially proposed as a categorical model of cycles in knots, and this graphical presentation is just a simplified version of the knot diagrams presented by Joyal, Street and Verity. Where they were concerned with knots, we are just concerned with graphs, so we have replaced their braided monoidal setting with a simpler symmetric monoidal one.

However, our graphs do not have a trace, because of the restriction that only traceable sorts can be declared recursively. Instead, we use a weaker notion of partial traceability, where we impose the restriction that feedback edges are traceable. In the case where all types are traceable, the two notions coincide.

In an an appendix we define partially traced cartesian categories, and show that when the categories of cyclic graphs:

CGraph(

_V)

CGraph(

_V,

_C)

CGraph(

_V,

_C,

_P)

form the initial triple of categories:

with:

V a partially traced cartesian category over _V.
C a strict symmetric monoidal category over _C.
P a strict symmetric premonoidal category over _P.
The inclusions are identity on objects symmetric premonoidal functors.

The axiomatization used for partially traced cartesian categories is more powerful that that of Joyal, Street and Verity's axiomatization for traced monoidal categories. Their axiomatization is sound and complete for graphs up to graph isomorphism, but in order to get completeness for graphs up to bisimulation, an additional property is needed (thanks to Peter Selinger for demonstrating a mistake in an earlier formulation, and for pointing out the connection with Plotkin uniformity).

A shuffle s is a morphism built only from composition, tensor, identity, symmetry, diagonal and terminal. A trace is uniform wrt shuffles whenever:

If: = then: = It is routine to show that Plotkin uniformity is equivalent to a trace which is uniform wrt strict morphisms, where a strict morphism is one such that: =

It is easy to show that any shuffle is strict, and so uniformity wrt shuffles is weaker than uniformity wrt strict morphisms.

Uniformity is, unfortunately, not algebraic, and it remains to be seen whether there is an algebraic axiomatization for flow graphs.

Previous | Next