🚀 go-pugleaf

Date: Mon, 14 Sep 92 15:41:38 +0200
To: linear@cs.stanford.edu

		About the questions by S. Courtenage


		Concerning the translation(s) of IL into LL the
following remarks mught be of interest :
	 i)LL is not the result of abstract philosophical
speculations; concretely studying the denotational semantics of
intuitionistic logic, (coherence spaces) i found out that that the
intuitionistic arrow was not primitive, but could be decomposed into
two steps (bang and -o). Therefore LL has been built along this
translation.
	ii) as long as we are interested in provability (Lindenbaum
algebras etc) surely many other translations are possible ; as noticed
by Vaughan, there is an esthetical malaise in front of unnecessary
bangs that occur in these alternative translations.
	iii) beyond esthetics we have to remember that the viewpoint
which is the most relevant to constructivism puts proofs at the
prominent place : one is not interested in knowing whether or not A is
provable, but how it is provable... This leads to denotational
semantics, geometry of interaction etc. In this respect we become
interested in more than mere equivalence of formulas. We get
interested in synonymy -a vague notion which can be approximated by
the idea of denotational isomorphism. Therefore one must read
translations as proposing isos. My translation has the advantage of
preserving the CCC properties of IL. This is the the strongest
argument for it.
	iv) 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).
	This to say that there are very few good translations, that
the one i proposed will presumably remain the standard one, but that
for specific purposes (eg lazyness) it might be worth studying
alternatives. 


Jean-Yves Girard

new address : 122E Bd Perier 13008 MARSEILLE (private : the address of
the Lab of Discrete Maths is not yet in use)

for the moment i am keeping my usual Email addresses
girard@margaux.inria.fr
girard@logique.jussieu.fr