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    <street@macadam.mpce.mq.edu.au>

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 <pt%doc.imperial.ac.UK@QUCDN.QueensU.CA>

        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 <pt@doc.ic.ac.uk>
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 <jds@charlie.math.unc.edu>

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 <pt%doc.imperial.ac.UK@QUCDN.QueensU.CA>

        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 <pt@doc.ic.ac.uk>

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 <jds@charlie.math.unc.edu>

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" <FLINTON@Wesleyan.bitnet>

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 <sjv%doc.imperial.ac.UK@QUCDN.QueensU.CA>

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" <niefiels@gar.union.edu>


	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

