# Operational semantics

## Examples

In this paper, we have given an equational characterization of programs. Categorically, we have:

- Vectors of types are objects.

- Graphs are morphisms.

To give a treatment of the dynamics of progams, we would like to give an operational semantics, for example:

In this example, the reductions are given as a type-preserving relation between terms. Following Milner's operational semantics for action calculi, we would expect to have the categorical picture:

- Vectors of types are objects.

- Graphs are morphisms.

- Reductions between graphs are 2-cells.

In the above case, the 2-cells are just a preorder, but in general we may be interested in labelled transition systems, which can be viewed as 2-categories where the 2-cells are labelled with an appropriate monoid, for example strings of actions. For example, we can give an lts semantics for programs containing print statements as a string-labelled 2-category:

'hello' |
'world' |

These 2-cells are generated from atomic reductions, in these examples:

|  |  | (where x + y = z)

and:

| s |

## Pre-2-categories

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 |  | ; |

For example this would give us:

'world' |
'hello' |

This is a similar problem to that solved by premonoidal categories, and the solution is to lift the premonoidal structure into the 2-cells. In the same way as we divided the 1-cells into central and process 1-cells, we divide the 2-cells into central and process 2-cells. Central reductions can take place anywhere in a computation, but process reductions have to happen in left-to-right order:

If |  |  |
and |  |  |
| then |  | ; |

and:

If |  |  |
and |  |  |
| then |  | ; |

and:

If |  |  |
and |  |  |
| then |  | ; |

This is just the usual definition of big-step reduction to normal form, replayed in categorical language.

Formally, define C P to be a pre-2-category whenever:

- C is a sub 2-category of P with the same objects.

- In addition to the usual hom-category P[XY] (the central hom-category) a category P[XY] (the process hom-category).

- P[XY] is a subcategory of P[XY] with the same objects (that is the same 1-cells).

- Two functors:

  ;L : P[XY] P[YZ] P[XZ]
  ;R : C[XY] P[YZ] P[XZ]

  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.

A pre-2-functor is a commuting square of functors respecting the pre-2-categorical structure.

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:

- C is a symmetric monoidal 2-category.

- Two pre-2-functors:

  : C P P
  : P C P

  such that:

  - the three pre-2-functors , and coincide on objects,
  - the three `obvious' pre-2-functors from C C to P coincide, and
  - the symmetry in C is a natural isomorphism X Y Y X in P.

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:

V[X (Y Z)] V[(X Y) Z]
V[X (Y Z)] C[(X Y) Z]
V[X (Y Z)] P[(X Y) Z]

allow value and central reductions to take place under function bodies, but not process reductions. For example we allow:

but not:
'hello'
As two extremes, we have:

- categories where the only central 2-cells are the trivial identity reductions, corresponding to languages where no reduction is allowed under lambda, and

- categories where the central and process 2-cells are the same, corresponding to langauges where reduction is allowed in any sub-term.

Thus the division of 2-cells into central and non-central categories gives a natural description of both the call-by-value lambda calculus with reduction allowed anywhere, and the canonical left-to-right reduction strategy.

Previous | Next