% File: locality4.tex
% Status: 28-DEC-1990 by Florian
%
\section{Soundness of the Type System}
\label{sec:sound} 

In order for a static type system to be useful, it must be {\em
sound\/} with respect to the run-time computation of the language.
Intuitively, the soundness states that the static type information of
an expression represents the actual properties of the value computed
at run-time from the expression. In our system, this implies that, as
in a conventional type system, a well-typed program will not produce
a run time type error but it also guarantees that a well-typed  program
will not produce a reference environment that violates the predefined
reachability constraint.  In this section we will explain the method
used to establish the soundness of our system and sketch the proof.

One approach to show the soundness of a type system is to model run-time
computation by a reduction relation and to show that typing judgements
are preserved by the reduction relation. We first define the set of {\em
canonical values\/} that represent run-time values of our language. For
each repository name $R$, we assume that there is a countably infinite
set of {\em reference atoms}. We further assume that a reference atom in
a given repository is identified by an integer.  The use of integers is
not essential. Any countable set of atomic elements with a linear
ordering can be used.  We write $r^\tau_R(i)$ for the reference atom in
the repository $R$ identified by the integer $i$. The set of {\em
canonical values\/} (ranged over by $v$) of the language is given by the
following syntax:  \begin{program}
$v$ \=$::=$ ($c$:$\tau$)\vbar fun($E$,$x$,$M$)
\vbar\record{$l$=$v$,$\ldots$,$l$=$v$}
\vbar\bdt{$v$,$\ldots$,$v$}\\
\>\vbar$r^\tau_R(i)$\vbar except\vbar wrong
\end{program}%
where {\tt except} is the value to denote a run-time exception (which
is needed for partially defined functions like \kwd{head} and
\kwd{tail}), {\tt wrong} represents a run-time type error and {\tt
fun($E$,$x$,$e$)} denotes function closures where  $E$ is a {\em
variable environment\/} which maps a finite set of variables to
canonical values.

In order to represent mutable references, we define a repository
environment ($R$-environment) as a record $\record{I=i,S=f}$ where $i$ is an
integer and $f$ is a function which maps the set of integers
$\{1,\ldots,i-1\}$ to canonical values.  This is to model the {\em
contents\/} of the repository $R$. The integer $i$ is used to maintain the
``next available reference index''. An ${\cal R}$-environment $\repenv$ is a
set of repository environments indexed by ${\cal R}$, i.e.\ it is a
function on ${\cal R}$ such that $\repenv(R)$ is an $R$-environment. A run
time value is then modeled by a pair $(\repenv,v)$ of an ${\cal
R}$-environment (modeling the state of the partitioned object store) and a
canonical value (maintaining the progress of program execution).  Following
\cite{Toft88}, we present the operational semantics as a  reduction
system for such pairs under a value environment $E$. We write
$\reduction{E}{\repenv}{M}{\repenv'}{v}$ if $(\repenv,M)$ is reduced to
$(\repenv',v)$ under $E$. Some of the reduction rules are shown in
Fig.~\ref{fig:reduction}. The rules for other expressions are similar to
those found in \cite{Toft88}.
 
\renewcommand{\rulelab}{3ex}
\renewcommand{\sepr}{\hspace*{0.3cm}}
\renewcommand{\sep}{\hspace{0.3cm}}
\begin{figure}
{\small\tt
\axiom{}
{$\reduction{E}{\repenv}{x}{\repenv}{if\ x\in dom(E)\ then\ E(x)\
else\ \code{wrong}}$}\rvsep\\
\axiom{}
{$\reduction{E}{\repenv}{\lambda\code{x:}\tau.M}{\repenv}
{\code{fun($E$,$x$,$M$)}}$}\rvsep\\
\ruleone{}
{{$\reduction{E}{\repenv_1}{M_1}{\repenv_2}{\code{fun($E'$,$x:\tau$,$M_2$)}}$}\\
{$\reduction{E}{\repenv_2}{M_3}{\repenv_3}{v_1}$}\\
{$\reduction{E'\{x\mapsto v_1\}}{\repenv_3}{M_2}{\repenv_4}{v_2}$}}
{$\reduction{E}{\repenv_1}{\code{$M_1$($M_3$)}}{\repenv_4}{v_2}$}\rvsep\\
\ruleone{}
{$\reduction{E}{\repenv_1}{M}{\repenv_2}{v}$}
{$\reduction{E}{\repenv_1}{\code{\kwd{new}($R$,$M:\tau$)}}
	{$\\$\repenv_2\{R\mapsto(\repenv_2(R).I +
            1, (\repenv_2(R).S)\{\repenv_2(R).I\mapsto
   		v\})\}}
        {r^{\tau}_R(\repenv_2(R).I)}$}\rvsep\\
\ruletwo{}
{$\reduction{E}{\repenv_1}{M_1}{\repenv_2}{r^\tau_R(i)}$}
{$\reduction{E}{\repenv_2}{M_2}{\repenv_3}{v}$}
{$\reduction{E}{\repenv_1}{\code{\asgn{$M_1$}{$M_2$}}}
  {\repenv_3\{R\mapsto (\repenv_3(R).I,
   \repenv_3(R).S\{i\mapsto v\})\}}
 {\code{Void}}$}\rvsep\\
}
\caption{Some of the reduction rules}
\label{fig:reduction}
\end{figure}

A canonical value $v$ is a value independent of any external environment.
We can define the locality $\clocality(v)$ of a canonical value $v$ as:
\begin{eqnarray*}
\clocality(\code{($c$:$\tau$)}) &=& \emptyset\\
\clocality(\code{fun($E$,$x:\tau$,$M$)}) &=& \bigcup\{\clocality(E(x))|x\in dom(E)\}\\
\clocality(\code{\record{$l_1$=$v_1$,$\ldots$,$l_n$=$v_n$}}) &=&
   \bigcup\{\clocality(v_i)|1\le i \le n\}\\
\clocality(\code{\bdt{$v_1$,$\ldots$,$v_n$}}) &=&
   \bigcup\{\clocality(v_i)|1\le i \le n\}\\
\clocality(r_R^\tau(i))&=&\{R\}\\
\clocality(\code{except})&=&\emptyset
\end{eqnarray*}
In order to reason about the properties of the run-time evaluation we use
the following notation: We write  $\ctyping{v}{\tau}$ for a typing of a
canonical value $v$.  A variable environment $E$ {\em respects\/} a type
assignment $\ass$, denoted by $E\models\ass$, if $dom(E) = dom(\ass)$ and
for all $x\in dom(\ass)$, $\ctyping{E(x)}{\ass(x)}$. A reference
environment $\repenv$ is a {\em model\/} of $\mu$, written
$\repenv\models\mu$, if for all $R\in{\cal R}$ and for for all
$r^\tau_R(i)\in dom(\repenv(R).S)$, $\ctyping{\repenv(R).S(i)}{\tau}$.
The rules for typings of canonical values are then given as:\rvsep\\
{\tt
\axiom{}
	{$\ctyping{\code{($c$:$\tau$)}}{\tau}$}\rvsep\\
\axiom{}
	{$\ctyping{r_R^\tau(i)}{\code{ref($\pi$,$\tau$)}}$}
	{{\rm for all integer} $i$ {\rm and }$R\in\pi$}\rvsep\\
\axiomc{}
        {$\ctyping{\code{except}}{\tau}$}{{\rm for all $\tau$}}\rvsep\\
\axiom{}
        {$\ctyping{\code{fun($E$,$x$,$M$)}}{\tau_1\funtype{\pi}\tau_2}$}
        {\rm \ \ \ if  $\clocality(E)\subseteq \pi$ and}}\\ 
\axiom{}
        {\ \ \ $\forall v\forall \repenv.$ if $\ctyping{v}{\tau_1}$,
         $\repenv\models\mu$ and
         $\reduction{E\{x\mapsto v\}}{\repenv}{M}{\repenv'}{v'}$}\\
\axiom{}
        {\ \ \ \ \ \ \ \ \ \ then $\repenv'\models\mu$ and
         $\ctyping{v'}{\tau_2}$.}\rvsep\\
\ruleone{}
       	{$\ctyping{v_i}{\tau_i}$}
       	{$\ctyping{\code{\record{$l_1$=$v_1$,$\ldots$,$l_n$=$v_n$}}}
      		{\code{\record{$l_1$:$\tau_1$,$\ldots$,$l_n$:$\tau_n$}}}$}\rvsep\\
\ruleone{}
       	{$\ctyping{v_i}{\tau}$}
{$\ctyping{\code{\bdt{$v_1$,$\ldots$,$v_n$}}}{\code{\bdt{$\tau$}}}$}\rvsep\\
\ruleonec{}
	{$\ctyping{v}{\tau_1}$}
 {$\ctyping{v}{\tau_2}$}
 {{\rm if } $\tau_1\torder\tau_2$}\rvsep\\

It should be noted that the definitions for $\clocality(v)$ and
$\ctyping{v}{\tau}$ are not syntactic but reflect the actual
computational properties of the value. Canonical values have in general
multiple typing but {\tt wrong} has none. 

We can then show the following theorem. 
\begin{theorem}[Soundness of the Type System]
Let $\eass,\emptyset_E,\emptyset_{{\cal E}}$ respectively be the empty
type assignment, 
the empty variable environment and the empty ${\cal R}$-environment.
For any closed expression $M$, if $\typing{\eass}{M}{\tau}$ and
$\reduction{\emptyset_E}{\emptyset_{{\cal E}}}{M}{\repenv}{v}$ then
$\repenv\models\mu$, 
$\ctyping{v}{\tau}$.
\end{theorem}
This is proved by showing the following stronger property
by induction on the structure of expressions.
\begin{quote}
For any variable environment $E$, any ${\cal R}$-environment
$\repenv$ and any typing $\typing{\ass}{M}{\tau}$, if
$E\models\ass$, $\repenv\models\mu$ and
$\reduction{E}{\repenv}{M}{\repenv'}{v}$ then
$\repenv'\models\mu$ and $\ctyping{v}{\tau}$.
\end{quote}
For details of this proof, the reader is referred to \cite{OMS90}. Since
{\tt wrong} has no typing, this theorem implies the following 
\begin{cor}
For any closed expression $M$, if $\typing{\eass}{M}{\tau}$ and
$\reduction{\emptyset_E}{\emptyset_{{\cal E}}}{M}{\repenv}{v}$ then
$v \not= \code{wrong}$.
\end{cor}
Since it can be shown that if $\ctyping{v}{\tau}$ then $\clocality(v)
\subseteq \locality(\tau)$, the above theorem also implies the following
desired property on the locality of expressions.
\begin{cor}
For any closed expression $M$, if $\typing{\eass}{M}{\tau}$ and
$\reduction{\emptyset_E}{\emptyset_{{\cal E}}}{M}{\repenv}{v}$ then
$\clocality(v)\subseteq \locality(\tau)$ and
$\repenv$ respects the repository constraint $\mu$.
\end{cor}
The difference between $\locality$ and $\clocality$ should be noted.
$\locality(\tau)$ is a static property available at compile-time.  On
the other hand, we have defined $\clocality(v)$ based on the actual
reference structure contained in $v$ so that it represents the {\em
actual\/} locality of the value $v$.  As such, this information is not
available at compile-time. The above corollary guarantees that the
locality of an expression represented by its type is always a correct
estimate of the actual locality of the result of the run-time
computation and that a type correct program will never produce a
reference environment that violates the predefined reachability
constraint. 

