Title: | Premonoidal categories and a graphical view of programs |
Author: | Alan Jeffrey |
Abstract: | This paper describes the relationship between two different presentations
of the semantics of 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. |
Full Paper: | [html] |