geometry of interaction & categorical models of LL

To: linear@cs.stanford.edu
Subject: geometry of interaction & categorical models of LL
From: Thomas Streicher <streiche@informatik.uni-muenchen.de>
Date: Tue, 18 May 93 15:31:09 +0200
Approved: types@dcs.gla.ac.uk



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?

Thomas Streicher