[Prev][Next][Index][Thread]
Report available
I'd like to announce a technical report relating Power and Robinson's
premonoidal categories to a category of mixed data-flow and
control-flow graphs.
Premonoidal Categories and a Graphical View of Programs
Alan Jeffrey
University of Sussex
The report is available electronically from:
http://www.cogs.susx.ac.uk/users/alanje/premon/
Abstract
--------
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.