%From: Oliver Michael Duschka <duschka@CS.Stanford.EDU>
%Date: Wed, 31 May 1995 15:05:07 -0700 (PDT)

\documentstyle[11pt,fleqn]{article}

\topmargin-15mm
\oddsidemargin5mm
\evensidemargin5mm
\textwidth160mm
\textheight220mm

%\newfont{\stmary}{stmary10 scaled 1100}
%\newcommand{\llpar}{\mbox{\stmary \symbol{79}}}
\newcommand{\llpar}{{\mbox{\raisebox{.4ex}{$\wp$}}}} % Par (gross)

\newcounter{mycounter}[section]

\newenvironment{definition}[1]%
{\refstepcounter{mycounter}
 \vspace{3mm}
 \parindent0mm
 {\bf \thesection.\arabic{mycounter}. Definition ({\sl #1}).}}%
{}

\newenvironment{example}%
{\refstepcounter{mycounter}
 \vspace{3mm}
 {\bf \thesection.\arabic{mycounter}. Example.}}%
{}

\newcommand{\coh}{\raisebox{-3pt}{$\stackrel{\textstyle\frown}{\smile}$}}
\newcommand{\icoh}{\raisebox{-3pt}{$\stackrel{\textstyle\smile}{\frown}$}}
\newcommand{\scoh}{\raisebox{-3pt}{$\stackrel{\textstyle\frown}{ \ }$}}
\newcommand{\sicoh}{\raisebox{-3pt}{$\stackrel{\textstyle\smile}{ \ }$}}
\newcommand{\atoms}[1]{\mbox{$\left|  #1 \right|$}}
\newcommand{\lneg}[1]{\mbox{$#1^\bot$}}
\newcommand{\coherence}[3]{\mbox{$#1 \coh #2$ [mod $#3$]}}
\newcommand{\icoherence}[3]{\mbox{$#1 \icoh #2$ [mod $#3$]}}
\newcommand{\scoherence}[3]{\mbox{$#1 \scoh #2$ [mod $#3$]}}
\newcommand{\sicoherence}[3]{\mbox{$#1 \sicoh #2$ [mod $#3$]}}

\begin{document}

\pagestyle{plain}
\begin{center}
{\bf \huge Coherent Semantics} \\
CS358, Spring 1995
\end{center}

\section{Coherent Spaces}

\begin{definition}{coherent space}

A {\sl coherent space} is a reflexive undirected graph, i.e. it consists
of a set \atoms{X} together with a {\sl coherence relation} between atoms,
noted \coherence{x}{y}{X}.

A {\sl clique} $a$ in $X$ is a subset $a$ of $X$ made of pairwise coherent
atoms.

Two atoms $x$ and $y$ are {\sl strictly coherent} in $X$ (\scoherence{x}{y}{X})
if they are coherent and distinct. They are {\sl incoherent} 
(\icoherence{x}{y}{X}) if they are not strictly coherent. They are
{\sl strictly incoherent} (\sicoherence{x}{y}{X}) if they are not
coherent.
\end{definition}

\begin{definition}{linear negation}

The {\sl linear negation} \lneg{X} of a coherent space $X$ is defined by
\begin{itemize}
\item $\atoms{\lneg{X}} = \atoms{X}$,
\item \coherence{x}{y}{\lneg{X}} \ iff \ \icoherence{x}{y}{X}.
\end{itemize}
\end{definition}

\begin{definition}{multiplicatives}

Given two coherent spaces $X$ and $Y$, the multiplicative connectives $\otimes$
and \llpar \ define a new coherent space with
\begin{itemize}
\item $\atoms{X \otimes Y} = \atoms{X \llpar Y} = \atoms{X} \times \atoms{Y}$, 
\item \coherence{(x,y)}{(x',y')}{X \otimes Y} \ iff \
      \coherence{x}{x'}{X} \ and \ \coherence{y}{y'}{Y},
\item \scoherence{(x,y)}{(x',y')}{X \llpar Y} \ iff \
      \scoherence{x}{x'}{X} \ or \ \scoherence{y}{y'}{Y}.
\end{itemize}
\end{definition}

\begin{definition}{additives}

Given two coherent spaces $X$ and $Y$ the additive connectives $\&$ and  
$\oplus$ define a new coherent space with
\begin{itemize}
\item $\atoms{X \& Y} = \atoms{X \oplus Y} = \atoms{X} + \atoms{Y}$,
\item \coherence{(x,0)}{(x',0)}{X \& Y} or $[$mod $X \oplus Y]$ \
      iff \ \coherence{x}{x'}{X},
\item \coherence{(y,1)}{(y',1)}{X \& Y} or $[$mod $X \oplus Y]$ \
      iff \ \coherence{y}{y'}{Y},
\item \scoherence{(x,0)}{(y,1)}{X \& Y} \ for all $x \in \atoms{X}$
      and $y \in \atoms{Y}$,
\item \sicoherence{(x,0)}{(y,1)}{X \oplus Y} \ for all $x \in \atoms{X}$
      and $y \in \atoms{Y}$.
\end{itemize}
\end{definition}

\begin{definition}{constants}

Up to isomorphism there is a unique coherent space whose web consists
of one atom, and a unique coherent space whose web doesn't contain any
atom. Both spaces are self dual. Denote the first one by {\bf 1} and
$\bot$, and the second by $\top$ and {\bf 0}.
\end{definition} 

\newpage

\begin{definition}{exponentials}

If $X$ is a coherent space, then $!X$ and $?X$ are defined as follows
\begin{itemize}
\item $\atoms{!X} = \{ \{x_1,\ldots,x_n\} \ | \ \coherence{x_i}{x_j}{X}$
                       \ for all $i$ and $j$ \},
\item $\atoms{?X} = \{ \{x_1,\ldots,x_n\} \ | \ \icoherence{x_i}{x_j}{X}$
                       \ for all $i$ and $j$ \},  
\item \coherence{\{x_1,\ldots,x_n\}}{\{y_1,\ldots,y_m\}}{!X} \
      iff \ \coherence{x_i}{y_j}{X} for all $i$ and $j$,
\item \scoherence{\{x_1,\ldots,x_n\}}{\{y_1,\ldots,y_m\}}{?X} \
      iff \ \scoherence{x_i}{y_j}{X} for some $i$ and $j$.
\end{itemize} 
\end{definition}

\section{Isomorphisms}

The following isomorphisms follow immediately from the definitions:

\begin{tabbing}
\hspace{10mm}\=\hspace{70mm}\=\kill
De Morgan equalities \\
\>$(X \otimes Y)^\bot \ = \ X^\bot \llpar Y^\bot$
\> $(X \llpar Y)^\bot \  = \ X^\bot \otimes Y^\bot$ \\
\>$(X \& Y)^\bot \ = \ X^\bot \oplus Y^\bot$ 
\> $(X \oplus Y)^\bot \ = \ X^\bot \& Y^\bot$ \\
\>$(!X)^\bot \ = \ ?(X^\bot)$ 
\> $(?X)^\bot  \ = \  !(X^\bot)$ \\

\vspace{2mm} \\

commutativity isomorphisms \\
\>$X \otimes Y \ \simeq \ Y \otimes X$
\> $X \llpar Y \ \simeq \ Y \llpar X$ \\
\>$X \& Y \ \simeq \ Y \& X$
\> $X \oplus Y \ \simeq \ Y \oplus X$ \\

\vspace{2mm} \\

associativity isomorphisms \\
\>$X \otimes (Y \otimes Z) \ \simeq \ (X \otimes Y) \otimes Z$
\> $X \llpar (Y \llpar Z) \ \simeq \ (X \llpar Y) \llpar Z$ \\
\>$X \& (Y \& Z) \ \simeq \ (X \& Y) \& Z$ 
\> $X \oplus (Y \oplus Z) \ \simeq \ (X \oplus Y) \oplus Z$ \\

\vspace{2mm} \\

distributivity isomorphisms \\
\>$X \otimes (Y \oplus Z) \ \simeq \ (X \otimes Y) \oplus (X \otimes Z)$
\> $X \llpar (Y \& Z) \ \simeq \ (X \llpar Y) \& (X \llpar Z)$ \\

\vspace{2mm} \\

neutrality isomorphisms \\
\>$X \otimes$ {\bf 1} $ \ \simeq \ X$ 
\> $X \llpar \bot \ \simeq \ X$ \\
\>$X \oplus$ {\bf 0} $ \ \simeq \ X$ 
\> $X \& \top \ \simeq \ X$ \\

\vspace{2mm} \\

absorption isomorphisms \\
\>$X \otimes$ {\bf 0} $ \ \simeq \ $ {\bf 0}
\> $X \llpar \top \ \simeq \top$ \\

\vspace{2mm} \\

exponential isomorphisms \\
\>$!(X \& Y) \ \simeq \ (!X) \otimes (!Y)$
\> $?(X \oplus Y) \ \simeq \ (?X) \llpar (?Y)$ \\
\>$!\top \ \simeq \ $ {\bf 1}
\> $?${\bf 0} $ \ \simeq \ \bot$

\end{tabbing}

\newpage

\section{Interpretation of Proofs}

\begin{definition}{interpretation of proofs}
A proof $\pi$ of a sequent $\vdash A_1, \ldots, A_n$ is interpreted 
by a clique $\pi^*$ of the coherent space $A_1 \llpar \ldots \llpar A_n$.
$\pi^*$ is defined by induction on the proof $\pi$ of 
$\vdash A_1, \ldots, A_n$:
\begin{enumerate}
\item
If $\pi$ is the axiom $\vdash A, A^\bot$, then 
$\pi^* = \{xx \ | \ x \in \atoms{A} \}$.
\item 
If $\pi$ is obtained from $\pi'$ and $\pi''$ by the cut rule
\[\frac{\vdash \Gamma, A \quad \vdash A^\bot, \Delta }{\vdash \Gamma, \Delta}\]
then $\pi^* = \{\vec{x}\vec{y} \ | \ 
\exists z \in \atoms{A} . \ ( \vec{x}z \in {\pi'}^* \
 \mbox{and} \ z\vec{y} \in {\pi''}^*) \}$.
\item 
If $\pi$ is obtained from $\pi'$ by the exchange rule replacing
$\Gamma$ by a permutation $\sigma(\Gamma)$, then 
$\pi^* = \{ \sigma(\vec{x}) \ | \ \vec{x} \in {\pi'}^* \} $.
\item
If $\pi$ is the axiom $\vdash $ {\bf 1}, then $\pi^*$ consists of
the single atom of the coherent space {\bf 1}.
\item
If $\pi$ is obtained from $\pi'$ by the rule $(\bot)$
\[ \frac{\vdash \Gamma}{\vdash \bot, \Gamma} \]
then $\pi^* = \{ 0\vec{x} \ | \ \vec{x} \in {\pi'}^* \}$ where $0$ is
the single atom of the coherent space {\bf 1}.
\item
If $\pi$ is obtained from $\pi'$ and $\pi''$ by $(\otimes)$
\[\frac{\vdash A,\Gamma \quad \vdash B,\Delta}%
{\vdash A \otimes B, \Gamma,\Delta\ } \] 
then $\pi^* = \{ (z,z')\vec{x}\vec{y} \ | \ z\vec{x} \in {\pi'}^* 
\ \mbox{and} \ z'\vec{y} \in {\pi''}^* \}$. 
\item 
If $\pi$ is obtained from $\pi'$ by the rule $(\llpar)$
\[ \frac{\vdash A,B,\Gamma}{\vdash A \llpar B, \Gamma} \]
then $\pi^* = \{ (x,y)\vec{z} \ | \ xy\vec{z} \in {\pi' }^* \}$.
\item 
If $\pi$ is the axiom $\vdash \top, \Gamma$, then $\pi^* = \{\}$.
\item
If $\pi$ is obtained from $\pi'$ and $\pi''$ by $(\&)$
\[\frac{\vdash A,\Gamma \quad \vdash B,\Gamma}{\vdash A \& B, \Gamma} \] 
then $\pi^* = \{ (x,0)\vec{y} \ | \ x\vec{y} \in {\pi'}^* \} \cup
 \{ (x,1)\vec{y} \ | \ x\vec{y} \in {\pi''}^* \} $.
\item 
If $\pi$ is obtained from $\pi'$ by the rule $(\otimes L)$
\[ \frac{\vdash A,\Gamma}{\vdash A \oplus B, \Gamma} \]
then $\pi^* = \{ (x,0)\vec{y} \ | \ x\vec{y} \in {\pi' }^* \}$.
\item 
If $\pi$ is obtained from $\pi'$ by the rule $(\otimes R)$
\[ \frac{\vdash B,\Gamma}{\vdash A \oplus B, \Gamma} \]
then $\pi^* = \{ (x,1)\vec{y} \ | \ x\vec{y} \in {\pi' }^* \}$.
\item
If $\pi$ is obtained from $\pi'$ by the weakening rule 
\[ \frac{\vdash \Gamma}{\vdash ?A, \Gamma} \]
then $\pi^* = \{ \{\}\vec{x} \ | \ \vec{x} \in {\pi' }^* \}$.
\item
If $\pi$ is obtained from $\pi'$ by the dereliction rule 
\[ \frac{\vdash A, \Gamma}{\vdash ?A, \Gamma} \]
then $\pi^* = \{ \{x\}\vec{y} \ | \ x\vec{y} \in {\pi' }^* \}$.
\item
If $\pi$ is obtained from $\pi'$ by the contraction rule 
\[ \frac{\vdash ?A, ?A , \Gamma}{\vdash ?A, \Gamma} \]
then $\pi^* = \{ x \cup y,\vec{z} \ | \ xy\vec{z} \in {\pi' }^* \}$.
\item
If $\pi$ is obtained from $\pi'$ by the storage rule 
\[ \frac{\vdash A, ?\Gamma}{\vdash !A, ?\Gamma} \]
then $\pi^* = \{ \{x_1,\ldots,x_n\}\vec{y}
 \ | \
\vec{y} = {y_{11}}\cup\ldots\cup{y_{n1}}, \ldots,
{y_{1m}}\cup\ldots\cup{y_{nm}}, \
x_i {y_{i1}}\ldots{y_{im}} \in {\pi'}^*
\ \mbox{for} \ i = 1,\ldots,n, \ 
\vec{y} \in ?\Gamma, \
\{x_1,\ldots,x_n\} \in \ !A
\}$.
\end{enumerate}
\end{definition}

\begin{thebibliography}{99}
\bibitem[1]{Gir87} J.-Y. Girard. Linear Logic. 
{\sl Theoretical Computer Science},
50:1-102, 1987.
\bibitem[2]{Gir93} J.-Y. Girard. Linear Logic: Its Syntax and Semantics.
In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, {\sl Advances in
Linear Logic}, Cambridge University Press, 1995.
Proceedings of the Workshop in Linear Logic, Ithaca, New York, June 1993.
\end{thebibliography}

\end{document}

