In this paper, we have given an equational characterization of programs. Categorically, we have:
'hello' | |
'world' |
These 2-cells are generated from atomic reductions, in these examples:
(where x + y = z) | |||
s |
Unfortunately, we cannot just replay Milner's presentation in the premonoidal setting, since one of the axioms of a 2-category is functoriality of composition, which implies:
If | |||
and | then | ; |
'world' | |
'hello' |
If | |||
and | then | ; |
If | |||
and | then | ; |
If | |||
and | then | ; |
Formally, define C P to be a pre-2-category whenever:
such that:
P[XY] P[YZ] | P[XZ] | |
P[XY] P[YZ] | P[XZ] |
and:
C[XY] P[YZ] | C[XY] P[YZ] | |
P[XY] P[YZ] | P[XZ] |
commute.
Note that any 2-category is automatically a pre-2-category, since we can take C and P to be the same 2-category, and identify all of the hom-categories and composition functors.
We can then replay the definition of a premonoidal category at the 2-level to get a categorical presentation of a language with its operational semantics.
A premonoidal pre-2-category is a pre-2-category C P with:
such that:
Following Power's presentation of premonoidal categories as Subset-enriched categories, we can present pre-2-categories using enriched categories. Define a category to be centralized if some of its objects are tagged as central, some of its morphisms are tagged as central, and satisfying the property that if f : X X and X is central, then f and X are central. Let Central be the category of centralized categories with functors respecting the central structure. Central has an asymmetric monoidal structure where C * D is the subcategory of C D where for any pair of morphisms (f,g) : (X,Y) (X,Y) either X is central or g is central. Then the above definition of a pre-2-category is equivalent to a Central-category with composition given as a functor P[X,Y] * P[Y,Z] P[X,Z]. We can then replay Power's definition of a premonoidal category replacing Subset-Cat with Central-Cat to find a definition of a premonoidal pre-2-category equivalent to the above.
For the closed structure, the isomorphisms:
allow value and central reductions to take place under function bodies, but not process reductions. For example we allow: