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

PAPER ABSTRACT





      NEW LINEAR LOGIC PROOF THEORY AND SEMANTIC -part I-
      Giorgia Ricci and Aldo Ursini

      Dipartimento di Matematica
      Universita' di Siena
      via del Capitano 15
      53100 SIENA-Italy-
      phone (577)288240
      fax   (577)270582
      e-mail URSINI@SIVAX.CINECA.IT

                   extended abstract
      Submitted for the Ninth Annual IEEE Symposium on
             LOGIC IN COMPUTER SCIENCE
            July 4-7 ,1994,Paris,France

      We propose a different presentation of linear logic, which
      is half-way between sequent calculus and natural deduction.
      Our "sequents" have at most one formula at the right side.
      This allows a quick and prompt proof of cut-elimination.
      Moreover,an interesting geometry -or semantic- of linear
      proofs is then at hand, and for full linear logic.
      Of course there are connections with proof nets, but
      we need no boxes...A proof of completeness, namely an
      abstract characterization of the graphs involved will
      be delayed for another occasion.

      Introduction.

      The title is ambiguous, and we wanted it to be so: here
      there is no "new linear logic", rather it is old dear linear
      logic (see GIRARD [1]) in disguise. However in future
      papers with the same title, somethimg new may arise there too.
      Also, we mean to deal here with proof theory of linear logic
      and with geometry of proofs therein. Namely, with a
      "proofnets-like" semantic of linear proofs.  Hence, semantic
      referes here to this.  But, in subsequent papers, something new
      on "truth" semantic, namely phase semantic, is likely to
      appear...

      Because the requirements of this Symposium on originality,
      copyrights, et cetera are so stringent, we decided to be vague,
      if such a behaviuor is allowed.  Here we base ourselves on the
      historical fact that: in Germany it is prohibited whatever
      is not explicitely allowed, in China it is prohibited whatever is
      explicitely allowed, in Italy it is allowed whatever is
      explicitely prohibited, BUT in England it is allowed whatever
      is not explicitely prohibited.

      1.LINEAR LOGIC IN DISGUISE.

      Let us take seriously the recurrent suggections by GIRARD about
      linear logic -shortly:LL- being apt for dealing with symmetric
      input-output relations . Hence formulas are really (physical)
      forms of plugs, a sequent is provable iff plugs in it fit well
      together, et cetera.
      In trying to make explicit this approach from the beginning of the
      deductive system, we are driven towards the following syntax.
      Let A,B,... denote formulas of (propositional) LL as in [1][;
      let S,S',T,... denote multisets, or finite sequences up to order,
      of formulas.
      A SEQUENT in LL* is a pair (S,S') such that S' has lenght
      at most 1. Notation:
                      S  ====> S'
      Notation for sequents of LL will be :
                       |- S
      In case  A,B,C,...F are formulas, we also write:
                A,B,C,...====> F
      or else
                A,B,C,...   ====>
      which will create the main question, namely: What the hell
      is the comma here ? We will address this question subsequently.

                        RULES OF LL*

        axiom          NOT A ====> A

                    S====>A      S'====> NOT A
        cut         _________________________
                         S,S' ====>

                      S====>A
        plus       ____________________
                      S====> A PLUS B


                      S====>A      S====>B
        with       ________________________
                          S====> A WITH B


                      S , B ====> A
        par        ________________________
                      S ====> A PAR B


                     S====>A     S'====>B
        tensor     ________________________
                       S,S'====> A TENSOR B

                                                 S , T ====> T'
        cross         Provided T,T' are short : _____________________
                                                 S , T' ====> T

        one              _____________
                           ====> ONE

        all              _____________
                          S ====> ALL

                           S ====>
        bottom           _____________
                           S ====> BOTTOM


                           S ====>               S====>A
        interrogation     _________            ___________
                           S====>?A              S====>?A

                                S,?A ====> ?A
                                _____________
                                 S,?A====>

                          ?S ====> A
        exclamation      ______________
                          ?S ====> !A


        (of course, why not S means empty if S empty, and means
        of course A,of course B,... if S is A,B,... )

        Proposition 1.

        There are translations from proofs in LL into proofs in LL*
        and viceversa, such that:
        i.given a proof of S====>S' in LL*, the translation is
        a proof of |- S,S' in LL;
        ii.given a proof of |-A,B,C,... in LL, the translation is
        a proof of  A,B,C,...====>   in LL*.
        Moreover, the translation does not introduce new cuts:
        a cut is present in the translated proof in LL* iff
        a cut were present in the source proof in LL.
        LL*  admits an Hauptsatz, based on the following

        Lemma.Given a proof of S====>S' (in LL*) whose last rule
        be a cut of degree  d ( greater than 0 )   , and  the
        degree of the proofs of both premisses is lower than d,
        one can construct  a proof of the same  SEQUENT  of degree
        lower then d.
        The proof of this  is remarkably neat and straight.
        Remark also that - of course via proposition 1 - you get
        cut elimination for LL....in a neat and straight way.

        2 . GEOMETRY OF PROOFS.

        We have to consider certain unoriented labeled finite
        graphs ,also called ULKs ,in each of which a certain
        finite multiset of (labeled) vertices, called the
        FRONTIER, is singled out.
        Labels will be formulas of LL, and  hence the frontier
        of an ulk  is a finite multiset of formulas,modulo
        some trivial bureaucracy.
        Ulks , and their frontiers, are defined inductively
        by following the inductive notion of proof in LL*.
        The following is the definition, and a double line
        means in it: a new link.

                  ULK                     FRONTIER

             A ====== NOT A           { A, NOT A}
        If
               G is an ulk    with frontier  S U {A,B}
        then   the following is an ulk:
        with frontier  S U {A PAR B }.(Here U is multi-union of
        multisets).
        If
             G and F  are ulks with frontiers S U {A} and
             S' U {B},
        then  the following is an ulk :
        with frontier S U S' U { A TENSOR B } ,

        Etc,Etc. Let us get into details for the  villain of
        the situation, namely WITH.

        The GLUEING of two ulks, relative to a multiset S,is a
        purely graph theoretic matter, and is defined separately
        below.(The idea is that you have that S is "common"to
        both, that they are written on two transparencies,so
        that S's formula occurrencies appear at the same spots,
        and that formula occurrences different from S's and
        the relevant links are in red for one ulk,and in blue
        for the other one: then you superimpose one on the other
        and you get their glueing -rel. to S-)
        Then we define:
        If
            G,F are ulks       with frontiers  S U {A},S U {B}
        then : first get the glueing of G and F relative to S,
        thus getting a graph  G.F,whose frontier be S'; secondly
        is, by definition, an ulk, with frontier S' U {A WITH B}.

        Another  tough  guy is  weakening ( on  ? ). But observe that
        -by  an easy induction- the frontier of an ulk is never empty
        (even the cut is not goig to annihilate a frontier....).
        Hence  we define :
        If
            G is an ulk        with frontier S
        then ,choose an entry X in S, and the following
        is an ulk, with frontier S U {?X}.
        The other induction steps corresponding to dereliction,
        contraction and the  rule (!) are  obvious.
        Then we get

        Proposition 2.If G is an ulk with frontier S , then
        there is a proof in LL* of  S ====>  .Moreover, the
        translation of this proof is  -modulo some redtape-
        exactly  G .

        Obviously, one has to pay attention to the separation
        of glued ulks, if one wants to recover the components of the
        glueing. That is why we postpone the investigation of
        a characterization (Correctness Criteria) of which graphs
        are possibly ulks.

                           REFERENCE
       [1] J-Y.Girard, Linear Logic, Theoretical Conmputer Science,
           50,1987.

        A P P E N D I X.
        This  appendix is dedicated to the definition of glueing
        of two ulks,relative to S; but this is left to the reader.

                  END OF THE EXTENDED ABSTRACT


Dear LINEAR customer,
in the  condensed form of the extended abstract of the paper:

   "New Linear Logic Semantic and Proof Theory,I"
which was in the e-mail box a couple of days ago, the pictures- in the
definition of ULK's-  where not present.The careful reader may easily
rebuild them, or otherwise please ask me for a hard copy of the
abstract.
Happy New Year,
Aldo Ursini

Aldo Ursini
Universita' di Siena
Dipartimento di Matematica
Via del Capitano 15
53100 Siena - Italy
ph: 577-286244
fax: 577-270581
email: ursini@sivax.cineca.it