Light logics vs. CoS

Hello!

Currently, I am interested in a class of subsystems
of Linear Logic that are collectively called light
logics. This class includes logical systems 
which are very different from the one originally defined by
Girard [2]. The main reason why these logics are
interesting is that they correspond, through
the Curry-Howard correspondence, to relevant
complexity classes such as deterministic 
polynomial time, nondeterministic polynomial time
and elementary time.
I am curious about the possibility of defining
deep inference systems for these logics
(at least for their multiplicative fragments, which
are enough to get the surprising results mentioned
above). After reading [4], I realized that the 
situation can change dramatically while switching 
from one logic to another. But let us briefly 
summarize the situation on different subsystems of MELL:


1. ELEMENTARY LINEAR LOGIC (ELL, [2])

This system is obtained from MELL discarding
dereliction and replacing promotion by the
following rule (called "functiorial promotion"):

 |- Gamma,A
 ------------
 |- ?Gamma,!A

A CoS system for ELL can be easily built from
the one in [4] by:
a. Dropping all the syntactic congruence rules
for the exponentials (except the ones expressing
the duality between ! and ?).
b. Replacing rules b^ and b_ by
  
 S[?R,?R]    S{!R}
 --------   --------
  S{?R}     S[!R,!R]

I think most proof-theoretical results about
MELL can be easily trasferred to this system



2. SOFT LINEAR LOGIC (SLL, [3])

This system is obtained from ELL replacing
contraction and weakening by the following
rule (called "multiplexor"):

 |- Gamma,A,...,A
 ----------------
 |- Gamma,?A

This new rule subsumes dereliction, weakening
and (a very restricted form of) contraction. 
In CoS, this rule can be formulated as

 S[R,...,R]      S{!R}
 ----------   ------------
  S{?R}       S[R,...,R]

I don't think, however, that this is a
satisfactory formulation (it is not local, is it?). 
The usual b^ and b_ are too powerful here.



3. LIGHT AFFINE LOGIC (LAL, [1])

This is a simplification on the original system
by Girard. Four modalities are needed, but the
interesting one is the usual !, which behaves
similarly to ELL but with the following, very
strict, constraint on functorial promotion: Gamma 
can contain at most one formula occurrence. In
other words, one replaces functorial promotion by

 |- A,B    |- A
 -------   -----
 |-?A,!B   |- !A
 
Naively, you can translate these two rules into
CoS rules
 
 [R,S]     [R]
 -------   ----
 [?R,!S]   [!R]

These rules, however, are not deep!
Currently, I am trying to understand whether 
light affine logic and deep inference
are inherently incompatible or not.


Help and Suggestions are welcome!

Ugo.


REFERENCES

[1] Andrea Asperti: Light Affine Logic. LICS 1998: 300-308

[2] Jean-Yves Girard: Light Linear Logic. Information and
Computation. 143(2): 175-204 (1998)

[3] Yves Lafont, Soft Linear Logic and Polynomial Time, 
to appear in Theoretical Computer Science

[4] Lutz Straßburger. MELL in the Calculus of Structures.
Technical Report WV-01-03, to appear in Theoretical Computer Science


-------------------------------
Ugo Dal Lago
Ph.D. Student
Department of Computer Science
University of Bologna
dallago-iEixELS/[email protected]
http://www.cs.unibo.it/~dallago
--------------------------------