
Constructing Specifications and
Modules in a KZdoctrine
<_author_search_(gillian hill)>Gillian Hill ?
Abstract
Using the structure of a KZmonad we create a general categorical workspace in
which diagrams can be formally constructed. In particular this abstract framework
of category theory is shown to provide a precise semantics for constructing
the specifications of complex systems from their component parts.
1 Introduction
The purely equational 2dimensional categorical algebra underlying the process of freely completing categories under a given suitable class of colimits is presented by Kock in [7]. A common feature of the category which freely completes another category is that it has diagrams (functors) as its objects. Using properties of adjointness Kock identifies a particular monad which is called either a `monad with the Kock property' or a `KZdoctrine'. Kock shows that this type of monad, which has structures which are adjoint to units, expresses precisely the properties of free cocompleteness and colimit formation in a category.
In this paper the properties of a KZdoctrine are presented before they are shown to provide a general categorical workspace for the construction of diagrams. These ideas are then extended to provide a specific categorical workspace within which specifications of system components can be both structured and implemented to configure the architecture of a final executable system. We show that the mathematical structure of a KZdoctrine, although complex, provides a powerful framework that expresses precisely the configuration of systems. We have already introduced a categorical framework for the configuration of complex systems in [4], and designed a language for configuration in [6]. The possible relationships between the component parts of systems are identified at an intuitive level in [5] in order to choose appropriate highlevel combinators for configuration. The highlevel combinators are then formally defined in terms of more primitive combinators that operate on recursively defined objects of sorts in the set fspecification, moduleg. Specifications are represented in the categorical workspace by recursively defined and structured diagrams, whereas modules are represented by the singleton diagrams created by colimit formation from their specifications. Our aim is to present the categorytheoretic framework for the configuration of modular systems as a mathematical workspace that is independent of any particular specification approach, design methodology or programming paradigm.
This paper is arranged as follows. In Section 2 we present the background to Kock's work and in Section 3 we build on Kock's definition of the KZdoctrine to provide a formal framework for the construction of diagrams. In Section 4 these ideas are applied to a particular categorical workspace for the configuration of complex systems from specifications and modules, and an example is given
?Department of Computing, Imperial College of Science, Technology and Medicine, London, SW7 2AZ, gah@doc.ic.ac.uk and City University, Northampton Square, EC1 VOH B, gah@cs.city.ac.uk