[Prev][Next][Index][Thread]
Re: A tale of two translations
-------
The following note from a month ago apparently was sent
to only a subset of linear recipients. I appologize to
those who get two copies.
Patrick Lincoln, linear moderator
-------
Phil Wadler wrote:
|There are at least two translations that have been discussed of
|intuitionistic logic into intuitionistic linear logic.
|
|(i) Standard. This takes A -> B into (!A) -o B.
|(ii) Less standard. This takes A -> B into !(A -o B).
He then remarked that the beta rule is not preserved by the
second translation, and that the second translation induces a
strict [rather than lazy] semantics.
In a personal message, Phil Wadler clarified that he translates the
atom A to !A in the second translation (which makes eminent sense).
I'm not sure atoms are translated as !A for the (!A -o B) standard
translation.
In response, Yves Lafont wrote:
> Two remarks about Phil Wadler's message
>
> 1) I prefer to say that the second translation takes A->B into !A-o!B. More
> precisely, it takes an intuitionistic proof of Gamma |- A into a linear proof
> of ![Gamma] |- ![A] where [A] is defined inductively as follows:
>
> [P] = P (atomic case), [A->B] = ![A]-o![B].
The !-prefixing of all formulae in the sequent suggests that the translation
is really [A] = !A and [A->B] = !([A] -o [B]). I prefer to think in LU
terms, using polarities, and so I see this as saying that all intuitionistic
types are hereditarily positive. That is, atoms are P (equivalent to !P),
and P->Q is translated as !(P -o Q), where P,Q are positive. Since we have
only positive polarities, we can freely use left structural rules. Note that
P -o Q itself is of neutral polarity, and so must be promoted to !(P-oQ). One
can think of this as "the best of translations, the worst of translations".
The best of translations, since it also works in non-intuitionistic contexts,
and the worst, since it is most profligate (derelict). That is, this chimera
does not rely on the fact that the contexts are themselves translations of
intuitionistic sequents --- and can also deal with neutral polarity head
variables. An example where the standard (!A -o B) will not work is:
Consider the term <f x, f x> % <_,_> is pairing
which is typed by the sequent (where we follow the first translation)
f:!(!A -o A), x: !A |- <f x,f x> : A*A
Now consider the non-intuitionistic deduction
!B, A |- A C |- C
------------------- % || is par
!B||C, A |- A, C
----------------
!B||C, !A |- A,C
-----------------
!B||C |- !A-oA,C
Unfortunately, we cannot use !-R to promote (!A -o A) and so cannot use
(Cut). (In intuitionistic contexts without head variables, the standard
works). Of course, we ought to exponentiate before introducing ||, but that
is the !(!A-o !B) translation... I have a note about
a "positive intuitionistic fragment of LU" (reference below). However,
I haven't looked at all at the denotational semantics, but only the cut
elimination aspect. My hope is that the usual positive correlation
space approach will suffice.
@TechReport(Sanjiva-POS-LU,
Author="Sanjiva Prasad",
Title="{The Positive Intuitionistic Fragment of {\bf LU}}",
Type="ECRC Technical Report",
Number="ECRC-94-11",
Institution="ECRC Munich",
Year=1994
)
>
> 2) You are right Phil! The first translation is lazy and the second one is
> strict. If your prefer, the reduction of proof nets implements a call-by-name
> strategy by the first translation, and a call-by-value strategy by the second
> translation. This assumes that we forbid reductions inside boxes and
> commutative reductions. This restricted reduction of proof nets is called
> "lazy" by Samson Abramsky. I prefer to say "external" in order to avoid
> confusion. See my paper "from proof nets to interaction nets" available by ftp
> anonymous on lmd@univ-mrs in pub/lafont.
I may be far off-base here, but it seems to me that Abramsky's intuition
was that terms with linearly maintained types have to be evaluated and so
they place a demand, whereas those with exponentiated types can be lazily
evaluated. In the case of the second translation, everything (in particular,
the type of the rhs term) is exponentiated, and so there is no demand-driven
evaluation. So if there is to be any evaluation it is data driven (strict).
Regards,
Sanjiva