\documentstyle[epsf,fullpageusa,tightlist]{jsc-zena}

\input{../../../Bk/tex/include-file}

\input{../../../Bk/tex/macros.tex}

\begin{document}

\title{Properties of a First-order  Functional Language with Sharing}

\author{{\it Zena M. Ariola}\\
Computer \& Information Science Department  \\
University of Oregon \\
{\it Arvind}\\
Laboratory for Computer Science\\
Massachusetts Institute of Technology
}

\maketitle{}

\begin{theorem}[Subcommutativity of a GRS$_{\sf NI}$]
\label{commutative}
Given a GRS$_{\sf NI}$ term $M$, and two distinct redexes $\rho_1$ and 
$\rho_2$ in $M$, if $M \reduce{\rho_1}{} M_1$ and 
$M \reduce{\rho_2}{} M_2$, then $\exists$ $M_3$ such that 
$M_2 \reduce{\rho_1 \setminus \rho_2}{} M_3$ and 
$M_1 \reduce{\rho_2 \setminus \rho_1}{} M_3$.
\end{theorem}
\begin{proof}
Let $\rho_1=(\tau_1,z_1,\sigma_1)$ and $\rho_2=(\tau_2,z_2,\sigma_2)$.

Then,
$M_1 \equiv {\tt GC}(\overline{M[z_1\leftarrow r_1^{\sigma_1}]})$,
where $r_1 = {\cal RHS}(\tau_1)$,
and 
$M_2\equiv {\tt GC}(\overline{M[z_2\leftarrow r_2^{\sigma_2}]}$,
where $r_2 = {\cal RHS}(\tau_2)$.

By non-interference, $z_1 \not\equiv z_2$. 

Furthermore, if for some x, 
$\sigma_1 (x) = z_2$, then x must
be a free variable of $\tau_1$.
Similar remark holds for $\sigma_2$.

We consider the effect of doing $\rho_1$ in M on $z_2$ and $\sigma_2$.
1. The replacement operation $M[z_1\leftarrow r_1^{\sigma_1}]$
does not affect $z_2$ and $\sigma_2$.
2. The first step of canonicalization, that is, 
$\overline{M[z_1\leftarrow r_1^{\sigma_1}]}$, cannot affect $z_2$
but will change $\sigma_2$ to $\sigma_2^\prime$ where

          $\sigma_2^\prime(x) = \sigma_2(x)$    if $\sigma_2(x) \neq z_1$ \\
                             $= Root(r_1^{\sigma_1})$   if $\sigma_2(x) = z_1 $\\
                                                     and $Root(r_1^{\sigma_1})
\neq z_1$ \\ 
                             $= \circ$               if $\sigma_2(x) = z_1$
                                                     and $Root(r_1^{\sigma_1})
= z_1$ 


3. The second step of canonicalization, that is, 
${\tt GC} (\overline{M[z_1\leftarrow r_1^{\sigma_1}]})$, 
will either eliminate
$z_2$ or leave $z_2$ and $\sigma_2^\prime$ unaffected. This is so because
if $z_1$ occurs in the range of $\sigma_2 (\ie \sigma_2 (x) = z_1)$, 
then x must be a free variable of $\tau_2$. We consider these two case 
now:

Suppose $z_2$ is not eliminated.

By previous proposition $(\tau_2, z_2, \sigma_2^\prime )$ must be a redex
in ${\tt GC} (\overline{M[z_1\leftarrow r_1^{\sigma_1}]})$.

Let 
$$\begin{array}{l}
M3 \equiv 
{\tt GC} (\overline{
{\tt GC} (\overline{M[z_1\leftarrow r_1^{\sigma_1}]})
[z_2\leftarrow r_2^{\sigma_2^prime}]}) \equiv \\
\\
{\tt GC} (\overline{
\overline{M[z_1\leftarrow r_1^{\sigma_1}]}
[z_2\leftarrow r_2^{\sigma_2^prime}]}) \equiv \\
\\
{\tt GC} (\overline{
M[z_1\leftarrow r_1^{\sigma_1}]
[z_2\leftarrow r_2^{\sigma_2}]}) \equiv\\
\\
{\tt GC} (\overline{
M[z_2\leftarrow r_2^{\sigma_2}]
[z_1\leftarrow r_1^{\sigma_1}]})
\end{array}$$

We can derive the same term by similar reasoning by reducing $\rho_2$
in M first. 
\end{proof}

\end{document}
