# 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
------------------------------------(R,!)
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
coalgebra.

[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.