# Central category

## Syntax

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:

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

and one for central constructors:

|  | M : (B1,...,Bm) in central
|  | c M : (C1,...,Cn) in central
| [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

## Graphical semantics

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:

Nodes labelled with constructors from C are drawn:
Graphs which only contain V nodes are drawn:
Graphs which contain V nodes and C nodes are drawn:
The graphical semantics of central expressions is the same as that of val expressions:

[[x in central]] | = |
[[c M in central]] | = |
[[c M in central]] | = |
[[(M1,...,Mn) in central]] | = |
[[D M in central]] | = |

The graphical semantics of central declarations is the same as that of val declarations:

[[let P = M; in central]] | = |
[[D1 D2 in central]] | = |
[[ in central]] | = |

In an appendix we adapt the notion of bisimulation between graphs to require that any bisimulation is an isomorphism on central nodes. This means that for central nodes there is no natural diagonal:

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:

Graph(V) Graph(V,C)

and show that this is the initial pair of categories:

V C

with:

- V a strict cartesian category over V.

- C a strict symmetric monoidal category over C.

- The inclusion an identity on objects symmetric monoidal functor.

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

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.

Previous | Next