[Prev][Next][Index][Thread]
A tale of two translations
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).
Regarding the second translation, Girard wrote the following
(to the linear mailing list on 14 Sep 92).
however it might be of interest to try other translations and
to study them in the spirit of denotational semantics. The
translation by means of !(A -o B) is far from preserving the
usual CCC isos, but it has its own virtues. Let us just mention
one : models of lambda-calculus can be indifferently described
as fixpoints of !X -o X or of !(Y -o Y)... the second choice is
in the spirit of lazy lambda-calculi and is reminiscent of the
modelisation by means of strictness/lifting proposed by
Abramsky (i remember a talk, not a paper, sorry).
[The paper he refers to is S. Abramsky, The lazy lambda
calculus, in D. Turner, editor, Research topics in functional
programming, Addison-Wesley, 1992.]
The second translation takes formulae and proofs (equivalently,
types and terms) of intuitionistic logic into those of linear logic.
However, the properties under proof reduction seem less desirable. The
beta rule is not preserved by the translation. Furthermore, if we
take the usual (degenerate) semantics of linear logic where !
corresponds to lifting, then the semantics induced by the translation
is strict. It is rather surprising that a translation corresponding
to Abramsky's lazy lambda calculus should induce a strict semantics!
Is this second translation described in more detail anywhere?
Is the surprising property that it induces a strict semantics well
known? Or have I perhaps inferred the wrong translation
at the `term' level -- is there another translation with better
properties?
Comments and clarification welcome! Yours, -- P
-----------------------------------------------------------------------
Professor Philip Wadler wadler@dcs.glasgow.ac.uk
Department of Computing Science tel: +44 41 330 4966
University of Glasgow fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND