Given two signatures V and C with the same sorts, define the language Exp(V,C) as as extending Exp(V) with:
M | ::= | ...as before... | |
| | c M | (Central constructor, c in C) |
and add a new category:
C | ::= | ...as before... |
| | central |
The judgements M : T in central are as before, but we now have two new rules, one for value constructors:
| [c : B1,...,Bm C1,...,Cn in V] |
and one for central constructors:
| [c : B1,...,Bm C1,...,Cn in C] |
Note that the two subsumption rules are sound, one for expressions:
M : T in val | ||
M : T in central |
and one for declarations:
D : in val | ||
D : in central |
The graphical semantics of central is the same as for val, but we now have two colours of nodes. Nodes labelled with constructors from V are drawn:
[[x in central]] | = | |
[[c M in central]] | = | |
[[c M in central]] | = | |
[[(M1,...,Mn) in central]] | = | |
[[D M in central]] | = |
[[let P = M; in central]] | = | |
[[D1 D2 in central]] | = | |
[[ in central]] | = |
nor a natural terminal:
For example, the following graphs are bisimilar:
let r:ref = ref(1+1); | let y:int = 1; |
return (r,r); | let r:ref = ref(y+y); |
return (r,r); |
but they are not bisimilar to:
let x:int = 1+1; | let y:int = 1; |
return (ref(x),ref(x)); | let x:int = y+y; |
return (ref(x),ref(x)); |
In an appendix we construct a category Graph(V,C) with:
and show that this is the initial pair of categories:
with:
Such pairs of categories have been studied by Benton in the form of mixed linear/non-linear logic, although he allows V and C to have different objects. The presentation here is based on Hasegawa's, although we have provided a graphical presentation rather than a term model construction. These categories form a natural model of computation where order of evaluation is unimportant, such as nondeterminism or unique name generation. In the next section we shall allow more general computations.