
\section{Formal Properties of the System}
In this section we present some formal properties of our language which will help us prove the soundness of the optimisations presented in the remaining part of this paper. We present only the interesting cases of the proofs here, leaving the remaining bulk to the appendix. \TODO{Contrast with relational approach, Benton, Bisimulation, Contexts, Denotational Semantics} Is a current area of research. Is a ``low level'' operational approach, contrasted with relational approach of Benton et al. Reason about ``what might be changed'' rather than ``what is preserved''.  Relational approaches have issues with region allocation, and higher order store. Our main focus is on expressiveness of the language, and production of the compiler. Taking the operational approach provides straightforward reasoning, and does not require us to restrict the expressiveness of the language. We will discuss limitations of the various approaches further when we consider validity of hoisting transform in \TODO{ref}.  


% -----------------------------------------------------------------------------
\subsection{Natural Semantics}
\input{04-Language/EvalNatural}
In addition to the small step operational semantics in Fig. \ref{fig:TermEvaluation} we use a big step natural semantics to reason about the equivalence of reductions. This semantics is given in Fig. \ref{fig:NaturalSemantics}. The judgement form $\eiJudge{H}{t}{H'}{t'}{B}$ reads: in store $H$ the term $t$ reduces to a new store $H$ and a (weak) value $v^\circ$ causing a set of heap actions $B$. Likewise for witness construction, the judgement form $\wiJudge{H}{\delta}{\Delta}{B}$ reads: in store $H$ type $\delta$ reduces to witness $\Delta$ causing a set of heap actions $B$. 

% -------------------------------------
\begin{definition}[Heap Actions]
Heap actions provide a summary of what regions, store bindings and properties were used during the reduction. The possible heap actions are as follows:

\medskip
\begin{tabular}{ll}
$\rcreate~ o$		&~~ Creation of a store property ($o$) such as $\rho$ or $(\rconst~ \rho)$.  \\
$\rtest~ o$		&~~ Store property ($o$) must be present for evaluation to progress. \\
$\ralloc~ l^\rho$	&~~ Allocation of a store binding at location $l$ in mutable region $\rho$. \\
$\rread~  l^\rho$	&~~ Read from a store binding in a mutable region. \\
$\rwrite~  l^\rho$	&~~ Write to a store binding in a mutable region.
\end{tabular}
\end{definition}

\bigskip
\begin{flushleft}
We also define some helper functions to extract interesting subsets of actions:
\end{flushleft}
\[	\begin{array}{llll}
	\rCreates(B)	& \equalsdef \setof{\rcreate~ o \in B} & \qq
	\rTests(B)	& \equalsdef \setof{\rtest~   o \in B} \\
	\rReads(B)~	& \equalsdef \setof{\rread~ l^p \in B}  & \qq
	\rWrites(B)	& \equalsdef \setof{\rwrite~ l^p \in B} \\
	\rAllocs(B)	& \equalsdef \setof{\ralloc~ l^p \in B} \\
	\end{array}
\]
\[	\begin{array}{llll}
	\rMakes(B)	& \equalsdef~ \rCreates(B) \cup \rAllocs(B)
\\
	\rNeeds(B)	& \equalsdef~ \rTests(B)   \cup \rReads(B) \cup \rWrites(B)
	\end{array}
\]


\pagebreak{}
% -------------------------------------
\begin{theorem}[Small to Big]
Reducing a well typed term via the small step semantics yields the same result as using the big step semantics. \emph{Proof:} by induction over the number of steps in the small step evaluations. 

\medskip
\statement{
	If	&~ $\tyJudgeGS
			{t}
			{\tau}
			{\sigma}$
		  ~~and~~ $\Sigma \models H$ ~and~ $\Sigma \vdash H$ \\
	 ~and	&~ $H ~;~ t \longtoa{n} H' ~;~ v^\circ$ \\
	then	&~ $\eiJudge{H}{t}{H'}{v^\circ}{B}$~ for some $B$
\\[1ex]
	If~	&~ $\kiJudgeGS
			{\delta}
			{\iPure~ \sigma}$
		  ~~and~~ $\Sigma \models H$ ~and~ $\Sigma \vdash H$ \\
	~and	&~ $H ~;~ \delta \ltoa{n} \delta'$ \\
	then	&~ $\wiJudge{H}{\delta}{\delta'}{B}$~ for some $B$
}
\end{theorem}

\TODO{Why do we need well typedness judgements? We've already said it reduces to a value. Gunter gives equiv theorem just using the eval judgements}

% -------------------------------------
\begin{theorem}[Big to Small]
Reducing a well typed term via the big step semantics yields the same result as using the small step semantics. \emph{Proof:} by induction over the derivations of \mbox{$\eiJudge{H_0}{t_0}{H_n}{v_n^\circ}{B}$} and $\kiJudgeGS{\delta}{\iPure~ \sigma}$. \medskip

\statement{
	If	&~ $\tyJudgeGS
			{t}
			{\tau}
			{\sigma}$
		  ~~and~~ $\Sigma \models H$ ~and~ $\Sigma \vdash H$ \\
	 ~and	&~ $\eiJudge{H}{t}{H'}{v^\circ}{B}$ \\
	then	&~ $H ~;~ t \longtoa{n} H' ~;~ v^\circ$~ for some $n$
\\[1ex]
	If	&~ $\kiJudgeGS
			{\delta}
			{\iPure~ \sigma}$
		  ~~and~~ $\Sigma \models H$ ~and~ $\Sigma \vdash H$ \\
	~and	&~ $\wiJudge{H}{\delta}{\delta'}{B}$ \\
	then	&~ $H ~;~ \delta \ltoa{n} \delta'$~ for some $n$
}
\end{theorem}


% -------------------------------------
\begin{lemma}[Simultaneous Creation]
Suppose we reduce term $t$ in heap $H$. If some region handle $\rho$ is in the initial heap, and property $(\rmutable~ \rho)$ is in the final heap, then that property was also in the initial heap. This also true for properties of the form $(\rconst~ \rho)$.

\medskip
\statement{
	If	&~ $\eiJudge{H}{t}{H'}{t}{B}$ 
			~and~ $\rho \in H$ 
			~and~ $\rmutable~ \rho \in H'$ \\
	~then	&~ $\rmutable~ \rho~ \in H$
}
\end{lemma}

\begin{proof}
By induction over the derivation of $\eiJudge{H}{t}{H'}{t}{B}$. This lemma can be verified directly from Fig. \ref{fig:NaturalSemantics}. The only rule that introduces handles or properties to the heap is (EiWithR), and these properties are based on the set of witnesses provided by (EiLetR). 
\end{proof}

% -------------------------------------
\begin{lemma}[Actions on Mutable Regions Require Mutability]
If a reduction performs a $\rmread~ l^\rho$, $\rwrite~ l^\rho$ or $\rmalloc~ l^\rho$ action on some region $\rho$ then the property $\rmutable~ \rho$ must be in the resulting heap.

\medskip
\statement{
	If	&~ $\eiJudge{H}{t}{H'}{t}{B}$  \\
	~and~ 	&~ $\alpha \in B$~ for $\alpha$ one of $\rmread~ l^\rho$,~ $\rwrite~ l^\rho$,~ $\rmalloc~ l^\rho$ \\
	then	&~ $\rmutable~ \rho~ \in H'$
}
\end{lemma}

\pagebreak{}

\begin{proof}
By induction over the derivation of $\eiJudge{H}{t}{H'}{t}{B}$. As before, this lemma can be verified directly from Fig. \ref{fig:NaturalSemantics}. All rules that cause these actions require the corresponding property to be in the heap, and properties are not removed from the heap once added. In contrast to the previous lemma, we only require the property to be in the \emph{resulting} heap, as the reduction may have added it itself.
\end{proof}

% -----------------------------------------------------------------------------
\subsection{Visible and Invisible Actions}
The following lemmas relate to the validity of our effect typing system. This includes the masking performed by the TyLetR, TyWithR and TyMaskPure rules from Fig. \ref{fig:TypesOfTerms}. The key point is as follows. Suppose the reduction of some term performs an action on a store location, but that location is in a region not in the current store typing. In this case the affected region had not been created before the reduction commenced. Due this, we view the action as being entirely local to the given reduction, or in other words, invisible to the surrounding context. The first lemma states that if a reduction of a term performs visible actions, then these actions are recorded in its effect. Conversely, the second states that all the actions performed by the reduction of a term with a pure effect are invisible. The proof of the second depends on the first to show contradictions. 


% -------------------------------------
\begin{theorem}[Visible Actions]
If the reduction of an term reads, writes or allocates mutable data in a pre-existing region then the term has the corresponding effect.

\medskip
\begin{tabular}{llll}
	If~	& $\tyJudgeGS{t}{\tau}{\sigma}$ & ~~and~~	& $\eiJudge{H}{t}{H'}{t'}{B}$ \\
	~and~~ 	& \mc{3}{$\Sigma \models H$ ~~and~~ $\Sigma \vdash H$ ~~and~~ $\un{\rho} \in \Sigma$} \\
	then~~  & \mc{3}{(If $\rmread~   l^\rho \in B$  for some $l$ then~ $\suJudgeGS{\iRead~  \un{\rho}}{\sigma}$)} \\
	~and~~	& \mc{3}{(If $\rwrite~~~~ l^\rho \in B$ for some $l$ then~ $\suJudgeGS{\iWrite~ \un{\rho}}{\sigma}$)} \\
	~and~~	& \mc{3}{(If $\rmalloc~ l^\rho \in B$   for some $l$ then~ $\suJudgeGS{\iAlloc~ \un{\rho}}{\sigma}$)}
\end{tabular}
\end{theorem}

\begin{proof}
By induction over the derivation of $\eiJudge{H}{t}{H'}{t'}{B}$, with full details in the appendix. This proof has two main aspects. Firstly, we must verify that when the reduction of a particular construct performs an action, then the typing rule for that construct includes the appropriate effect term. The interesting constructs are  $\kcase$,~ $\iupdate$, and~ $K~ \ov{\varphi}~ \ov{t}$, which perform reads, writes and allocations respectively. We must also verify that the propagation of actions in the evaluation rules mirrors the propagation of effects in the typing rules. The most obvious example of this is the rule pair EiApp and TyApp. In EiApp we have have $B_1 \cup B_2 \cup B_3$ for the actions, while in TyApp we have $\sigma_1 \lor \sigma_2 \lor \sigma$ for the effects. 

Secondly, we must verify that whenever we have a construct that performs effect masking, such as $\kletregion$, $\kwithregion$ or $\kmask$, if one of its subterms performs a visible action, then the corresponding effect is not erroneously masked. For example, the following case proves the reads on mutable regions cannot be masked by a $\kmask$ construct. When presenting proofs we underline the statement numbers of assumptions, and write statements resulting from inversion lemmas in the same style as the corresponding rules. 

\medskip
\clearpage{}
% -----------------
\pCase $t = \kmask...$ / TyMask / EiMask\\
\[	\infer	{ (\un{1})~
		  \tyJudgeGS
			{\teMask{\delta}{t}}
			{\tau}
			{\sigma \setminus \sigma'}
		}
		{ (6)~
		  \tyJudgeGS{t}{\tau}{\sigma}
	  	  \quad
	  	  (7)~
		  \kiJudgeGS{\delta}{\iPure~ \sigma'}
		}
\]
\[	\infer	{ (\un{2})~
		  \eiJudge
			{H_0}{\teMask{\delta}{t}}
			{H_1}{v^\circ}
			{B_1 \cup B_2}
		}
		{ (8)~
		  \wiJudge{H_0}{\delta}{\un{\rpure~ \sigma'}}{B_1}
		  \quad
		  (9)~
		  \eiJudge
			{H_0}{t}
			{H_1}{v^\circ}
			{B_2}	
		}
\]

\tabbedstmts{
	(IH)	\> Vis. Actions holds for all subderivations of 
			$\eiJudge
				{H_0}{\teMask{\delta}{t}}
				{H_1}{v^\circ}
				{B_1 \cup B_2}$
\\
	(\un{1..2})
		\> ...
		\> \hspace{-5em}(assume)
\\
	(\un{3..5})~
		\> $\Sigma \models H_0$,~ $\Sigma \vdash H_0$,~ $\un{\rho} \in \Sigma$
		\> \hspace{-5em}(assume)
\\
	(10)~ 	\> $\rmread~ l^\rho \notin B_1$,~ $\rwrite~ l^\rho \notin B_1$~ $\rmalloc~ l^\rho \notin B_1$
		\> \hspace{-5em}(Only tests in Wit. Eval. 8)
\\
	(11)~	\> If~ $\rmread~ l^\rho \in B_2$ then $\suJudgeES{\iRead~ \un{\rho}}{\sigma}$
		\> \hspace{-5em}(IH 6 9 3 4 5)
\\[0.5ex]
	(12)~	\> $\rmread~ l^\rho \in B_2$
		\> \hspace{-5em}(assume)
\\
	(13)~	\> ~~~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma}$
		\> \hspace{-5em}(Imp. Elim. 11 12)
\\
	(14)~	\> ~~~ $\rho \in H_0$
		\> \hspace{-5em}(Store Model 3 5)
\\
	(15)~	\> ~~~ $\rmutable~ \rho \in H_1$
		\> \hspace{-5em}(Actions on Mut. Regions 9 12)
\\
	(16)~	\> ~~~ $\rmutable~ \rho \in H_0$
		\> \hspace{-5em}(Sim. Creat. 9 14 15)
\\
	(17)~	\> ~~~ $\un{\rmutable~ \rho} \in \Sigma$
		\> \hspace{-5em}(Store Model 3 16)
\\[0.5ex]
	(\un{18})~	
		\> ~~ Suppose we had a derivation of~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma'}$
\\
	(19)~	\> ~~~~~~~~ $\kiJudgeGS{\un{\rpure~ \sigma'}}{\iPure~ \sigma'}$
		\> \hspace{-5em}(Prog. Purity 8 7)
\\
	(20)~	\> ~~~~~~~~ $\suJudgeGS{\sigma'}{\bot}$
		\> \hspace{-5em}(SubPure 19)
\\
	(21)~	\> ~~~~~~~ $\neg(\suJudgeGS{\sigma'}{\bot})$
		\> \hspace{-5em}(No Purif. of Impurity 18 17)
\\
	(22)	\> ~~~~~~~ Contradiction
		\> \hspace{-5em}(20 21)
\\
	(23)	\> ~~~ $\neg(\suJudgeGS{\iRead~ \un{\rho}}{\sigma'})$
		\> \hspace{-5em}(Neg. Intro. 18-22)
\\
	(24)~	\> ~~~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma \setminus \sigma'}$
		\> (Prop. of $\setminus$ 13 23)
\\
	(25)~	\> If $\rmread~ l^\rho \in B_1 \cup B_2$ ~then~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma \setminus \sigma'}$
		\> (Imp. Intro. 12-23 10)
\\[0.5ex]
		\> Cases for $\rwrite~ l^\rho \in B_2$ and $\rmalloc~ l^\rho \in B_2$ similarly.
}

In (10) we use the fact that the reduction of a witness, such as in $\wiJudge{H_0}{\delta}{\un{\rpure~ \sigma'}}{B_1}$ can only perform test actions, which is easy to verify from Fig. \TODO{ref}. In (15) we use the Actions on Mutable Regions lemma to show that a $\rmread~ l^\rho$ action can only be performed when the store contains the corresponding $(\rmutable~ \rho)$ property. In  and in (16) we show that this property must have been in the initial store all along. In (18-23) we proved that the effect $\sigma'$ which is being subtracted from overall effect of the body of the mask expression cannot contain the term $\iRead~ \un{\rho}$ where $\un{\rho}$ is mutable. This in turn guarantees that if the body has this visible effect, then so does the overall \textbf{mask} expression.
\end{proof}

\clearpage{}
% -------------------------------------
\begin{theorem}[Invisible Actions]
The reduction of a pure expression does not read, write or allocate mutable data in a pre-existing region.

\medskip
\begin{tabular}{llll}
	If~	& (\un{1})~ $\tyJudgeGS{t}{\tau}{\sigma}$ ~~and~~ (\un{2})~ $\eiJudge{H}{t}{H'}{t'}{B}$ \\
	 ~and~~	& \mc{3}{ 	(\un{3})~ $\Sigma \models H$ 
			~~and~~ (\un{4})~ $\Sigma \vdash H$ 
			~~and~~ (\un{5})~ $\suJudgeGS{\sigma}{\bot}$ } \\
	 ~and~~	& \mc{3}{(\un{6})~ for $\alpha$ 
				any of ~$\rmread~ l^\rho,~ \rwrite~ l^\rho,~ \rmalloc~ l^\rho$~
				we have $\alpha\in B$} \\
	then~	& \mc{3}{$\un{\rho} \notin \Sigma$} \\
\end{tabular}
\end{theorem}

\begin{flushleft}
\emph{Proof}
\end{flushleft}
\tabbedstmts{
	(\un{1..6})	
		\> ...
		\> \hspace{-2em}(assume)
\\
	(7)~	\> Suppose~ $\un{\rho} \in \Sigma$
\\
	(8)~	\> Case: $\alpha$ = $\rmread~ l^\rho$ ~where~ $\alpha \in B$
\\
	(9)	\> ~~~ If~ $\rmread~ l^\rho \in B$~ for some $l$ ~then~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma}$
		\> (Vis. Actions 1 2 3 4 7)
\\
	(10)	\> ~~~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma}$
		\> \hspace{-2em}(Imp. Elim. 8 9)
\\
	(11)	\> ~~~ $\rmutable~ \rho \in H'$
		\> \hspace{-2em}(Actions on Mut. Regions 2 8 )  
\\
	(12)	\> ~~~ $\rho \in H$
		\>\hspace{-2em}(Store Model 3 7)
\\
	(13)	\> ~~~ $\rmutable~ \rho \in H$
		\> \hspace{-2em}(Sim. Creat. 2 12 11)  
\\
 	(14)	\> ~~~ $\un{\rmutable~ \rho} \in \Sigma$
		\> \hspace{-2em}(W.T. Store 13 4)
\\
	(15)	\> ~~~ $\neg (\suJudgeGS{\sigma}{\bot})$
		\> \hspace{-2em}(No Puriif. of Impurity 10 14)
\\
	(16)	\> ~~~ Contradiction
		\> \hspace{-2em}(5 15)
\\
	(17)	\> $\un{\rho} \notin \Sigma$
\\[1ex]
		\> Cases for $\alpha = \rwrite~ l^\rho$ and $\alpha = \ralloc~ l^\rho$ similarly. \hspace{15pt}\proofbox
}

% -----------------------------------------------------------------------------
\subsection{Residues and Heap Factoring}
In this section we build up the definition of what it means for two reductions to the non-interfering. We do this in stages, starting from reasoning about the changes made to the heap, then defining the actions that result in commutable changes, then defining the effects that result in commutable actions. Metaphorically, each of the following definitions ``level'' of our reasoning, with the interspersed lemmas functioning as the ``stairs'' to get back to the previous level.


% -------------------------------------
\begin{definition}[Residue of Evaluation]
The residue of an evaluation, written \tbf{R}$(H,H')$ is the difference between two heaps $H$ and $H'$ resulting from the reduction $\eiJudge{H}{t}{H'}{t'}{B}$ for some terms $t$ and $t'$. Whereas we use a bold face \tbf{R} for the function that computes the residue, by convention use normal face \trm{R} to range over such residues. 

\[	\begin{array}{llll}
	\Residue(H,H')
	 & \equalsdef 	& \{~ \pi \in H' & \trm{where}~~ \pi \notin H ~\}
					 ~~\equiv~~ H' \setminus H
	\end{array}
\]
\end{definition}

% -------------------------------------
\begin{lemma}[Heap Factoring]
The heap resulting from a reduction can be written in terms of the initial heap and a residue. 

\smallskip
\statement{
	If~~	& $\eiJudge{H}{t}{H'}{t'}{B}$ \\
	then~~	& $H' = H \succ \Residue(H,H')$~~ for some $\Residue(H,H')$
}
\end{lemma}


\clearpage{}
% -----------------------------------------------------------------------------
\subsection{Non Interference and Commutability}


% --------------------------------------
\begin{definition}[Commutable Residues]
Two residues are commutable when we can change the order in which they are added to the heap, without changing the end result. This commutability property is given formally in the following lemma.

\medskip
\begin{tabular}{lllll}
	\mc{4}{CommutableResidues($R_1$,~ $R_2$)} \hspace{20em}\\
	& ~~~$\equalsdef$~	& forall~~ $l \mtoa{\rho} \mu \in R_1$ 
				& ~~ we have $l \mtoa{\rho} \mu' \notin R_2$ for any $\mu'$  
\\
	& ~~~and~~		& forall~~    $\rmutable~ \rho \in R_1$
				& ~~ we have  $\rconst~   \rho \notin R_2$
\\
	& ~~~and~~		& forall~~    $\rconst~ \rho   \in R_1$
				& ~~ we have  $\rmutable~ \rho \notin R_2$
\\
\end{tabular}
\end{definition}


% -------------------------------------
\begin{lemma}[Commutable Heap Updates]

\begin{tabular}{ll}
	If	& CommutableResidues($R_1$,~ $R_2$) \\
	~then~~	& 	$R_1 \succ R_2  \equiv	R_2 \succ R_1$ 
\end{tabular}
\end{lemma}

% -------------------------------------
\begin{definition}[Commutable Actions]
We define commutable actions to be actions performed by reductions that are essentially independent. Such reductions do not both write to the same heap binding, or write to one that the other one reads. They also do not add conflicting store properties to the heap, or add one that the other needs to progress.

\medskip
\begin{tabular}{llllllllll}
	\mc{4}{CommutableActions($B_1$,~ $B_2$)} \\
	& ~~~$\equalsdef$~	& $(\rMakes(B_1)$	& $~\cap~~ \rMakes(B_2)$	& $~ = \emptyset)$ &
	& ~~~~and~~~~		& $(\rWrites(B_1)$	& $~\cap~~ \rWrites(B_2)$	& $~ = \emptyset)$ \\
	& ~~and~~		& $(\rNeeds(B_1)$	& $~\cap~~ \rMakes(B_2)$	& $~ = \emptyset)$ &
	& ~~~~and~~~~		& $(\rReads(B_1)$	& $~\cap~~ \rWrites(B_2)$	& $~ = \emptyset)$ \\
	& ~~and~~		& $(\rMakes(B_1)$	& $~\cap~~ \rNeeds(B_2)$	& $~ = \emptyset)$ &
	& ~~~~and~~~~		& $(\rWrites(B_1)$	& $~\cap~~ \rReads(B_2)$	& $~ = \emptyset)$
\end{tabular}

\end{definition}

% -------------------------------------
\begin{lemma}[Commutable Actions Yield Commutable Residues]
When two reductions have commutable actions, then any modifications they make to the heap (heap residues) are also commutable. 

\medskip
\begin{tabular}{ll}
	If~~		&~ (\un{1})~ $\eiJudge{H}{t_1}{H \succ R_1}{t_1'}{B_1}$ \\
	~~and~~		&~ (\un{2})~ $\eiJudge{H}{t_2}{H \succ R_2}{t_2'}{B_2}$ \\
	~~and~~		&~ (\un{3})~ CommutableActions ($B_1,~ B_2$) \\
	then~~		&~ CommutableResidues($R_1,~ R_2$)
\end{tabular}

\medskip
\emph{Proof:} By Contradiction. Assume (\un{1..3}). Now, suppose $\neg$CommutableResidues($R_1,~ R_2$). By the definition of CommutableResidues we have at least one of the following: $l \mtoa{\rho} \mu \in R_1$ and $l \mtoa{\rho} \mu' \in R_2$ for some $l,~ \rho,~ \mu,~ \mu'$; or we have $(\rmutable~ \rho \in B_1)$ and $(\rconst~ \rho \in B_2)$. For the first case, by inspection of the evaluation rules, the only rules that can add or modify bindings to the heap are (EiAlloc) and (EiUpdate). This results in either $(\ralloc~ l^\rho \in B_1)$ or $(\rwrite~ l^\rho \in B_1)$ or both, and likewise for $B_2$. Each of these sub cases can be shown to be contradictory via (3) using the conjuncts in the definition of CommutableActions. For the second case, by inspection of the evaluation rules, the only rule that can add properties to the heap is (EiLetR). When it does so $\rho$ is fresh, so two reductions cannot create a property referring to the same $\rho$. Contradiction.~~ \proofbox

\end{lemma}
\pagebreak{}


% -------------------------------------
\begin{definition}[Non-Interfering Effects]
Here we define what it means for two effect terms to be noninterfering. Important point is that we want to make this judgement at compile time, where we do not have the access to the store typing. \TODO{talk about loss of precision in next theorem}. Actions reveal what ``actually'' happens, whereas our effect information only provides an approximation of this.

\medskip
\begin{tabular}{lcl}
	$\rWrites(\Gamma,~ \sigma)$ 
		& ~~$\equalsdef$~~
		& $\setof{~\iWrite~ \varphi 
				~~\trm{where}~~ \suJudgeES{\iWrite~ \varphi}{\sigma_1}}$
\\[1ex]
	$\rUReads(\Gamma,~ \sigma)$ 
		& ~~$\equalsdef$~~
		& $\{~\iRead~ \varphi
				~~~\trm{where}~~ \suJudgeES{\iRead~ \varphi}{\sigma_1}$
\\
	&	& \qq \qq \quad ~~and~ $w : \iConst~ \varphi \notin \Gamma$ for any $w$ \}
\end{tabular}

\medskip
\begin{tabular}{cclcl}
	\mc{5}{NonInterfering$(\Gamma,~ \sigma_1,~ \sigma_2)$} \\
	 & ~~$\equalsdef$~~ 
			& $(\rWrites(\Gamma,~ \Sigma,~ \sigma_1) = \emptyset$ 
			& ~~and~~ 
			& $ \rWrites(\Gamma,~ \Sigma,~ \sigma_2) = \emptyset)$ 
\\
	 & ~~or~~ 	& $(\rWrites(\Gamma,~ \Sigma,~ \sigma_1) = \emptyset$
			& ~~and~~
			& $\rMReads(\Gamma,~ \Sigma,~ \sigma_1) = \emptyset)$
\\
	 & ~~or~~	& $(\rWrites(\Gamma,~ \Sigma,~ \sigma_2) = \emptyset$
			& ~~and~~
			& $\rMReads(\Gamma,~ \Sigma,~ \sigma_2) = \emptyset)$
\end{tabular}
\end{definition}

Although this is a fairly weak definition of non-interference, it is simple, and will suffice for now. We regard it as ``weak'' because it classifies  $\iWrite~ r_1$ and $\iWrite~ r_2$ as potentially interfering for distinct $r_1$ and $r_2$. The issue here is with aliasing. Although distinct region handles are guaranteed to correspond to distinct regions in the store, this is not the case for region \emph{variables}, as the same handle could be substituted for both in a later reduction. We will discuss this issue further in the next section, and improve the above definition in \S\ref{WitnessesOfDistinctness}. 


\medskip
% -------------------------------------
\begin{lemma}[Non-Interfering Effects Yield Commutable Actions]

\medskip
\begin{tabular}{llll}
	If~~		&~ $\tyJudge{\Gamma}{\Sigma_1}{t_1}{\tau_1}{\sigma_1}$	
			& ~~and~~ 
			&  $\eiJudge{H_1}{t_1}{H_1'}{t_1'}{B_1}$ 
\\
	~and~~		&~ $\tyJudge{\Gamma}{\Sigma_2}{t_2}{\tau_2}{\sigma_2}$
			& ~~and~~ 
			& $\eiJudge{H_2}{t_2}{H_2'}{t_2'}{B_2}$ 
\\
	~and~~		& \mc{3}{~NonInterfering($\Gamma,~ \sigma_1,~ \sigma_2$)} \\
	then~~		& \mc{3}{~CommutableActions($B_1,~ B_2$)}
\end{tabular}
\end{lemma}

Important point is that we evaluate the expressions in the same type environment, but in different store typings.

