[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