|dc.contributor.author||Rydeheard, David Eric||
|dc.description.abstract||Category theory is proving a useful tool in programming and program specification - not only as a descriptive language but as directly
applicable to programming and specification tasks.
Category theory achieves a level of generality of description at
which computation is still possible. We show that theorems from
category theory often have constructive proofs in the sense that they
may be encoded as programs. In particular we look at the computation
of colimits in categories showing that general theorems give rise to
routines which considerably simplify the rather awkward computation
The general routines arising from categorical constructions can be
used to build programs in the 'combinatorial' style of programming.
We show this with an example - a program to implement the semantics
of a specification language. More importantly, the intimate
relationship between these routines and algebraic specifications
allows us to develop programs from certain forms of specifications.
Later we turn to algebraic specifications themselves and look at
properties of "monadic theories". We establish that, under suitable
1. Signatures and presentations may be defined for monadic
theories and free theories on a signature may be
2. Theory morphisms give rise to ad junctions between
categories of algebras and moreover a collection of
algebras of a theory give rise to a new theory with
3. Finite colimits and certain factorisations exist in
categories of monadic theories.
4. Many-sorted, order-sorted and even category-sorted
theories may be handled by somewhat extending the notion
of monadic theories.
These results show that monadic theories are sufficiently
well-behaved to be used in the semantics of algebraic specification
languages. Some of the constructions can be encoded as programs by
the techniques mentioned above.||en_US
|dc.publisher||The University of Edinburgh||en_US
|dc.relation.hasversion||Burstall R.M. and Rydeheard D.E. (1979) The Free Algebraic Theory on a Signature. Unpublished Report. Dept. of Artificial Intelligence, Univ. of Edinburgh.||en_US
|dc.title||Applications of Category Theory to Programming and Program Specification||en_US
|dc.type||Thesis or Dissertation||en_US
|dc.type.qualificationname||PhD Doctor of Philosophy||en_US