% -*- Mode: LaTeX -*-

\section{Proof Sketch for the Soundness Theorem} 

First, we state some useful properties of the evaluation rules
(\fig{dynamic}), static rules (\fig{static}) and the semantic model
(\defn{consistent}). The details of all these proofs appear in
\cite{Gupta94}. 

\subsection{Properties of the Evaluation Rules}
The following propositions are shown by induction on the length
of the evaluation derivation for the expression $a$, doing a case
analysis on the last evaluation rule used in the derivation.
\begin{proposition}[Fresh Locations]\label{prop:fresh-loc}
Let $a$ be an expression, $v$ be a value, $e$ be an environment, and
$s_{0},s_{1}$ be initial and final stores respectively such that
$e\vdash{}a/s_{0}\Rightarrow{}v/s_{1}$. Then, 
\[l'\in\fn{Reachable}{v,s_{1}} \implies  l'\not\in\fn{Dom}{s_{0}}
\bigvee l'\in\fn{Reachable}{e,s_{0}} \]
and for all locations $l\in\fn{Dom}{s_{0}}$, 
\[l'\in[\fn{Reachable}{l,s_{1}}\setminus\fn{Reachable}{l,s_{0}}]
\implies l'\not\in\fn{Dom}{s_{0}} \bigvee l'\in\fn{Reachable}{e,s_{0}}\]
That is, locations reachable from a value computed in an
evaluation are reachable from the environment
or they are fresh locations.
\end{proposition}
\begin{proposition}[Changed Locations]\label{prop:env-loc}
Let $a$ be an expression, $v$ be a value, $e$ be an environment, and
$s_{0},s_{1}$ be initial and final stores respectively such that
$e\vdash{}a/s_{0}\Rightarrow{}v/s_{1}$. Then for any location
$l\in\fn{Dom}{s_{0}}$, 
\[\fn{value}{s_{0},l}\neq\fn{value}{s_{1},l} \implies
l\in\fn{Reachable}{e,s_{0}}\] 
That is, only the locations reachable from the environment may change
their value during an evaluation.
\end{proposition}

\subsection{Properties of the Typing Rules} 
The following proposition states that typing is stable under type
substitution. The proof of this proposition is done using
structural induction over $a$, doing a case analysis on the last
typing rule used in the typing derivation of $a$. 

\begin{proposition}[Stability under Type Substitution]
\label{prop:stable}
Let $a$ be an expression, $\tau$ be a type, $E$ be a type
environment, and $\varphi$ be a substitution. If
$E\vdash{}a:\tau$, then $\varphi(E)\vdash{}a:\varphi(\tau)$.
\end{proposition}

\subsection{Properties of the Semantic Model}
The following proposition shows that a semantic relation such as
$S\models{}v:\tau$ that holds true at some point during evaluation,
remains true under an extended store typing. 
\begin{proposition}[Store Typing Extension] \label{prop:st-extn}
If $S'$ extends $S$, then $S\models{}v:\tau$ implies
$S'\models{}v:\tau$. Similarly, $S\models{}e:E$ implies
$S'\models{}e:E$.
\end{proposition}

The following proposition establishes the fact that it is semantically
safe to generalize the non-dangerous variables of a type. It is proved
using structural induction over $v$ using the definition of $\models$
(\defn{consistent}). 

\begin{proposition}[Semantic Generalization]
\label{prop:sem-gen} 
Let $v$ be a value, $\tau$ be a type and $S$ be a store typing such
that $S\models{}v:\tau$. Let $\alpha_{1},\ldots,\alpha_{m}$ be type
variables such that for all i,  $\alpha_{i}\not\in\dvar{\tau}$. Then,
for all substitutions $\varphi$ with
$\fn{Dom}{\varphi}\subseteq\{\alpha_{1}\ldots\alpha_{m}\}$, we have
$S\models{}v:\varphi(\tau)$. As a consequence,
$S\models{}v:\forall\alpha_{1}\ldots\alpha_{m}.\tau$.
\end{proposition}

\subsection{The Soundness Theorem}
Now, we sketch the proof of the \cbx{close} case of the soundness
theorem. 
\begin{proof} 
The proof is by induction on the size of evaluation derivation. The
argument is by case analysis on $a$. Refer to the static
(\fig{static}) and dynamic (\fig{dynamic}) \cbx{close} rules. Using
the induction hypothesis on $a$, we obtain
$e\vdash{}a/s\Rightarrow{}l/s_{1}$ with the store typing $S_{1}$ such
that $S_{1}\models{}l:\tau\;\fn{ref}{r}$, $\models{}s_{1}:S_{1}$ and
$S_{1}\;\bx{extends}\;S$. From the first two clauses and the
definition of $\models$ for mutable locations, we obtain,
$l\in\fn{Dom}{S_{1}}$, $S_{1}(l)=\tau\;\fn{ref}{r}$,
$s_{1}(l)=v,\/\rw$ and $S_{1}\models{}v:\tau $.  Thus, the \cbx{close}
evaluation rule applies. Define
$s'=s_{1}\mid_{L}+\{l\mapsto{}v,\/\ro\}$ and
$S'=S_{1}\mid_{L}+\{l\mapsto\tau\;\fn{ref}{\epsilon}\}$.  Now, we have
to show the following:
\begin{equation}\label{eqn:eval6}
S'\models{}l:\tau\;\fn{ref}{\epsilon} \hmm \bx{and} \hmm
\models{}s':S' \hmm \bx{and} \hmm S'\;\bx{extends}\;S 
\end{equation}
The first clause follows directly from the definition of $\models$
for non-mutable locations since we have chosen $l\in\fn{Dom}{S'}$ and
$S'(l)=\tau\;\fn{ref}{\epsilon}$. 

Next, we show that $l \not\in \fn{Reachable}{e,s}$. If not,  
$r\in\rvar{S_1(l)}=\rvar{S(l)}$ (as $S_1$ extends $S$)
$\subseteq\rvar{E}$ (by \prop{reg-loc}) 
$\subseteq\fvar{E}$, which contradicts  the condition $r \not\in \fvar{E}$ 
of the typing rule. Similarly, we can show that
$l \not\in \fn{Reachable}{e,s_1}$.

Now, we show that $S'$ extends $S$. Note that $S_{1}$ extends $S$
if and only if $l\not\in\fn{Dom}{S}$, since that is the only location at which
$S_{1}$ and $S'$ differ. As we know that $l \not\in \fn{Reachable}{e,s}$,
\prop{fresh-loc} on the evaluation $e\vdash{}a/s\Rightarrow{}l/s_{1}$ 
implies that $l \not\in \fn{Dom}{s} = \fn{Dom}{S}$.

As the final step in proving \eqn{eval6}, we have to show
$\models{}s':S'$. By construction of $S'$, the tags of $s'$ are
consistent with $S'$. To show consistency for values in the store,
consider a location $l'$ such that $\fn{value}{s',l'}=v'$ and $S'(l')=
\tau'$. If $v'$ does not contain $l$, we can show that
$S'\models{}v':\tau'$ by a simple structural induction on $v'$ (using
the fact that $S_1\models{}v':\tau'$ and that $l$ is the only location
in which $S_1$ and $S'$ differ). To complete the proof, we show that
$l$ is not {\em reachable} from any $v'$ (in $s_1$ and hence in $s'$)
which implies the above property.

Assume that $l\in\fn{Reachable}{v',s_{1}}$. Looking at the components of
$\fn{Dom}{s'}$, there are three possibilities for $l'$:
\begin{tightenum}
\item $l'=l$ --- Then $v'=v$. Given
$l\in\fn{Reachable}{v,s_{1}}$, we apply \prop{reg-loc} to
$l$ and $v$ to conclude that
$r\in\rvar{S_{1}(l)}\subseteq\rvar{\tau}\subseteq\fvar{\tau}$ which
contradicts the condition $r\not\in\fvar{\tau}$ in the typing rule.
\item $l'\in\fn{Reachable}{e,s_{1}}$ --- This implies $l \in
\fn{Reachable}{e,s_1}$, a contradiction.
\item $l'\in\fn{Reachable}{\fn{Dom}{s},s_{1}}$ --- We know that $l$
was not reachable from any value present in the domain $s$ initially,
\ie, $l\not\in\fn{Reachable}{\fn{Dom}{s},s}$ because we have already
shown that $l\not\in\fn{Dom}{s}$.
Thus, the only way $l$ could become reachable from $\fn{Dom}{s}$ after
the evaluation $e\vdash{}a/s\Rightarrow{}v/s_{1}$ is if some location
in $\fn{Dom}{s}$ was assigned a new value from which $l$ was
reachable.  Without loss of generality, let us assume that location is
$l'$ and the newly assigned value is $v'$, \ie,
\begin{equation}
\exists\;l'\in\fn{Dom}{s}: \hm
\fn{value}{s,l'}\neq\fn{value}{s_{1},l'}=v' \hm \bx{and}\hm
l\in\fn{Reachable}{v',s_{1}}
\end{equation}
By \prop{env-loc}, $l' \in \fn{Reachable}{e,s}$.
Applying \prop{reg-loc} to $l$ and $v'$, we obtain $r \in \rvar{S_1(l')}$. 
Thus, $r \in \rvar{S(l')}$. Applying \prop{reg-loc} to $l'$ and $e$,
we obtain $r \in \rvar{E} \subseteq \fvar{E}$, a contradiction.
\end{tightenum}
\end{proof}

