algebraic semantics of NLL

• To: types
• Subject: algebraic semantics of NLL
• From: Thomas Streicher <streiche@fmi.uni-passau.de>
• Date: Fri, 24 Jan 92 17:09:50 EST
• Sender: meyer@theory.lcs.mit.edu

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

• Prev: "Essentials of Programming Languages" -- free instructor's copies
• Next: non-commutative linear logic
• Index(es):
  • Main
  • Thread