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