[Prev][Next][Index][Thread]
Coherent Banach Spaces : A Continuous Denotational Semantics

To: lineaire <linear@cs.stanford.edu>

Subject: Coherent Banach Spaces : A Continuous Denotational Semantics

From: girard@lmd.univmrs.fr (JeanYves 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.univmrs.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
nonreflexivity 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}

JeanYves GIRARD
Directeur de Recherche
CNRS, Institut de Mathematiques de Luminy
163 Avenue de Luminy, case 930
13288 Marseille cedex 9
<girard@iml.univmrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)