5 Jul 20:51 1994

### 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(Continue reading)