Re: Light logics vs. CoS

At 12:11 PM +0200 8.6.04, Lutz Strassburger wrote:
>On Monday 07 June 2004 16:37, Ugo Dal_Lago wrote:
>  > 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_

Just a quick observation (I'm completely submersed in the summer 
school organisation, but I cannot resist nitpicking what Lutz says).

It's true that the rules Lutz proposes, in isolation, are local. BUT 
the resulting system wouldn't have the property that the search space 
is finitely branching, which, for a propositional system in CoS, is 
not very nice.

So, the real question is whether we can do better than that. 
Unfortunately, my brain is so fried now that I cannot be constructive.

-Alessio