[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