[Prev][Next][Index][Thread]
Relations and non-commutative linear logic
Date: Fri, 15 Nov 91 18:27:13 +0100
To: linear@cs.stanford.edu
Quantales are a generalisation of locales, introduced by Mulvey [4] with the
aim of providing a constructive formulation of the foundations of quantum
mechanics. Interest in quantales has recently been stimulated by the
fact that intuitionistic linear logic can be interpreted in any commutative
quantale, and that commutative quantales constitute a sound and complete class
of models [5].
We study relational quantales, in which the elements are relations on a set A
ordered by inclusion, and the monoid operation is relational composition. Such
structures have been proposed by Hoare and He Jefing [3] as models for the
semantics of non-deterministic while programs and for program specification.
Our central result is that relational quantales provide a sound and complete
class of models for a non-commutative intuitionistic linear logic. The
result rests on a representation theorem [1] for quantales which states that
every quantale is isomorphic to a relational quantale.
Our non-commutative intuitionistic linear logic has several attractive
properties. It discards even the limited commutativity of Yetter's
logic [5] in which cyclic permutations of formulae are permitted. It arises in
a natural way from the system of intuitionistic linear logic presented in [2],
and satisfies a cut elimination theorem. In linear logic, the rules of
weakening and contraction are recovered in a restricted sense by the
introduction of the exponential modality (!). In our logic the modality !
recovers non-commutative analogues of these structural rules.
The value of this result is that it provides natural models in which the
non-commutative $\otimes$ is interpreted by the familiar notion of relational
composition and the exponential !A has a natural interpretation as the largest
reflexive and transitive relation contained in A. In addition, it suggests
that non-commutative linear logic may be a suitable language to describe the
structures proposed by Hoare and He Jefing.
If you wish to receive a copy of a draft paper about this work then send
email to cbrown@daimi.aau.dk or dgurr@daimi.aau.dk.
Carolyn Brown Doug Gurr
------------------------------------------------------------------------------
[1] C. T. Brown and D. J. Gurr. "A representation theorem for quantales".
JPAA (to appear).
[2] J-Y. Girard and Y. Lafont. "Linear logic and lazy computation".
In Proc. TAPSOFT 87 (Pisa), volume 2, pp 52-66, 1987. LNCS 250.
[3] C. A. R. Hoare and He Jefing. "The weakest pre-specification".
Information Processing Letters, 24:127-132, 1987.
[4] C. J. Mulvey. "&".
Suppl. ai Rend. del Circ. Mat. di Palermo, Serie II, pp 99-104, 1986.
[5] D. Yetter. "Quantales and non-commutative linear logic".
Jour. Symb. Logic, 55-I:41-64, 1990.