[Prev][Next][Index][Thread]

Coherent Banach Spaces : A Continuous Denotational Semantics


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


The following paper
COHERENT BANACH SPACES : A CONTINUOUS DENOTATIONAL SEMANTICS
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.

\begin{abstract}
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 what there was never any 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 $<1$ is enough to cope with this  
problem. The logical status of the new system (which also allows new  
exotic connectives inspired from the norms $\ell^p$) should be  
clarified.
\end{abstract}

---

Jean-Yves GIRARD
Directeur de Recherche

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

<girard@iml.univ-mrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)