Re: Light logics vs. CoS

Hello,

I'd like to give some comments on Ugo's observations.

On Monday 07 June 2004 16:37, Ugo Dal_Lago wrote:
> 1. ELEMENTARY LINEAR LOGIC (ELL, [2])

> 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

In fact, I also played around with that system, but without knowing that it 
already had a name. I can confirm that all the results of [4] do also hold 
for ELL. Furthermore, the proofs become simpler. In particular, the proof of 
the decomposition theorem can be simplified a lot if !!R is not equivalent to 
!R. 
Another, maybe unrelated observation is that the (still open) decidability 
problem for the two logics is equivalent, i.e., if one is decidable then so 
is the other, and vice verca.


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

That depends on the definition of local and the definition of the rule(s).
What I would do, is to present an infinite number of rules, one for each 
natural number. For example, for n=4, we would get

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

Then these two rules are not more and not less local as the usual b^ and b_


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

Did you try the naive deep versions of these rules, i.e.:

  S[R,T]     S[R]
  --------   -----
  S[?R,!T]   S[!R]

My first wild guess would be that your are not more powerful (in the sense of 
provability) than with the shallow versions. If I am wrong, it would be 
interesting to see the formulae that can be proved with the deep versions, 
but not with the shallow ones.


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

It appeared already: TCS Vol. 309 (2003), pp. 213-285
However, Elsevier managed to put in several mistakes. If you are really 
interested in the proofs, I'd suggest using my thesis (ch. 4), where the 
exposition is more detailed.

I hope, I could help a little.

Best
Lutz