Process category

Syntax

C | ::= | ...as before...
| | | proc

Type system

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

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

Equations

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' = Ø)

Syntactic categories

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]

Graphical presentation

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:

=
This equation is not true in proc where order of evaluation is important. We would like to retain the notion that if two terms have isomorphic graphs then they are provably equal, so we shall not use the `obvious' graphical presentation. Instead we shall introduce new control arcs in addition to the existing data arcs. Each generator now has incoming and outgoing control arcs in addition to its data arcs, for example:

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):

ref | : | central (int) : ref
:= | : | proc (ref,int) : ()
! | : | proc (ref) : int

or graphically:

For example:

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

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

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.

Currying: |
Evaluation: |

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.

Previous | Next