Information Technology Reference
In-Depth Information
notational and operational semantics have far too much detail to convey the
desired understanding and illumination. It is only the algebra that captures the
essence of the concepts at an appropriately high level of abstraction. It is per-
haps for the same reason that algebraic laws are also the most useful in practice
for engineering calculation.
The primary role of algebraic laws is recognised in the most abstract of
branches of algebra, namely category theory. Categories provide an excellent
source of elegant laws for programming. Its objects nicely represent the types of
a programming language, and its basic operation of composition of arrows is a
model for the combination of actions evoked by parts of a program. Additional
important operators and their types are specied entirely by the algebraic laws
that they satisfy. The specication of an operator is often accompanied by a proof
that there is only one operator that satises it { at least up to isomorphism. This
gives assurance that the stated laws are complete: no more are needed, because
all other categorial properties of the operator can be proved from them. Finally,
a wide range of diering categories can be explored and classied simply by
listing the operators which they make available and the laws which they satisfy.
These considerations suggest a third approach to the development of pro-
gramming theory, one that starts with a collection of algebraic laws as a deni-
tive presentation of the semantics of a programming language [Baeten and Wei-
jland]. The theory then develops by working outwards in all directions. Working
upwards explores the range of denotational models for languages which satisfy
the laws. Working downwards explores the range of correct implementations for
these languages. And working sideways explores the range of similar theories
and languages that might have been chosen instead. The work of the theorist is
not complete until the consequences of theory have been fully developed in all
relevant directions.
Such an ambitious programme can be achieved only by collaboration and ac-
cumulation of results by members of dierent research traditions, each of whom
shares an appreciation of the complementary contributions made by all the oth-
ers.
Acknowledgements
The views put forward in this paper evolved during a long collaboration with
He Jifeng on research into unifying theories of programming. They contribute
towards goals pursued by the partners in the EC Basic Research Project CON-
CUR; and they have been subjected to test in the EC Basic Research Project
PROCOS. They are more fully expounded in the reference [Hoare, He], which
contains a list of 188 further references. Signicant contributors to this work
at Oxford include Carroll Morgan, Je Sanders, Oege de Moor, Mike Spivey,
Je Sanders, Annabelle McIver, Guy McCusker, and Luke Ong. Other crucial
clarications and insights were obtained during a sabbatical visit to Cambridge
in conversations with Robin Milner, Andy Pitts, Martin Hyland, Philippa Gard-
ner, Peter Sewell, Jamey Leifer, and many others. I am also grateful to Microsoft
Search WWH ::
Custom Search