Show simple item record

dc.contributor.authorRydeheard, David Eric
dc.date.accessioned2013-04-03T14:47:32Z
dc.date.available2013-04-03T14:47:32Z
dc.date.issued1982
dc.identifier.urihttp://hdl.handle.net/1842/6611
dc.description.abstractCategory 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 of colimits. 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 conditions: 1. Signatures and presentations may be defined for monadic theories and free theories on a signature may be constructed. 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 certain properties. 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.language.isoenen_US
dc.publisherThe University of Edinburghen_US
dc.relation.hasversionBurstall 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.subjectCategory theoryen_US
dc.subjectprogrammingen_US
dc.subjectprogram specificationen_US
dc.subjectspecification language.en_US
dc.subjectsemanticsen_US
dc.subjectmonadic theoriesen_US
dc.titleApplications of Category Theory to Programming and Program Specificationen_US
dc.typeThesis or Dissertationen_US
dc.type.qualificationlevelDoctoralen_US
dc.type.qualificationnamePhD Doctor of Philosophyen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record