\section{Confluence of a GRS without interfering rules}
\label{orthogonal}
Not all GRSs are confluent, however, we can show that for a restricted
class, namely GRSs without interfering rules, confluence is
guaranteed.  We introduce the notion of {\it compatible terms}
\cite{Huet1} which
will be used, among other things, to define the notion of interference
among rules. The idea is that terms which are not ordered, may still
have a common upper bound. As we shall see later, such terms potentially
interfere with each other.

\begin{definition}[Compatible terms]
Given GRS terms $M_1$ and $M_2$ in canonical form,
$M_1$ and $M_2$ are said to
be compatible,
written as $M_1 \uparrow_{\sf \omega} M_2$, iff
$\exists M_3$ such that $M_1 \leq_{\sf \omega} M_3$ 
and $M_2 \leq_{\sf \omega} M_3$.
\end{definition}


For example, consider the following terms: 
$$\begin{array}{l}
M_1 \equiv \{x_1 = {\sf G}(x_2,x_2); \; x_2 = \Omega; \; {\sf In} \; x_1\}, \\
M_2 \equiv \{x_1 = {\sf G}(x_2,x_3);\; x_2 = {\sf F}(0);\;
x_3 = {\sf F}({\sf 0}); \; {\sf In} \; x_1 \}, \\
M_2 \equiv \{x_1 = {\sf G}(x_2,x_3);\;
x_2 = {\sf F}({\sf 0});\; x_3 = {\sf H}({\sf 0}); \; {\sf In} \; x_1\}
\enspace .
\end{array}$$
$M_1$ and $M_2$ are compatible 
with least upper bound:
$\{x_1 = {\sf G}(x_2,x_2); \; x_2 = {\sf F}(0);\; {\sf In} \; x_1\}$.
On the other hand, 
$M_3$ is not compatible either with $M_1$ or $M_2$.

\begin{definition}[Interference]
Given two distinct GRS rules $\tau_1$ and $\tau_2$, $\tau_1$ is said to
interfere with $\tau_2$ iff
$\exists x \in {\tt BV}({\cal P}(\tau_1))$ such that
$ {\cal C}l(\tau_1) @  x \uparrow_{\sf \omega} {\cal C}l(\tau_2)$.
\end{definition}

\begin{definition}[Self-interference]
Given a GRS rule $\tau$, $\tau$ is said to
be self-interfering iff
$\exists x \in {\tt BV}({\cal P}( \tau_1 ))\! - \! {\tt Root}({\cal P}(\tau))$
such that
$ {\cal C}l(\tau) @  x \uparrow_{\sf \omega} {\cal C}l(\tau)$.
\end{definition}

\begin{definition}[GRS$_{\sf NI}$]
If all rules in a GRS are non-self-interfering and  pairwise non-interfering
then the GRS is called a GRS$_{\sf NI}$. 
\end{definition}

%\begin{definition}[Interference]
%Given GRS rules $\tau_1$ and $\tau_2$, $\tau_1$ is said to
%interfere with $\tau_2$ iff
%$\tau_1=\tau_2$ and $\tau_1$ is a multi-rooted rule or 
%$\exists x \in {\tt BV}({\cal P}(\tau_1))$
%such that
%\begin{tightlist}
%\item[(i)]
%if $\tau_1 \neq \tau_2$ then 
%$ {\cal C}l(\tau_1) @  x \uparrow_{\sf \omega} {\cal C}l(\tau_2)$; 
%\item[(ii)]
%if $\tau_1 = \tau_2$ then
%$ {\cal C}l(\tau_1) @  x \uparrow_{\sf \omega} {\cal C}l(\tau_2)$,
%where $x$ is not ${\tt Root}({\cal P}(\tau_1))$; 
%%\item[(iii)]
%%if $\tau_1 = \tau_2$ and $\tau_1$ is a multi-rooted rule.
%\end{tightlist}
%If all rules in a GRS are pairwise non-interfering then the GRS will be
%called a GRS$_{\sf NI}$. 
%\end{definition}
\noindent
For example, the following rule:
%{\small
\[\tau: \;\; \frag{x_1={\sf L}(y)} {x={\sf L}(x_1) \reduce{}{} x ={\sf 0} }\]
%}
interferes with itself because 
${\cal C}l(\tau) @  x_1 \uparrow_{\sf \omega} {\cal C}l(\tau)$.
The following rules: 
\[ \begin{array}{l}
\tau_1:\;\;x={\sf Or}(y,{\sf True}) \reduce{}{} x={\sf True}\\
\tau_2:\;\;x={\sf Or}({\sf True},y) \reduce{}{} x={\sf True}
\end{array} \]
also interfere because 
${\cal C}l(\tau_1) \uparrow_{\sf \omega} {\cal C}l(\tau_2)$,
with
${\sf Or}({\sf True}, {\sf True})$
being the upper-bound.
%Notice that the following two rules are not interfering,
%\[ \begin{array}{l}
%\tau_1: \;\;\frag{x_1 = {\sf G}(y)}{x={\sf F}(x_1) \reduce{}{} x={\sf 0}} 
%\hspace{1cm}
%\tau_2: \;\;\frag{x_1 = {\sf G}(y)}{x={\sf D}(x_1) \reduce{}{} x={\sf 1}}
%\end{array} \]
%This suggests that the preconditions
%of non interfering rules are not affected by a reduction.


\begin{definition}[Ordering on Redexes]
\label{redexordering}
Given two distinct redexes $\rho_1 = (\tau_1,z_1,\sigma_1)$
and $\rho_2=(\tau_2,z_2,\sigma_2)$ in a GRS term $M$ in canonical form:
\begin{tightlist}
\item[(i)]
$\rho_1$ occurs inside $\rho_2$, written as $\rho_1 \preceq \rho_2$, iff
$z_1 \in \{ {\sigma_2}(x) \mid x \in {\tt BV}({\cal P}(\tau_2))\}$;
\item[(ii)]
$\rho_2$ occurs inside $\rho_1$, written as $\rho_2 \preceq \rho_1$, iff
$z_2 \in \{ {\sigma_1}(x) \mid x \in {\tt BV}({\cal P}(\tau_1))\}$;
\item[(iii)]
$\rho_1$ and $\rho_2$ are disjoint iff $\rho_1 \not\preceq \rho_2$, and
$\rho_2 \not\preceq \rho_1$.
\end{tightlist}
Furthermore, if $\rho_1 \preceq \rho_2$ and $\rho_2 \preceq \rho_1$
then $\rho_1$ and $\rho_2$ are said to overlap at the root.
\end{definition}

\begin{proposition}
\label{lemmadisjoint}
Given a GRS$_{\sf NI}$ term $M$ in canonical form, any two distinct redexes $\rho_1$ and 
$\rho_2$ in $M$  are mutually disjoint.
\end{proposition}
\begin{proof}
Let $\rho_1=(\tau_1,z_1,\sigma_1)$ and $\rho_2 =(\tau_2,z_2,\sigma_2)$.
Suppose $\rho_1 \preceq \rho_2$. Then by Definition \ref{redexordering},
$\exists x \in {\tt BV}({\cal P}(\tau_2))$, say $x_2$,
such that $z_1 = {\sigma_2}(x_2)$.
Therefore, we have ${\cal C}l(\tau_2) @ x_2 \uparrow_{\sf \omega} 
{\cal C}l(\tau_1)$, with $M @ z_1$ being the upper bound.
%IS THIS OBVIOUS????? \\
Since rules $\tau_1$ and $\tau_2$ are non-interfering, we have reached 
a contradiction.
Similarly, if $\rho_2 \preceq \rho_1$. Hence $\rho_1$ and $\rho_2$ must 
be disjoint.
\end{proof}

\begin{proposition}
\label{propinterf} 
In a GRS$_{\sf NI}$ reduction, the descendant of a redex, except for the
redex being reduced, if it exists,
is always a redex.
\end{proposition}
\begin{proof}
Let $M \reduce{\rho}{} M_1$, where $\rho=(\tau,z,\sigma)$.
Let 
$\rho_1 = (\tau_1,z_1,\sigma_1)$ be a distinct redex occurring in $M$, such that
%\in {\cal R}(M)$, $\rho \not\equiv \rho_1$, and  
$z_1 \in {\tt BV}(M_1)$. 
We want to show that
$\rho_1 \setminus \rho = (\tau_1,z_1,\sigma_1')$ is a redex, that is,
$\sigma_1'$ is a substitution function from
${\cal C}l(\tau_1)$ to $M_1 @ z_1$. 
According to the definition of descendant of a redex (Definition \ref{descendantredex}),
$\sigma_1'$ differs from $\sigma_1$ only at $z$, the root
of redex $\rho$.
%Furthermore,
%$\sigma_1$ is the
%substitution function from ${\cal P}(\tau_1)$ to $M$.
Therefore, there are only two reasons why $(\tau_1,z_1,\sigma_1')$ may not be a redex:
\begin{tightlist}
\item[(1)]
the new definition of $z$;
\item[(2)]
the canonicalization of $M[z \leftarrow {\cal RHS}(\tau)^\sigma]$ removes
some elements in the range of $\sigma_1$.
\end{tightlist}
The first reason is not possible because,
by Proposition \ref{lemmadisjoint}, all distinct redexes in $M$ are disjoint,
and 
therefore, if $\exists x \in {\tt Var}({\cal P}(\tau_1))$, such that 
$\sigma_1(x) = z$ then $x \in {\tt FV}({\cal P}(\tau_1))$. 
The second reason is also not possible because if 
a variable  or a constant in the range of $\sigma_1$ is
accessible from $z_1$ in $M$ then it has to be accessible
from $z_1$ in $M_1$.
\end{proof}

\begin{theorem}[Subcommutativity of a GRS$_{\sf NI}$]
\label{commutative}
Given a GRS$_{\sf NI}$ term $M$ in canonical form,
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}{0/1} M_3$ and 
$M_1 \reduce{\rho_2 \setminus \rho_1}{0/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)$.  \\


The proof is by cases on the existence of the descendant of
redexes $\rho_1$ and $\rho_2$, respectively.
\begin{mycases}
\item {$\rho_2 \setminus \rho_1 = (\tau_2, z_2,\sigma_2')$ and 
$\rho_1 \setminus \rho_2 = (\tau_1, z_1, \sigma_1').$ }\\
By Proposition \ref{propinterf}, $(\tau_2, z_2,\sigma_2')$ and 
$(\tau_1, z_1, \sigma_1')$  must be redexes. Thus,
we want to show the following:
$$ {\tt GC}( \overline{M_1 [z_2 \leftarrow r_2^{\sigma_2'}]})
\equiv 
{\tt GC}( \overline{M_2 [z_1 \leftarrow r_1^{\sigma_1'}]})$$

%\noindent
%We prove this by showing that both sides can be reduced to
%$${\tt GC}(\overline{M[z_2 \leftarrow r_2^{\sigma_2}] 
%                      [z_1 \leftarrow r_1^{\sigma_1}]} ) \hspace{1cm}  $$

We have
$$\begin{array}{lll}
& {\tt GC}( \overline{M_2 [z_1 \leftarrow r_1^{\sigma_1'}]}) \\
\equiv  &
{\tt GC} (\overline{
{\tt GC}   (\overline{M[z_2\leftarrow r_2^{\sigma_2}]})
                       [z_1\leftarrow r_1^{\sigma'_1}]})  \\
\equiv &
{\tt GC}(\overline{ 
            \overline{M[z_2\leftarrow r_2^{\sigma_2}]}
                       [z_1\leftarrow r_1^{\sigma_1'}]})  &
\mbox{(by Proposition } \ref{garbage}) \\
\equiv & 
{\tt GC} (\overline{M[z_2 \leftarrow r_2^{\sigma_2}] 
                       [z_1 \leftarrow r_1^{\sigma_1}]})   &
\begin{minipage}[t]{6cm}
(implied by the definition of the descendant of a redex (Definition
\ref{descendantredex}) and of the canonicalization procedure
(Definition \ref{canonical}))
\end{minipage}  \\
\equiv & 
{\tt GC}(\overline{M[z_1 \leftarrow r_1^{\sigma_1}] [ z_2 \leftarrow
r_2^{\sigma_2}]} ) &
\begin{minipage}[t]{6cm}
(by Proposition \ref{repl})
%since $z_1 \neq z_2$, $z_1 \not\in {\tt BV}(r_2^{\sigma_2})$,
%and $z_2 \not\in {\tt BV}(r_1^{\sigma_1})$
\end{minipage} \\
\equiv &
{\tt GC}(\overline{\overline{M[z_1 \leftarrow r_1^{\sigma_1}]}
[ z_2 \leftarrow r_2^{\sigma_2'}]} ) &
\mbox{(Definition } \ref{descendantredex} \mbox{ and } \ref{canonical}) \\
\equiv &
{\tt GC}({\tt GC}(\overline{\overline{M[z_1 \leftarrow r_1^{\sigma_1}]})
[ z_2 \leftarrow r_2^{\sigma_2'}]} )
& \mbox{(by Proposition } \ref{garbage}) \\
\equiv & 
{\tt GC}(\overline{M_1[z_2 \leftarrow r_2^{\sigma_2'}]})
\end{array}$$

\item {$\rho_1 \setminus \rho_2  = (\tau_1, z_1, \sigma_1') 
\mbox{ and } \rho_2  \setminus \rho_1$ does not exist.}\\
We need to show
$$ M_1 \equiv 
 {\tt GC}( \overline{M_2 [z_1 \leftarrow r_1^{\sigma_1'}]}) $$
We have 
$$ \begin{array}{lll}
& {\tt GC}( \overline{M_2 [z_1 \leftarrow r_1^{\sigma_1'}]})  \\
\equiv  & 
{\tt GC}(\overline{M[z_1\leftarrow r_1^{\sigma_1}]
                       [z_2\leftarrow r_2^{\sigma_2}]})  &
\mbox{(following the argument in Case  1)} \\
\equiv & 
{\tt GC}(\overline{\overline{M[z_1\leftarrow r_1^{\sigma_1}]}
                       [z_2\leftarrow r_2^{\sigma_2'}]}) \\
\equiv & 
{\tt GC}({\tt GC}(\overline{M[z_1\leftarrow r_1^{\sigma_1}]}))
& \begin{minipage}[t]{7cm}
(since $z_2$ is not reachable in 
$\overline{M[z_1\leftarrow r_1^{\sigma_1}]}$ )
\end{minipage}  \\
\equiv & {\tt GC}(\overline{M[z_1\leftarrow r_1^{\sigma_1}]})  & \\
\equiv & M_1
\end{array}$$

\item {$\rho_2 \setminus \rho_1  = (\tau_2, z_2, \sigma_2') 
\mbox{ and } \rho_1  \setminus \rho_2$ does not exist.}\\
The same as Case 2.

\item {Both $\rho_2 \setminus \rho_1$
and  $\rho_1  \setminus \rho_2$ do not exist.}\\
If $\rho_1 \setminus \rho_2$ does not exist
then
there must be a path from $z_2$ to $z_1$ in $M$. 
Analogously, if
$\rho_2 \setminus \rho_1$ does not exist
then
there must be a path from $z_1$ to $z_2$ in $M$. 
Therefore, it
must be the case that there exists a cycle involving
$z_1$ and $z_2$. Without loss of generality, let us assume there exists
a path from the root of $M$ to $z_1$ without visiting $z_2$.
This implies that 
independently of the reduction 
of $\rho_2$, $z_1 \in {\tt BV}(M_2)$, that is,
$\rho_1 \setminus \rho_2$ exists in $M_2$. 
We reach a contradiction, therefore, 
this case cannot arise.
\end{mycases}
\end{proof}

\begin{corollary}
\label{diamond}
A GRS$_{\sf NI}$ is confluent up to $\alpha$-equivalence.
\end{corollary}

\blank
\noindent
Consider the following projection rules:
\[ \begin{array}{lll}
\tau_1: \;x={\sf I}(y) & \reduce{}{} & x = y\\
\tau_2: \;x={\sf J}(y) & \reduce{}{} & x = y
\end{array} \]
and the following term $M$:
\[ \{ \begin{array}[t]{l}
       x = {\sf I}(y);\\
       y = {\sf J}(x);\\
       \;\; {\sf In} \; x \}
      \end{array}
\]
then $M$ will have the following reduction:
\[ \begin{diagram}
& & M & & \\
& \SW & & \SE  & \\
%M_1 \equiv \{ \begin{array}[t]{l}
%   x = {\sf I}(x);\\
%    \;\; {\sf In} \; x \}
%   \end{array}
M_1 \equiv \{ 
   x = {\sf I}(x); \; {\sf In} \; x \}
& & & &
%M_2 \equiv \{ \begin{array}[t]{l}
%   x = {\sf J}(x);\\
%    \;\; {\sf In} \; x \}
%   \end{array} \\
M_2 \equiv \{ x = {\sf J}(x); \;
    {\sf In} \; x \} \\
& \SE & & \SW & \\
& & \mbox{{\bf $\odot$}} & & 
\end{diagram}
\]
Notice that if both $M_1$ and $M_2$ are not reduced to {\bf $\odot$},
the confluence property will be lost, as was observed in \cite{Klop91}.
Barendregt's graph reduction system is not confluent precisely
because of the absence of such a reduction. \\


%\begin{corollary}
%\label{completedev}
%In a GRS$_{\sf NI}$
%all complete developments end up with the same normal form
%up to $\alpha$-equivalence.
%\end{corollary}

Hereafter, we will use the notation $GRS_{\sf C}$ to
denote a confluent GRS.
