December 2002 - Categories - categories.org.au

New mail list
by Bill Rowan 24 Dec '02

24 Dec '02

Hello everyone, I have finally done what I said I would do a few years ago, and started up an email list, at yahoogroups, centered around Beck modules. (If A is an algebra in a variety V, then the category of Beck modules over A [and in V] is the category of abelian group objects in the comma category (V,A). At least, that is how category theorists define it. I have some other ideas about it that lead to an equivalent category.) There was some interest in such a list at the time, I think it was around 9 or 10 years ago. I have found managing my univalg list (for universal algebra) to be easy enough that I want to start this list also. The univalg list includes mostly universal algebraists, not all of whom are interested in things with a category-theoretic flavor. I am, however, inviting the members of that list to join this new one. To subscribe, send an email to beckmodules-subscribe(a)yahoogroups.com. I have set it up so that I have to approve any subscriptions, in order to avoid certain spammers who seem to have automated the process of subscribing. Your email address will be visible only to other members of the list. For the greatest access to the features of the group, you can get a yahoo id by going to http://groups.yahoo.com and registering. Or, if you have a yahoo id already, you can easily join the beckmodules group. The service is free, being supported by advertising which is tolerably nonintrusive. Possible topics for posts include the controversy about how best to define Beck modules, cohomology theories (such as Jon Beck explored in his thesis), the related theory of enveloping ringoids (which I introduced in my thesis), connections with universal algebra and commutator theory (invented by JDH Smith) and lots of other ideas that I probably never heard of but am looking forward to hearing about. Best regards, Bill Rowan 29-Dec-2002 17:03:56 -0400,4542;000000000001-00000000

1 0

ETAPS03 - grants
by Konferencja ETAPS'03 23 Dec '02

23 Dec '02

We apologize if you receive multiple copies of this message. ********************************************************** *** ETAPS 2003 *** *** APRIL, 5-13, 2003 *** *** WARSAW, POLAND *** *** *** *** http://www.mimuw.edu.pl/etaps03/ *** ********************************************************** ============================================================================= EC GRANTS FOR YOUNG RESEARCHERS AND ETAPS GRANTS FOR PARTICIPATION ============================================================================= Important dates: Application: before January 31st, 2003 Notification: before February 15th, 2003 A grant from the European Commission, High-Level Scientific Conferences, has been approved for supporting the participation to the Conference of young researchers (up to the age of 35 years at the time of the conference) who are nationals of a Member State or an Associated State, and who are actively participating in one of the ETAPS 2003 main conferences or in a satellite event. The organizers offer additional limited support possibilities for ETAPS 2003 participants who are not eligible for the EC-HSC grants above. So, if you need some financial support, apply under the scheme described below. Financial support may cover (up to 100% of): - ETAPS main conferences and satellite events registration fees - travel expenses - subsistence and accommodation costs in Warsaw For applying, please send an e-mail to etaps03-grants(a)mimuw.edu.pl The email should contain the following information about the applicant: name, gender, birth date, nationality, current student/working position and affiliation, and contact information (email address, fax, postal address). Please also state duration and the planned dates of your stay in Warsaw for ETAPS 2003, as well as the character of participation in ETAPS 2003 (in particular: please indicate if you are an author or a co-author of an accepted paper at one of the main conferences, an author or a co-author of a presentation at one of the satellite workshops, tutorials, etc). Those who wish to apply for refund of travel costs must additionally send: - an estimate of travel expenses (with the above application), and - not later than March, 24th 2003, a copy of the ticket with explicitly stated cost of the ticket. In case the ticket does not contain an explicit cost, an invoice of the purchase of the ticket should be sent as well. The copy of the ticket or an invoice should be faxed at the number +4822-5544400. Please bring the originals with you to Warsaw. Eligible costs are the cheapest airfare in economy class, or a second class train ticket, or a bus ticket. Grant applicants should register at the web site of ETAPS 2003 <tu URL>, as all other participants. However, do not forget to mark that you're applying for support from ETAPS 2003 organizers, and refrain from paying the participation fees until we send you our decision concerning the support. If you apply for support to cover your registration and you are not granted this support, your registration fee will be calculated according to the date of your registration, and not that of your actual payment, as long as you pay the fee within 7 days after your application was rejected. In any case you should yourself take care of your hotel reservation. If you book your hotel using the service provided via the conference web page you should also pay the hotel deposit as required.

1 0

[CSL03] Call For Papers: Computer Science Logic 2003
by csl03 21 Dec '02

21 Dec '02

[ We apologize for the inevitable multiple copies of this announcement. Please see the note on mailing lists at the end. ] [ There is a PostScript copy of this Call at http://www.logic.at/csl03/CSL03-cfp.ps for display on notice boards. ] First Call for Papers Annual Conference of the European Association for Computer Science Logic and 8th Kurt Goedel Colloquium CSL'03 & KGC 25 August afternoon - 30 August 2003, Vienna, Austria Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The Kurt Goedel Colloquium (KGC) is the biennial conference of the Kurt Goedel Society (KGS). The joint conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Suggested topics of interest include: automated deduction and interactive theorem proving; constructive mathematics and type theory; equational logic and term rewriting; fuzzy logic; modal and temporal logics; computational proof theory; linear logic; finite model theory; bounded arithmetic; logical aspects of computational complexity; higher order logic; logic programming and constraints; lambda and combinatory calculi; logical foundations of programming paradigms; model checking; specification, extraction and transformation of programs; categorical logic and topological semantics; game semantics; domain theory; database theory. A lecture, jointly invited by CSL'03 & KGC and ESSLLI (European Summer School in Logic Language and Information) will be given by Sergei Artemov (CUNY, USA) Additional invited lectures will be given by (tentative): Bruno Buchberger (Johannes Kepler University, Austria) Dov Gabbay (King's College London, England) Helmut Veith (Vienna University of Technology, Austria) Nikolai Vorobjov (University of Bath, England) Andrei Voronkov (University of Manchester, England) The following tutorials are planned: Verification of infinite state systems (Ahmed Bouajjani, University of Paris 7, France) Computational epsilon calculus (Georg Moser, University of Muenster, Germany, and Richard Zach, University of Calgary, Canada) Quantifier elimination (Nikolai Vorobjov, University of Bath, England) Winning strategies and controller synthesis (Igor Walukiewicz, University of Bordeaux, France) The proceedings of the conference will be published in the Springer Lecture Notes in Computer Science series. Submitted papers must describe work not previously published. They must not be submitted concurrently to another conference with refereed proceedings. Research that is already submitted to a journal may be submitted to CSL, provided that (a) the PC chair is notified in advance that this is the case, and (b) it is not scheduled for journal publication before the conference. Submissions authored or coauthored by members of the Programme Committee are not allowed. Papers should preferably be submitted either in LNCS format or in 12pt A4 format. Papers should not exceed 14 pages; full proofs may appear in a technical appendix which will be read at the reviewers' discretion. The title page must contain: title and authors; physical and e-mail addresses; identification of corresponding author, if not the first author; an abstract of no more than 200 words; a list of keywords. The key dates for the conference are: Submission: The submission process is in two stages, both with strict deadlines: 31 March 2003 for the title and abstract, and 7 April 2003 for the full text. Notification: 2 June 2003 Final copy due: 18 June 2003 Prospective authors should check the conference Web page for any subsequent changes to these dates. Further information on all aspects of the conference will be found on the conference Web page: http://www.logic.at/csl03/ Programme Committee: Matthias Baaz (chair) Arnold Beckmann Lev Beklemishev Maarten de Rijke Chris Fermueller Didier Galmiche Harald Ganzinger Erich Graedel Petr Hajek Martin Hyland Reinhard Kahle Helene Kirchner Daniel Leivant Johann Makowsky (co-chair) Jerzy Marcinkowski Franco Montagna Robert Nieuwenhuis Michel Parigot Jeff Paris Helmut Schwichtenberg Jerzy Tiuryn [ Note on mailing lists. The To: header in each copy of this message contains the entry in our mailing list to which it was sent. If you wish the entry to be removed from our list, or have any problem with the mail, please contact csl03+calls(a)logic.at . ] 26-Dec-2002 11:38:04 -0400,2431;000000000001-00000000

1 0

Rene Lavendhomme
by Francis Borceux 21 Dec '02

21 Dec '02

It is with great sadness that I announce the death of our colleague Rene Lavendhomme, which occured this Thursday 19 december, some days before his 74th birthday. He has produced nice pieces of mathematics in non-abelian cohomology, categorical logic and synthetic differential geometry. More recently, he published works on philosophy, poetry, psychanalysis and their relations with category theory, in particular topos theory. He founded the category theory group in Louvain-la-Neuve and has been the supervisor of numerous PH.D. thesis, including mine. He was a very friendly person with a constructively critical mind. Francis Borceux -- ******************************************* PLEASE NOTICE THE NEW E-MAIL ADDRESS ******************************************* Francis Borceux Département de Mathématique Université Catholique de Louvain 2 chemin du Cyclotron 1348 Louvain-la-Neuve Begium phone +32 (0)10 473170 fax +32 (0)10 472530 e-mail borceux(a)math.ucl.ac.be 21-Dec-2002 12:30:28 -0400,5656;000000000000-00000000

1 0

preprint: The fundamental groupoid of the quotient of a Hausdorff space...
by Ronnie Brown 20 Dec '02

20 Dec '02

New preprint: R. Brown and P.J. Higgins TITLE: The fundamental groupoid of the quotient of a Hausdorff space by a discontinuous action of a discrete group is the orbit groupoid of the induced action ABSTRACT: The main result is that the fundamental groupoid of the orbit space of a discontinuous action of a discrete group on a Hausdorff space which admits a universal cover is the orbit groupoid of the fundamental groupoid of the space. We also describe work of Higgins and of Taylor which makes this result usable for calculations. As an example, we compute the fundamental group of the symmetric square of a space. The main result, which is related to work of Armstrong, is due to Brown and Higgins in 1985 and was published in sections 9 and 10 of Chapter 9 of the first author's book on Topology (Ellis Horwood, 1988). This is a somewhat edited, and in one point (on normal closures) corrected, version of those sections. Since the book is out of print, and the result seems not well known, we now advertise it here. It is hoped that this account will also allow wider views of these results, for example in topos theory and descent theory. math.AT/0212271 http://www.informatics.bangor.ac.uk/public/mathematics/research/preprints/0… http://www.bangor.ac.uk/~mas010/orbitgpdxx.pdf Other Information: 1) A previous announcement of fields-art3.pdf had a url of bangor.as.uk/~mas010/fields-art3.pdf instead of bangor.ac.uk 2. Our web sites on sculpture and knots have just been reorganised and given a new look by Mike Yates under an EPSRC grant. There are new animations, and navigation is much easier. Have a look! (see below) -- Professor Emeritus R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Raising Public Awareness of Mathematics CDRom Version 1.1 Symbolic Sculpture and Mathematics: Centre for the Popularisation of Mathematics http://www.cpm.informatics.bangor.ac.uk/centre/index.html 20-Dec-2002 14:53:27 -0400,1780;000000000001-00000000

1 0

on the logic of unique existentials
by Peter Freyd 19 Dec '02

19 Dec '02

The first solution to the "logic of cartesian categories" (I insist that Descartes invented equalizers as much as he invented products) presented itself with the introduction of essentially algebraic theories in 1971. It's an exercise. But it was always clear to me -- long before 1971 --that unique existential quantification was the central feature. (Yes, of course you can avoid it in the same way you can avoid ordinary existential quantification. Skolem taught us that.) There's no question one can assert unique existentials using finite limits. (As a sample: given a couple of binary predicates P on objects A,B and Q on objects B,C (modeled by maps from P to A and B and from Q to B and C) the assertion that for all a,b such that aPb there's a unique c such bQc is equivalent to the assertion that the map Pullback[P -> B, Q -> B] -> P is an iso. The rules of inference for unique existential quantification is what I saw as the central question. I wrote in Cartesian Logic: Twenty-five years ago this writer started listing these rules. Their remarkable inelegance caused him to conclude that he was staring at one of the very reasons for category theory. The notion of a cartesian category is much simpler than that of cartesian syntax. The language of cartesian categories has permeated mathematics as a whole, even among those who are convinced that there is nothing worth noting in the theory of categories (the usefulness of a language does not, in fact, imply the usefulness of its associated theory) and there is no chance that cartesian syntax is going to do any such thing....The particular impetus that propelled the present effort arose from the necessity [in an attempt to formalize the semantics of "logical programming"] of getting a handle on the process of adjoining generic subobjects to objects in cartesian categories. [The 25 years ago referred to the very first NY topos seminar. The rules at that point were horrendous.] Yes, once the solution for the generic subobject is stated one doesn't need cartesian logic. But it's a useful tool to find the solution. So here's a challenge. Take an arbitrary cartesian category and an object C therein. Now adjoin a generic category structure to the object C (use the one-sorted "pure category" theory). What are the objects? Try it just for the free cartesian category on C, in other words, what's the free cartesian category on a category-object? What are its objects? And harder: what are its maps? 18-Dec-2002 14:45:54 -0400,2705;000000000001-00000000

2 1

Internal logic of lex categories
by Andrej Bauer 19 Dec '02

19 Dec '02

I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.) Here is an attempt at reconstructing the logic. We want a logic that can be interpreted in any category C with finite limits, and we want a suitable completeness theorem, i.e., the semantics in lex categories is complete. Since C has pullbacks, Sub(A) has finite limits for any A. This means we should have the logical constant truth T and conjunction: T phi and psi Since there are equalizers in C, we should also allow equality (at each type A): t =_A u So now the question is what else is needed. We're not done yet since, semantically speaking, we have axiomatized equalizers and only pullbacks of monos along monos. Presumably we have to axiomatize the terminal object: 1 type ("1 is a type") * : 1 ("* is an element of 1") t =_1 * ("every element of 1 is equal to *") This still isn't enough because we don't have general pullbacks, or is it? I suspect we need not worry about binary products because the syntactic model will have them "for free". What did Peter Freyd say about this? Andrej Bauer Deptatment of Mathematics and Physics University of Ljubljana Slovenia http://andrej.com/ 16-Dec-2002 17:26:10 -0400,1208;000000000001-00000000

5 7

The Fun of Programming
by Jeremy Gibbons 19 Dec '02

19 Dec '02

Dear colleagues: We would like to advertise the following symposium, and are pleased to invite you to participate. We apologize if you receive multiple copies of this announcement. Jeremy and Oege * THE FUN OF PROGRAMMING A symposium in honour of Professor Richard Bird's 60th birthday Examination Schools, Oxford 24th and 25th March 2003 Professor Richard Bird is well known for his contributions to functional programming: for his two textbooks, his "Functional Pearls" column in the Journal of Functional Programming, his work on synthesizing programs from specifications, his influence in the design of the language Haskell and its predecessors, and so on. This symposium is to celebrate Richard Bird's work on the occasion of his sixtieth birthday. The symposium will coincide with the publication by Palgrave of an eponymous book. This book is intended as much as a textbook for an advanced course in functional programming as it is a festschrift; its twelve chapters cover applications (pretty printing, musical composition, hardware description, graphical design) and techniques (the design of efficient data structures, interpreters for little languages, program testing and optimization) in functional programming. The contributors to the book will give short lectures at the symposium, and every participant at the symposium will receive a copy of the book. The symposium will take place from 10.30am on Monday 24th March 2003 to 4pm on Tuesday 25th, in Oxford's historical Examination Schools. The registration fee includes participation, buffet lunch and tea and coffee on both days, a formal dinner on the Monday night in Worcester College, and a copy of the book. There is a lower price for early registration; the capacity of the lecture room is limited and offered on a first-come first-served basis, so early registration is recommended. The speakers are as follows: Chris Okasaki (West Point) John Hughes (Chalmers) Jeremy Gibbons (Oxford) Paul Hudak (Yale) Oege de Moor (Oxford) Simon Peyton Jones (Microsoft) Conal Elliott Mary Sheeran (Chalmers) Mike Spivey (Oxford) Ross Paterson (City) Philip Wadler (Avaya) Ralf Hinze (Bonn) For further details, including registration information, see the website at http://www.comlab.ox.ac.uk/oucl/research/areas/ap/fop/ In particular, there is an early registration deadline (with reduced fee) of 7th February 2003, and a late registration deadline of 7th March. Jeremy Gibbons and Oege de Moor (organizers) -- Jeremy.Gibbons(a)comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html 18-Dec-2002 14:45:54 -0400,3138;000000000001-00000000

1 0

None
by Andrei Popescu 18 Dec '02

18 Dec '02

Dear Sir or Madame, I am Andrei Popescu, junior scientist at the University of Bucharest, Romania. I dear to ask for your help in the following matter: does there exist any characterization of the projective objects in the category of all the algebras of a given (arbitrary) signature? Thank you very much. Respectfully, Andrei 17-Dec-2002 19:04:31 -0400,5776;000000000001-00000000

1 0

Re: internal logic for lex categories
by Taylor Paul 17 Dec '02

17 Dec '02

Andrej Bauer asked about the INTERNAL LOGIC OF LEX CATEGORIES. He gave a sketch of such a logic, based primarily on EQUALITY. Another conspicuous feature is the SYMMETRY in the notions of equality, conjunction, product and pullback. The reason for being interested in such a logic is presumably in order to give interpretations of "generalised", "dependent-type" or "essentially" algebraic theories. The theory of categories is the leading example of this, the TYPE Hom(x,y) being dependent on the TERM-variables x and y. I would argue that lex categories are the WRONG structure in which to interpret such theories. SEMANTICALLY, there are lots of interesting categories (of domains, of locally compact spaces, of differentiable manifolds, and so on) that don't have all finite limits, but in which one would nevertheless like to interpret such theories. What, for example, is a locally compact topological groupoid? SYNTACTICALLY, equations conditional on equations are not how we think about, for example, composition in categories. When we are about to form "f;g", we already know that the target of f is the same object as the source of g - it is not an accidental situation whose validity we have to test "on the fly". (This point was made, using Kant's synthetic/analytic distinction, by John Cartmell in his treatment of generalised algebraic theories in JPAA in 1986.) Mathematicians have, traditionally, not bothered about such issues - "either the objects are equal or they're not" - but in a computational setting, it becomes significant if this equality needs to be tested "at run time". Proof theory also distinguished between INTENSIONAL and EXTENSIONAL equality. Generalised algebraic theories come first, equality is an add-on. In particular, we need to give account of the more basic syntactic notion of SUBSTITUTION. This is interpreted by pullback, but is by no means symmetric between the two legs: one is the term containing the free variable, the other the term to be substituted. On the semantic side, pullback often encodes INVERSE IMAGE, which is also asymmetrical. For example, in topology we use inverse images of OPEN subspaces and maps along ARBITRARY continuous functions. It was to capture this situation (specifically, in categories of domains) that I introduced CATEGORIES WITH DISPLAY MAPS in my 1987 PhD thesis (and earlier in CTCS1, LNCS 240). A class of display maps is simply one that is closed under pullback along any map in the category. I use an open-triangle arrowhead for such maps. Syntactically, a display map is a map between contexts that simply omits one (the last) typed variable: Gamma, z:Z ----|> Gamma This corresponds to WEAKENING in type theory. An arbitrary map Delta = [y1:Y1, ..., ym:Ym] ----> Gamma = [x1:X1, ..., xn:Xn] in this category assigns a term ai:Xi, possibly involving the ys, for each position in the target context. Pullback of the display map along this map substitutes these terms for the xs in the type Z, which may have depended on these variables. Terms of type Z in context Gamma are splittings of the display; these undergo substitution in the same way when we pull the splittings back along Delta->Gamma. You may think that, given a highly dependent system of types, this category (the CLASSIFYING CATEGORY or CATEGORY OF CONTEXTS AND SUBSTITUTIONS) would be complicated to construct. Indeed it is, if you approach it in the wrong way, as a huge structural recursion. But this is because, as functional programmers know very well, recursion does not interact well with associativity. There is, in fact, an EASY AND UNIFORM CONSTRUCTION of the category from ANY TYPE THEORY that has all of the usual structural rules, in particular weakening (so this doesn't apply to linear logic). However, we obtain the category via an (elementary) SKETCH: - the objects are contexts, - the morphisms are GENERATED from two classes: - display maps (weakening by a typed variable) and - their splittings (cut with a typed term). - the equations are (those of the theory) plus five more, of which the well known SUBSTITUTION LEMMA is the most complicated. The place to look for the details of this is not my thesis, but CHAPTER VIII of my book, "Practical Foundations of Mathematics" Cambridge University Press, 1999 http://www.dcs.qmul.ac.uk/~pt/book/html/c8.html As I said, I introduced display maps in my thesis for domain theory, and in particular to discuss dependent products (polymorphism). The point was that NOT ALL SUCH PRODUCTS EXIST, as they do in Set, for which Lawvere had introduced the notion of HYPERDOCTRINE. As I was interested in constructing dependent products in semantic categories, it was important to seek ways of simplifying the calculations as much as possible. Ultimately, I found that only the special case of so-called PARTIAL PRODUCTS was needed. This reduction is in Section 9.4 of the book. The rest of Chapter IX deals with other aspects of type theories. Paul Taylor 17-Dec-2002 19:04:31 -0400,3589;000000000001-00000000

1 0