C		M : T in central
C		M : T in proc

C		D : C' in central
C		D : C' in proc

The equations for proc are the same as those for central, except that the following is not valid:

D D'

=

D' D

(bv D fv D' = fv D bv D' = Ø)

We can construct the category proc as for val. Because there are fewer axioms for proc than for central, proc is not a symmetric monoidal category. It is instead premonoidal, a notion introduced (in slightly different form) by Power and Robinson.

A premonoidal category is a category P together with:

• A symmetric monoidal category C with the same objects as P (called the center 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.

The syntactic category proc is premonoidal, with centre central, and has closed structure given by an adjunction (natural in X and Z):

val[X, Y Z] proc[X Y, Z]

The graphical presentation of proc is rather different from that of central and val. If we were to use the `obvious' presentation, then we would discover that not all graph-isomorphic terms are equal. In particular, in central we have:

The values hello and world come from val, so order of evaluation is unimportant. The print statements, however, come from proc, where order of evaluation is significant, so print has an incoming and outgoing control arc as well as its incoming data arc:

As another example, the ML reference functions can be typed (using only integer references for this example):

or graphically:

For example:

Graphs with one incoming control arc and one outgoing control arc form a premonoidal category.

We can also introduce graphical representation for the closed structure, in a similar way as for central, although we now need to take a control line as an extra parameter to a curried morphism, and the evaluation morphism now takes an extra control line argument.

The axiomatization for these graphs is the same as for central, that is to say the graph isomorphism axioms, plus beta, eta, and naturality axioms for the closed structure.