Re: Red and blue (again)

Hello everybody,

I've read Dale's message and had a look at David's paper. I have some 
moral remarks.


1)  Dale asks whether non-canonicity of exponentials/dots is an 
artefact of the sequent calculus. In my opinion, it is not, and it is 
in fact something the sequent calculus does right. The only artefacts 
the sequent calculus creates are with conjunction and disjunction: 
specifically, when one maps connectives into meta-level conjunctions 
and disjunctions one gets artefacts. For example, an artefact is the 
equivalence between red and blue conjunctions (or disjunctions). It 
might be desirable, but it is an artefact.

My criticism towards the sequent calculus is that it is not a 
transparent syntax, for example because it creates this kind of 
distortions. (Of course, I'm saying this because my mission is to get 
rid of syntax and bureaucracy in proofs as far as possible.)


2)  Dale seems to imply that canonicity can be desirable or not 
depending on circumstances. If so, I agree with him, and I think that 
the best a syntactic formalism can do is to provide means for getting 
canonicity when desired and not forcing it otherwise.

In my opinion, the best one can do with the sequent calculus when 
trying to force canonicity is resorting to its only source of 
canonicity: the meta-level. The examples that Dale mentions seem to 
me to show this: one gets canonicity for exponentials by resorting to 
`tricks' with conjunctions and disjunctions (doesn't matter whether 
finitary/infinitary or multiplicative/additive). As far as I 
understand it, the situation is similar in categorical semantics, 
where the role of the meta-level is played by universal constructions 
like the product.

My point is that all of this is fine as long as you get what you want 
and as long as you have independent reasons for staying with the 
sequent calculus or its categorical semantics. However, one might not 
have these constraints...


3)  David's rules for the exponentials/dots are basically the deep 
inference rules you get in the deep inference presentation of linear 
logic: modalities just match with their mates and they don't check 
their environment (see Lutz's paper at 
<http://www.ps.uni-sb.de/~lutz/papers/lls-lpar.pdf>).

I understand that CoS is more exotic than the sequent calculus, 
however, I believe that the rules like in Lutz's paper are more 
elegant than their sequent calculus counterparts. In CoS, `matching' 
rules like David's are the norm, while in the sequent calculus they 
are the exception.

Please don't take this as an argument about a competition between 
formalisms. I'm just trying to offer my very biased point of view. I 
know that (at present!) deep inference is no use for verification, 
etc., so I understand you might prefer having more standard rules.


4)  Dale, aren't you worried about your keeping Girard's sybillic 
messages in mind for 11 years!?


Ciao,

-Alessio


At 17:31 +0200 29/9/05, Dale Miller wrote:
> Dear Alessio,
>
> Yesterday I finally read the thread at 
> Frogs-oCDm4u4wUTdmSpRlfIrTPQ@xxxxxxxxxxxxxxxx
> titled "Red and blue (again)" that was cc:'ed to me.  Sorry for
> not having read it before since the topics addressed in it are
> quite interesting to me.
>
> I write the following response and it might be appropriate as a
> follow-up to that thread.
>
> I'm not sure I really follow the debate about whether or not the
> "non-canonical" behavior of the exponentials in linear logic is an
> artifact of the sequent calculus or not.  I am, however, forming
> the opinion that linear logic does, in fact, have many
> exponentials that might be fruitful to consider.
>
> In the Types mailing list in 1994, there was this question about
> the exponentials of linear logic.
> http://www.seas.upenn.edu/~sweirich/types/archive/1994/msg00096.html
> Girard responded with the following message.
> http://www.seas.upenn.edu/~sweirich/types/archive/1994/msg00109.html
>
> I've been trying to understand this response better recently.  As
> a first try at the first comments about infinity and the modals, I
> see things roughly as follows.
>
> Pick some set I a subset of the natural numbers.  Denote by B^i
> the i-fold tensor of B.  Use the following "infinite rules" for
> !_I (dually for ?_I, if you want).
>
>     Gamma, B^i --> Delta               {Gamma --> B^i, Delta | i in I }
>    ===================== some i in I   ================================
>    Gamma, !_I B --> Delta                   Gamma --> !_I B, Delta
>
> Thus the !_I B is simply defined as a big & of tensors of B, where
> the multiplicity of tensors is taken from the set I.  This is a
> typical enough approach to providing a semantics for !
> (particularly, when I is the set of all natural numbers).
>
> Notice that now, !_I is canonical in the sense that red and blue
> copies are provability equivalence (if we allow the natural but
> oxyimoronic notion of "infinite proof").  The price, however, is
> clear: infinity has entered the proof system and we now have lots
> of !'s, indexed by different sets.  So, we haven't escaped the
> non-canonical aspects of !.  There is some structure in all this,
> however: if I subset J then |- !_J B -o !_I B is provable.  Etc.
>
> I think David Pym's comments on that that one doesn't expect "two
> different monoidal co-monads should be equivalent" is probably
> related to this kind of observation.
>
> I now see the original rules of linear logic as being some
> particular and natural choice for dealing "generically" with
> infinity, but the above argument suggests that this is not the
> only choice.  From Girard's response, he had in mind other
> choices: Light LL, Elementary LL, etc.
>
> Apart from the notion of infinity, let's turn to a truly "sequent
> calculus" based notion: when doing the promotion rule in sequent
> calculus, one must examine the entire sequent and make sure all
> the other formulas have the right modal in front of them.  This
> kind of rule is an easy target of ridicule.  So let's pick a more
> mild case to consider.
>
> In a report he wrote for a training project as part of his Masters
> (http://www.lix.polytechnique.fr/parsifal/baelde05stage.ps), David
> Baelde considered the problem of adding to linear logic a simple
> primitive for synchronization (in the sense of process calculus).
> He added the "logical connective" dot (arity one) and the one rule
>
>          --> Gamma, P, Q
>     =========================
>      --> Gamma, dot P, dot Q
>
> Notice that this connective is not canonical (a red dot must match
> a red one and not a blue one).  Thus, there can be many such dots,
> so index them with labels, say, a, b, c, ...  And instead of
> writing dot_a P, dot_b Q, etc, one can write them like Milner in
> CCS and get a.P, b.Q, etc.  It seems to me to be a nice story to
> have the non-canonical nature of dot lead to a familiar notation.
>
> Specific question then for Alessio: Is this issue about
> non-canonical dots an artifact also of the sequent calculus?
>
>     -Dale