% -*- Mode: TeX -*-

\section{Correctness}
\label{proof}

In this section we outline the proof of correctness for our
incremental type inferencing system. The detailed proofs of the
lemmas and theorems appearing below are given in \cite{Gupta90}. 

We need to show a correspondence between the incremental type
inference strategy outlined in the previous section and the batch-mode
Hindley/Milner type system that infers types for complete expressions. As
given in equation~\ref{complete-program}, a program in the incremental
system is an unordered sequence of bindings with the program query at
the end. In the batch system, one would have to appropriately group
mutually recursive bindings, reorder these groups bottom up according
to their calling order, and process all of them together as a giant
nested expression, with the program query occurring innermost. These
two situations are contrasted in \fig{corresp}. The incremental
system corresponds to an interactive user session, while the
batch system processes entire programs.

\begin{figure}
\begin{tabular}{|p{\hhalfmm}|p{\hhalfmm}|}
\hline
\multicolumn{1}{|c|}{Incremental System} & \multicolumn{1}{c|}{Batch System} \\
\hline
\begin{display}
$\ibx{TE}_0=\ibx{TE}_{\sibx{lib}}+\{x_i\mapsto\forall\alpha.\alpha\}:$
                $x_1 = e_1$
\vsp
$\ibx{TE}_1:$
                $x_2 = e_2$
                  $\vdots$
$\ibx{TE}_{i-1}:$
                $x_i = e_i$
\vsp
$\ibx{TE}_i:$
                  $\vdots$
                $\tbx{it}=e_{\sibx{main}}$
$\ibx{TE}_f.$
\end{display} &
\begin{display}
$\ibx{TE}_{x_1}^t=\ibx{TE}_{\sibx{lib}}:$
         $\tbx{let} x_1 = e_1 \tbx{in}$
\vsp
$\ibx{TE}_{x_2}^t=\ibx{TE}_{x_3}^t:$
           $\tbx{let} x_2,x_3 = e_{23} \tbx{in}$
             $\vdots$
$\ibx{TE}_{x_i}^t:$
                 $\tbx{let} x_i = e_i \tbx{in}$
                   $\vdots$
$\ibx{TE}_{e_{\ssbx{main}}}^t:$
                     $e_{\sibx{main}}.$
\vsp
$\ibx{TE}_t=\ibx{TE}_{e_{\ssbx{main}}}^t+\{\tbx{it}\mapsto{}\sigma_{e_{\ssbx{main}}}\}$.
\end{display} \\
\hline
\end{tabular}
\caption{A user session in the Incremental System and the Batch System.}
\label{fig:corresp}
\end{figure}

We intend to show that the type environment created in the batch system
after typing the innermost program query ``$e_{\sibx{main}}$'' is
exactly the same as the final environment reached in the incremental
system after all the bindings have been processed and all their
assumption checks have been passed in that environment, \ie,
$\ibx{TE}_f=\ibx{TE}_t$.

\subsection{Some Results on Type Assumptions}

Before we show the correspondence between the incremental system and the
batch system, it is instructive to identify the importance of
assumptions and assumption checks. The upper bound type assumptions
collected \via the algorithm $W'$ serve as an exact type specification
of the interface between the current top-level definition and other
definitions. Thus, by recording them, we capture all the external type
requirements of the given definition in the form of a type signature,
which can be used later to reconstruct its type derivation in a
different environment, simply by checking if all these assumptions were
satisfied in that environment. This notion of assumption based type
derivation tree is defined as follows.

\begin{definition}\label{assume-notation} Given a typing
$\ibx{TE}\vdash{}e:\tau$ and its associated derivation tree, we write
 $A^{\sibx{TE}}\vdash{}e:\tau$, or simply $A\vdash{}e:\tau$ (when
\ibx{TE} is clear by context),
as another typing representing the same derivation tree that
explicitly records all type instances of its free (external)
identifiers.  $A^{\sibx{TE}}=\fn{assumptions}{e}$ is the set of
assumptions constructed inductively as follows:

\begin{display}
\tbx{Def} assumptions(e) =
  \tbx{case} e \tbx{of}
    x       $\Longrightarrow$ $\{(x\mapsto\tau)\}$
\vsp
    $\lambda{}x.\:e_1$ $\Longrightarrow$ \tbx{let} $\ibx{TE}'=\ibx{TE}+\{x\mapsto\tau_2\}$ ; 
                      $A^{\sibx{TE}'} = \fn{assumptions}{e_1}$
                  \tbx{in} 
                      $A^{\sibx{TE}'}\setminus_{\{x\}}$
\vsp
    $e_1$ $e_2$  $\Longrightarrow$ \tbx{let} $A_1^{\sibx{TE}} = \fn{assumptions}{e_1}$ ; 
                      $A_2^{\sibx{TE}} = \fn{assumptions}{e_2}$
                  \tbx{in} 
                      $A_1^{\sibx{TE}}\cup{}A_2^{\sibx{TE}}$
\vsp
    \tbx{let $x = e_1$ in $e_2$} $\Longrightarrow$
                 \tbx{let} $\ibx{TE}'=\ibx{TE}+\{x\mapsto\fn{close}{\ibx{TE},\tau_1}\}$ ;
                      $A_1^{\sibx{TE}} = \fn{assumptions}{e_1}$ ; 
                      $A_2^{\sibx{TE}'} = \fn{assumptions}{e_2}$
                  \tbx{in}
                      $A_1^{\sibx{TE}}\cup{}A_2^{\sibx{TE}'}\setminus_{\{x\}}$
  \tbx{endcase}.
\end{display}
\end{definition}

Note that there may be several type instances recorded in
$A^{\sibx{TE}}$ for the same identifier $x$ corresponding to its
various occurrences within $e$. Also note that $A^{\sibx{TE}}$ is not
a type environment in itself, but it serves as a cumulative record of
the use of the free identifiers of the expression $e$ during the
derivation of the typing $\ibx{TE}\vdash{}e:\tau$. 

The range of an assumption set $A^{\sibx{TE}}$ is a set of types, so we can
apply substitutions to assumption sets just like we do to type
environments.  The only restriction is that substitutions do not apply to
those type-variables in the range that were ``closed'' \via the
generalization operation during the typing of expression $e$. We call such
type-variables $\fn{genvars}{A^{\sibx{TE}}}$. This restriction has the same
effect as in the case of type environments, where by definition,
substitutions do not apply to the bound type-variables in their range. The
algorithm $W'$ achieves this automatically by always using fresh
type-variables to instantiate a previously closed type-variable. Thus, at
each stage of the typing derivation, the substitutions used at that point
never interfere with the previously closed type-variables.

The following lemma forms the backbone of the assumption based reasoning
in the subsequent proofs for correctness of our incremental system.

\begin{lemma}\label{assume-subst} Let $A^{\sibx{TE}}\vdash{}e:\tau$ be a
typing corresponding to $\ibx{TE}\vdash{}e:\tau$
defined \via definition~\ref{assume-notation}. Then for any
substitution $S$ that does not 
involve $\fn{genvars}{A}$ in its domain or range,
$S(A^{\sibx{TE}})\vdash{}e:S\tau$ is also a valid typing corresponding
to $S(\ibx{TE})\vdash{}e:S\tau$.
\end{lemma}

The above lemma provides a way to use the assumption sets to
obtain new correct typings from old typings for the same
expression. 

Now we come back to the algorithm $W'$ (refer \fig{algo-w'})
and show that the assumptions collected there  actually correspond to
the typing generated by the algorithm. The proof of this lemma is
by structural induction on $e$ and uses lemma~\ref{assume-subst}.

\begin{lemma}\label{assume-soundness} If assumption set $A$ is
collected in the invocation $W'(\ibx{TE},e)=(S,\tau,A)$ then
$A\vdash{}e:\tau$ is a valid typing that corresponds to the typing
$S(\ibx{TE})\vdash{}e:\tau$ generated using structural induction on
$e$ under the type environment \ibx{TE}.
\end{lemma}

The above lemma shows that the assumptions collected by algorithm
$W'$ are sound in the sense that they denote a valid typing.

\subsection{Correctness of Algorithm $W_1$}

The correctness of algorithm $W_{1}$ is established in two phases. First, we
show that it is complete, \ie, at all times the type environment resulting
from type-checking a binding is a generalization of the final type environment
$\ibx{TE}_{t}$ obtained in the batch system. 

\begin{lemma}\label{TEi-TEt} If $\ibx{TE}_t$ is the final type
environment in the batch system with the type-scheme obtained
for the final program query being assigned to the special variable
``\tbx{it}'', then for every $i\geq0$,  $\ibx{TE}_i\succeq\ibx{TE}_t$.
\end{lemma}

The above lemma implies that starting with the most general type-scheme
$\forall\alpha.\alpha$, the type-schemes of the top-level identifiers
get constantly refined as their definitions are type-checked, but at
each stage they remain complete with respect to their actual type-schemes.
The proof of this lemma requires a similar statement regarding the SCC
of top-level identifiers, that they grow monotonically from the empty
set $\phi$ stablizing at their actual SCC. 

The second step in proving the correctness of algorithm $W_1$ is to
show that the process of incrementally refining the compilation
environment eventually terminates, and when it does, it exactly
corresponds to the compilation environment obtained in the batch
system.  As noted in section~\ref{overall-plan}, we stop further
compilation only when all the assumption checks collected during the
various invocations to $W_1$ are passed successfully by the existing
property-values in the current compilation environment. The assumption
checks play an important role here in guaranteeing that only a sound
compilation environment is acceptable, otherwise the process of
incremental refinement continues. Termination is shown by proving that
the assumptions checks are eventually passed by some environment.

\begin{lemma} \label{TEt-TEf} In the sequence of type
environments $\ibx{TE}_0,\ldots,\ibx{TE}_i,\ldots$ generated from the
various invocations to $W_1$, there exists an environment $\ibx{TE}_f$ (and
every environment after that) that passes all the
upper bound type assumptions (M) for all the top-level identifiers, \ie,
\[\forall{}x\in{}X,\;\forall{}(y\mapsto\tau_y^i)\in{}M_x,\;\;\ibx{TE}_f(y)\succeq\tau_y^i\]
and moreover, $\ibx{TE}_t\succeq\ibx{TE}_f$.
\end{lemma}

The proof of this lemma uses the earlier lemmas~\ref{assume-subst} and
\ref{assume-soundness} about the properties of assumptions collected. This
also requires a similar lemma for the soundness of SCC environment. 

The soundness of the types obtained in our incremental system depends on
whether all the upper bound type assumptions checks have been passed or
not. We state this in the form of a termination strategy. 

\begin{term-strategy} Assuming that all the top-level definitions in the given
program are compiled at least once, the incremental compilation system
terminates when all the upper bound type assumptions (M) for each of the
top-level identifiers pass their check in the latest compilation
environment. 
\end{term-strategy}

Finally, we state the correctness theorem. 

\begin{theorem}\label{corr-theorem} Given a complete and type-correct
program, when the incremental system terminates, it has computed
exactly the same type and SCC environments as computed in a batch
system.
\end{theorem}
\begin{proof} The incremental system starts in an empty compilation
environment ($\ibx{TE}_0$ and $\ibx{SE}_0$) as given by
equations~\ref{TE-init-eq} and \ref{SE-init-eq}.  So the completeness
lemma~\ref{TEi-TEt} is applicable. The termination strategy ensures
that the system terminates in an environment ($\ibx{TE}_f$ and
$\ibx{SE}_f$) that satisfies the soundness lemma~\ref{TEt-TEf}.
Combining the result of these lemmas we straightaway obtain
$\ibx{SE}_f=\ibx{SE}_t$ and $\ibx{TE}_f=\ibx{TE}_t$.
\end{proof}

