[Prev][Next][Index][Thread]
Semantical considerations on linear logic notation
Date: Sun, 22 Dec 91 21:21:37 PST
Date: Fri, 20 Dec 91 23:28:17 EST
From: anne@fwi.uva.nl (Anne S. Troelstra )
...a confusing aspect in Girard's original choice is
that dual operations do not have "similar" symbols.
Barr [Bar91a,Bar91b], Seely [See89], and Cockett and Seely [CS] meet
this criterion in a way that combines good taste in notation with
otherwise minimal disturbance to Girard's notation, as follows.
1. Swap 1 and T.
2. Use + and x for the additive operations
3. Write par as \oplus (per Cockett and Seely; Barr uses *).
The additives then become +,0,x,1, the multiplicatives become
oplus,bot,otimes,top, and the rest is unchanged.
In particular linear negation, A-perp, should not be written as though
it were ordinary negation. While it is linear logic's only necessarily
involutory negation, it is not its only negation, consider A=>0 for
example. This along with algebraic tradition (V-star for the dual of
vector space V) and elementary examples such as complement-of-converse
vs. converse in the calculus of binary relations (see below) mitigates
against renaming A-perp, which has both a horizontal and a vertical
component (in the 2-category sense), to anything suggestive of a purely
vertical negation.
The rest of this note investigates the mathematical basis for the two
proposed criteria for pairing symbols, distributivity and duality. The
conclusion is that while neither has much of a leg to stand on, duality
does justifying pairing the additives "plus" and "with," in which case
the multiplicatives "times" and "par" are stuck with each other. Arnon
Avron should appreciate this application of semantics to an ostensibly
syntactic issue.
The Distributivity Criterion
Girard's distributivity criterion presumes a fixed
"distributor-distributand" matching. However while a fixed category
may admit at most one cartesian closed structure (up to isomorphism),
it may simultaneously admit any number of distinct closed structures
each giving rise via the distributivity criterion to a matching of
coproduct with the tensor product of that structure. Each symmetric
(commutative) closed structure is defined by an adjunction between a
tensor product x@y and its matching "tensor quotient" or internal
hom x -o z, namely:
Hom[x@y, z] ~ Hom[y, x -o z]
For example the standardly ordered (as category) set of natural numbers
with infinity oo admits (i) the cartesian closed structure (min,oo)
with internal hom x=>y = (x<=y ? oo : y), and at the same time (ii)
the closed structure (+,0) (natural number addition) with internal hom
x -o y being truncated subtraction (x<=y ? y-x : 0).
If the tensor product x@y is not symmetric then "closed" becomes "left
closed" and/or "right closed", each with its own "left tensor quotient"
or left residual x\z and "right tensor quotient" or right residual z/y
defined by adjunctions:
Hom[x@y, z] ~ Hom[y, x\z] "divide on the left by x"
Hom[x@y, z] ~ Hom[x, z/y] "divide on the right by y"
For example the set of all languages on an alphabet Sigma, ordered by
inclusion (as category), admits simultaneously the following three
closed structures: (i) the cartesian closed structure
(intersection,Sigma^*) with internal hom R=>S = R'+S (complement-of-R
union S), (ii) the symmetric closed structure (||,e) (|| = language
shuffle, e = epsilon) with internal hom L -o M = {w : w||L < M} (< =
inclusion), and (iii) the biclosed structure (.,e) (. = concatenation)
with left internal hom L\M = {w : L.w < M} and right internal hom M/L =
{w : w.L < M}.
Every such closed structure on a given category then gives rise to a
distributivity law in which the tensor product of that structure
distributes (in the relevant argument) over not only sums (i.e.
coproducts, including 0 and infinitary coproducts) but all colimits of
the category. In the first example both min and + distribute over the
coproduct, namely max. In the second example intersection, shuffle,
and concatenation all distribute over the coproduct, namely union.
Thus the distributivity criterion permits direct (categorical) sum to
be paired with any of the tensor products but gives no criterion for
preferring one tensor product as *the* mate of sum.
The Duality Criterion
The duality criterion presumes a fixed duality A' = A -o D for some
dualizing object D satisfying A'' ~ A. This creates a contravariant
self-equivalence, that is, an equivalence between the category and its
opposite, which takes all limits to colimits and vice versa. However
not only need the closed structure defining -o not be unique but given
any such -o there may exist multiple dualizers D.
For example the set of all binary relations on a set X, ordered by
inclusion, has the empty relation as a dualizer for the cartesian
closed structure, defining Boolean complement as one duality. Yet at
the same time it has 0', the (Boolean) complement of the identity
relation, as a common dualizer for each of the left and right residuals
R\S and S/R each right adjoint to composition in one or the other
argument, defining complement-of-converse as another duality (it turns
out to be the same duality whichever of R\S or S/R one takes as
defining it).
Any such duality A' makes product and coproduct into De Morgan pairs
satisfying A'+B' = (AXB)'. However different dualities can equip the
other tensor products with different De Morgan duals. In the binary
relation example, composition as a tensor product has two candidates
for its De Morgan dual "tensor sum", defined by respectively complement
and complement-of-converse.
The tensor sum defined by complement received much attention from
Peirce and Schroeder between 1870 and 1895. This is Peirce's "scorpion
tail" A+,B, the notation for which (of interest given that this is a
note about notation) was derived by what linguists call "back
formation" in which the multiplicative conjunction (composition) A;B is
construed as the additive conjunction (intersection) A.B with a comma
subjoined. Schroeder had this neatly punchcut as a backward t:
|
|
-----------
|
\ |
\__/
for his 1895 tome [Schr95]. Peirce objected strenuously to this
typography [Pei], insisting that it should have looked more like
|
|
-----------
|
| \
\__/
(This was towards the end of Peirce's career, a seemingly unhappy
period for him in which he reacted with irrational bitterness to some
of Schroeder's ideas.)
I know of no mention in the relation algebra literature of the De
Morgan dual of composition defined by complement-of-converse, call it
A#B. This rather than A+,B is the true analog in the relation calculus
of Girard's par. However since the two are the same up to order of
arguments, A#B = B+,A, the equational properties of one are easily
derived from those of the other. For example Peirce's inequalities
[Pei,3.334]
A;(B+,C) < (A;B)+,C (1)
(A+,B);C < A+,(B;C) (2)
just become
A;(C#B) < C#(A;B) (3)
(B#A);C < (B;C)#A (4)
In considerably more modern (1991) terminology the latter two are half
of the defining inequalities, or more generally morphisms, of weak
distributivity [CS], the other two being (1) and (2) with +, changed to #.
However (1) and (2) so modified are not theorems about relations on X,
witness X = {0,1}, A = {(0,1)}, B = X^2, and C = {}. This contradicts
modified (1), that is, A;(B#C) < (A;B)#C, or A;(C+,B) < C+,(A;B). For
in that case B#C = B, so A;(B#C) = A;B = {(0,0),(0,1)}, whereas (A;B)#C
= {}. Hence the calculus of binary relations is not a weakly
distributive category, modified (1) and (2) constituting a weakened
form of symmetry that does not hold for binary relations. In the
language of [CS,p18], the monoidal category of binary relations with
inclusions for morphisms and composition for tensor product is overly
noncommutative.
==================================================
The bottom line is that, in a given category, the only canonical
pairing would appear to be that of product and coproduct. Making this
pairing then precludes basing pairing on distributivity of any given
tensor product over coproduct (or dually of any given tensor sum over
product).
In any event, unless a given tensor sum arises naturally as a useful
operation in its own right, as opposed to merely one of several
possible duals of a useful tensor product, it would seem to be rather a
waste of time arguing about the proper notation for it.
In this connection it is noteworthy that the tensor sum a+,b, which
enjoyed the considerable attention of both Peirce and Schroeder in the
19th century, did not survive the passage of the calculus of binary
relations into the 20th century, starting promptly with Russell's 1901
paper "The Logic of Relations": "I have not found the relative addition
of Peirce and Schroeder necessary." It will be interesting to see
whether any recently proposed tensor sum does any better in the
millennium. If weak distributivity does not carry par, what will?
Vaughan Pratt
@Article(
Bar91a, Author="Barr, M.",
Title="{$*$-A}utonomous categories and linear logic",
Journal="Math Structures in Comp. Sci.",
Volume=1, Number=2, Year=1991)
@Article(
Bar91b, Author="Barr, M.",
Title="Accessible categories and models of linear logic",
Journal="J. Pure and Applied Algebra", Note="To appear", Year=1991)
@Unpublished(
CS, Authors="Crockett, J.R.B. and Seely, R.A.G.",
Title="Weakly Distributive Categories",
Note="Manuscript", Month=Nov, Year=1991)
@InCollection(
Pei, Author="Peirce, C.S.",
Booktitle="Collected Papers of Charles Sanders Peirce. {III}.
{E}xact Logic", Publisher="Harvard University Press", Year=1933)
@Book(
Schr95, Author="Schr{\"o}der, E.",
Title="Vorlesungen {\"u}ber die {A}lgebra der {L}ogik ({E}xakte
{L}ogik). {D}ritter {B}and: {A}lgebra und {L}ogik der
{R}elative", Publisher="B.G. Teubner", Address="Leipzig", Year=1895)
@inProceedings(
See89, Author="Seely, R.A.G",
Title="Linear logic, {$*$}-autonomous categories and cofree algebras",
Booktitle="Categories in Computer Science and Logic",
Address="held June 1987, Boulder, Colorado", Pages="371-382",
Series="Contemporary Mathematics", Volume=92, Year=1989)