# Coherent Banach Spaces : A Continuous Denotational Semantics

• To: lineaire <linear@cs.stanford.edu>
• Subject: Coherent Banach Spaces : A Continuous Denotational Semantics
• From: girard@lmd.univ-mrs.fr (Jean-Yves GIRARD)
• Date: Thu, 25 Apr 96 13:58:43 +0100
• Approved: types@dcs.gla.ac.uk


[------ 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)