[Prev][Next][Index][Thread]

Answer to Carolyn

[This message is an answer by Jean-Yves Girard to questions posed by
Carolyn Brown in an earlier message.  As a reminder, the message from
Brown appears first.  -- Phil Wadler, moderator, Types Forum]

-----------------------------------------------------------------------------

>Date: Fri, 30 Oct 92 16:13:15 +0100
>From: Carolyn Brown <cbrown@cs.chalmers.se>
>Subject: question about rules for !

I have a simple question about the two common presentations of the
rules for !. I've discussed this with several linear-logicians, without
reaching a conclusion. 

Two presentations commonly used (for single-conclusion calculi) are

(I)  !Gamma |- A        Gamma, !A, !A |- B      Gamma, A |- B      Gamma |- B
     -----------        ------------------      --------------     ------------
     !Gamma |- !A       Gamma, !A  |- B         Gamma, !A |- B    Gamma, !A |-B

and

(II) The last three rules above with the first rule replaced by:
 
        B |- I    B |- A    B |- B \otimes B   (where I is the unit of \otimes)
        ------------------------------------
                  B |- !A

System (II)  is the categorical combinator version of the rules, characterising
!A as a greatest fixed point (coinductive type).

My question is, when are the same sequents derivable in linear logic using 
presentations (I) and (II) of the rules for ! ? The answer may  differ 
depending on the fragment of linear logic we are interested in. 

Clearly rules (I) are derivable from rules (II) (using rules for the unit I
and \otimes, together with Cut and the Identity axiom).

Can anyone tell me under what circumstances the same sequents are provable
using (I) and (II)?

Thanks,
Carolyn

-----------------------------------------------------------------------------



                          Answer to Carolyn

        This is not an answer ; just one remark together with questions !
For me the problem is not to determine the relative strength of (I) and (II), 
but rather to determine which is the correct formulation. In this respect,
the main problem is with the proof-theoretical status of (II), (I) being
unproblematic.
QUESTION 1 : does (II) enjoy cut-elimination ? I mean a real result, not
something without any subformula property. It seems that the premises
B /- 1 and B /- B times B can be used to handle erasing and duplication
of B. Of course the subformula property is spoiled with 1 and tensors, but
it is not definitely destroyed.
QUESTION 2 : what is the denotational status of (II) ? A usual bang is a
comonoid, but arbitrary weakenings and duplication will not enjoy (co)
neutrality and (co) associativity.
QUESTION 3 : what about geometry of interaction of (II) ? It might be quite
cumbersome...
        As far as phase semantics is concerned, the natural way to form !A
is to consider the double perp of the intersection of A with a given set of
phases F ; F is in turn the intersection of the fact 1 with a set of phases G :
in the case of (I) G is the set of idempotents, whereas in the case of (II)
G consists of those x such that, for all y, if xxy is in BOTTOM, so is xy.. If
one wants to obtain completeness wrt very concrete phase spaces (eg integers),
(I) must be excluded for want of idempotents.
        Again this was everything but an answer : just an attempt to compare
the two formulations.

        By the way I take this opportunity to give my new coordinates :
Laboratoire de Mathematiques Discretes, UPR 9016
163 Avenue de Luminy, case 930
13288 Marseille cedex 09

Please do not use my previous home address (rue Sibuet) that I was using
only because of the unreliability of the mail in Jussieu-Paris VII.

        Tel : (33) 91827025
                   91827026 (secretary : Mme Bodin)
        Fax :      91827015

the new Email is not yet working

jean-yves girard