Subj: CTCS 91, last announcement Date: Wed, 07 Aug 91 09:38:45 ADT From: curien@FRULM63.BITNET (Pierre-Louis Curien) FOURTH BIENNAL CONFERENCE ON CATEGORY THEORY AND COMPUTER SCIENCE (C.T.C.S.) 3-6 September 1991 LAST ANNOUNCEMENT LATE REGISTRATIONS ARE ACCEPTED The Fourth of the Biennal Summer Conferences on Category Theory and Computer Science will be held in Paris (France). The main purpose of these conferences is to link research in category theory with computer science. The importance of categories in understanding basic issues in computer science is now well established. Other structures in logic, algebra and topology are also seen as fundamental and the scope of the conference is to cover applications of these structures as well. Proceedings are published in the Springer LNCS series. Organising and Program Committee Samson Abramsky, Pierre-Louis Curien, Peter Dybjer, Giuseppe Longo, John Mitchell, David Pitt, Andrew Pitts, Axel Poigne', David Rydeheard, Don Sannella, Eric Wagner. INVITED SPEAKERS Albert Burroni Eugenio Moggi Thierry Coquand Ugo Montanari Peter Freyd Robert Tennent Local Arrangements Office C.A.I.M.E.N.S/E.N.S. 45, rue dUlm 75230 Paris Cedex 05 Tel : (33) (1) 43 29 12 25 ext. 3279 Fax : (33) (1) 46 34 05 31 Email: butery@dmi.ens.fr Person in charge: Chantal Butery Sponsorship: MRT (Ministe`re de la recherche et de la technologie), CNRS (Centre national de la recherche scientifique), MEN (Ministe`re de l'e'ducation nationale). Location: The conference will take place at: FIAP Jean Monnet 30, rue Cabanis 75014 Paris France (Me'tro station : Glacie`re) Accommodation, breakfast and self facilities for lunch or dinner will be provided by FIAP and are included in the registration fees (as well as a conference dinner). Accommodation : On the basis of students prices, the FIAP arranged for CTCS participants the possibility of booking double rooms to be shared or single rooms (in a limited number). Both types of rooms are provided with private shower, wash-basin, toilets and telephone. Other events : There will be a conference dinner. FIAP can also provide information on touristic or cultural activities in Paris and Paris area. Accommodation :Please fill and return your registration form to the Local Arrangements Office (CAIMENS/ENS), accompanied with a cheque of the corresponding amount in French Francs payable at CAIMENS. If you find it easier, you can also make a bank transfer to CAIMENS : Bank name and address : Socie'te' Ge'ne'rale 37, rue Gay-Lussac, 75005 Paris. Account number: 00037266208 with the reference CTCS, and making sure that your name will appear clearly. Acknowledgment will be dispatched in due time. C.T.C.S - 91 Registration Form Please complete and return this Registration Form(or a copy of it) before July 19th to C.A.I.M.E.N.S - 45, rue dUlm - 75005 Paris - France . One Form per participant is requested. Enclose your payment of the corresponding amount by cheque in french francs, (or join a copy of your bank transfer) payable to C.A.I.M.E.N.S. NAME _________________________________ Surname (M / F)__________________________ Address : ______________________________ Organisation (or Private) ______________________________________ ______________________________________ ______________________________________ City(+code)_____________________________ Country _______________________________ E-mail __________________________________ Arrival date ________ Departure date :__________ Extension of accommodation cannot be guaranteed before and after the end of the conference). To be registered at the Conference, you have to pay the general fees for an amount of 1000,- (ff) (proceedings and conference dinner included) and ADD accommodation expenses: Monday 2nd untill Thursday 5th = 4 nights including breakfast and self for lunch or dinner Single room (limited number) : 1100,- (ff) or Double room *: 800,- (ff) Total amount : * Preferably to be shared with; Name, surname: C.T.C.S. - 91 P R O G R A M M E Tuesday (September 3rd) 9:30 - 10:30 P. Freyd, invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 T. Ehrhard & P.Malacaria, Stone Duality for Stable Functions 11:40 - 12:20 R. Amadio, Bifinite Domains: Stable Case Lunch 14:00 - 15:00 R. Tennent , invited talk 15:00 - 1540 A. Edalat & M. Smyth, Categories of Information Systems 15:40 - 16:10 Coffee / Tea Break 16:10 - 16:50 R. Hoofman & H.Schellinx,Collapsing Graph Models by Preorders 16:50 - 17:30 P. O'Hearn, Linear Logic and Interference Control Wednesday (September 4th) 9:30 - 10:30 A. Burroni, Invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 S. Hirokawa, BCK-formulas Having Unique Proofs 11:40 - 12:20 R. Blute, Proof Nets and Coherence Theorems Lunch Afternoon free Conference Dinner Thursday (September 5th) 9:30 - 10:30 E. Moggi, Invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 G. Jarzembski, Programs in Partials Algebras - a Categorical Approach 11:40 - 12:20 B. Jay, Tail Recursion from Universal Invariants Lunch 14:00 - 15:00 T. Coquand, Invited talk 15:00 - 15:40 D. Pavlovic, Constructions and Predicates 15:40 - 16:10 Coffee / Tea Break 16:10 - 16:50 B. Jacobs, E. Moggi & T.Streicher, Relating Models of Impredicative Type Theories 16:50 - 17:30 W. Phoa, Set-theoretic Polymorphism after Robinson Friday (September 6th) 9:30 - 10:30 U. Montanari, Invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 E. Stark, Dataflow Networks are Fibrations 11:40 - 12:20 P. Degano,S. Kasangian & S.Vigna Applications of the Calculus of Trees to Process Description Languages Lunch END OF CONFERENCE ========================================== Subj: Online bibliography for Information and Computation From: dmjones@theory.lcs.mit.edu (David M. Jones) Date: Tue, 13 Aug 91 21:13:57 EDT A bibliography for the journal Information and Computation (formerly Information and Control) covering the years 1982--present is now available via anonymous ftp and mail server from theory.lcs.mit.edu (18.52.0.92). The file is in BibTeX format and is in the file ftp/pub/meyer/iandc.bib. To retrieve the file via ftp, connect to theory using "anonymous" as the login name and "guest" as the password. To retrieve the file via mail server, send a message to the address archive-server@theory.lcs.mit.edu with the following line in the body: send meyer iandc.bib An index of other files can be retrieved with the command send meyer Index More information on the archive-server can be obtained by sending a message with only the word "help" in the body. David M. Jones Editorial Assistant Information and Computation ic-request@theory.lcs.mit.edu ================================ Subj: Logical Frameworks Workshop: Informal Proceedings Date: Wed, 14 Aug 91 15:54:07 ADT From: ccmj@dcs.ed.ac.uk The informal proceedings of the 2nd Workshop on Logical Frameworks (Edinburgh May 1991) are now available by ftp. To obtain the document by ftp use the internet address 129.215.160.150 You should be connected to the machine 'cumbrae' at Edinburgh. Use the login name 'anonymous' (any password accepted), and the file name /export/bra/proc91.dvi.Z (file is compressed). The contents include: F. Barbanera, S.Berardi Witness Extraction in Classical Logic through Normalization D. A. Basin, R. L. Constable Metalogical Frameworks Y. Bertot A Canonical Calculus of Residuals T. Coquand A semantics of evidence for classical arithmetic R. Diaconescu, J. Goguen Logical Support for Modularisation P. Stefaneas G. Dowek A Complete Proof Synthesis Method for the Cube of Type Systems A. Felty A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs G. Huet A case study in Axiomatisation and Proof Development in the Coq Proof Assistant C. Jones Completing the Rationals and Metric Spaces in LEGO Y. Lafont Negation versus Implication S. Matthews, A. Smaill Experience with FS as a Framework D. Basin Theory T. F. Melham A Mechanized Theory of the pi-calculus in HOL D. Miller Unification of Simply Typed Lambda-Terms as Logic Programming C. Murthy Finding the Answers in Classical Proofs: A Unifying Framework T. Nipkow Order-Sorted Polymorphism in Isabelle C. Phillips Well-founded Induction and Program Synthesis Using Proof Plans D. Pym Towards an Algebraic Framework for Defining Sequential Logics J. M. Smith An Interpretation of Kleene's Slash in Type Theory N. Szasz A Machine Checked Proof that Ackermann's Function is not Primitive Recursive Claire Jones ccmj@dcs.ed.ac.uk ===================================== Subj: Free categories Date: Wed. Aug. 14 From: "P. B. Johnson" The underlying functor : cat ----> graph, from small categories to small graphs, is tripleable. I would like to consider the same question over an arbitrary topos, and would appreciate any hints from topos theorists. It seems to me that, given a topos E, the underlying functor: cat(E) ----> graph(E) is "equationally defineable", that is to say, each internal category in E can be described by (in fact finitary) operations on some object of graph(E), subject to some equations. Then cat(E) ----> graph(E) is tripleable if and only if it has a left adjoint. It seems that constructing free categories over graphs requires some kind of countable colimits, which I don't imagine are always available. Perhaps the existence of a natural numbers object (which seems to be in some sense the most primordial of infinite colimits that a topos might possess) ensures the existence of free categories. Can such toposes with free categories be characterized? Thank you, Paul. ================================= Date: Wed, 14 Aug 91 15:54:29 ADT Subj: Online bibliography for TACS'91 A bibliography for the upcoming International Conference on Theoretical Aspects of Computer Software (TACS'91) is now available via anonymous ftp and mail server from theory.lcs.mit.edu (18.52.0.92). The file is in BibTeX format and is in the file ftp/pub/meyer/tacs91.bib. Also available are tacs91.tex and tacs91.ps, which are LaTeX and PostScript versions of the file for those who prefer that format. To retrieve the file via ftp, connect to theory using "anonymous" as the login name and "guest" as the password. To retrieve the file via mail server, send a message to the address archive-server@theory.lcs.mit.edu with the following line in the body: send meyer tacs91.bib An index of other files can be retrieved with the command send meyer Index More information on the archive-server can be obtained by sending a message to the archive-server with only the word "help" in the body. David M. Jones Secretary to Professor Albert R. Meyer ======================================== Subj: Re: Logical Frameworks Workshop: Informal Proceedings From: wald@theory.lcs.mit.edu (David Wald) Date: Thu, 15 Aug 91 11:26:07 EDT >Subject: Logical Frameworks Workshop: Informal Proceedings >From: ccmj@dcs.ed.ac.uk > >The informal proceedings of the 2nd Workshop on Logical Frameworks >(Edinburgh May 1991) are now available by ftp. For readers who are closer to Massachusetts than to Edinburgh, the proceedings are also available by anonymous ftp from theory.lcs.mit.edu, in the file pub/lf/1991/proc91.dvi.Z (the file is compressed). The file can also be retrieved from our archive server by sending the line send lf 1991/proc91.dvi.Z to archive-server@theory.lcs.mit.edu. The file will be uuencoded and shipped in pieces. You can send the line "help" instead for further information on using the archive-server. -David Wald ================================= Subj: Re: free categories Date: Sat, 17 Aug 91 16:57:03 ADT Two replies to Paul Johnson's question follow. I returned from vacation today and take the opportunity to thank my colleague Daniel Perron for minding the mailing list during this absence and several others. Bob Rosebrugh +++++++++++++++++++++++++++++++++ From: David N Yetter Date: Fri, 16 Aug 91 11:53:57 EDT Re : Free categories Toposes with free categories are precisely toposes with NNO: in particular TFAE: 1) NNO 2) the forgetful functor from the category of internal monoids is tripleable 3) the forgetful functor from the category of internal categories to the category of internal graphs is triplable The equivalence of 1) and 2) is Theorem 6.41 in Johnstone's Topos Theory. That 3) implies 2) is immediate. That 1) implies 3) follows from the fact that Finite Limit Theories (aka Essentially Algebraic Theories) have tripleable categories of models over any topos with NNO (I don't recall a reference on that last result, but I suspect it must be in Barr and Wells Toposes, Triples and Theories). Re: e-mail address As you can see from the header, my e-mail address is now dyetter@math.ksu.edu Best Thoughts, David Yetter +++++++++++++++++++++++++++++++++++++++ Date: Fri, 16 Aug 91 16:26:54 EDT From: "Andreas R. Blass" This is in reply to Paul Johnson's question about constructing free categories over graphs in elementary topoi (with natural numbers object). Your own work on the indexed adjoint functor theorem is relevant to this(see note from Bob R. below), as are the following: B. Lesaffre, Structures algebriques dans les topos elementaires, C.R. Acad. Sci. Paris, 277 (1973) A663-666. D. Schumacher, Absolutely free algebras in a topos containing an infinite object, Canad. Math. Bull. 19 (1976) 323-328. Later, I wrote a paper (Words, free algebras, and coequalizers, Fund. Math. 117 (1983)117-160) showing that the usual set-theoretic existence proof works in the internal logic of topoi. (The emphasis there was on varieties with infinitary operations, and things can be simplified in the finitary case.) Andreas Blass ++++++++++++++++++++++++ The article of mine Andreas refers to is: On algebras defined by operations and equations in a topos, JPAA 17(1980) 203-221 but David's reply answers the question completely ... Bob Rosebrugh ======================================== Subj: Query on initial algebras ... Date: Mon, 19 Aug 91 08:43:49 EDT From: barr@triples.math.mcgill.ca (Michael Barr) Someone at the recent meeting in Durham mentioned that he had shown that the canonical map from the intial algebra of some endofunctor on Set to the terminal coalgebra was always monic. Is that ``someone'' on the distribution list and can he communicate with me. Michael ========================================== Subj: Finite Limit Theories Date: Sun, 18 Aug 91 20:09:22 -0400 From: cfw2@po.CWRU.Edu (Charles F. Wells) David Yetter's comments concerning toposes with free categories contains a misstatement. It is not true that finite limit theories have tripleable categories of models over any topos with NNO. For example, the category of small categories is not regular, hence not tripleable over Sets for any underlying functor (p. 120 of Triples, Toposes, and Theories). --Charles Wells ================================= Subj: Partial morphisms in toposes From: Date: 23 Aug 91 16:15 What is known about partial morphisms in toposes? A partial morphism from A to B is a morphism from a subobject of A to B. Composition needs certain pullbacks to exist, which they do in a topos, so every topos has a category of partial morphisms. What is known about it? E.g. it isn't a topos, since its initial and terminal objects are the same. Failing that, does it have other nice properties, e.g. limits and colimits? Johnstone's book touches on the subject in chapter 1: all partial morphisms from A to B are representable by (ordinary) morphisms from A to an object B~, and the mapping from B to B~ is a functor with a natural transformation from the identity to that functor. Monads seem about to make an entrance (is there a product transformation from B~~ to B~?), but he doesn't explore the matter any further. Goldblatt's book and Fourman's chapter in the Handbook of Mathematical Logic cover the same ground. What else is known? -- Richard Kennaway SYS, University of East Anglia, Norwich, U.K. Internet: jrk@sys.uea.ac.uk uucp: ...mcsun!ukc!uea-sys!jrk ============================================ Subj: latest update to CTCS Date: Mon, 26 Aug 91 15:18:38 EDT From: barr@triples.math.mcgill.ca (Michael Barr) \documentstyle[12pt]{article} \input diagram \newcounter{lister} \newenvironment{labeledlist}[1] {\begin{list}{{\rm#1\arabic{lister}. }}{\usecounter{lister} }}%begin text {\end{list}}% \def\blist#1{\begin{labeledlist}{#1}} \def\elist{\end{labeledlist}} \newcommand{\afour}{\oddsidemargin 18pt\evensidemargin 18pt \textwidth 420pt\textheight 45\baselineskip\advance\textheight by \topskip} %% Kludge to make article.sty width correct for A4 %% This works only for article.sty using the standard margin given \textheight8in \headsep 0in \headheight0in \topmargin0in \textwidth 6.5in \oddsidemargin0in \mathchardef\Csc="0243 \mathchardef\Dsc="0244 \mathchardef\Esc="0245 \mathchardef\Gsc="0247 \mathchardef\Ssc="0253 \def\lncs#1{Lecture Notes in Computer Science {\bf#1}} \def\springer{Sprin\-ger-Ver\-lag} \def\mathrm#1{\expandafter\def\csname#1\endcsname{\mathop{\rm#1}\nolimits}} \def\mathbf#1{\expandafter\def\csname#1\endcsname{\mathop{\rm\bf#1}\nolimits}} \mathrm{id} \mathrm{eval} \mathrm{mult} \mathrm{proj} \mathbf{R} \mathbf{Set} \mathbf{Cat} \mathbf{Mod} \mathbf{Rel} \mathrm{Hom} \def\op{{}^{\rm op}} \let\x=\times \def\o{\mathop{\raise.3ex\hbox{$\scriptscriptstyle\circ$}}} \mathcode`\<="4268 %left delimiter \mathcode`\>="5269 %right delimiter \def\inc{\subseteq} \def\iso{\cong} \def\[{[\kern-1.3pt [} \def\]{]\kern-1.3pt ]} \begin{document} %\afour \title{Category Theory for Computing Science: \\ Update} \author{Michael Barr and Charles Wells} \maketitle We intend to maintain our text, {\bf Category Theory for Computing Science}, Prentice Hall, 1990 (ISBN 0-13-120486-6), % Our text, {\bf 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: \ref{errors}: A list of errors discovered so far. \ref{newtext}: Additional examples, problems and pointers to the literature. \ref{refs}: Additions and updates 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. {\footnotesize \begin{center}\begin{tabular}{ll} Michael Barr & Charles Wells \\ Department of Mathematics & Department of Mathematics \\ Burnside Hall & Case Western Reserve University \\ McGill University & University Circle \\ 805 Sherbrooke St. West & Cleveland, OH 44106-7058, USA \\ Montr\'eal, P. Q., Canada H3A 2K6 & cfw2@po.cwru.edu \\ barr@triples.math.mcgill.ca & \end{tabular}\end{center} } \newpage \section{Errors}\label{errors} \begin{description} \item?p. xv? In the Chapter Dependency Chart, there should be a diagonal line from Chapter 5 to Chapter 7. \item?p. 23? (Jean-Pierre Marquis). SM--2 should read, ``If $m$, $n\in S$, then $mn\in S$''. \item?p. 31? (Jean-Pierre Marquis). S--1 should say $\Dsc_0\inc\Csc_0$ and $\Dsc_1\inc\Csc_1$. \item?p. 54? (Andrew Malton). Line 8: read ``$g \o h = f$'' for ``$h \o g = f$'' \item?p. 56? (Han Yan). Line 7: $g:C\to C$ should be $g:B\to C$. \item?p. 57? (Han Yan). Line 1: $f:A\to A$ should be $f:C\to A$. \item?p. 57? (Han Yan). Line 2: $g:B\to C$ should be $g:B\to D$. \item?p. 63? (Jean-Pierre Marquis). Last line: $TF(S)$ should be $FT(S)$. \item?p. 64? (Jean-Pierre Marquis). Definition 3.3.2, line 4: $G(f)$ should be $F(g)$. \item?p. 66? (Jean-Pierre Marquis). Section 3.3.10, line 2: ``is to said'' should be ``is said''. \item?p. 73? (Jean-Pierre Marquis). The reference to Wells ?1989? should be deleted. \item?p. 74? (Jean-Pierre Marquis). The reference to Wells ?1989? should be to Wells ?1990? (see updated reference in Section~\ref{refs} of this document). \item?p. 79? Line 3: ``diagram'' should be capitalized. \item?p. 79? (Al Vilcius). Line 7: replace ``$\id_i$'' by $\id_{D_i}$. \item?p. 83? (Andrew Malton). Line --7: change ``of shape $U$'' to ``of shape ${\cal U}$''. \item?p. 87? (Al Vilcius). In Theorem 4.2.20, line 2 replace ``$\Csc$'' by ``$\Gsc$'. In the last line replace ``$\Mod(\Gsc,\Csc)$'' by ``$\Mod(\Gsc,\Dsc)$''. \item?p. 90? (Andrew Malton). Line 5: change ``$f: {\cal E}\to V{\cal G}_1$'' to ``$f: {\cal E} \to {\cal G}_1$'' \item?p. 92? In Proposition 4.3.12 and its proof, the letter $C$ (not the script $\Csc$) 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). \item?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.) \item?p. 101? (Jean-Pierre Marquis, Han Yan). In the figure, $\Hom(f,C)$ should be $\Hom(C,f)$. \item?p. 102? ``The'' not ``the'' in line 7. \item?p. 103? (Al Vilcius). Change ``set'' to ``collection'' in the second line of 4.6.2 and the sixth line of 4.6.3. ?We are using ``collection'' as an informal synonym for ``class'', without getting into set theory.? \item?p. 103? Between the fourth and fifth lines of 4.6.3, add the following: ``We write $M:\Ssc\to\Csc$ for such a model. This use of the same symbol to denote both the sketch homomoprhism and the graph homomorphism is a bit of notational overloading that in practice is always disambiguated by context.'' \item?p. 105? The sentence before 4.6.9 has a misplaced parenthesis. It should read ``If you want a sketch for graphs which have a loop on every node, but not a distinguished loop (so that a homomorphism takes the loop on $n$ to some loop on $\alpha N(n)$, but it does not matter which one), you will have to wait until we can study regular sketches in 9.4.5." \item?p. 105? (Jean-Pierre Marquis). LT--1, second line: $a$ should be $f$. \item?p. 108? (Al Vilcius). Change ``set'' to ``collection'' in line 3 of 4.7.2. \item?p. 137? (Jean-Pierre Marquis). Line 3 of proof of Theorem 5.5.5: $u_i\o s$ should be $s\o u_i$. \item?p. 173? (Jean-Pierre Marquis). The second line of N--5 should be $$f_1\x f_2\x\cdots\x f_n:a_1\x a_2\x\dots\x a_n\to b_1\x b_2\x\cdots\x b_n$$ (no angle brackets around the arrow). \item?p. 184? (Jean-Pierre Marquis). In the next to last line of Example 7.7.3, ``sort $\tau$'' should be ``sort $\sigma$''. \item?p. 186? (Jean-Pierre Marquis). Line 4 of Example 7.7.7: ``Let $u$ be the term $x$ of arity $\sigma$ and sort `$\sigma$' '' should be changed to ``Let $u$ be the term $x$ of arity `$\sigma$' and sort $\sigma$''. \item?p. 186? (Jean-Pierre Marquis). In line 8 of Example 7.7.7, the path of $u$ is $\id:\sigma\to\sigma$. \item?p. 190? (Nico Verwer).There is a series of errors in FE--5 to FE--8. The correct versions are as follows: \blist{FE--}\setcounter{lister}{4} \item$ + \o < {\id} , 0 \o <> > = + \o < 0 \o <> , {\id} > = \id : f \to f$ \item $ * \o < j , {j} \o 1 \o <> > = * \o < {j} \o 1 \o <> , j > = j : u \to f$ \item $ + \o {< \id , - >} = + \o {< - , \id >} = 0 \o <> : f \to f$ \item $ * \o (j \times j) \o {< \id , ()^{-1} >} = * \o (j \times j) \o {< ()^{-1} , \id >} = 1 \o <> : u \to u$ \elist \item?p. 208? (Al Vilcius). Top diagram should have a $B$, not $C$ in the SE corner. The fourth line should say that $p_2$, not $p_1$ is the pullback of $f$ along $g$. \item?p. 227? (Jean-Pierre Marquis). Line 2 of Exercise 2 should have $B_i$ for $B$ and $C_i$ for $C$. \item?p. 228? (Al Vilcius). Last line: Word ``be'' is missing. \item?p. 232? (Jean-Pierre Marquis). The first line of the second paragraph of section 9.1.5 has a font error (it is not mathematically wrong): the second parenthesized expression should read $(D,\mult_D,{\rm unit}_D)$ \item?p. 255? (Al Vilcius). Line --5: Replace ``cleavage'' by ``opcleavage''. \item?p. 256? (Al Vilcius). Line --8: the expression has misplaced brackets. Should be $$Fg?Ff(u)? \o\kappa(g,Ff(X))\o\kappa(f,X)$$ \item?p. 256? (Al Vilcius) Line --2 should be ``functors $\Csc\op\to\Cat$.'' \item?p. 258? (Al Vilcius). Definition 11.2.3: GS--1 should be ``object of $G_0(\Csc,F)$''. \item?p. 259? (Al Vilcius). Line 8 should read ``$x'=Ff(x)$''. In paragraph starting line 11, orientation of $G_0(\Csc,F)$ requires the functor $G_0(F)$ to be the projection on the second coordinate, not first. \item?p. 261? (Al Vilcius). In Theorem 11.2.9, first projection should be second as above. \item?p. 263? (Jean-Pierre Marquis and Han Yan). Line 15: Change ``then $F(C)$ and $G(C)$'' to ``then $F(C)$ and $F(D)$''. \item?p. 264? (Al Vilcius). In Definition 11.3.4, FI--1, replace ``$P:\Esc\to\Cat$'' by ``$P:\Esc\to\Csc$''. \item?p. 272? (Jean-Pierre Marquis). Line --4: The reference to 12.1.2 should be to 12.1.1. \item?p. 281? (Jean-Pierre Marquis). In Exercise 1, $f(S_0)\inc T_0$ should be $f_{*}(S_0)\inc T_0$. \item?p. 287? (Jean-Pierre Marquis). The second line should read $$\Hom_{\Csc/A}(u\x v,w) =\Hom_{\Csc/A}(\Sigma_u(u^*(v)),w)$$ \item?p. 302? Line --4ff should say, ``In particular, ${\rm\bf Cat}$ is enriched over ${\rm\bf Cat}$ itself, since its hom sets are themselves categories (with the arrows as objects and the natural transformations as arrows) and the hom functors preserve the extra structure.'' \item?p. 303? (Jean-Pierre Marquis). In the second line of SP--4, the $E$ should be $A$. \item?p. 307? (Jean-Pierre Marquis). In line 5 of the second paragraph, $(a_0, a_1, a_2, a_4\ldots)$ should be $(a_0, a_1, a_2, a_3\ldots)$. \item?p. 319? (Jean-Pierre Marquis). $G_0$ and $G$ in the diagram should be $\Gsc_0$ and $\Gsc$. \item?p. 331? (Jean-Pierre Marquis). Line 2: ``That of (C)'' should be ``That of (c)''. \item?p. 333? (Jean-Pierre Marquis). In line 4 of the paragraph after REAL--2, $\?fa_1=fa_2\?$ should be $\?\phi a_1=\phi a_2\?$. \item?p. 335? In the fourth paragraph of the discussion of the internal category of modest sets, the sentence, ``We want to describe this subset as consisting of those relations that are symmetric and transitive'', should have the following phrase added: ``and double negation closed''. \item?p. 345? Line 2 of the answer to exercise 12.a: the last letter should be ``B'', not ``b''. \item?p. 357? (Jean-Pierre Marquis) In the top diagram, one of the arrows from BOOLEAN to BOOLEAN should be reversed. \item?p. 358? (Jean-Pierre Marquis) In the answer to Exercise 5, delete the phrase ``$\beta$ satisfies''. \item?p. 365? In the answer to problem 8, $\beta C:\Hom(C,C)\to F(C)$. \item?p. 368? (Jean-Pierre Marquis) In the second line of the answer to Exercise 3, the $B$'s should be $C$'s. \item?p. 370? (Jean-Pierre Marquis) Line --2: Both occurrences of $f$ should be $F$. \item?p. 372? (Jean-Pierre Marquis) In the answer to Exercise 1, the arguments to $f$ are reversed. The end of the sentence should read: ``$\ldots$by letting $f(b,0)=f_0(b)$ and having defined $f(b,i)$ for $i\le n$, define $f(b,n+1)=t(f(b,n))$''. \item?p. 373? (Jean-Pierre Marquis) In the answer to Exercise 1 of Section 6.1, every occurrence of $(\lambda\o\eval)$ should be $\lambda(\eval)$. \item?p. 380? (Jean-Pierre Marquis) In the diagram in the answer to Exercise 2, the upper right arrow (labeled $<\id,e\o<>>$) should go in the opposite direction. \item?p. 381? (Jean-Pierre Marquis) The answer to number 3 is confused. Here is the entire answer rewritten: We give the answer for the case of real vector spaces; the other is similar. We assume the real number field $\R$ as a given structure. We suppose, for each $r\in R$, a unary operation we will denote $r^*:s\to s$. We require a unit element $z:1\to s$ for the operation $c$ and a diagram similar to the previous exercise to say that $z$ is the unit element. The following diagram says that $c$ is commutative: $$ \Atriangle?s\x s`s\x s`s;<\proj_2,\proj_1>`c`c? $$ We have to add a unary negation operator $n:s\to s$ together with a diagram to say it is the negation operator: $$\bfig \setsqparms?0`1`1`1;1500`500? \putsquare(0,0)?s`s\x s`1`s;`<>`c`z? \putmorphism(0,500)(1,0)?\phantom{s}`s\x s`<\id,\id>?{750}1a \putmorphism(750,500)(1,0)?\phantom{s\x s}`\phantom{s\x s}`\id\x n?{750}1a \efig$$ In addition, we need diagrams that express the following identities: \begin{eqnarray*} 0^*(x)&=&z\\ r^*(c(x,y))&=&c(r^*(x),r^*(y))\\ (r+s)^*(x)&=&c(r^*(x),s^*(x))\\ 1^*(x)&=&x\\ r^*(s^*(x))&=&(rs)^*(x) \end{eqnarray*} We give, for example, the diagram required to express the third of the equations above: $$ \settriparms?1`1`1;600? \qtriangle?s`s\x s`s;`(r+s)^*`c? $$ \item?p. 386? (Jean-Pierre Marquis) Line 4 of answer to 3b: $D_m$ should be $Dm$. \item?p. 402? (Jean-Pierre Marquis). The answer to Exercise 6 of 12.2 (page 281) uses Theorem 12.3.6, which comes in a later section. Here is an answer using only the definition of adjoint: If the functor defined in 12.2.4 has a left adjoint $F$, then by definition of left adjoint there is for any set $X$ an arrow $\eta X:X\to FX\x A$ with the property that for any function $f:X\to Y\x A$ there is a unique function $g:FX\to Y$ for which $(g\x A)\o \eta X=f$. Now take $Y=1$, the terminal object (any one element set). There is only one function $g:FX\to 1$, so there can be only one function $f:X\to 1\x A\iso A$. If $A$ has more than one element, this is a contradiction. \item?p. 431? The word ``relation'' should also be indexed on p. 21. \end{description} \section{Additional text}\label{newtext} \begin{description} \item?p. xiii? (First paragraph). Another book that develops most of the topics further, except sketches, is ?Freyd-Scedrov, 1990?. (Additional comment). The reader may find the following discussions of the uses of category theory in computing science useful: The tutorials in ?Pitt, Abramsky, Poign\'e and Rydeheard, 1986?, and ?Goguen, 1991?. \item?p. xiii? (Second paragraph).Another collection of papers is ?Pitt, Rydeheard, Dybjer, Pitts and Poign\'e, 1989?. \item?p. 17? ?Additional example of category.? Let $\alpha$ be a relation from a set $A$ to a set $B$ and $\beta$ a relation\index{relation} from $B$ to $C$ (see 1.3.4). The {\bf composite} $\beta\o\alpha$ is the relation from $A$ to $C$ defined as follows: If $x\in A$ and $z\in C$, $(x,z)\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 {\bf category of sets and relations} has sets as objects and relations as arrows. \item?p. 53? Add to third paragraph of 3.1.7: Freyd-Scedrov ?1990?, pages 9 and 19, give a formal definition of forgetful functor. \item?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)\mid (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)\mid 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. \item?p. 96? The applications of 2-categories have mushroomed and include ?Ji-Feng and Hoare, 1990?, ?Moggi, 1989? and ?Power, 1989? in addition to the papers already listed. \item?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. \item?p. 158? The assumption that every object in a cartesian closed category has fixed points is inconsistent with other desirable assumptions on the category. See ?Huwig-Poign\'e, 1990?. \item?p. 213? Freyd-Scedrov ?1990? have a different but closely related definition of ``regular''. If a category is regular in our sense it is regular in theirs, and if it is regular in their sense and has coequalizers, then it is regular in our sense. \item?p. 257? Besides ?Coquand, 1988?, Moggi ?1989? also uses the Grothendieck construction in modeling polymorphism. \item?p. 283? Another reference for the Adjoint Functor Theorem (with a different point of view) is ?Freyd-Scedrov, 1990?, pages 144-146. \item?p. 287? Just before the exercise: See also ?Ehrhard, 1989?. \item?p. 301? Some applications of triples (monads) in computing science are in ?Moggi, 1991?, ?Power, 1990? \item?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. \item?p. 325? Goguen ?1990? has developed a sheaf semantics for object oriented programs. \end{description} \section{Additional references}\label{refs} \fontdimen2\twlrm=4.3pt% space instead of 3.91663 \fontdimen3\twlrm=4.2pt%stretch instead of 1.95831 \fontdimen4\twlrm=1.7pt%shrink instead of 1.30554 \begin{list}{}{\leftmargin 8mm \itemindent -8mm \parsep 0pt \itemsep 0pt plus 1pt} \def\itm{\item??} \itm \mbox{T. Ehrhard}, {\it Dictoses}. In {\bf Category theory and computer science}, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors. \lncs{389}, \springer, 1989. \itm \mbox{P. Freyd and A. Scedrov}, {\bf Categories, Allegories}. North-Holland Mathematical Library {\bf39}, North-Holland, 1990. \itm \mbox{J.\ Goguen}, {\it Semantics of concurrent interacting objects}. Preprint, Programming Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD, England. \itm \mbox{J. Goguen}, {\it A categorical manifesto}. Mathematical Structures in Computer Science {\bf 1}, 1991, 49--68. \itm \mbox{C.\ A.\ R.\ Hoare}, He Jifeng and C. Martin, {\it Pre-adjunctions in order-enriched categories}. Preprint, Programming Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD, England. \itm \mbox{He Ji-Feng and C. A. R. Hoare}, {\it Categorical semantics for programming languages}. In M.\ Main {\it et al.}, eds., {\bf Mathematical Foundations of Programming Semantics}. \lncs{442}, \springer, 1990, 402--417. \itm\mbox{H. Huwig} and A. Poign\'e, {\it A note on inconsistencies caused by fixpoints in a cartesian closed category}. Theoretical Computer Science {\bf73}, 1990, 101--112. \itm \mbox{E. Moggi}, {\it A category-theoretic account of program modules}. Mathematical Structures in Computer Science {\bf 1}, 1991, 103--139. % In {\bf Category theory and computer science}, D. H. Pitt, D. % E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors. % \lncs{389}, \springer, 1989. \itm \mbox{D.\ Pitt}, D. Rydeheard, P. Dybjer, A. Pitts and A. Poign\'e, eds. {\bf Category theory and computer science}. \lncs{389}, \springer, 1989. \itm \mbox{A.\ J.\ Power}, {\it An abstract formulation for rewrite systems}. In {\bf Category theory and computer science}, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors. \lncs{389}, \springer, 1989. \itm \mbox{A. J. Power}, {\it An algebraic formulation for data refinement}. In M.\ Main {\it et al.}, eds., {\bf Mathematical Foundations of Programming Semantics}. \lncs{442}, \springer, 1990, 390--401. \itm \mbox{R.\ Seely}, {\it Modelling computations: a $2$-categorical framework.} In {\bf Proceedings of the Conference on Logic in Computer Science}, IEEE, 1987. ?Corrected reference?. \itm \mbox{P.\ Taylor}, {\it Quantitative domains, groupoids and linear logic}. In {\bf Category theory and computer science}, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors. \lncs{389}, \springer, 1989. \item \mbox{C.\ Wells}, {\it A generalization of the concept of sketch}. Theoretical Computer Science {\bf 70} (1990), 159-178. ?Updated reference?. \pagebreak?3? \end{list} \end{document} ============================= Subj: Online bibliography for Symposium on Logic in Computer Science Date: Mon, 26 Aug 91 15:21:36 EDT From: dmjones@theory.lcs.mit.edu (David M. Jones) An online bibliography for the Annual IEEE Symposium on Logic in Computer Science is now available via anonymous ftp and mail server from theory.lcs.mit.edu (18.52.0.92). The bibliography is in BibTeX format and is in the file pub/meyer/lics.bib. To retrieve the file via ftp, connect to theory using "anonymous" as the login name and "guest" as the password. To retrieve the file via mail server, send a message to the address archive-server@theory.lcs.mit.edu with the following line in the body: send meyer lics.bib An index of other available files can be retrieved with the command send meyer Index More information on the archive-server can be obtained by sending a message with only the word "help" in the body. David M. Jones Secretary to Professor Albert R. Meyer, General Chair, LICS =============================== Subj: Re: Partial morphisms in toposes Date: Wed, 28 Aug 91 10:55:43 +0200 From: Thomas Streicher The subject of partial morphisms in a topos has been dealt with extensively in Adam Obtulowicz's Theses which has appeared in Dissertationes Mathematicae. He gives an essentially algebraic definition of what is a category of partial maps in a topos. There is a lot of work on categories of partial maps : Robinson & Rosolini (in Inform. & Comp.) Curien & Obtulowicz (also in Inf. & Comp ) Carboni (Cahiers de Topologie et Geometrie Differentielle) the Theses of Rosolini and Moggi etc. If you are interested not in arbitrary partial maps but in those whose domain of definition is semidecidable you must work with so called dominions. This is a class of subobjects of a topos which contains all iso, is closed under composition and stable under pullpacks along arbitrary maps. The notion of dominion already appears in Rosolini's Thesis. Most prominently it also has been explained by Alex Heller in his paper 'Dominical Categories' which has appeared in J.S.L. Recently Barry Jay has been working on categories of partial maps from the point of view of order enriched categories. I think there are some Edinburgh LFCS repo rts on that. Thomas Streicher ======================== Subj: Re: Finite Limit Theories Date: 27 Aug 91 14:02 From: Steven John Vickers To try to clarify the remarks of David Yetter and Charles Wells on essentially algebraic theories, let me pass on an extract from the paper "Preframe Presentations Present" which I recently wrote with Peter Johstone (for "CT '90", to appear in Springer Lecture Notes in Mathematics). I ought to say that the section from which this extract is taken, which was intended to be a brief yet helpful account of essentially algebraic theories, is a distillation of Peter's knowledge rather than mine. "For a small essentially algebraic theory T, the forgetful functor from T-models to Set (or Set^n if T is many-sorted) has a left adjoint, just as in the algebraic case: the free T-model on a set X is constructed in the usual way as the set of words (i.e. terms) in the elements of X, modulo T-provable equality. The adjunction will not be monadic unless T is algebraic, but it will be possible to factor it as a tower of monadic adjunctions in the style of MacDonald and Stone ("The tower and regular decomposition", pp. 197-213 in Cahiers Top. Geom. Diff 23 (1982))." I presume, again without being an expert in these fields, that for finitary theories this all works over arbitrary elementary toposes with NNO. Steve Vickers