Date: 03 Nov 91 20:17:42 PST (Sun) From: pratt@cs.stanford.edu ------- Forwarded Message Date: Mon, 4 Nov 1991 00:17:17 GMT From: lincoln@Neon.Stanford.EDU (Patrick D. Lincoln) Organization: Computer Science Department, Stanford University, Ca , USA Subject: Linear Logic Mailing List Message-Id: <1991Nov4.001717.6180@CSD-NewsHost.Stanford.EDU> Sender: owner-logic@cs.Stanford.EDU To: logic@cs.stanford.edu I believe the time is ripe for a mailing list on linear logic. The main idea is to provide a forum for the discussion of linear logic and related topics, such as interesting fragments of linear logic, proof nets, decision problems, affine logic (linear logic with unrestricted weakening), semantics, implementation, etc. I have set up a mailing list named "Linear@CS.Stanford.EDU". If you would like to be added to this mailing list, please send mail to Linear-Request@CS.Stanford.EDU Please forward this announcement on to others who might be interested.. Patrick Lincoln ================================== Subj: Urgent message to all category theorists From: street@macadam.mpce.mq.edu.au (Ross Street) Date: Thu, 7 Nov 91 13:32:04 GMT Categorical colleagues: I am pleased to announce that the Australian Research Council has decided to continue to fund category theory for three more calendar years 92-94. Our six year Program Grant comes to an end this calendar year 91, and these 6 year grants no longer exist. Of course we did not get all we asked for, but the assurance of 3 year funding allows us to make long-term plans. It is also pleasing that Michael Johnson has joined the group of "Chief Investigators" for the Grant. -->POSTDOC POSITION<-- Included in the funding is the possibility of employing a Research Associate to work with our group for 3 years. We are meeting in two weeks to decide on the successful applicant for this position. So, if you are interested in applying or know of someone who is, please send CV and references as soon as possible to me by email or by FAX Ross STREET, MATHEMATICS, +61-2-805-8983 BEFORE 22 NOVEMBER 1991. Regards Ross ++++++++++++++++++++++++++++++++++ From: street@macadam.mpce.mq.edu.au (Ross Street) Subject: Rider to Urgent Message Date: Thu, 7 Nov 91 13:51:34 GMT On behalf of the Chief Investigators, I would sincerely like to thank those who wrote references to the ARC concerning our Grant Proposals. We appreciate that these things take time and energy, and that some people have been asked several times before for references. Ross ============================================ Subj: We've been shafted again Date: Sun, 10 Nov 91 13:39:11 EST From: barr@triples.Math.McGill.CA (Michael Barr) By we I mean the world of category theorists. Twice, I have tried to publish something on categories in the so-called Mathematical Intelligencer. Not that it's relevant, but earlier this year they published an article on the philosophy of mathematics by such an ignoramus that he didn't know the difference between the axiom of choice and the axiom of pairs. The most recent one contains an article by Barwise on non-well-founded set theory. Barwise has discovered that there are no non-trivial solutions to domain equations (the one he is looking at is S = N x S, where N is the natural numbers and he really means equals) in WF set theory, because it is clear that a set satisfying it and WF could only be empty. (Although he doesn't mention it, for such an equation as S = 1 + S, there's no solution at all.) Of course, these equations are important in computer science and something has to be done etc, etc. And what does he propose? Rather than accepting what is staring him in the face, that set theory founded on the epsilon relation is irrelevant to the workings of virtually the entire world of mathematics, he proposes to compound the felony by taking as mathematical foundations Aczel's theory of NWF sets. Consider that probably not one mathematician in ten could give a coherent account of ZF axioms. Have you ever seen a complex analyst begin a paper by saying if his complex numbers are ordered pairs of reals or 2 x 2 matrices with certain properties (and what are the elements of the matrix ring anyway?) or equivalences classes of R[x] mod (x^2 + 1) or ... ? Of course not. And there is no problem with domain equations in a categorical framework. Nor for that matter, with what Barwise calls the largest solution, by which he apparently means the terminal one. Peter Freyd once asked how you know that the largest sporadic simple group isn't the smallest counter-example to the Riemann Hypothesis. Actually, I suspect that for all the constructions of the complex numbers I know of, that cannot happen. But the very answer points up the irrelevance of the elements of a set. Certainly not very many mathematicians could give you the categorical axioms for sets either. The difference is that if you explained to him the categorical axioms, he would recognize in them constructions he uses daily. It is the categorical notion of subobject that is used when she considers the integers as a subset of the rationals, the rationals of the reals and the reals of the complexes. On the other hand, it now appears that Barwise is proposing to move set theory even further from practice by introducing an even more complicated set of axioms with the anti-foundation axiom that Aczel has introduced. I can only hope that someone with enough prestige that the Intelligencer might feel constrained to accept it would write a paper pointing out these things and suggesting that the topos-based axioms (which can be easily described) lead to a much simpler and more natural approach to the same thing. As for me, I've decided to drop my subscription. They have irritated me just once too often. Michael =================================== Subj: RE: We've been shafted again Date: Wed, 13 Nov 1991 19:00:01 EST Note from moderator: A human error (mine) has caused the repetition of Mike's message. (so the emphasis is mine, not his.) That also caused a delay in sending Vaughan's reply which follows, and a contribution (on another subject) still to come from Paul Taylor. +++++++++++++++++++++++++++++++++++++++++++++++++++++++ Date: 11 Nov 91 21:53:11 PST (Mon) From: pratt@cs.stanford.edu Mike is basically right about the AFA-vs-ZF distinction being irrelevant to "working mathematics." I feel the same about the IEEE floating point standard vis a vis various "good" NA algorithms I was exposed to long ago. But just now I was looking at an instance of Stone duality where I wanted to say of two partial lattices that each was the partial lattice of ultrafilters of the other. This is gibberish for ZF but not for AFA. The ZF expression of this requires me to stick in an "isomorphic to." AFA is not about doing something you couldn't do before, it is merely about not having to say you're sorry when you talk dirty. -v ============================= Subj: RE: We've been shafted again Date: Wed, 13 Nov 91 09:43:03 EST From: barr@triples.Math.McGill.CA (Michael Barr) Ah, but my point is that Barwise was just continuing the great set-theoretic illusion by making it just possible to actually do mathematics with sets instead of admitting their intellectual poverty. With a categorical foundation, these problems simply don't appear as problems. What is really wrong with traditional sets is the irrelevance of their elements. Who cares what the elements of a set really _are_? All that matters are the structures it bears and they are always expressed by functions (or relations). Michael ============================ Subj: FTP archive at Imperial etc Date: Tue, 12 Nov 91 17:28+0000 From: Paul Taylor Public FTP archive at Imperial College, London The Theory and Formal Methods section of the Department of Computing in Imperial College, London, now has a public FTP archive for its papers. You can access this by the fairly memorable ftp theory.doc.ic.ac.uk and then log in using the name "anonymous" or "ftp" and your email address as password. The IP address is currently 129.31.81.37 but is going to change shortly, so please note the name (which cost a three month fight within the department!), not the number. Papers, in various formats (DVI, LaTeX source, PostScript, RTF, ASCII), are in the directory /theory/papers/... where the next subdirectory is the surname of the author. For example, /theory/papers/Abramsky/cill.dvi.Z is the compressed DVI of Samson Abramsky's "Computational Interpretation of Linear Logic". There isn't a great deal of stuff there at the moment, but hopefully it will expand. It is intended to include papers from the CLiCS (Categorical Logic in Computer Science: European Community Basic Research Action 3003) project as well as local ones. If you believe one of us has written a paper but you cannot find it in the archive, please send email to the author (not me); in most cases the email address consists of the initials with @doc.ic.ac.uk. There is also a directory /theory/software, which contains some tex bits (including my commutative diagrams) and wp (Mark Dawson's omega Prolog). Finally, you can write to /theory/tmp (within reason!). ============================================================================= Since I'm here: Perhaps other sites who have FTP archives of theoretical computer science and category theory papers would declare themselves for future reference. On-line bibliographies and address lists, too. Also: My commutative diagrams package (/theory/software/tex/diagrams.tex) hasn't changed much since July 1990, but when I have time (one day) I intend to overhaul it, fix some bugs and incorporate some features people have suggested. Please would those who have acquired the package indirectly, or passed it on to others, advise me so as to ensure that you get the new version when it becomes available (NOT YET!). Bugs and suggestions are also welcome. Paul Taylor Dept of Computing, Imperial College, London SW7 2BZ, UK +44 71 589 5111 x 5057 =================================== Subj: RE: We've been shafted again From: street@macadam.mpce.mq.edu.au (Ross Street) Date: Thu, 14 Nov 91 13:36:49 GMT What a wonderful essay by Mike!! It reminds me of the talk H. Linstra gave here on "How to play the complex numbers". A move is to give an element of a declared construction of the set at hand; the player left with the empty set loses. Ross +++++++++++++++++++++++++++++++++++++ Date: Thu, 14 Nov 91 10:31:32 EST From: James Stasheff To Michael Barr Yes, but... Elements are occassionally useful. Avoiding them entirely is like insisting on writing po russki without the `Cyrillic' alphabet. And then there are those of us who don't speak the categorical dialect fluently. jim ================================= Subj: RE:FTP archive at Imperial etc Date: Fri, 15 Nov 1991 00:49:25 EST From: Paul Taylor Linear logic font (llwith) and Commutative Diagrams It has been pointed out to me that Samson Ambramsky's linear logic paper, which I used as an example of something in our archive, requires the font "llwith10". I did point out that some TeX stuff is in another directory theory/software/tex on the archive, but I apologise for not making it sufficiently clear that this includes llwith10 as well as the commutative diagrams. Now that I've got the hang of MetaFont (at least for symbols - I wouldn't attempt to design an alphabet with it!) I shall probably develop a font including "llwith", "lasy" and some other symbols. Any suggestions for logical, categorical and computing symbols not available in othet fonts welcome (within reason & no promises). As I said, I recommend using the name not the number, but the new IP address is theory.doc.ic.ac.uk 146.169.22.37 as of Wednesday 20 November Another piece of trivia I meant to mention before: anyone (in the south east of England) who would like to receive email announcements of theory seminars in Imperial College (on Wednesdays) - please email me Paul Taylor ======================= Subj: RE: We've been shafted again Date: Fri, 15 Nov 91 10:09:43 EST From: barr@triples.Math.McGill.CA (Michael Barr) Reply to Jim Stasheff: Dear Jim: I use elements all the time and cannot imagine not using them. I have proved one major embedding theorem that sanctions the use of elements in exact categories. but my elements aren't sets and don't have elements inside them and so my sets (objects, really) have no irrelevant structure. I just happened to read a very nice essay by Colin McLarty on this very ssubject that I received the same day I posted my flame. Incidentally, I have had a pleasant exchange with Barwise. First off, apologies to his collaborator Larry Moss, for not mentioning him (although it is not clear he lost anything thereby). He said, in effect, that he likes categories, in their place, but not when they leave that place. He then left for two weeks (I think it was in Japan) before it could continue. I will try to get more deeply into that when he returns. Michael ===================== Subj: NNO Date: Wed, 13 Nov 91 12:11:16 EST From: barr@triples.Math.McGill.CA (Michael Barr) I went too far when I said in my recent flame that there was no solution to 1 + X = X in standard set theory. If we take 1 = {0}, where 0 is the empty set and take A + B = A x {0} u B x {1}, then the set {(0,0), (0,0,1), (0,0,1,1), (0,0,1,1,1), ... } satisfies it on the nose, where I use (a,b,c,d,...) for the left associated ((...(a,b),c),d),e),...). I guess typical covariant domain equations have initial solutions, but not final ones in standard set theory. Thanks to Bob Tennent for pointing this out. Note that this is not the Von Neumann NNO. Michael ++++++++++++++++++++++++ Apologies to Mike for sending this late - it got lost temporarily in the shuffle of mailer problems. Bob Rosebrugh =========================== Subj: Are there French words for locales and frames Date: Fri, 15 Nov 91 14:21:13 GMT+0100 From: curien@FRULM63.BITNET (Pierre-Louis Curien) I wonder whether a terminology exists in French for the kind of stuff in Johnstone's book Stone Spaces. In particular: locales and frames. Due to the French speaking Canadian category theorist at least, the question must have arisen at some stage. Thanks to anyone for help in this matter. ============================ Subj: RE: We've been shafted again From: koslowj@math.ksu.edu (Juergen Koslowski) Date: Sat, 16 Nov 91 10:16:23 CST Dear Michael, How about a reference to Colin McLarty's essay you mentioned in your reply to Jim Stasheff? J"urgen Koslowski ++++++++++++++++++++++++++++++++ Date: Sun, 17 Nov 91 12:03:29 EST From: barr@triples.Math.McGill.CA (Michael Barr) It is called, ``Numbers can be just what they have to''. It appears to be a preprint and done, unfortunately, on a typewriter. I have written to Charles asking him to ask Colin if he wants to post it, but Colin, in a Philosophy Dept, isn't into computers and almost certainly doesn't have in computer readable form. You can of course write him at Dept of Philosophy, Case Western, Cleveland, OH USA 44106. There is something I would like to add. I got one query from someone who didn't believe that it was possible to use categories or toposes as a foundation because a category has a set of objects and a set of morphisms (or a class, but that's not the issue here) and you cannot talk about the domain or codomain functions and the rest of the structure unless you have some underlying set. Right? No! You have no more need (or exactly the same need) to have an underlying set as you do when axiomatizing sets. If you need to have a set to talk about a function, then you need a set to talk about the membership relation. In both cases, it would be nice to have a set; it puts us on familiar territory, but when founding mathematics you have to start somewhere. It is as legitimate to start with a pre-existing notion of morphism, domain, codomain and so on as with a pre-existing notion of set and membership. Are your intuitions well-founded? How do I know? I think mine are, but I cannot prove it to my satisfaction, let alone prove that yours are. That's the way it is with foundations. Michael ++++++++++++++++++++++++++++++++ Date: Sat, 16 Nov 91 12:35:03 EST From: James Stasheff thanks one of the delights is the current rage of applications of category theory to mathematical physics - of all things!! but it's particularly crucial there to emphasize the useful and not be too pedantic about max generality anybody there interested in the relevant physics Patera et al are one step removed ======================= Subj: Re: Are there French words for locales and frames Date: Mon, 18 Nov 1991 09:35:28 -0500 From: lamarche@FRULM63.bitnet (Francois Lamarche) La seule chose que je sais est que Joyal insiste pour employer l'expression "treillis localique" pour "local(e)" ++++++++++++++++++++++++++++++++++++++++++++++++++++++ Date: Mon, 18 Nov 1991 08:22:30 -0500 From: "Fred E.J. Linton" I believe Ehresmann (and some of his school) used "treillis local[e]" (sorry, I've lost the gender of "treillis" :-( ) for what Dowker and his followers later called "frame". You can see then how the English term "locale" might have arisen, from either a misinterpretation of (or, more generously, a simple borrowing from) the French. -- Fred ====================== Subj: Re: Are there French words for locales and frames Date: Wed, 20 Nov 91 09:33:53 +11 From: kelly_m@maths.su.oz.au (Max Kelly) Quand Joyal e'tait a` Sydney il y a plusieures anne'es, il employait "espace" pour ce qu'on appelle en anglais "locale" - dans ce contexte un espace n'est pas force'ment TOPOLOGIQUE, quoiqu'il puisse tre`s bien l'e^tre. Je ne suppose pas, cependant, que cela se trouve facilement accepte' par le publique mathe'matique. Max Kelly. ======================= Subj: Re: Are there French words for locales and frames Date: Wed, 20 Nov 91 10:20+0000 From: Steven John Vickers One could ask what are the English words for locale and frame. Joyal and Tierney ("An extension of the Galois theory of Grothendieck"), in English, called frames "locales" and locales "spaces", and I would say that the resulting ambiguity in the word "locale" hampers precise expression. Therefore, when Francois Lamarche reports Andre Joyal as insisting on using the expression "treillis localique" for "local(e)", one must be careful what this means. I would guess that "locale" here is not in the Isbell sense as used in Johnstone's "Stone Spaces" (as I like to put it, a locale is a frame "pretending to be" a topological space), but in the Joyal & Tierney sense, i.e. a frame. If the Francophones haven't established terminology yet, then perhaps this is a fine opportunity for them to avoid the problems of English by agreeing on a standard. Purely as a suggestion from an outsider, let me propose - "treillis local[e]" for frame: it seems to be the original French phrase for the concept ("Stone Spaces" refers to Benabou's "Treillis locaux et paratopologies", 1958). It also makes it plain that the object being considered is a lattice, exploding any pretence that it's a space. "locale" (assuming that's a good French noun) for locale in Isbell's sense. Steve Vickers. =========================== Subj: Union Conference Date: 23 Nov 91 16:35:00 EDT From: "NIEFIELD, SUSAN" UNION COLLEGE MATHEMATICS CONFERENCE Saturday and Sunday Schenectady April 25-26, 1992 New York KEYNOTE SPEAKER John Milnor This is a preliminary announcement of the eighth occasional Union College Mathematics Conference. This year the conference topics are category theory, dynamical systems, and number theory. The dynamical systems session will be directed towards complex dynamics and chaos. In addition to the keynote lecture, of interest to the entire Conference audience, there will also be shorter contributed talks in parallel sessions. Anyone interested in giving such a talk should contact one of the organizers. The meeting will begin with a reception from 9:00pm to 11:30pm on Friday, 24 April, and end on Sunday afternoon. A more detailed notice (including registration and hotel information) will be mailed in January. Organizers Category Theory Susan Niefield NiefielS@Union.Bitnet NiefielSGar.Union.Edu Kimmo Rosenthal RosenthK@Union.Bitnet RosenthK@Gar.Union.Edu Number Theory William F. Hammond (SUNY Albany) Hammond@Leah.Albany.Edu Karl Zimmermann ZimmermK@Union.Bitnet ZimmermK@Gar.Union.Edu Dynamical Systems Michael Frame FrameM@Union.Bitnet FrameM@Gar.Union.Edu Department of Mathematics Union College Schenectady, New York 12308-2311 Telephone (518) 370-6426 FAX (518) 370-6789 ============================= Subj: Two-sided proof nets with units Date: Fri, 29 Nov 91 17:09:02 EST From: rags@triples.Math.McGill.CA (Robert A. G. Seely) We wish to announce the following preprint: The logic of weakly distributive categories I: Two sided proof nets with units R. Blute R.A.G. Seely Abstract We define a two sided notion of proof nets, suitable for logics, like the logic of weakly distributive categories, which have the two-tensor structure (with/par) of linear logic, but lack a negation operator. These proof nets have a structure more closely parallel to that of traditional natural deduction than Girard's one-sided nets do. In particular, there is no cut, and cut elimination is replaced by normalization. We prove a sequentialisation theorem for these nets and the corresponding sequent calculus, and deduce the coherence theorem for weakly distributive categories as an application. We extend these techniques to cover the case of non symmetric tensors ("planar logic"). One significant feature of this version of proof nets is that we are able to include the units for the tensors in our presentation. With this, we are able to extend these nets to the full case of multiplicative linear logic (with units), and prove sequentialisation there. This represents an improvement over the treatment via one sided nets, which cannot handle the units successfully. ==================================================== The preprint may be obtained by anonymous ftp from triples.Math.McGill.CA (132.206.150.30) in the usual manner, or by contacting one of the authors. Via ftp: Login as anonymous, use your email ID as password. The various files are located in the directory pub/rags/nets You will find a PostScript file, a DVI file, and the TeX source code. If you want to take the TeX source code, read the nets.README file first, to find out what macro files are also necessary. (And for other instructions.) At the moment only the extended abstract will be found in this ftp directory; shortly the full paper (including other results, such as conservativity of the extension from weakly distributive categories to *-autonomous categories, in the unit-free case,) will be placed there as well. If you wish to be notified of such "upgrades", drop one of us a line. (Or just browse, from time to time.) Authors' address: Department of Mathematics McGill University 805 Sherbrooke St. W. Montreal Quebec H3A 2K6 Canada FAX: (514) 398-3899 Phone: (514) 398-3804 Authors' email addresses: Blute: blute@triples.math.mcgill.ca Seely: rags@triples.math.mcgill.ca