[Prev][Next][Index][Thread]
paper available by ftp : definite version
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
A definite version of the paper
COHERENT BANACH SPACES : A CONTINUOUS DENOTATIONAL SEMANTICS
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
syntax.
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 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.
\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@lmd.univ-mrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)