Some fundamental algebraic tools for the semantics of computation Part 1: Comma Categories, Colimits, Signatures and Theories

AbstractThis paper develops a number of fundamental tools from category theory and applies them to problems in computation. The tools include algebraic theories, colimits, comma categories and two-dimensional categories. The applications concern making program specifications understandable by expressing them as interconnections of smaller ‘mind sized’ specifications in a variety of ways, as in our language spCLEAR. The link between these tools and applications is the idea of using algebraic theories as program specifications. To carry out this programme requires developing a formal calculus of operations for constructing, modifying and interconnecting theories. These operations include: constructing free theories, combining given theories, deriving new computational functions from old, abstracting (or ‘hiding’) parts of theories, inductively completing a theory, and applying a theory-valued procedure to an actual theory. Because a number of different notions of theory are relevant to computation, this paper also sketches an axiomatically based calculus of operations applicable to any notion of theory which satisfies certain axioms. The paper also presents a number of sample calculations illustrating how the various tools can be used, and proves some general theorems which justify such calculations. Part 1 develops comma categories, colimits, signatures and sorted theories, while Part 2 (to appear in Theoretical Computer Science 31 (3)) introduces signed theories, abstract theories, and further applications to specification