[Prev][Index][Thread]
Re: Linear notation

To: types

Subject: Re: Linear notation

From: pratt@cs.Stanford.EDU

Date: Tue, 31 Dec 91 09:28:40 EST

InReplyTo: Your message of Sun, 29 Dec 91 12:43:51+020. <9112291043.AA15931@math.tau.ac.il>

Sender: meyer@theory.lcs.mit.edu
Date: 29 Dec 91 23:32:36 PST (Sun)
To: linear@cs.stanford.edu
From: aa%taurus.bitnet@TAUNIVM.TAU.AC.IL
Date: Sun, 29 Dec 91 12:43:51+020
J.Y. has admitted himself that relevance logicans were the first to
distinguish between the "multiplicative" and "additive" conjunction and
disjunction
This distinction surely belongs to C.S. Peirce, who in 1870 [Pei] gave
De Morgan's calculus of binary relations pretty much exactly the form
used today by relation algebraists.
Here are the twotyped lattice notations I'm aware of.
Binary Residuated Closed Relevance Linear
Relations Lattices Categories Logic Logic
Peirce, Ward Eilenberg Anderson Girard
Schroeder Dilworth Kelly Belnap
[Pei] 1870 [WD] 1939 [EK] 1965 [AB] 1960's [Gir] 1980's
AB [A,B] AxB A^B A&B "with"
1 i 1 T T
A+B (A,B) A+B AvB Ao+B "plus"
0 z 0 F 0
A;B A.B or AB AoxB AoB AoxB "times"
1' i I t 1
A+,B A+B A~8B "par"
0' f __
The notation favored by Barr, Cockett, Seely, and myself is basically
the EilenbergKelly notation with the concession that I is changed to T
(whose dual is then naturally __ ) and with the dual of ox being taken
to be o+ (sorry about the overloading, Paul).
I don't know why Ward and Dilworth insisted on identifying the units i
of the two conjunctionsit rules out many residuated lattices
occurring "in nature" as Max Kelly likes to put it. Nor do I know why
latticetheoretic notation deteriorated so badly in the first third of
this centuryin 1933 Birkhoff wrote meet as (A,B) [sic] and join as
A\cap B [sic!]after both sides of the Atlantic, Peirce in the US and
Schroeder in Germany, seemed to have converged on a very nice notation
in the last third of the 19th century. Maybe competing obscure and
mysteriously powerful notations, particularly Peano's as adopted by
Russell and Whitehead but also those of Lukasiewicz, Schoenfinkel,
etc., had thrown the whole business of logical notation into
confusion.
I omitted from the table the notation in Robert and Ferland's [RF] 1968
semiring abstraction of the 1962 FloydWarshall algorithm, and no doubt
other semiring notations too, but enough is enough.
I believe relevance logic's tensor product AoB, cotenability, first
appeared in Mike Dunn's thesis [Dun66], which is why I put relevance
logic chronologically after Eilenberg and Kelly (La Jolla'65). However
given the vagaries of publication (the proceedings appeared in 1966)
this should probably count as a tie for third place, at least for the
conjunction.
However the only place I've seen "relevant disjunction" is in [Avr84].
I don't recall seeing it in what I've read of Dunn, Routley, Meyer,
McRobbie, Urquhart, or Maksimova. In particular a pass through Mike
Dunn's 105page chapter on relevance logic in HPL3 [Dun86], the most
recent comprehensive survey of relevance logic that I have to hand,
turned up no occurrences. While it may appear elsewhere it clearly
does so at best sparsely, and seems to be going places at the same
speed as Peirce's relative sum, probably for similar reasons. Not only
is it the last operation on the above list, but as I argued a few days
ago on both technical and historical grounds, it is also likely to be
the last operation anyone wants to spend much time debating the proper
notation for.
Vaughan Pratt
PS. A reminder, a propos of linear logic, that a draft of "Event Spaces
and Related Structures", pub/esrs.tex, can be retrieved by anonymous
ftp from boole.stanford.edu. See pub/README for abstracts of other
papers in the same directory..
========================
@Book(
AB, Author="A. R. Anderson and N. D. Belnap",
Title="Entailment", volume=1, Publisher="Princeton University Press",
Address="Princeton, NJ", Year=1975)
@Article(
Avr84, Author="Avron, A.",
Title="Relevant EntailmentSemantics and Formal Systems",
Journal="J. Symbolic Logic", Month=Jun, Year=1984)
@PhDThesis(
Dun66, Author="Dunn, J.M.",
Title="The Algebra of Intensional Logics",
School="Univ. of Pittsburgh", Year=1966)
@InCollection(
Dun86, Author="J. M. Dunn",
Title="Relevant Logic and Entailment",
Booktitle="Handbook of Philosophical Logic",
Volume="III", Editor="D. Gabbay and F. Guenthner", Pages="117224",
Publisher="Reidel", Address="Dordrecht", Year=1986)
@InProceedings(
EK66a, Author="Samuel Eilenberg and G. Max Kelly",
Title="Closed Categories",
Pages="421562",
Editor="S. Eilenberg and D. K. Harrison and S. MacLane and
H. R{\"o}hrl",
Booktitle="Proceedings of the Conference on Categorical Algebra,
La Jolla, 1965", Publisher="SpringerVerlag", year=1966)
@Article(
Gir, Author="Girard, J.Y.",
Title="Linear Logic", Journal="Theoretical Computer Science",
Pages="1102", Volume=50, year=1987)
@InCollection(
Pei, Author="Peirce, C.S.",
Title="Description of a notation for the logic of relatives,
resulting from an amplification of the conceptions of {B}oole's
calculus of logic. 1870",
Booktitle="Collected Papers of Charles Sanders Peirce. {III}.
{E}xact Logic", Publisher="Harvard University Press", Year=1933)
@Article(
RF, Author="Robert, P. and Ferland, J.",
Title="G\'en\'eralisation de l'algorithme de {W}arshall",
Journal="Revue francaise d'Informatique et de
Recherche Operationnelle", Volume=2, Number=7, pages="1325", Year=1968)
@Article(
WD, Author="Ward, M. and R.P. Dilworth",
Title="Residuated Lattices",
Journal="Trans. AMS", Volume=45, Pages="335354", Year=1939)