This paper tries to explain why and how category theory is useful in computing science, by giving guidelines for applying seven basic categorical concepts: category, functor, natural transformation, limit, adjoint, colimit and comma category. Some examples, intuition, and references are given for each concept, but completeness is not attempted. Some additional categorical concepts and some suggestions for further research are also mentioned. The paper concludes with some philosophical discussion. 0 Introduction This paper tries to explain why category theory is useful in computing science. The basic answer is that computing science is a young eld that is growing rapidly, is poorly organised, and needs all the help it can get, and that category theory can provide help with at least the following: Formulating deenitions and theories. In computing science, it is often more diicult to formulate concepts and results than to give a proof. The seven guidelines of this paper can help with formulation; the guidelines can also be used to measure the elegance and coherence of existing formulations. Carrying out proofs. Once basic concepts have been correctly formulated in a categorical language, it often seems that proofs \just happen": at each step, there is a
atural" thing to try, and it works. Diagram chasing (see Section 1.2) provides many examples of this. It could almost be said that the purpose of category theory is to reduce all proofs to such simple calculations. Discovering and exploiting relations with other elds. Suuciently abstract formulations can reveal surprising connections. For example, an analogy between Petri nets and the-calculus might suggest looking for a closed category structure on the category of Petri nets 52]. Dealing with abstraction and representation independence. In computing science , more abstract viewpoints are often more useful, because of the need to achieve independence from the often overwhelmingly complex details of how things are represented or implemented. A corollary of the rst guideline (given in Section 1) is that two objects are \abstractly the same" ii they are isomor-phic; see Section 1.1. Moreover, universal constructions (i.e., adjoints) deene their results uniquely up to isomorphism, i.e., \abstractly" in just this sense.
Mendeley saves you time finding and organizing research
There are no full text links
Choose a citation style from the tabs below