Subject: Re: Red and blue (again)
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-09-29 15:31:47 GMT (2 years, 32 weeks, 1 day and 34 minutes ago)
Dear Alessio, Yesterday I finally read the thread at Frogs@... 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