[Prev][Next][Index][Thread]
non-commutative linear logic
Date: Fri, 24 Jan 92 05:21:24 PST
To: linear@cs.stanford.edu
Date: Thu, 23 Jan 92 21:44:23 EST
From: Thomas Streicher <streiche@fmi.uni-passau.de>
Is the following result already well known ?
...
I think up to that point it should be known to a lot of people.
The crucial point is NEGATION for which we write R BorthB :
R BorthB = { (x,y) | not (y R x) } .
This is complement-of-converse, whose application to "linear negation"
is due to Peirce, cf. some of my earlier correspondence to this list
mentioning complement-of-converse, e.g. Dec 23. I've concatenated a
few of the longer messages in /pub/llmsgs on boole.stanford.edu,
retrievable by anonymous ftp.
The history of complement-of-converse gets off to a shaky start with De
Morgan's "Theorem K", which captures the essence of residuation
(currying) for binary relations. De Morgan distributes complement and
converse to distinct variables rather than stacking them up together on
the one variable, which would appear to be a conscious esthetic
judgement.
The picture clears up with Peirce, who was the first to explicitly use
complement-of-converse as negation, in several papers around 1882 ("On
the Logic of Relatives", "On Relative Terms", and "Remarks on B.I.
Gilman's `On Propositions and the Syllogism'"). In this last he
asserts the equivalence of what in Girard's notation would be (writing
ox for tensor and A' for linear negation) A ox B |- C, C' ox A |- B',
and B ox C' |- A', "linear contraposition" if you will. He also
asserts A ox A' |- _|_ and 1 |- A o+ A', recognizable as the linear
versions of A and not A implies false, and true implies A or not A.
I related some of this history (but spent rather too long on the
notorious De Morgan-Hamilton dispute at the expense of Peirce) at the
1989 Edinburgh Jumelage, where I also described complement-of-converse
as linear negation. Later during the conference I discussed with
Girard the prospects of relation algebra as a model of noncommutative
linear logic. It was clear that !A would be the Boolean-behaved 1&A,
but Jean-Yves did not seem terribly enthusiastic about this
interpretation of !, though he seemed to like the residuation
structure.
Shortly before the Jumelage I had given a talk at Stanford about both
binary relations and languages (sets of strings) as models of linear
logic, interpreting tensor noncommutatively for binary relations as
composition, with complement-of-converse as linear negation, and
commutatively for languages as shuffle or interleaving, where I did not
have a candidate for linear negation.
I was therefore very pleased when Martin Abadi and Gordon Plotkin, who
had attended my Stanford talk, found the "right" linear negation for
languages, described in their POPL'91 paper (p.323). They describe the
linear negation of the language M as the set of "not-crashes-with"
strings. This can be seen to be exactly the language analog of
relational complement-of-converse, modulo the details of the "crashes
with" relation between strings.
To make this connection, think of pairs (x,x) in a relation as
"crashing" in the sense of failing to make progress. Under this
interpretation the set of those pairs that do not "crash with" any pair
in relation R are just those pairs (y,x) such that (x,y) is not in R
(since their composition would yield a (x,x) pair). But this is just
complement of converse of R! From this perspective the "crashes with"
relation would appear to actually generalize complement-of-converse,
since one can imagine repeating this exercise for various notions of
"crashes with." In fact I'm none too clear on just how canonical
Martin and Gordon's crashes-with is.
I think this provides an easy intuitive TRUTH VALUE SEMANTICS
for a noncommutative linear logic. The equational
characterization of this structure is quite straight-forward
and can be read off from what I have written above.
While binary relations are indeed attractive in these and other
respects, they seem not to measure up to certain prevailing standards
for models of linear logic. On the one hand these standards appear to
be defined by coherence spaces. On the other hand coherence spaces are
algebraically untidy---they don't form a variety for example---and they
are also of rather limited applicability compared say to event
structures or Scott domains.
The category St of state spaces, posets with all nonempty meets, and
their bottom-and-nonempty-meet-preserving morphisms, would seem to
model linear logic every bit as well as coherence spaces but without
the above defects. In particular it is a variety (monadic in Set), yet
it properly embeds Scott domains which embed (the dual of) event
structures which embed coherence spaces which embed Boolean algebras.
These embeddings are depicted in a series of diagrams in section 2 of
/pub/algecon.{tex,dvi} on boole.stanford.edu.
Of particular interest to anyone designing parallel programming
languages is that this category interprets A & B (LL "with", i.e.
product) as asynchronous parallel composition, A o+ B (plus) as guarded
choice, and A ^8 B (par) as "orthocurrence" (describing such flow
situations as trains through stations, signals through circuits, etc.)
It also admits straightforward definitions of other programming
operations such as blind choice, sequential composition, and Winskel's
notorious partially synchronous parallel composition as tamed by
Vaandrager, none of which however bear any visible relationships to the
operations of linear logic.
These advantages notwithstanding, this category is simpler to define
than any of those it subsumes, coherence spaces included. Moreover,
although its morphisms are new, its objects, up to isomorphism, are
familiar as the intersection structures prominently featured in Davey
and Priestley's "Lattices and Order" (CUP 1990).
The operations of perp (as A -o _|_ ) and converse (as order dual)
lead, by analogy with binary relation perp as complement-of-converse,
to the notion of *complement* of a state space defined as
perp-of-converse. When all the calculation has been done (and note
that every point of perp has to be calculated as a strict
meet-preserving function, though the order dual is nothing), we end up
with the notion of complementation being merely the following: delete
the bottom element (the state q_0, representing total absence of
information) and reinstall it as top (the event oo, representing the
unperformed event). This innocent-looking operation has the somewhat
surprising effect of creating all nonempty joins, at the cost of some
meets that may disappear.
After 13 months of looking at this gadget from all sides and seeing
more in it all the time I am still amazed that so much structure could
come out of so trivial a definition. More information in es.tex,
esrs.tex, and algecon.tex in /pub on boole.stanford.edu.
Vaughan Pratt