Completeness proof: premonoidal categories

A strict symmetric premonoidal category is a category P together with:

A strict symmetric monoidal category C with the same objects as P (called the centre of P).
An identity on objects inclusion C P.
Two functors:
: C P P
: P C P
such that:
- the three functors , and coincide on objects,
- the three `obvious' functors from C C to P coincide, and
- the symmetry in C is a natural isomorphism X Y Y X in P.

This definition is based on Power's presentation of Power and Robinson's definition.

A three-coloured flow graph over three signatures _V, _C and _P with the same sorts is a two-coloured flow graph over _V and _C except that:

Each edge is either labelled E : X or E : S.
Each node is either labelled N : c, N : c or N : c.
If N : E F, N : c and c : X Y, then E : XS and F : YS.
Each S-labelled edge occurs exactly once either as an outgoing edge of the graph, or an incoming edge of a node.

A simulation between three-coloured flow graphs is the same as for two-coloured flow graphs except that:

R is a function on nodes labelled by _P (that is for any node N : c of G there is precisely one node N of G such that N R N).

We can define the following operations on graphs (and below we shall show that they satisfy the equations necessary to be a premonoidal category):

Identity:
Composition:
Tensor left:
Tensor right:
Symmetry:

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,_P) be the category of acyclic flow graphs over (_V,_C,_P) where the morphisms from X to Y are graphs from XS to YS, viewed up to bisimulation.

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

Proposition (Flow graphs form a premonoidal category). Graph(_V,_C,_P) is a premonoidal category over _P with centre Graph(_V,_C).

Define Term(_V,_C,_P) as the free premonoidal category over _P with central category Term(_V,_C).

f,g	::=	f
	\|	f ; g
	\|	f g
	\|	f g
	\|	c

If terms can be proved equal using the axioms for a premonoidal category 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 (Normalization). For any f we can find normal g such that f = g.

Proposition (Cancellation of permutations). For any:

we can find h such that:

Proposition (Cancellation of val nodes). For any:

we can find h such that:

Proposition (Cancellation of central nodes). For any:

we can find h such that:

Proposition (Cancellation of proc nodes). For any:

we can find h such that:

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

Proposition (Initiality). Graph(_V,_C,_P) is the initial strict symmetric premonoidal category over _P with Graph(_V,_C) as centre.

Previous | Next