Re: Structural Rules and Exponentials

This is an answer to the message by Maurizio Castellan sent from  
marco@nextiac.iac.rm.cnr.it (Thu, 2 Feb 95).

Yves Lafont.

The fact that the promotion rule in ILL (or in LL) cannot be replaced by

   A |- B   A |- 1   A |- A \otimes A
                  A |- !B

was already known. A related fact is that, if we have two exponentials ! and !'  
with the same rules in the syntax, then it is impossible to relate !A with !'A.  
In other words, ! is not determined by its rules.

Also, in coherence semantics, there are several possible definitions for  
exponentials (see [4]). One of them (not the original one) uses multisets (see  
[3]): It is a cofree (cocommutative) comonoid in the sense of [1], which is the  
categorical analogue of the above rule.

It is not so easy to give a general categorical formulation of exponentials.  
The notion given in [2] is enough to get a cartesian closed coKleisli category,  
but not for modeling linear logic. I think that the correct formulation has  
been given by G.M. Bierman.

[1] Y. Lafont, (1988). The linear abstract machine. Theoretical Computer  
Science 59, pp. 157-180 (corrections Ibidem 62, pp. 327-328).

[2] R. Seely, (1989). Linear logic, *-autonomous categories and cofree  

[3] J.Y. Girard, (1991). A new constructive logic: classical logic.  
Mathematical structures in Computer Science, 1(3), pp. 255-296.

[4] M. Quatrini, (1995). S\'emantique coh\'erente des exponentielles : de la  
logique lin\'eaire \`a la logique classique, Th\`ese de doctorat, Universit\'e  
Aix-Marseille II.