[Prev][Next][Index][Thread]
ON DENOTATIONAL COMPLETENESS
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following paper is available through anonymous ftp
lmd.univ-mrs.fr,dir pub/girard :
ON DENOTATIONAL COMPLETENESS
in the compressed files
denotational.dvi.Z or denotational.ps.Z
\begin{abstract}
The founding idea of linear logic is the duality between $A$ and
$A\Ortho$, with values in $\bot$. This idea is at work in the
original denotational semantics of linear logic, coherent spaces, but
also in the phase semantics of linear logic, where the
\Guill{bilinear form} which induces the duality is nothing but the
product in a monoid $\Bbb M$, $\bot$ being an arbitrary subset $\Bbb
B$ of $\Bbb M$. The rather crude phase semantics has the advantage of
being complete, and against all predictions, this kind of semantics
had some applications. Coherent semantics is not complete for an
obvious reason, namely that the coherent space $\Bbbk$ interpreting
$\bot$ is too small (one point), hence the duality between $A$ and
$A\Ortho$ expressed by the cut-rule cannot be informative enough. But
$\Bbbk$ is indeed the simplest case of a Par-monoid, i.e. the dual of
a comonoid, and it is tempting to replace $\Bbbk$ with any
commutative Par-monoid $\Bbb P$. Now we can replace coherent spaces
with \Guill{free $\Bbb P$-modules over $\Bbb P$}, linear maps with
\Guill{$\Bbb P$-linear maps}, with the essential result that all
usual constructions remain unchanged~: technically speaking cliques
are replaced with $\Bbb P$-cliques and that's it. The essential
intuition behind $\Bbb P$ is that it accounts for arbitrary
contexts~: instead of dealing with $\Gamma,A$, one deals with $A$,
but a clique of $\Gamma,A$ can be seen as a $\Bbb P$-clique in $A$.
In particular all logical rules are now defined only on the main
formulas of rules, as operations on $\Bbb P$-cliques.
The duality between $A$ and $A\Ortho$ yields a $\Bbb P$-clique in
$\Bbbk$, i.e. a clique in $\Bbb P$~; strangely enough, one must keep
the phase layer, i.e. a monoid $\Bbb M$ (useful in the degenerated
case), and the result of the duality is a $\Bbb M\Bbb P$-clique. We
specify an arbitrary set $\Bbb B$ of such cliques as the
interpretation of $\bot$. Soundness and completeness are then easily
established for closed $\Pi^1$-formulas, i.e. second-order
propositional formulas without existential quantifiers. We must
however find the equivalent of $1 \in \cal F$ (which is the condition
for being a \Guill{provable fact})~: a $\Bbb M\Bbb P$-clique is $\em
essential$ when it does not make use of $\Bbb M$ and $\Bbb P$, i.e.
when it is induced by a clique in $A$. We can now state the
theorem~:\\
{\em Let $A$ be a closed $\Pi^1$ formula, and let $a$ be a clique in
the (usual) coherent interpretation $A^\bullet$ of $A$, which is the
interpretation of a proof of $A$~; then $a$ (as an essential clique),
belongs to the \Guill{denotational fact} $A^\circ$ interpreting $A$
for all $\Bbb M$, $\Bbb P$ and $\Bbb B$. Conversely any essential
clique with this property comes from a proof of $A$.}
\end{abstract}
--
Jean-Yves GIRARD
Directeur de Recherche
CNRS, Laboratoire de Mathematiques Discretes
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)