[Prev][Next][Index][Thread]
Linear notation
Date: Tue, 24 Dec 91 23:54:59 PST
To: linear@cs.stanford.edu
Date: Tue, 24 Dec 91 22:59:58 EST
From: rags@triples.math.mcgill.ca (Robert A. G. Seely)
Jean-Yves has expressed the essence of the matter in this way -
he would be quite willing to change notation if everyone else
could agree on what to change to! Of course, the common answer
(mine too) is "my notation - it is so natural".
Right. No consensus --0 no point in fiddling with J.-Y.'s notation.
A corollary is that there will be no change unless people either
identify a specific reason to change, or spontaneously line up behind
some other notation. The latter is wishful thinking.
The purpose of my previous note (sent by mistake to types instead of
linear) was to support Anne's reason for change, if not the details of
his changes, namely that duals should be paired, and to put in a vote
for the Barr-Cockett-Seely (BCS) notation, which meets that criterion
in a pretty minimal way and at the same time seems generally an
extremely nice notation.
The definitive version of BCS notation is as in Cockett and Seely's
Durham paper [CS]. This notation is Girard's notation with the
additives and multiplicatives and their associated units changed as
follows.
additives + 0 x 1
multiplicatives oplus bot otimes top
So if you like the original notation stick with it. If you want to be
different for the sake of being different, consider Morse code. But if
you really want to see a change made, don't propose a new notation
before asking yourself whether you could live with BCS notation. If
your biggest druther is to pair by duality instead of by
distributivity, that's the main change that BCS makes.
Vaughan Pratt
@InProceedings(
CS, Authors="Crockett, J.R.B. and Seely, R.A.G.",
Title="Weakly Distributive Categories",
Note="To appear",
Booktitle="Proc. LMS Symp. on the Applications of Category Theory in
Computer Science", Address="Durham", Year=1991)
PS. I should add that I've been using exactly BCS notation myself for
twelve months now, when pomsets suddenly needed the full range of
linear logic operations on account of the endomorphic duality that
showed up in event spaces. (They also need some operations not in
linear logic such as concatenation, blind choice, and Winskel's
synchronous parallel composition, a sort of enriched coproduct of event
spaces.) This resulted from balancing up the Birkhoff-Stone duality of
schedules and automata by moving the nonempty joins and the empty meet
>from the automata side to the schedule side, details in
boole.stanford.edu:pub/es.{tex,dvi}, see also esrs.{tex,dvi} which
joined it just the other day.
Prior to event structures there was no tensor sum for pomsets, just
tensor product or orthocurrence, flow of one process through another.
It first appeared in Logics of Programs'85, LNCS 193, p.270, line 6,
where I mistook it for ordinary product because Poset is cartesian
closed. With the help of my collaborators I got it right in Temporal
Structures (LNCS 389 p.29, Manchester 1989). What tipped us off was
that in those temporal categories that were not cartesian closed it was
clear that the intended operation was not ordinary product.