(( A glitch in passing mailing list jobs resulted in an apparent failure to resend the following with less delay. R.R. )) The double parentheses are actually square brackets. Category Theory for Computing Science: Update Michael Barr and Charles Wells Our text, Category Theory for Computing Science, Prentice Hall, 1990 (ISBN 0-13-120486-6) has just been published. We intend to maintain the text in the sense that programmers maintain their programs, by keeping a list of known errors and also of additions to the text that we think might be useful. (The latter will probably come in spurts as we go to meetings and find out about wonderful new applications of category theory to computing science.) We will periodically announce new errata and addenda on the category theory bulletin board. The latest TeX version of the complete list is available by e-mail or p-mail from either author. The update consists of three parts: 1. A list of errors discovered so far. 2. Additional examples, problems and pointers to the literature. 3. Additions to the list of references, pp. 417ff. of the text. Page references refer to the text. Any further corrections or suggestions for additional text will be welcome. 1. Errors ((p. xv)) In the Chapter Dependency Chart, there should be a diagonal line from Chapter 5 to Chapter 7. ((p. 92)) In Proposition 4.3.12 and its proof, the letter C (not the script C) is used with two different meanings. This can be corrected by changing C to S in the first line of the proposition, third line (first occurrence only), fourth line (last occurrence only) and in the first line of the proof (second occurrence only). ((p. 96)) The reference to Seely should be ((1987)) (the entry in the list of references, p. 425, was incomplete and is updated in the list of references below.) ((p. 102)) ``The'' not ``the'' in line 7. ((p. 345)) Line 2 of the answer to exercise 12.a: the last letter should be ``B'', not ``b''. ((p. 365)) In the answer to problem 8, beta C:Hom(C,C) to F(C). ((p. 431)) The word ``relation'' should also be indexed on p. 21. 2. Additional text ((p. xiii)) (Second paragraph) Another collection of papers is ((Pitt, Rydeheard, Dybjer, Pitts and Poigne, 1989)). ((p. 17)) ((Additional example of category.)) Let alpha be a relation from a set A to a set B and beta a relation from B to C (see 1.3.4). The composite beta o alpha is the relation from A to C defined as follows: If x is in A and z is in C, (x,z) is in beta o alpha if and only if there is an element y in B for which (x,y) in alpha and (y,z) in beta. With this definition of composition, the category of sets and relations} has sets as objects and relations as arrows. ((p. 71)) ((New exercise)) Show that the category of sets and relations is equivalent, in fact isomorphic, to its own dual (see 2.6.7). Answer: Let Rel denote the category of sets and relations. For a relation alpha from A to B, that is, a subset of A x B, let alpha\op denote the subset {(b,a) | (a,b) in A x B} of B x A. Let F:Rel to Rel\op be the identity on objects and for a relation alpha:A to B, let F(alpha)=alpha\op. F(alpha) is a relation from B to A in Rel, hence a relation from F(A)=A to F(B)=B in Rel\op. It is easy to check that if beta:B\to C, then F(beta o alpha)= alpha op o beta\op in Rel, so (beta o alpha)\op=beta\op o alpha\op in Rel\op. This says F(beta o alpha)=F(beta) o F(alpha), so F preserves composition. The identity relation on A is Delta_A= {(a,a) | a in A}, so Delta=Delta\op and F preserves identities. Since for any relation alpha, (alpha\op)\op=alpha, we have F o F is the identity functor on Rel, so is its own inverse. Hence F is an isomorphism. By Exercise 1, it is therefore an equivalence of categories. ((p. 96)) The applications of 2-categories have mushroomed and include ((Hoare, Ji Feng and Martin, 1990)), ((Moggi, 1989)), and ((Power, 1989)) in addition to the papers already listed. ((p. 97)) Second paragraph of Section 4.5: In addition to generalizing the Cayley Theorem, the Yoneda Lemma also has as a special case the embedding of a poset into its down-closed subsets. Also: set-valued functors are studied further in Sections 11.2 and 14.4. ((p. 257)) Besides ((Coquand, 1988)), Moggi ((1989)) also uses the Grothendieck construction in modeling polymorphism. ((p. 287)) Just before the exercise: See also ((Ehrhard, 1989)). ((p. 318)) Add comment: We considered presheaves as actions in Section 3.2. They occur in other guises in the categorical and computer science literature, too. For example, a functor F:A to Set, where A is a set treated as a discrete category, is a ``bag'' of elements of A. If a in A, the set F(a) denotes the multiplicity to which a occurs in A. See ((Taylor, 1989)) for an application in computing science. ((p. 325)) Goguen ((1990)) has developed a sheaf semantics for object oriented programs. 3. Additional references T. Ehrhard, Dictoses. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989. J. Goguen, Semantics of concurrent interacting objects. Preprint, Programming Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD, England. C. A. R. Hoare, He Jifeng and C. Martin, Pre-adjunctions in order-enriched categories. Preprint, Programming Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD, England. E. Moggi, A category-theoretic account of program modules. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989. D. Pitt, D. Rydeheard, P. Dybjer, A. Pitts and A. Poigne, eds. Category theory and computer science. Lecture Notes in Computer Science 389, Springer Verlag, 1989. A. J. Power, An abstract formulation for rewrite systems. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989. R. Seely, Modelling computations: a 2-categorical framework. In Proceedings of the Conference on Logic in Computer Science, IEEE, 1987. ((Corrected reference)). P. Taylor, Quantitative domains, groupoids and linear logic. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989.
participants (1)
-
Michael Barr