\documentstyle[10pt]{article}  % -*- Mode:TeX -*-

%\input /home/faculty/ariola/BK/tex/include-file
\input prelude1


\def\psfileprefix{/fs/abp/ariola/CONFLUENCE/PS/}


%                    HERE BEGINS THE DOCUMENT


\begin{document}

\title{Notes\\
on \\
the Confluence Property \\
of\\
Term Rewritings Systems and the $\lambda$-calculus}

\author{{\it Zena M. Ariola}\\
Aiken Computational Laboratory\\
Harvard University 
}

%\date{November 1, 1990}
%\today


\maketitle


In this document we will prove the Church-Rosser theorem
for both Regular\footnote{Researchers have coined the word ``{\em Orthogonal}'' 
for this subclass of TRS's. However, 
in this document we will play conservative and still use the widely
known term ``Regular''.} Term Rewriting Systems (TRS's) and 
the $\lambda$-calculus.\\

We also review some powerful proof methods, which 
require the introduction of basic notions about ordering relations.\\

%In the appendix we introduce more elaborate structures, such as,
%directed sets, complete partial orders and we give a proof
%of the least fixed point theorem.

\newpage

\section{Basic Definitions and Properties}
Throughout the paper we will make use of the following
notation:\\
$\begin{array}{ll}
\reduces{}{}_R & \mbox{reduction relation induced by } R\\
\reduces{}{+} & \mbox{1 or more steps reduction}\\
\reduces{}{n} & n\mbox{ steps reduction}\\
\reduce{}{\rho} & \mbox{reduction of redex }\rho\\
\rho \subseteq M & \mbox{$\rho$ is a subterm of term }M
\end{array}$

\subsection{Ordering Relations}
We first give a number of examples of
ordering relations on a set $X$.
\begin{itemize}
\item[1.]
$X= \{ \{a\},\{b\},\{a,b\}\} \mbox{  and  }
x\;R \; y := x \subseteq y $ 
$$\begin{diagram}
& & \{a,b\} & & \\
& \subseteq & & \subseteq & \\
\{a\} & & & & \{b\}
\end{diagram}$$
\item[2.]
$X = {\cal{P}} (\{ a, b \})=\{\emptyset, \{ a \}, \{ b \}, \{ a,b \} \}
\mbox{   and   }
x\;R \; y := x \subseteq y $
$$\begin{diagram}
& & \{a,b\} & & \\
& \subseteq & & \subseteq & \\
\{a\} & & & & \{b\}\\
& \supseteq & & \supseteq & \\
& & \emptyset & & \\
\end{diagram}$$
\item[3.]
$X= \{ 2,3,4,6,8,12\} \mbox{   and   }
x\;R \; y := x \mbox{ is a divisor of } y$
\illustration{ex1}
\item[4.]
$X= \{ 1,2,3,4,6,8,12, 24\} \mbox{   and   }
x\;R \; y := x \mbox{ is a divisor of } y$
\illustration{ex2}
\item[5.]
$X$= $\cal{Z}$ $\mbox{   and   } x \;R \; y := x \leq y$
\illustration{ex3}
\item[6.]
$X$= $\cal{N}$ $\mbox{   and   } x \;R \; y := x \leq y$
\illustration{ex4}
\item[7.]
$X$= $\cal{N}$ $\times$ $\cal{N}$ $\mbox{   and   }
\langle a,b\rangle R \langle x,y\rangle
:= a \leq x \vee (a=x \wedge b \leq y)$.
$$ \langle 0,0 \rangle ,\;\;
\langle 0,1 \rangle ,\;\;
\langle 0,2 \rangle ,\;\; \cdots \;\;
\langle 1,0 \rangle ,\;\;
\langle 1,1 \rangle ,\;\;
\langle 1,2 \rangle ,\;\; \cdots \;\;
\langle 2,0 \rangle ,\;\; \cdots$$
\end{itemize}

\begin{definition}
Let R be a binary relation on a set $X$. We say
\begin{tightlist}
\item[-]
R is reflexive if $ \forall  x  \in  X \;  [x \; R\; x]$
\item[-]
R is irreflexive if $ \forall  x  \in  X \;  [\neg x \; R\; x]$
\item[-]
R is  antisymmetric if $\forall  x, y  \in X \;[x \; R \; y \;
\wedge \; y \; R \; x \; \Longrightarrow \; x = y ] $
\item[-]
R is  transitive if $\forall  x, y, z \in X \;[x \; R \; y \;
\wedge \; y \; R \; z \; \Longrightarrow \; x \; R \;  z] $
\item[-]
R is trichotomous if $\forall  x, y \in X \;[x \; R \; y \;
\vee \;  y \; R \; x \; \vee \; x = y ] $
\end{tightlist}
\end{definition}

\begin{definition}[Weak Partial Ordering]
A relation R on a set $X$ is a weak partial ordering on $X$ iff
R is reflexive, antisymmetric, and transitive. 
\end{definition}

\noindent
The one satisfying irreflexivity is named {\it strict partial ordering}.
Hereon, if otherwise specified, we will assume that the
partial order is a weak partial order.
It is customary to use the symbol $\sqsubseteq$ for a weak partial order,
and $\sqsubset$ for a strict partial order.
Note that the reason for the qualification {\it partial} is that some questions
about order may be left unanswered.

\noindent
Check that in the Examples $1$ through $7$, $R$ is a
weak partial ordering on $X$.\\

\noindent
Instead of ``$R$ is a partial ordering on $X$'' one sometimes
says that ``$\cal{X}$=$\langle X,R \rangle$ is a partially ordered set''.
In the following, we will not make the distinction between a partially
ordered set and the domain of the partial order, that is, we will use
$\cal{X}$ and $X$ interchangeably.


%\begin{definition}[Partially Ordered Set]
%A partially order set $\cal{X}$ is an ordered pair ($X,\leq$), where
%$X$ is a set and $\leq$ is a partial order in $X$.
%\end{definition}

\begin{definition}[Minimal element]
A minimal element of a partially ordered set ($X,\sqsubseteq$) is a $y$ in
$X$ such that
\[ \not\exists\;  x  \in X \; [x \; \sqsubseteq \; y \; \wedge \; x \neq y]\]
\end{definition}

\begin{definition}[Least element]
The least element of a partially order set ($X,\sqsubseteq$) is a $y$ $\in$
$X$ such that
\[\forall  x  \in X,\; y \; \sqsubseteq \; x \]
\end{definition}

\noindent
Note that the least element, if it exists, is unique, 
and the least element is necessarily a minimal element. But,
conversely, a minimal element is not necessarily a least element.
In Example 1. $\{ a\}$ and $\{b\}$ are minimal elements of $X$, but
$X$ does not have a least element.\\
In Example 2. $\emptyset$ is the least element of $X$ and hence also
a minimal element of $X$.\\
In Example 3. 2 and 3 are minimal elements of $X$, but $X$ does 
not have a least element.\\
In Example 4. 1 is the least element and hence also a minimal
element of $X$.\\
In Example 5. $X$ has not minimal elements and hence no least
element either.\\

\noindent
{\bf Maximal element} of $X$ and the {\bf greatest element}
of $X$ are defined analogously. 

\begin{definition}[Upper Bound]
Let the set $X$ be partially ordered by $\sqsubseteq$,
$z$ is the upper bound of a subset $S$ of $X$ 
($S \sqsubseteq z$) iff 
$\forall x \in S\;\; [x \sqsubseteq z] $
\end{definition}

\begin{definition}[Least Upper Bound (Lub)]
Let the set $X$ be partially ordered by $\sqsubseteq$,
$z$ is the least upper bound of a subset $S$ of $X$ (denoted as $\bigsqcup S$)
iff:
\begin{enumerate}
\item
$S \sqsubseteq z$ ($z$ is an upper bound);
\item
$\forall x \in X$, $S \sqsubseteq x \Longrightarrow z \sqsubseteq x$. 
\end{enumerate}
\end{definition}

\noindent
Note that a subset $S$ of a partially ordered set $X$ can have at most
one least upper bound (by antisymmetry). Hence, in case that $S$ has
a greatest element, then this is clearly the least upper bound (lub).
However, the lub for $S$ does not need to belong to $S$
and thus does not need to be the greatest element of $S$.

\noindent
In Example 3. the set $\{8,12\}$ does not
have an upper bound, so no lub. The set
$\{ 4,6\}$ has two upper bounds, 8 and 12, respectively, but no lub.
12 is the lub of $\{ 2,3,6,4,12 \}$.\\

\noindent
{\bf Lower bound} and {\bf greatest lower bound} are defined 
analogously. 

\begin{definition}[Weak Linear Ordering]
A relation R is a weak linear (total) ordering on $X$ iff
R is a weak partial ordering and R is trichotomous.
\end{definition}

\noindent
Analogously, we can define a {\it strict linear ordering}.
A linear order is frequently called a {\it chain}.
Examples 5.,6. and 7. are weak linear orders.

\begin{definition}[Weak Well-ordering]
A relation $R$ on a set $X$ is a weak well-ordering on $X$ iff
\begin{tightlist}
\item[i)] $R$ is a weak linear ordering;
\item[ii)] iff each non-empty subset has a least element.
\end{tightlist}
\end{definition}

\noindent
The definition of a {\it strict well-ordering} implies that
$R$ is irreflexive.
The relation $R$ as defined in Example 6. is a weak well-ordering, while
$R$ in Example 5. is not, because $X$ has no least element.\\
As an exercise you can show that $\cal{N}$
is weakly well-ordered by $\leq$.
On the other hand, ($\cal{Z},\leq$) is not
a weakly well-ordered set.\\

\noindent
{\bf Remark}: One consequence of the above definition is that every well-ordered
set $X$ is totally ordered. Let $x,y  \in  X$, then $\{x,y\}$ is
a non-empty subset of $X$ and has therefore a least element.
If the least element is $x$, then $x \; \sqsubseteq \; y$,
otherwise, $y \; \sqsubseteq \; x$. \\

\noindent
We are interested in strict well-ordered sets because 
we can prove properties of their elements using a process
similar to {\bf mathematical induction}.

\begin{definition}[Initial segment]
Let X be a partially ordered set, if x  $\in$  X, then
\[ \{ y  \in  X \mid  y \; \sqsubset \; x\} \]
is called the
initial segment of x; we shall denote it by s(x). 
\end{definition}

\noindent
Note that in the above definition we used the symbol $\sqsubset$ and
not $\sqsubseteq$. For this reason the above is usually called the {\it strict}
initial segment of $x$.

\begin{theorem}[Transfinite induction]
Given a subset $S$ of a strict well-ordered set $X$, then
\[ [\forall x  \in  X,\; s(x)  \subseteq  S \; \Longrightarrow \;
x \in  S] \;\; \Longrightarrow \;\;
S = X \]
\end{theorem}
\begin{proof}
Suppose that $S \neq X$.
Since $X$ is well-ordered then
$(X \setminus S)$ has a least element, say $x_0$.
Thus, $x_0 \not\in S \;  \wedge \; s(x_0) \subseteq S$.
Since $s(x_0) \subseteq S$, it follows from
the hypothesis that $x_0$ $\in$ $S$. 
We reached a contradiction. Therefore, $S=X$.
\end{proof}\\

\noindent
Notice that in the above we didn't make any assumption about a starting
element.
This is so because all the minimal elements of $X$ are included in $S$ by
definition. If $x$ is the minimal element of $X$, then
$s(x)$ is empty, and since $s(x)  \subseteq  S$ then $x  \in  S$. \\


If the set $X$ is the set of terms defined over a given
signature, it is interesting to think under which
conditions the reduction relation $\reduces{}{}$
defines a partial ordering on $X$.
We can think of the reduction relation as 
establishing an ordering between terms.
For example, you can read $x  \reduces{}{n}  y$,
with $n \geq 1$,
as saying $y \sqsubset x$.
By definition $\sqsubset$ is irreflexive and transitive,
but, in general it is not antisymmetric, in fact, 
we can have terms $M$ and $N$, such that
$$(M \reduces{}{} N)  \; \wedge \; 
(N \reduces{}{} M)  \; \wedge \;  (M \neq N). $$
However, if $\reduces{}{}$ is strongly normalizable then it is
easy to verify that $\sqsubset$ does satisfy the antisymmetric
property, because it will never happen that
$(M \reduces{}{} N)  \; \wedge \; (N \reduces{}{} M)$.
Moreover, the strong normalization property guarantees that
each non-empty subset of $X$ has a minimal element.

\begin{definition}[Minimum condition]
A partially ordered set $X$ satisfies  the minimum condition if
each non-empty subset of $X$ has a minimal element.
\end{definition}

\begin{definition}[Noetherian Relation]
\label{minimum}
Given a TRS $(X,R)$, $R$ is said to be noetherian if $\langle X,R\rangle$
satisfies the minimum condition.
\end{definition}

Before introducing the {\it noetherian principle} we introduce
a new definition, which says that
a predicate is complete if it holds for an arbitrary
element $x$ of $X$ whenever it holds for all elements
less than $x$.

\begin{definition}[Complete]
Let P be a predicate defined on a partially order set $X$. We say that P is
complete iff 
\[ \forall  x  \in X, \; \; (\forall y  \sqsubset x
\;\; P(y)) \;\;
\Longrightarrow \;\; P(x) 
\]
\end{definition} 

\noindent

\begin{theorem}[Noetherian Induction]
Given TRS $(X,R)$, if $R$ is noetherian and P is a complete predicate then 
\[ \forall  x  \in X, \; \;  P(x) \]
\end{theorem}
\begin{proof}
Suppose, by contradiction, that P does not hold in each element of
$X$, therefore, the set $S$ of all elements
which do not satisfy P is non-empty. Since
$R$ is noetherian from its definition we have: 
\[ \exists  m \in S \mbox{ such that } \forall
 z \in S, \; m \sqsubset z \]
This means that $s(m) \cap S \neq \emptyset$ (otherwise $m$ would not be
a minimal element). We then have 
\[ s(m) \not\subseteq  S \; \wedge \; m \in S \]
This contradicts the hypothesis that P is a complete predicate.
Therefore, $S$ is the empty set.
\end{proof}\\

%
%\noindent
%We now state the following theorem without proof.
%
%\begin{theorem}[Noetherian induction]
%Given S, a subset of a partially ordered set X with minimum condition, 
%\[ [\forall \; x  \in  X,\;\; s(x) \; \subseteq \; S \; \Longrightarrow \;
%x  \in  S] \;\; \Longrightarrow \;\;
%S = X \]
%\end{theorem}


At this point the reader may feel confused about the difference
among the various kinds of {\it induction principles} he may have come
across. In the following, we will try to throw some light on these
differences, if any. We will consider mathematical induction,
structural induction and transfinite induction.
Let's first say that noetherian induction is the general version
of structural induction. Structural induction, as the name may recall,
consists in reasoning on the structure of a term or formula. For example,
most of the proofs in propositional logic, go like this:
$$ \mbox{suppose } \phi \mbox{ and } \psi \mbox{ are true, then prove that }
\phi \; \wedge \; \psi \mbox{ is true} $$
We clearly have a partial ordered set
(\ie $ \phi \sqsubset (\phi \; \wedge \; \psi)$ \mbox{ and } 
$ \psi \sqsubset (\phi \; \wedge \; \psi)$),
which satisfy the minimum condition, where the minimal elements
are the atomic terms or formulae.\\
The main difference between structural induction and both mathematical
induction and transfinite induction, is that the first is defined on
partially ordered sets, where each chain has a least element,
while both mathematical induction and transfinite induction require that
an arbitrary subset of $X$ has a least element.
Moreover, structural induction, like transfinite induction,
passes to each element from the set of its
predecessors, and, as said before,
does not make any assumption about a starting element.\\

%\subsection{Application of Noetherian Induction}
%It is left to the
%reader to check that the relation ``$\leq$'' is a partial
%order.
%We would like to have a tool that allows us to reason about
%terms. In order to do that we have to require that
%the reduction relation be SN, otherwise, we
%would not have the minimun element property.\\

An an application of noetherian induction we give the proof
of the following lemma.

\begin{lemma}[Newman's Lemma]
SN $\wedge$  WRC $\Longrightarrow$ CR .
\end{lemma}
\begin{proof}
Since the reduction relation is SN then all we have to show
is that the following predicate $P(x)$ is complete
\[ P(x): \;\;  \forall y,  z, \; [x  \reduces{}{}  y \;\; \wedge \;\;
x  \reduces{}{}  z \;\; \Longrightarrow \;\;
\exists \; s \; \mbox{such that } y  \reduces{}{}  s \;\;
\wedge \;\; z  \reduces{}{} s ] \]
Without loss of generality assume that 
\[x  \reduce{}{}  y_1  \reduces{}{}  y
\;\; \wedge \;\; x  \reduce{}{}  z_1  \reduces{}{} z \]
By WCR:
\[ \exists \; u, \; y_1 \; \reduces{}{} \; u \;\; \wedge \;\;
z_1 \; \reduces{}{} \; u\]
By induction hypothesis P holds in $y_1$ (since $y_1
\sqsubset x$),
\[ \exists \; v, \; y \; \reduces{}{} \; v \;\; \wedge
\;\; u \; \reduces{}{} \; v \]
By induction hypothesis P holds in $z_1$ (since $z_1
\sqsubset x$),
\[ \exists \; s,\;\; v \; \reduces{}{} s \;\;
\wedge \;\; z \; \reduces{}{} \; s  \]
Thus proving P($x$). See the diagram below: 

$$\begin{diagram}
x & \rTo & z_1 & \rTo & z \\
\dTo & WCR & \dOnto & & \dOnto \\ 
y_1 & \reduces{}{} & u & HP &  \\
\dOnto & HP & \dOnto &  & \\
y & \reduces{}{} & v & \reduces{}{} & t \\
\end{diagram}$$
 
\end{proof}

\subsection{Reduction Properties}
Hereon we will not make the distinction between a set of rules $R$ and
the induced reduction relation $\reduce{}{}_R$.
 
\begin{definition}[Diamond Property]
Let R be a reduction relation on a set X. Then R has the diamond
property (notation R $\models$ $\diamond$ ) if 
\[
\forall \; t, \; t_1,  \; t_2  \in X \; [ t \reduce{}{} t_1 \; 
\wedge \;  t \reduce{}{} t_2 \;\; \Longrightarrow \;\; \exists \; t_3  \;
[t_1 \reduce{}{} t_3 \; \wedge \; t_2 \reduce{}{} t_3 \; ]]
\]
\end{definition}
See diagram below:\\
$$\begin{diagram}
    &     & t   &     &      \\
    & \SW &     & \SE &      \\
t_1 &     &     &     & t_2  \\
    & \SE &     & \SW &      \\
    &     & t_3 &     &      \\
\end{diagram}$$

\noindent
\begin{fact}
\label{lemma1}
R $\models$ $\diamond$ $\;\; \Longrightarrow \;\; $
R$^*$ $\models$ $\diamond$.
\end{fact}

\begin{fact}
\label{lemma2}
R $\models$ $\diamond$ $\;\; \Longrightarrow \;\; $
R $\models$ CR.
\end{fact}

\begin{definition}[Underlining]
Let R be a reduction relation in X,
define \underline{R} and \underline{X} as follows
\begin{tightlist}
\item[-] \underline{R} is the reduction relation
in \underline{X},
obtained by
underlining all the leftmost function symbols in the
left-hand-side of the reduction rules in R.
\item[-] \underline{X} is the set containing all terms in X, plus
terms with some function symbols underlined.
\end{tightlist}
\end{definition}

\noindent
There are operations that allow us to go from the structure (X,R) to
(\underline{X},\underline{R}) and vice-versa.
One can convert a term $t$ in X to
$t'$ in \underline{X} by possibly underlining some function symbols
({\it lifting}).
Conversely, a term $t'$ in \underline{X} can be converted to $t$ in X
by erasing all underlnings ( \ie $t = \mid t' \mid$) .\\
More formally:

\begin{lemma}
\hfill \linebreak
\begin{itemize}
\item[(i)]
$$\begin{diagram}
t'               & \rDashto & t_1'                 & \hspace{1.5cm} t',t_1' \in \underline{X} \\
\dTo^{\mid \mid} &          & \dDashto_{\mid \mid} &            \\
t                & \reduces{}{}   & t_1                  &  \hspace{1.5cm} t,t_1 \in X \\
\end{diagram}$$

\item[(i)]
$$\begin{diagram}
t'               & \reduces{}{}   & t_1'             & \hspace{1.5cm} t',t_1' \in \underline{X}  \\
\dTo^{\mid \mid} &          & \dTo_{\mid \mid} &            \\
t                & \rDashto & t_1              & \hspace{1.5cm} t,t_1 \in X \\
\end{diagram}$$
\end{itemize}
\end{lemma}

%\begin{definition}[Finite Development] Given a term
%$t_1 \in R$, if $t'_1 \in \underline{R}$ is
%a term obtained by underlining some of its function symbols, and there is a reduction
%sequence $\sigma: \; t'_1 \rightarrow t'_2 \rightarrow \ldots \rightarrow t'_n$ in
%\underline{R}, and further,  $t_n = \mid t_n' \mid$ 
%the $\sigma$ is called a finite development of
%the  $t_1 \in R$.
%\end{definition}

\begin{definition}[Development with respect to $\cal{F}$]
Given a term $t \in X$,
and $\cal{F}$ a set of redex occurrences in $t$,
let $t' \in \underline{X}$ be
the term obtained by underlining
the redexes in $\cal{F}$,
then the reduction sequence $\sigma:
\; t' \rightarrow t'_1 \rightarrow \ldots \rightarrow t'_n$
in \underline{R}
is called a development of
$t$ with respect to $\cal{F}$ . 
A development of a term $t$ is a development of $t$ with respect to
the set of all redex occurrences in $t$.
\end{definition}

\noindent
Informally, the previous definition says that a {\it development}
of a term $t$ is a reduction in which only ``old'' redexes (\ie,
redexes already present in $t$), are rewritten.


\begin{definition}[Complete Development with respect to $\cal{F}$]
Given a term $t \in X$,
and $\cal{F}$ a set of redex occurrences in $t$,
let $t' \in \underline{X}$ be
the term obtained by underlining
the redexes in $\cal{F}$,
then the reduction sequence $\sigma:
\; t' \rightarrow t'_1 \rightarrow \ldots \rightarrow t'_n$  in \underline{R}
is called a complete development of
$t$ with respect to $\cal{F}$, if $t'_n$ does not contain any
more underlines.
A complete development of a term $t$ is a complete development of $t$
with respect to set of all redex occurrences in $t$.
\end{definition}


%The notions of developments and complete developments
%are very important because as we will see, they will allow us to
%prove confluence for both Regular TRS's and the $\lambda$-calculus.

\section{Confluence for Regular TRS's} 
The proof of CR for Regular TRS's follows the steps below:
\begin{enumerate}
\item[(i)]
R Regular $\Longrightarrow$ \underline{R} is Regular (lemma \ref{regular})
\item[(ii)] 
\underline{R} $\models$ WCR ( lemma \ref{regular} and lemma \ref{wcr})
\item[(iii)]
\underline{R} $\models$ SN (lemma \ref{sntrs})
\item[(iv)]
(ii $\wedge$ iii) $\Longrightarrow$ \underline{R} $\models$ CR (by Newman's lemma)
\item[(v)]
R $\models$ CR (because R$^*$ = \underline{R}$^*$)
\end{enumerate}

\noindent
The main point to grasp here is that in order to show that a reduction
relation $R$ is CR, we define a new reduction relation \underline{$R$},
for which it's easier to show that is CR.
We reduce the problem to something more tractable, and the translation
between the two different problems is given by showing that the two
reduction relations have the same transitive closure.
Therefore, once proved that  \underline{R} is CR, it follows that $R$
is also CR.
 
\begin{lemma}
\label{regular}
R Regular $\Longrightarrow$ \underline{R} Regular.
\end{lemma}
\begin{proof}
Left to the reader.
\end{proof}

\begin{fact}
Given a Regular TRS (X,R), 
$\forall  t \in X, \; t  \reduce{}{\rho_1}  t_1 \; \wedge \;
t  \reduce{}{\rho_2}  t_2$ 
then the $(\rho_1) \; \rho_2$-reduction does not modify the $(\rho_2)$
$\rho_1$-redex.
\end{fact}

\noindent
At first look it seems that the above is only due to non-overlapping
patterns. Instead also non-left linearity can cause problems.
As an example, given the rules
\[ \begin{array}{l}
{\sf D }\;  x\; x  \;\; \reduce{}{} \;\; x \\
{\sf I} \; x \; \; \reduce{}{} \;\; x
\end{array} \]
consider the term
\[ 
\underbrace{{\sf D }\; \underbrace{({\sf I} \; x)}_{\rho_1} \;({\sf I} \; x)}_{\rho_2} 
\]
the $\rho_1$-reduction modify the $\rho_2$-redex. 

\begin{lemma}
\label{wcr}
Given a  Regular TRS (X,R), R is WCR.
\end{lemma}
\begin{proof}
We want to show the following:
\[ \forall  t \in  X, \; t \; \reduce{}{\rho_1} \; t_1 \;\;
t \; \reduce{}{\rho_2} \; t_2 \;\; \Longrightarrow \;\; 
\exists \; t_3, \; 
t_1 \; \reduces{}{} \; t_3  \;\;\; \mbox{ and }
t_1 \; \reduces{}{} \; t_3  \]
\noindent
We  do the proof by case analysis.
 
\begin{mycases}
\item {\bf Redexes $\rho_1$ and $\rho_2$ are disjoint} \\
%The $\rho_1$-reduction does not disturb the $\rho_2$.
Trivial. See diagram below:
$$\begin{diagram}
    &              & t   &             &      \\
    & \SW^{\rho_1} &     & \SE^{\rho_2} &      \\
t_1 &              &     &             & t_2  \\
    & \SE^{\rho_2}  &     & \SW^{\rho_1} &      \\
    &              & t_3 &             &      \\
\end{diagram}$$
\item  Without loss of generality assume that {\bf $\rho_1$ is nested inside
$\rho_2$ } \\
Since R is regular, by the previous fact, only two cases are possible
\begin{itemize}
\item[(2.1)]
$\rho_2$-reduction destroys the $\rho_1$-redex;
\item[(2.2)]
$\rho_2$-reduction duplicates the $\rho_1$-redex;
\end{itemize}

\noindent
We consider the two cases above separately.

\begin{mysubcases}
\item  {\bf $\rho_2$-reduction destroys the $\rho_1$-redex } \\
This means that $\rho_2$ occurrs in $t_1$ ($\rho_2 \subseteq  t_1)$.
Suppose by contradiction that the above is not true, \ie
the $\rho_1$-reduction must have erased $\rho_2$. The only
way this could have happened is if $\rho_2$ $\subseteq$ $\rho_1$.
In conclusion:
\[ \rho_1  \subseteq   \rho_2 \;\;
\wedge \;\;
 \rho_2  \subseteq   \rho_1 \;\;
\Longrightarrow \;\; 
\rho_1 \;\; = \;\; \rho_2
\]
We reached a contradiction, since R is not  ambiguous. \\

Therefore,
$$\begin{diagram}
t             & \rTo^{\rho_2}  & t_2 \equiv t_3 \\
\dTo^{\rho_1} & \NE_{\rho_2}   &                 \\
t_1           &               &                 \\  
\end{diagram}$$

\item {\bf $\rho_2$-reduction duplicates $\rho_1$ }\\
For the same reasons as before $\rho_2  \subseteq  t_1$, therefore\\
$$\begin{diagram}
t             & \rTo^{\rho_2}  & t_2           \\
\dTo^{\rho_1} &               & \dTo^{\rho_1}  \\
              &               & \vdots         \\
              &               & \dTo^{\rho_1}   \\
t_1           & \rTo^{\rho_2}  &  t_3            \\
\end{diagram}$$

\end{mysubcases}
\end{mycases}
\end{proof}


\begin{lemma}
\label{sntrs}
For any TRS (X,R), \underline{R} is SN.
\end{lemma}
\begin{proof}
The proof strategy is similar to the one given in the next section.
\end{proof}

%\blank
%\noindent
%With these lemmas and definitions in our pocket, we can now state and
%prove the main theorem of this discussion.

\begin{theorem} Given a Regular TRS (X,R), R is CR.
\end{theorem}
\begin{proof}
%From lemma2 and lemma1 we can conclude that
%\underline{R} is WCR. But then from lemma5 and lemma1 we conclude
%that \underline{R} is CR.
%And since $R$ and $\underline{R}$ have the same transitive closure we conclude that
%$R$ is CR.
Left to the reader.
\end{proof}\\



\section{ The $\lambda$-calculus}
\label{lambdac}

Hereon $\Lambda$ indicates the set of $\lambda$-terms, and
$\beta$ indicates a reduction relation on $\Lambda$.\\

\begin{fact}
$\beta$ $\not\models$ $\diamond$.
\end{fact}

\noindent

For an example, consider:
$$\begin{diagram}
(_{\rho}\; (\lambda\; x.x \; x)(_{\tau} \; I I)) & \rTo^{\rho} &
(_{\tau_0} \; II)\;(_{\tau_1}\; II) \\
\dTo^{\tau}                                        &               &
\dTo^{\tau_0}  \\
                                                    &               &
I \; (_{\tau_1}\; II ) \\
                                                    &               &
\dTo^{\tau_1}   \\
(_{\rho} \; (\lambda\; x.x \; x)\; I              & \rTo^{\rho} & 
II           \\
\end{diagram}$$
\noindent
In the above example the reduction of redex $\rho$
duplicates the redex $\tau$,
the two copies are named $\tau_0$ and $\tau_1$ respectively.
For this reason the $\lambda$-calculus has the so called
{\em duplicative} property. This 
raises many issues regarding efficient implementations.\\ 

\noindent
Proof strategy of CR for $\lambda$-calculus:
\begin{enumerate}
\item[(i)]
Define a new type of reduction relation, $\reduce{1}{}$
\item[(ii)]
$\reduce{1}{}$ $\models$ $\diamond$
\item[(iii)]
$\beta^*$ = $\reduces{1}{}$.
\end{enumerate}

\subsection{Marked $\lambda$-calculus ( $\Lambda\prime$) }
In order to formalize the ideas of development and
complete development, we introduce the new calculus
$\Lambda\prime$. The $\Lambda\prime$ terms are given by the following production:
\[
E = x \mid \lambda\; x.E \mid E \; E \mid
(\underline{\lambda} \; x.E) \; E
\]

\noindent
The rules of $\Lambda^\prime$ are:
\[ \begin{array}{l}
\beta_0 : \;\;\;  (\underline{\lambda} \; x.M) \; N \reduce{}{}
M\; [N/x] \\
\beta : \;\;\;  (\lambda \; x.M) \; N \reduce{}{}
M\; [N/x]
\end{array} \]

\noindent
Notice that we do not underline arbitrary $\lambda$'s, only the ones
that constitute the operator part of a redex.
Thus, given the well-know term
$(\lambda \; x. x \; x) \; (\lambda \; x. x \; x) $,   
you can certainly underline the first $\lambda$, obtaining
$(\underline{\lambda} \; x. x \; x) \; (\lambda \; x. x \; x) $.
However, you should convince yourself that
$(\lambda \; x. x \; x) \; (\underline{\lambda} \; x. x \; x) $
is not a term in $\Lambda^\prime$. \\

\begin{definition}[Development with respect to $\cal{F}$]
Let M $\in$ $\Lambda$ and $\cal{F}$ a set of redex occurrences in M,
then $\sigma$ is a development of M relative to $\cal{F}$
iff the lifted reduction $\sigma$', starting with \underline{M},
is a $\beta_0$-reduction, where \underline{M} is M
with all the redexes in $\cal{F}$ underlined,
\end{definition}


\begin{definition}[Complete Development with respect to $\cal{F}$]
Let M $\in$ $\Lambda$ and $\cal{F}$ a set of redex occurrences in M,
then $\sigma \; :
M \reduces{}{} M_1$
is a complete development of M relative to $\cal{F}$
iff the lifted reduction $\sigma':  \underline{M} \reduces{}{} \underline{M_1}$ 
is a $\beta_0$-reduction and \underline{$M_1$} is a normal form
with respect to $\beta_0$.
\end{definition}

\noindent
As an example, consider:
$$\begin{diagram}
(_{\rho}\; (\underline{\lambda}\; x.x \; x)(_{\tau} \; \underline{I} (I \;a))) & \rTo^{\rho} &
(_{\tau} \; \underline{I}\; (I \;a))\;(_{\tau}\; \underline{I}\;(I\;a)) \\
\dTo^{\tau} &               & \dTo^{\tau}  \\
              &               &  (I\;a) \; (_{\tau}\; \underline{I} \;(I\;a) ) \\
              &               & \dTo^{\tau}   \\
(_{\rho} \; (\underline{\lambda}\; x.x \; x)\; (I \; a) 
           & \rTo^{\rho}  &   (I\;a)\;(I\;a)           \\
\end{diagram}$$

\subsection{Confluence for $\lambda$-calculus}

\begin{definition}[Variable Convention]
Given a $\lambda$-term $M$ then all bound variables
of $M$ are supposed to be different from the free variables.
\end{definition}

From now on we will always assume that all terms satisfy the
variable convention.

\begin{lemma}[Substitution lemma]
If $x \not\equiv y$ and $x \not\in$ FV(L), then
\[ M \;[N/x][L/y] \equiv M \;[L/y][N\;[L/y]/x] \] 
\end{lemma}
\begin{proof}[By structural induction]
\begin{mycases}
\item {\bf M is a variable}
\begin{mysubcases}
\item {\bf M $\equiv$ x}\\
Perform the substitution in both sides and you obtain
\[ N\;[L/y] \equiv N\;[L/y] \]
\item {\bf M $\equiv$ y}\\
Perform the substitution in both sides and you obtain
\[ L \equiv L \;[N\;[L/y]/x] \equiv L\;\;\;x \not\in FV(L) \]
\item {\bf M $\equiv$ z $\not\equiv x,y$}\\
In both sides we obtain z
\end{mysubcases}
\item {\bf M $\equiv M_1 \;  M_2$} \\
Follows directly from induction hypothesis
\item {\bf M $\equiv \lambda \; z.M_1$} \\
By the variable convention we may assume $z \not\equiv x,y$ and
$z \not\in FV(N) \cup FV(L)$.
$$\begin{array}{llll}
(\lambda \; z.M_1)\;[N/x][L/y] & \equiv & \lambda \; z.(M_1\;[N/x][L/y]) &
\mbox{ by definition of substitution}  \\ 
& \equiv  & \lambda \; z.(M_1\;[L/y][N\;[L/y]/x]]) & \mbox{ by induction hypothesis} \\
&  \equiv & (\lambda \; z.M_1)\;[L/y][N\;[L/y]/x]] & \mbox{ by definition of substitution}
\end{array}$$
\end{mycases}
\end{proof}


\begin{lemma}
\label{wcr1}
$\beta_0$ $\models$ WCR.
\end{lemma}
\begin{proof}
\noindent
Let $\rho_1$ and $\rho_2$ be the two redexes contracted, we will do
the proof by case analysis on the relative position of
$\rho_1$ and $\rho_2$.
\begin{mycases}
\item {\bf $\rho_1$ and $\rho_2$ are disjoint}\\
Trivial
\item  Without loss of generality assume that {\bf $\rho_1$ $\subseteq$  
$\rho_2$ } \\
Assume that $\rho_1  \equiv  (\underline{\lambda}\;y.P) \; Q$ 
and $\rho_2  \equiv  (\underline{\lambda}\;x.M) \; N$.
\begin{mysubcases}
\item {\bf $\rho_1$ $\subseteq$ M}.\\ 
Follows from Substitution lemma.
\item {\bf $\rho_1$ $\subseteq$ N}.\
$$\begin{diagram}
(_{\rho_2}\; (\underline{\lambda}\; x. \cdots x \cdots  x)(
 \cdots (_{\rho_1} \; (\underline{\lambda}\; y. P )Q) \cdots )
& \rTo^{\rho_2} &
\cdots (_{\rho_1} \; (\underline{\lambda}\; y. P )\;Q) \cdots 
(_{\rho_1} \; (\underline{\lambda}\; y. P)\; Q) \cdots \\
\dTo^{\rho_1} &               & \dTo^{\rho_1}  \\
& & \vdots \\
&               & \dTo^{\rho_1}   \\
(_{\rho_2}\; (\underline{\lambda}\; x. \cdots x \cdots  x) ( \cdots P\;[Q/y] \cdots) )
           & \rTo^{\rho_2}  &   
\cdots P\;[Q/y]  \cdots P\;[Q/y]  \cdots \\
\end{diagram}$$
\end{mysubcases}
\end{mycases}
\end{proof}

We are going to show next that $\beta_0$ is SN.
The main technique to prove that a reduction relation in a set $X$ is SN,
is to show that the reduction relation {\em well-orders}
$X$, that is, each chain in $X$ has a minimal element. 
Thus we proceed as follows:
\begin{tightlist}
\item 
Assign a {\em weight} to each $M \in \Lambda^\prime$,
call the term so obtained  $\mid M \mid$
\item
show:
$$M \reduce{}{} N \; \Longrightarrow \; \mid N\mid \;< \; \mid M \mid$$
that is, the ``weight'' of a term is decreasing as we reduce it.
\end{tightlist}


\begin{definition}[Weighting]
Given M in $\Lambda$, associate a positive integer to each variable
occurrence in M.
\end{definition}

\noindent
We thus obtain a new calculus, $\Lambda^*$, that has the usual
inductive definition with the variables ranging over 
$x^0 \cdots x^n$. The definition of reduction on $\Lambda^*$ ($\beta_0^*$)
carries over in the usual way.


\begin{definition}[Weight]
Let M in $\Lambda^*$, define $\mid M \mid$
as the sum of the weights occurring in M. 
\end{definition}


\begin{definition}[Decreasing Weighting Property]
\hfill \linebreak
Let M in $\Lambda^*$, then M has decreasing weight property (dwp) if
for every $\beta_0^*$-redex $(\underline{\lambda} x.P)Q$ in M :
\[ \forall x \in P, \;  \mid x \mid \; > \; \mid Q \mid  \]
\end{definition}

\noindent
Example: $(\underline{\lambda}x.x^6x^7)(\underline{\lambda}x.x^2x^3)$
has the {\it dwp}, while
$(\underline{\lambda}x.x^4x^7)(\underline{\lambda}x.x^2x^3)$ does not.

\begin{lemma}
For all M in $\Lambda^*$, there exists an initial weight assignment
so that M has decreasing weight property.
\end{lemma}
\begin{proof}
Start enumerating all variables occurrences in $M$ from right to left,
and assign to the $m^{th}$ variable occurrence the
weight $2^m$. Since
$$ 2^m \; > \; 2^{m-1} + 2^{m-2} + \cdots 2 + 1 $$
$M$ has the {\it dwp}.
\end{proof}

\begin{lemma}
If $M \reduce{}{} N$, and M has dwp then
\[ \mid N \mid \;  < \; \mid M \mid \] 
\end{lemma}
\begin{proof}
Let $M$ be $\cdots (\underline{\lambda}x.P)Q \cdots$
\begin{mycases}
\item {\bf $x \not\in P$}\\
Then $Q$ vanishes
\item {\bf $x \in P$}\\
The weight must decrease because the weight of the substituted
expression, \ie $\mid Q \mid$, is less than every $x$.
\end{mycases}
\end{proof}

\begin{lemma}
Let $M \reduce{}{} N$, then if M has dwp so does N.
\end{lemma}
\begin{proof}
Suppose $M \reduce{}{R_0} N$, where $R_0 \equiv
(\underline{\lambda}x.P_0)Q_0$.
Examine the effect of $R_0$-reduction on some other redex $R_1 \equiv
(\underline{\lambda}y.P_1)Q_1$ in M.
We will do the analysis on the relative positions of $R_0$ and $R_1$.
\begin{mycases}
\item {\bf $R_0 \cap R_1 = \emptyset$}\\
$R_0$-reduction does not affect $R_1$
\item {\bf $R_1 \subseteq R_0$} 
\begin{mysubcases}
\item {\bf $R_1$ is inside the rator $\underline{\lambda}x.P_0$}
$$R_0 \equiv  (\underline{\lambda}x. \cdots ((\underline{\lambda}y.P_1)Q_1)\cdots)Q_0.$$ 
By the dwp of M,
$$ \forall  y \in P_1, \; \mid y \mid \; > \; \mid Q_1 \mid $$
and, by the fact that $y \not\in$ FV($Q_0$),
$$ \forall  y \in P_1\;[Q_0/x], \; \mid y \mid \; > \; \mid Q_1 \mid $$
And, 
$$\forall  x \in R_0, \; \mid x \mid \; > \; \mid Q_0 \mid $$
then
$$ \mid Q_1 \mid \; > \; \mid Q_1 \; [Q_0/x] \mid$$
In conclusion,
$$\forall  y \in P_1\;[Q_0/x], \; \mid y \mid \; > \; \mid Q_1\;[Q_0/x]\mid $$
\item {\bf $R_1$ is inside the rand $Q_0$} 
$$R_0 \equiv (\underline{\lambda}x.P_0)(\cdots R_1 \cdots) $$
$R_0$-reduction does not modify $R_1$ (may just copy it or destroy it)
\end{mysubcases}
\item {\bf $R_0 \subseteq R_1$} 
\begin{mysubcases}
\item {\bf $R_0 \mbox{ is inside the rator of } R_1$}
$$ R_1 \equiv ( \underline{\lambda} y. \cdots ((\underline{\lambda}x.P_0)Q_0)\cdots)Q_1$$
The weights of any $y$'s in $R_1$ are not affected by $R_0$-reduction.
\item {\bf $R_0 \mbox{ is inside the rand of } R_1$}
$$ R_1 \equiv ( \underline{\lambda} y. P_1)( \cdots ((\underline{\lambda}x.P_0)Q_0)\cdots)$$
The weight  of $Q_1$ after $R_0$-reduction decreases.
\end{mysubcases}
\end{mycases}
\end{proof}

\noindent
From the previous lemma we can infer,
\begin{lemma}
\label{sn}
$\beta_0$ $\models$ SN.
\end{lemma}


\begin{corollary}
\label{cr}
$\beta_0$ $\models$ CR.
\end{corollary}
\begin{proof}
By Newman's lemma, since $\beta_0$ is WCR and SN.
\end{proof}

\begin{theorem}[Finite Development]
\label{finitedev}
Let M $\in$ $\Lambda$ and $\cal{F}$ $\subseteq$ M
\begin{itemize}
\item[(i)]
All developments of M related to $\cal{F}$ are finite;
\item[(ii)]
All complete developments of M related to $\cal{F}$ 
end up with the same term.
\end{itemize}
\end{theorem}
\begin{proof}\\
(i) follows from lemma  \ref{sn}\\
(ii) follows from corollary  \ref{cr}
\end{proof}

\blank
\noindent
We can now define the new reduction relation,

\begin{definition}[Parallel reduction]
M $\reduce{1}{}$ N, iff N is the result of a complete
development of M with respect to some $\cal{F}$.
\end{definition}

\noindent
Notice that one step of the parallel reduction consists in
reducing multiple redexes.\\
Exercise:\\
Let M $\equiv (\lambda \; x. x \; x) ( I \; I)$. Then
it is a good exercise to see what M parallel reduces to.
In particular, does M $\reduces{1}{}  I\;(I\;I)$ ?. 


\begin{theorem}
\label{diam}
$\reduce{1}{} \;\models\; \diamond$.
\end{theorem}
\begin{proof}
$$\begin{diagram}
t   & & \rTo^{{\cal{F}}_2} & t_2  &  \\
\dTo^{{\cal{F}}_1} &   \SE^{\small{{\cal{F}}_1 \cup {\cal{F}}_2}} & & \dDashto_{{\cal{F}}'_1} &  \\
t_1     &  & \rDashto_{{\cal{F}}'_2}  & t_3     &  \\
\end{diagram}$$
Follows from the finite development (theorem \ref{finitedev})
that $\exists$ a complete development of $t$
with respect to ${\cal F}_1 \cup {\cal F}_2$:
$t \reduce{1}{} t_1 \reduce{1}{} t_3'$. 
Analogously, we have the complete development with respect to
${\cal F}_2 \cup {\cal F}_3$:
$t \reduce{1}{} t_2 \reduce{1}{} t_3''$. 
Since $\beta_0$ is CR, it must be the case that
$t_3' \equiv_{\alpha} t_3''$.
\end{proof}

\begin{theorem}
\label{transitive}
$\reduces{\beta}{} = \reduces{1}{}.$
\end{theorem}
\begin{proof} 
Left to the reader.
\end{proof} 

\begin{theorem}
$\beta \models CR$.
\end{theorem}
\begin{proof}
Follows from the diamond property of the
parallel reduction (theorem \ref{diam}) and the fact that
$\beta$ and the parallel reduction do have the same transitive closure
(theorem \ref{transitive}).
\end{proof}


\section*{Acknowledgements}
Funding for this work has been 
provided in part by the Advanced Research Projects Agency of the Department
of Defense under the Office of Naval Research contract N00014-84-K-0099 (MIT)
and N0039-88-C-0163 (Harvard).

Many thanks to Arthur Lent and Allyn Dimock
for reading the current draft of the paper
and for providing  insightful comments.
\bibliography{paper}
\bibliographystyle{abbrv}


\end{document}
