\section{Proof Sketches of the Theorems}
\label{section:proof}
In this section, we present proof sketches of some of the main
theorems presented in the paper. Refer to \cite{Coorg94} for
full versions of these.

\begin{proof}(Sketch of theorem~\ref{theorem:basic})
We only prove the sufficiency of these conditions here. Assume (for
contradiction) that $b_Q$ is not correct. That is, there is an
environment $bve$ such that ${\cal E}^{pr} \ld b \rd \: bve \neq
{\cal E}^{pr} \ld b_Q \rd \: bve$. By the property of partitioning,
this can only be true if one of the outputs (say $o$) has a value
in the first case, and is $\bot$ in the second. As $o$ has a value,
each of inputs $I$ of $b$ that are connected to $o$ 
should be defined in $bve$. As $o$ is $\bot$ in the second case and 
$b_Q$ is acyclic, one of the inputs $I_Q$ of $b_Q$ must be $\bot$ in
$bve$. Thus, $I \neq I_Q$, a contradiction to the second condition.
\end{proof}

The proof of correctness of algorithms 1 and 2 make use of 
the following properties of demand and tolerance sets of a basic
block.
\begin{lemma} [Demand-Tolerance Relation]
\label{lemma:dem-tol-relation}
For a node $n$, $Demand(n) \subseteq Tolerance(n)$.
\end{lemma}

\begin{lemma} [Demand and Tolerance Monotonicity]
If node $n$ is transitively connected (from $n$) to node $m$ in a basic 
block, then $Demand(m) \subseteq Demand(n)$ and $Tolerance(m) \subseteq
Tolerance(n)$.
\end{lemma}

\begin{theorem} [Correctness of Algorithm 1]
\label{theorem:correctness-algorithm-1}
Algorithm 1 correctly partitions a basic block.
\end{theorem}
\begin{proof} (Sketch) We use the basic block correctness criterion
to prove that each step of the algorithm (where a clique is identified
and merged) is correct. The correctness of the entire algorithm follows
by an easy induction.
\begin{enumerate}
\item{First, we prove that the connectivity condition is satisfied. For
simplicity, consider the merging of just two nodes $n$ and $m$ such that
$(n,m)$ is an edge of $G_{merge}$. For input-output connectivity, this
is equivalent to adding an edge from $m$ to each of the outputs connected
to $n$ (\ie, $Demand(n)$) and vice-versa. By the definition of tolerance
sets, this does not affect input-output connectivity if $Demand(n) \subseteq
Tolerance(m)$, which is true.}
\item{Now, we prove that the graph corresponding to the reduced basic
block is acyclic. Assume (for contradiction) that a cycle is caused by
merging the nodes in the clique. Without loss of generality, 
there are two nodes $n$ and
$m$ in the clique and a node $n'$ not in the clique, such that
$n$ is connected to $n'$ and $n'$ is connected to $m$ in $b$. Due
to monotonicity of demand and tolerance sets, for any other node $m'$,
if both $(n,m')$ and $(m,m')$ are in $G_{merge}$, then so is $(n',m')$. Thus,
$n'$ could also be included in the clique and hence, the clique is not
maximal, a contradiction.}
\end{enumerate}
\end{proof}


\begin{theorem} [Correctness of Algorithm 2]
\label{theorem:correctness-algorithm-2}
Algorithm 2 correctly partitions a basic block.
\end{theorem}\begin{proof}(Sketch)
Correctness of Algorithm 2 follows from the fact that nodes with
the same demand (or tolerance) set form a clique of the graph $G_{merge}$
in algorithm 1. Consider two nodes $n$ and $m$ such that $Demand(n) = Demand(m)$. By lemma~\ref{lemma:dem-tol-relation}, $Demand(m) \subseteq Tolerance(m)$.
Thus, $Demand(n) \subseteq Tolerance(m)$ and vice-versa. Thus, the edge
$(n,m)$ is present in $G_{merge}$. A similar argument proves that
merging nodes with the same tolerance set is also safe. Acyclicity of
the reduced graph follows from the monotonicity of demand and tolerance
sets.
\end{proof}

\begin{theorem} [Correctness of Algorithm 3]
\label{theorem:correctness-algorithm-3}
Algorithm 3 correctly partitions any block.
\end{theorem}
\begin{proof}(Sketch)
Let $b$ be the input block and $f$ the
function being called. For simplicity, assume that the node calling
$f$ is only non-primitive node in $b$ (\ie, there are no nodes
to be disconnected). First, note that the partitions generated
for $b$ are also correct partitions for $b_1,\ldots,b_P$. This
is ensured as we are taking the unions of the demand and tolerance
sets of each $b_j, 1 \leq j \leq P$.
Next, it is possible to give precise
definitions to the primitive operators introduced in $b_1,\ldots,b_P$
such that for any environment $bve$, ${\cal E}^{pr} \ld b \rd \: bve = 
{\cal E}^{pr} \ld b_j \rd \: bve$, for some $1 \leq j \leq P$
(this follows from the safety of path semantics).

Thus, if a partitioning is incorrect, it will be incorrect
for one $b_j$ too. This contradicts that fact that we are using
a correct partitioning algorithm on $b_j$, which is a basic block.
\end{proof}