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

linear decorations



Date: Thu, 18 Jun 1992 17:30:10 +0200
X-Organisation: Faculty of Mathematics & Computer Science
                University of Amsterdam
                Kruislaan 403
                NL-1098 SJ Amsterdam
                The Netherlands
X-Phone:        +31 20 525 7463
X-Telex:        10262 hef nl
X-Fax:          +31 20 525 7490
To: linear@cs.stanford.edu

         OPTIMAL LINEARIZATION OF INTUITIONISTIC DERIVATIONS
         ===================================================
                           (*Abstract*)

                V.Danos, J-B.Joinet & H.Schellinx


Technically speaking, we construct a minimal (proof by proof) embedding
of intuitionistic logic into linear logic.
There exist uniform translations from classical (intuitionistic) sequent 
calculi to (intuitionistic) linear sequent calculus. A common defect, however,
is their plethoric use of exponentials, which generally prohibits any 
computational interpretation.
The purpose of the work presented here, is to produce linearizations 
(we call them "decorations") of derivations given in (some version of) sequent 
calculus such that : 
       1/ the "skeletons" of original proofs are preserved, 
       2/ each exponential in the resulting linear proof is there for a 
"good" (= necessary) reason, i.e. because of some instance of a contraction 
or weakening rule somewhere in the proof.

In principle the decoration works as follows: 
       1/ replace intuitionistic connectors by the corresponding linear ones,
       2/ locate the structural sources (contractions and weakenings) and
          decorate them with exponentials, 
       3/ propagate the modalities so that the proof becomes a linear one.

In the standard intuitionistic sequent calculus, many strategies of  
decoration are available (depending on which place we choose to introduce 
!-marks in succedents) among which no one has canonical properties.
In the case of the neutral fragment of IUL (Intuitionistic fragment of  
Unified Logic), a notion of 'lower decoration strategy' can be defined, which 
is "sub-girardian" in the sense that the decorated conclusion-sequents are 
sub-translations of Girard's well-known translation of intuitionistic into
linear logic.

Because each exponential in such a decorated proof is imperative, one might 
think that for each sub-proof determined by a "right"-! (a "box" in terms of 
proof-nets), at least one normalisation strategy exists, in the course of which
it will be duplicated or erased. In fact this is not the case: even when
(logically speaking) they seem necessary, exponentials can be computationally  
superfluous.

This work can be seen as a technical counterpart of the folklore saying
that exponentials are in charge of duplication/erasure, non linear effects.

Applications to refined type synthesis in ML-like languages are hoped for.