[Prev][Next][Index][Thread]

non-commutative linear logic

Date: Thu, 23 Jan 92 15:31:13 -0800
To: LINEAR@cs.stanford.edu

Is the following result already well known ?

If one takes an arbitrary set M and then the set Rel of all binary
relations on M ordered by set inclusion then this lattice can be made into
a model for non-commutative linear logic with only ONE NEGATION as opposed
to the work of M. Abrusci !

The additives are interpreted as the usual lattice operations.
We denote them as
			BtopB BzeroB BorB BandB .
The tensor  BtenB is defined as follows :
	 R BtenB S  = { (x,y) | x R z  and  z R y  for some  z }
i.e.  the tensor operation is the composition of relations !!

The unit
		BoneB  is defined as  { (x,x) |  x in M }
which obviously is a neutral element for tensor

The exponential  !  is defined as follows
		 ! R  =  R BandB B1B = { (x,x) | x R x },
and we also have an operation c making out of R its commutative version
		  c R = { (x,y) | x R y  or  y R x }  .

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) }  .

Then we define the other multiplicative connector BparB as follows
	    R BparB S  =  ((S BorthB) BtenB (R BorthB)) BorthB
and get the following Galois connections (where for the lattice order we
write BleB )
	 T BtenB S   BleB  R    IFF   T  BleB  (S BorthB) BparB R
and
     S  BtenB T   BleB  R    IFF    T  BleB  R BparB (S BorthB)    .

Thus - as expected we have two implications, but only one negation, i.e.
	    R -o BbotB  =  R BorthB =  BbotB o- R    for all R
where
	    BbotB = BoneB BorthB = { (x,y)  |  not x = y }  .

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.

Of course, instead of starting from the relation algebra of ALL relations
on a set M one can start from an ARBITRARY RELATION ALGEBRA A :
		 generally   R BorthB :=  - (R*) = (- R)*
where  (_)*  is involution and  -(_)  is negation.

In the light of a recent representation result due to C. Brown and D. Gurr
any such algebraic model of NLL (Noncommutative Linear Logic) can be
represented as such a non-full relation algebra !!!

A remarkable fact is that in our case the subset of objects of the form !R
do not only form a Heyting but actually a boolean algebra.

This, of course, can be weakened by studying INTUITIONISTIC instead of
CLASSICAL relation algebras.  In that case it is impossible to prove that
BorthB is involutory !!

Nevertheless one can axiomatize the operation BorthB as suggested from the
particular case above. It simply will not be definable in term of
involution of relations and intuitionistic negation (as a lattice
operation).

Surely, there is still a lot of details to check for the non-classical
case !  Another point of interest is to look at the corresponding phase
space semantics .

A final remark concerning proof semantics : by using the techniques of
Valeria de Paiva one can construct from truth value semantics as given
above a nice Dialectica like model of noncommutative linear logic.  The
key idea is to start form a model L of the kind studies above and then
consider the category
				  Pr(L)
whose objects are triples (U,X,R) where U and X are sets and
			     R : U x X -> L .
A morphism from  (U,X,R)  to  (V,Y,S)  then simply is a pair of
set-theoretic functions
		     f : U -> V     and   g : Y -> X
such that
     R ( u , g (y) ) BleB S ( f (u) , y ) for all u in U and y in Y .

How to define the operators of linear logic on Pr(L) is in some sense
straightforward using essentially the ideas of ValeriaBs work.  How to do
this exactly will be detailed in a next mail.

Thomas Streicher