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

algebraic semantics of NLL



Date: Fri, 24 Jan 92 10:10:11 MET
To: LINEAR@cs.stanford.edu

The underlying algebraic notion for non commutative linear logic  
without exponentials is the following one.

Let  L  be a semi-sup-lattice enriched monoid together with an  
involution, i.e.

     (_) BorthB : L -> L

which is antitonic and self inverse satisfying the following condition:
 

 x BtenB y  BleB z    iff   (z BorthB) BtenB x   BleB  (y BorthB) .

An equivalent characterization would be to have two forms of  
implication :  -o  and  o-  together with a distinguished object
BbotB  for which we have

 BbotB o- (x -o BbotB)  =  (BbotBo- x) -o BbotB  for all  x

or equivalently for all x,y:

  x BtenB y  BleB BbottomB   iff   y BtenB x  BleB BbottomB   .


REMARK It does not seem to be straightforward to extend the Brown & Gurr
representation theorem in a way such that orthogonalization is easily
expressible in terms of operations on the representing relations.

Brown&GurrBs representaion thm uses a function rep with

   rep(x) =  { (y,z) | y BtenBx BleB z }  .

I have been unable to express rep(x BorthB) in terms of rep(x) by a simple
relation algebraic operation.


Thomas Streicher