Process category

Syntax

Given three signatures V, C and P with the same sorts, define Exp(V,C,P) as extending Exp(V,C) with:

M ::= ...as before...
| c M(Process constructor, c in P)

and add a new category:

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

The judgements M : T in central are as before, but we now have three new rules, one for value constructors:

M : (B1,...,Bm) in proc
c M : (C1,...,Cn) in proc
[c : B1,...,Bm C1,...,Cn in V]

one for central constructors:

M : (B1,...,Bm) in proc
c M : (C1,...,Cn) in proc
[c : B1,...,Bm C1,...,Cn in C]

and one for process constructors:

M : (B1,...,Bm) in proc
c M : (C1,...,Cn) in proc
[c : B1,...,Bm C1,...,Cn in P]

Again, we have the soundness of the two subsumption rules, one for expressions:

M : T in central
M : T in proc

and one for declarations:

D : in central
D : in proc

Graphical semantics

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

=
This 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 this graphical presentation. Instead we shall introduce new control arcs in addition to the existing data arcs. Each proc node has incoming and outgoing control arcs in addition to its data arcs, for example:

let (h:string, w:string) = ('hello', 'world');
print (h);
print (w);

The values 'hello' and 'world' come from val, so order of evaluation is unimportant. The print nodes, 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:


let r:ref = ref(0);
r := (1 + !(r));
return r;

The semantics of proc terms is given as a graph with one incoming and one outgoing control edge:

Note that we can embed central graphs into proc graphs by adding a control edge:
The graphical semantics of proc expressions is (we give the semantics for nullary tuples and pairs below, other tuples are similar):
[[x in proc]] =
[[c M in proc]] =
[[c M in proc]] =
[[c M in proc]] =
[[() in proc]] =
[[(M,N) in proc]] =
[[D M in proc]] =
The graphical semantics of proc expressions is:
[[let P = M; in proc]] =
[[D1 D2 in proc]] =
[[ in proc]] =
Graphs with one incoming control arc and one outgoing control arc form a strict symmetric premonoidal category, a notion introduced (in slightly different form) by Power and Robinson. In an appendix we construct a category Graph(V,C,P) of graphs with one control line, with:

Graph(V) Graph(V,C) Graph(V,C,P)

and show that this is the initial triple of categories:

V C P

with:

Thus the graphical semantics defined above uniquely determines a semantics in any such triples of categories.

Such triples of categories have been studied by Power and Thielecke, and compared with indexed categories. The presentation here is slightly different, in that we have presented V and C a priori rather than synthesizing it from P. Since central constructors play an important role in languages such as the -calculus, it seems natural to include C in the categorical presentation. See Selinger's discussion in his presentation of control categories. Our presentation of premonoidal categories is based on Power's presentation using Subset-enriched categories.

Previous | Next