paper available by ftp : definite version

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

A definite version of the paper
has superseded the provisional version sent two weeks ago. Besides  
small bugs, typos etc. this new version gives a more accurate syntax.  
An appendix discusses Gustave's function. The alternative additives  
have been expelled from the final version for want of a satisfactory  


The following paper
is available through anonymous ftp
iml.univ-mrs.fr \pub\girard\banach.ps.Z or banach.dvi.Z

The paper is basically an expension of the notes given in my lecture  
of April 1st (!) at Keio University ; it is surely not the definite  
version, but ulterior modifications or additions should be limited.  
The paper is dedicated to the memory of Robin Gandy.

We present a denotational semantics based on Banach spaces~; it is  
inspired from the familiar coherent semantics of linear logic, the  
role of coherence being played by the norm~: coherence is rendered by  
a supremum, whereas incoherence is rendered by a sum, and cliques are  
rendered by vectors of norm at most $1$. The basic constructs of  
linear (and therefore intuitionistic) logic are implemented in this  
framework~: positive connectives yield $\ell^1$-like norms and  
negative connectives yield $\ell^\infty$-like norms. The problem of  
non-reflexivity of Banach spaces is handled by \Guill{specifying the  
dual in advance}, whereas the exponential connectives (i.e.  
intuitionistic implication) are handled by means of analytical  
functions on the open unit ball. The fact that this ball is open (and  
not closed) explains the absence of simple solution to the question  
of a topological cartesian closed category~: our analytical maps send  
an open ball into a closed one and therefore do not compose. However  
a slight modification of the logical system allowing to multiply a  
function by a scalar of modulus $<1$ is enough to cope with this  
problem. The logical status of the new system should be clarified.

Jean-Yves GIRARD
Directeur de Recherche

CNRS, Institut de Mathematiques de Luminy
163 Avenue de Luminy, case 930
13288 Marseille cedex 9

(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)