[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.