Comparisons

Action calculi

The graphical presentation of programming most similar to that given here is Milner's action calculi. This is a framework for describing concurrent languages, based on symmetric monoidal 2-categories.

Since they are based on symmetric monoidal 2-categories, they are similar to the central categories presented here, but in action calculi the nodes (called controls) may contain sub-graphs.

For example, the lambda-calculus is given as having controls:

lambda for building lambda-abstractions (originally written _) This control has one sub-graph (the body of the function), no incoming arcs, and one outgoing arc (the function).
ap for function application. This control has no sub-graphs, two incoming arcs (the function and its argument), and one outgoing arc (the result).

We can draw these (this graphical presentation is slightly different from Milner's, to make comparisons with this paper simpler) as: The operational semantics is given by the reduction:

Reductions can take place anywhere in a graph, but not inside controls, for example the reduction of (

x.xx) (

x.xx) is given by:

A simple language of print statements can be modelled with controls for string constants and a print control, containing a subgraph for the continuation: The operational semantics can be given as a 2-category where the 2-cells are strings, generated by the reduction:

'string'

For example:


'hello'
'world'

Since reduction is not allowed inside controls, we do not have:


'world'

In action calculi, control over reduction order is achieved by the use of sub-graphs inside controls, where in our presentation reduction order is given by control arcs.

Categorically, action calculi are based on symmetric monoidal 2-categories rather than premonoidal pre-2-categories, so the categorial presentation is simpler. There is a tradeoff here between the simpler categorical presentation, or the simpler graphical view given by control arcs.

To see the difference between these two presentations categorically, note that there are two ways to embed a premonoidal category into a monoidal category. The presentation here is based on an embedding into state transformers, described in an appendix. But it is also possible to use a CPS translation, in which any computation whose evaluation is delayed is placed in a continuation. Graphically, this corresponds to boxing the delayed computations, in a manner similar to the graphs above. Whether this informal connection can be formalized is left for future work.

Lambda calculus with cyclic definitions

In his thesis, Hasegawa presents a similar categorical model for lambda-calculi with explicit sharing. His setting is:

A category with finite products V.
A traced symmetric monoidal category C.
An identity-on-objects inclusion V C.
Closed structure given by an adjunction:

V[X, Y Z] C[X Y, Z]

This is very similar to the setting described here, with two important differences:

The addition of the premonoidal category P.
In Hasegawa's setting, there is a trace on C rather than a partial trace on V.

The first difference is the most important: Hasegawa's graphs are pure data flow graphs, and do not require control edges. The work presented here generalizes his work from the monoidal case to the premonoidal case.

The second difference is an orthogonal issue, caused by different motivating examples. Hasegawa's motivating denotational example is the cartesian closed category Dom, where all objects have least elements, but maps are not necessarily strict: this provides a semantics for call by name or call by need languages. Our motivating example is the categories Cpo Cpo where Cpo only has a partial trace: this provides a semantics for call by value languages.

Previous | Next