[Prev][Next][Index][Thread]
translating classical to linear logic (338 lines)
Date: Wed, 17 Jun 92 15:44:10 +0200
Yes, it's me again.
Sorry to bother all of you!
I received several new answers for my request of a simple embedding
of Classical Logic inside Linear Logic.
I mail them to the net because they could be of general interest.
From: stefano@di.unito.it ( Stefano Berardi )
Date: Mon, 25 May 92 15:55:54 +0200
A quick question to linear people:
what is the simplest interpretation of First Order Classical Logic in Linear
Logic known up to now?
Of course I heard of several of them, but I found all of them a bit tricky.
I consider only complete interpretations, i.e. mapping:
Phi: {First Order Classical Formulas} -> {First Order Linear Formulas}
such that A is a classical theorem iff Phi(A) is a linear theorem.
Please answer me, not to the net, since I suppose the argument be widely
known, except by me!
S. Berardi
>From murthy@margaux.inria.fr Wed May 27 14:52:24 1992
Hi, Stefano,
Every interpretation of CL into CLL that I know of factors THRU a
translation of CL into IL. Thus, if one wants to know what equations
between classical proofs are enforced by a particular translation into
CLL, it suffices to consider the equational theory of the translation
into IL.
Essentially, any translation is going to end up sequentializing the
program completely, so one might as well just stick with CPS.
(omissis)
See you soon,
--chet--
Date: Thu, 28 May 92 13:07:08 -0500
From: "Uday S. Reddy" <reddy@cs.uiuc.edu>
what is the simplest interpretation of First Order Classical Logic in Linear
Logic known up to now?
Hi, The only translation I know of is Girard's in his paper on LC.
(MSCS, 1991, 255-296). Are there others? I would be interested to
know what you find out.
Cheers,
Uday Reddy
From: Stefano Berardi
Dear Prof. Randy,
you asked me which translation of Classical Logic inside Linear Logic I
was thinking about in my message to the net.
I was considering three of them:
(1) compose any (sound & complete) embedding of Classical Logic inside
Intuitionistic Logic with the canonical embedding of Intuitionistic
Logic inside Linear Logic.
(2) The first Girard's translation:
phi(Atom) = ?!Atom
phi(AvB) = phi(A) par phi(B)
phi(not A) = ?(dual of phi(A))
phi(ForAll x A) = ?!(Any x phi(A))
(3) The second Girard's translation:
p(Atom) = Atom
n(Atom) = Atom
p(AvB) = p(A) plus p(B)
n(AvB) = !n(A) par !n(B)
p(not A) = dual of n(A)
n(not A) = dual of p(A)
p(ForAll x A) = Any x ?p(A)
n(ForAll x A) = Any x n(A)
A sequent A1 ... An |- B1 ... Bm is interpreted as:
|- n(A1) ... n(An), p(B1) ... p(Bm)
These three translation agree on one point:
they all give a very tricky interpretation to the Cut Rule,
i.e. to the application of a function to an argument.
This makes unpractical the use of Linear Logic in extracting
the constructive content of Classical proofs.
Constructive content of proofs is my actual research field.
Does anyone know better translations?
Stefano Berardi
Date: Fri, 5 Jun 92
From: glb@dcs.edinburgh.ac.uk (Gianluigi Bellin)
Dear Stefano,
this is in relation to a comment that all translations of Cl in LL
<<factor through intuitionistic logic.>>
In Linear Logic, TCS 1987, pag.90-92, there are two translations of classical
logic into linear logic.
I agree that the first one (that you called Girard's First Translation)
<<factors through>> a translation of Cl into IL.
The second one (you called it Girard's Second Translation)
is a translation of cut-free classical logic,
based on the idea of translating positive and negative occurrences of the
same classical connective into different linear connectives.
The translation in <<A new constructive logic ...>> (MSCS, 1991, 255-256)
seems a refinement of the first translation using the main idea of the second.
We have cut elimination, but we need the notion of formula with polarity.
(omissis)
Date: Mon, 8 Jun 92 10:25:04 -0700
From: Jean-Yves Girard
dear stefano
this question is the center of my recent paper
A NEW CONSTRUCTIVE LOGIC : CLASSICAL LOGIC
published in MSCS
ciao
jy
From: Andrea Masini <masini@di.unipi.it>
Date: Mon, 8 Jun 92 10:32:46 +0200
In their important paper in LICS'91, Lincoln, Scedrov and Shankar give
a translation of a contraction- and cut-free system for implicational
intuitionistic logic into a fragment of propositional linear logic.
In the short LaTeX abstract below, we present how, somewhat in a similar
spirit, we can give a translation of the full propositional classical
logic into the full propositional linear logic without exponentials.
Comments and remarks are welcome.
Simone Martini e Andrea Masini
Dipartimento di Informatica,
Universita' di Pisa, Italy.
(paper omitted, because it was sent to the net)
Date: Tue, 9 Jun 1992 10:49:46 +0200
From: harold@fwi.uva.nl (Harold A.J.M. Schellinx)
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
Dear Stefano,
Regarding your question on translations of first order classical
logic into linear logic you might be interested in the following
class of translations, that have been considered by myself and
Jean-Baptiste Joinet of Universite Paris 7. They have the property
of translating faithfully proofs in a two-sided version of sequent-
calculus for classical logic into proofs in two sided sequent-
calculus for classical linear logic (faithful in the sense that the
'skeleton' of the derivation remains unchanged);
moreover cut-free proofs remain cut-free after translation.
t(p) = !p for atoms
t(A \/ B) = !(?t(A) par ?t(B))
t(A /\ B) = !(!?t(A) tensor !?t(B))
t(A -> B) = !(?t(A) --o ?t(B))
t(Forall x A) = !(Any x ? t(A))
t(Exists x A) = !(Some x ? t(A))
It's then easy to prove the following:
(G, D denote mulsitsets; ?D means putting a '?' in front of all formulas
in D; t(G) means the sequent consisting of t-translation of all formulas
in G)
Thm.: In CL a sequent G => D is provable if and only if in CLL the
sequent t(G) => ?t(D) is provable. Moreover this is a faithful
translation of derivations.
I'm speaking of a 'class' of translations, because all kinds of variations
are possible: you might as well start with translating atoms by ?p and
then 'dualize' the above; or use additives: e.g. put
t(A /\ B) = !(?t(A) 'additive and' ?t(B)).
(Note the obvious relation of these translations with what you
called 'Girard's first translation'.)
Hope this is an appropriate addition to the answers you already obtained.
Could you explain to me what you mean by a 'tricky interpretation of
the cut-rule'? (In the above case, an instance
G1 => A, D1 G2, A => D2
----------------------------
G1, G2 => D1, D2
of cut in a classical derivation is interpreted by
t(G2) , t(A) => ?t(D2)
------------------------
t(G1) => ?t(A), ?t(D1) t(G2), ?t(A) => ?t(D2)
---------------------------------------------------
t(G1), t(G2) => ?t(D1), ?t(D2)
Note that the ?-introduction in the right branched is possible because
all t-translated formulas start with a 'bang'.)
Kind regards,
Harold Schellinx
Amsterdam
From: Stefano Berardi
First of all, thank to all of you for your kind answers.
Here some comments of mine.
1) I (and C. Murthy)
had opinion that to interpret Classical Logic inside Linear Logic you have
to pass through Intuitionistic Logic. I also dared to say that interpretation
of Classical Cut rule in Linear Logic was <<tricky>>.
This seems to be correct only for the first generation of translations; the
translation described by H. Schellinx does not <<factorize>> through
Intuitionistic Logic (or, at least, I did not find a way to factorize it)
and has a natural interpretation of Classical Cut Rule..
2) G. Bellin, Simone Martini and Andrea Masini
pointed out that I did not consider, among the <<simple>> interpretations,
those for the cut free (and maybe contraction-free) fragment of
Classical Logic.
I owe some explainations. I was considering the practical use
of linear logic to extract the computational content of real classical proofs.
For this purpose, I need to to consider proofs with Cut and contractions. It is
true that I could normalize classical proofs before translating them, but this
procedure makes difficult to <<see>> which program you obtain out of a
classical proof.
Moreover, (differently from Martini& Masini)
I consider first order proofs, thus I cannot in general remove
contraction from proofs. Consider a predicate P and the Minimum Principle for P:
There is an x s.t. For all y, P(x)->P(y)
This formula is classically provable, but not without contractions.
3)I still do not know a perfectly satisfying tranlsation CL -> LL
(I am really a bad guy!).
I was looking, again for reasons of
simplicity and practical use,
for an interpretation the purely symmetrical version of classical
logic, with sequents with only the right side, (i.e. |- Gamma)
and negation interpreted not as connective, but as
<<switching>> of conjuction and disjonction. In particular, I tried to find
an interpretation phi such that:
phi(not not A) = phi(A),
phi(not(A or B)) = phi((not A) and (not B))
phi(not (A and B)) = phi((not A) or (not B)))
but I did not succed.
In Schellinx and Joinet's translation, phi(not not A) = !?phi(A), because
in a sequent Gamma |- Delta the left and the right side are not interpreted
in the same way.
All the best,
Stefano Berardi
17 Giugno 1992