Premonoidal categories and a graphical view of programs

December 1997

Alan Jeffrey
School of Cognitive and Computing Sciences
University of Sussex
Brighton BN1 9QH
UK
alanje@cogs.susx.ac.uk

This paper describes the relationship between two different presentations of the semantics of programs:

Mixed data and control flow graphs are commonly used in software engineering as a semi-formal notation for describing and analysing algorithms.
Category theory is used as an abstract presentation of the mathematical structures used to give a formal semantics to programs.

In this paper, we formalize an appropriate notion of flow graph, and show that acyclic flow graphs form the initial symmetric premonoidal category. Thus, giving a semantics for a programming language in flow graphs uniquely determines a semantics in any symmetric premonoidal category.

For languages with recursive definitions, we show that cyclic flow graphs form the initial partially traced cartesian category.

Finally, we conclude with some more speculative work, showing how closed structure (to represent higher-order functions) or two-categorical structure (to represent operational semantics) might be included in this graphical framework.

The semantics has been implemented as a Java applet, which takes a program text and draws the corresponding flow graph (all the diagrams in this paper are drawn using this applet).

The categorical presentation is based on Power and Robinson's premonoidal categories and Joyal, Street and Verity's monoidal traced categories, and uses similar techniques to Hasegawa's semantics for recursive declarations. The closed and two-categorical structure is related to Gardner's name-free presentation of Milner's action calculi.

Previous | Next