geometry of interaction & categorical models of LL
I have tried to make a categorical model out of the ingredient's of
Girard's GEOMETRY of INTERTACTION I.
It all works well for the multiplicative part.
Objects : countable sets
Morphisms : a morphism fromm X to Y is a partial injective map
m : X + Y -> X + Y
Composition : if m : X + Y -> X + Y and
n : Y + Z -> Y + Z
then n o m is defined as the union over all i : N :
[inl,0,0,inr] o ((n+m) o [in1,in3,in2,in4])^i o (n + m) o [in1,in4]
Of course, this is a model where linear negation is the identity on
objects, i.e. what I call strong involution.
There are no additives in this model.
W.r.t. to EXPONTIALS there is some good candidate for obtaining a
comonad ! .
But there is a severe problem which already shows up on the level of
DYNAMIC ALGEBRA :
!(f) = !(f o d*) o t* does not hold
or in other words
!(f) = lift(deril(f)) does not hold.
QUESTION Has anyone overcome this problem ? I guess in the
Abramsky&Jagadeesan approach this problem can be avoided. WHY?