\section{GRS: Terms, Rules and Reduction}
\label{formalGRS} 

\subsection{GRS terms}

\begin{definition}[GRS term]
\label{grsterm}
A GRS term over signature ${\cal F}={\cal F}^0 \cup
{\cal F}^1 \cup \cdots $ is defined inductively as follows:
\begin{tightlist}
\item[(i)]
a variable $x$ is a term;
\item[(ii)]
a constant $c$, where $c \in {\cal F}^0$, is a term;
\item[(iii)]
$\Omega$ is a term;
\item[(iv)]
${\sf F}^k(y_1,\cdots,y_k)$ is a term if
$\forall i, 1  \!\leq  \!i  \! <  \! k$, $y_i$ is either a variable
or a constant, and ${\sf F}^k \in {\cal F}^k$;
\item[(v)]
$\{ 
x_1=e_1; \cdots ;x_p=e_p; \;\; {\sf In} \; x \}$
is a term if
\begin{tightlist}
\item[(v.1)]
$\forall i, 1 \! \leq  \!i  \!\leq  \!p$,
$x_i$ is a variable and $e_i$ is a term;
\item[(v.2)]
$x$ is either a constant or a variable;
\item[(v.3)]
$\forall i,j, 1  \!\leq  \!i  \! <  \!j
 \!\leq  \!p$, $x_i \not\equiv x_j$.
\end{tightlist}
\end{tightlist}
The order of bindings in a block term is irrelevant.
\end{definition}

\noindent
Clause $(v.3)$ prevents multiple definitions of a variable;
for example, $\{ x={\sf 3}; \; x ={\sf 4}; \cdots {\sf In} \; z \}$
is not a legal term.
For technical convenience we assume that if the main term
$M$ is of the form ${\sf F}^k(y_1,\cdots, y_k)$ or $\Omega$ then $M$ has
a name associated to it, that is,
$M \equiv \{ t =M; \; {\sf In} \; t \}$.
We also assume that $\{ {\sf In} \; x \} \equiv x$.

\begin{definition}[Root of a term]
Given a GRS term $M$, the root of $M$, 
${\tt Root}(M)$, is :
\begin{tightlist}
\item[(i)]
$M$, if $M$ is either a constant or a variable;
\item[(ii)]
$x$, if $M$ is $\{x_1 = e_1; \cdots x_p = e_p; \;
{\sf In} \; x \}$.
\end{tightlist}
\end{definition}

\begin{definition}[Free Variables of a GRS term]
The set of free variables of a GRS term $M$, ${\tt FV}(M)$, is defined
inductively as follows:
\begin{tightlist}
\item[(i)]
${\tt FV}(x)=\{x\}$
\item[(ii)]
${\tt FV}(c)= \emptyset$
\item[(iii)]
${\tt FV}(\Omega)= \emptyset$
\item[(iv)]
${\tt FV}({\sf F}^k(y_1,\cdots,y_k))= 
\bigcup \{ {\tt FV}(y_i) \mid 1  \!\leq  \!i  \!\leq  \!k \}$
\item[(v)]
${\tt FV}(
\{ 
x_1=e_1; \cdots ;x_p=e_p; \; {\sf In} \; x \})
= ( \bigcup \{ {\tt FV}(e_i) \mid 1 \leq i \leq p \}
\cup {\tt FV}(x) ) 
- \{x_1,\cdots,x_p\}$. 

Where $-$ is the set difference operator.
\end{tightlist}
\end{definition}

\begin{definition}[Bound Variables of a GRS term]
The set of bound variables of a GRS term $M$, ${\tt BV}(M)$, is defined
inductively as follows:
\begin{tightlist}
\item[(i)]
${\tt BV}(x)= \emptyset $
\item[(ii)]
${\tt BV}(c)= \emptyset $
\item[(iii)]
${\tt BV}(\Omega)= \emptyset $
\item[(iv)]
${\tt BV}({\sf F}^k(y_1,\cdots,y_k))= \emptyset $
\item[(v)]
${\tt BV}(
\{ x_1=e_1; \cdots ;x_p=e_p; \; {\sf In} \; x \})
= \{x_1,\cdots,x_p\} \cup
( \bigcup \{ {\tt BV}(e_i) \mid 1  \! \leq  \! i  \! \leq  \! p \}). $
\end{tightlist}
\end{definition}

\begin{definition}[Variables of a GRS term]
The set of variables of a GRS term $M$, ${\tt Var}(M)$, is defined
to be ${\tt FV}(M) \cup {\tt BV}(M)$.
\end{definition}

\begin{definition}[Constants of a GRS term]
The set of constants of a GRS term $M$, ${\tt Constants}(M)$, is defined
inductively as follows:
\begin{tightlist}
\item[(i)]
${\tt Constants}(x)= \emptyset $
\item[(ii)]
${\tt Constants}(c)= \{ c \} $
\item[(iii)]
${\tt Constants}(\Omega)= \emptyset $
\item[(iv)]
${\tt Constants}({\sf F}^k(y_1,\cdots,y_k))= 
\bigcup \{ {\tt Constants}(y_i) \mid 1  \!\leq  \!i  \!\leq  \!k \}$
\item[(v)]
${\tt Constants}(
\{ x_1=e_1; \cdots ;x_p=e_p; \; {\sf In} \; x \})
= 
( \bigcup \{ {\tt Constants}(e_i) \mid 1  \! \leq  \! i  \! \leq  \! p \})
\cup {\tt Constants}(x). $
\end{tightlist}
\end{definition}

\noindent
For technical convenience we will assume the
following variable convention.\\
{\sc Variable convention}: \\
{\it i.)  all bound variables of a term are distinct};\\
{\it ii.) all bound and free variables of a term are distinct}.

The following two terms are illegal because of this variable convention.
\[ \begin{array}{lll}
\{ \begin{array}[t]{l}
x = \{ \begin{array}[t]{l}
y = {\sf +}(w,w);\\
\;\; {\sf In} \; y \};
\end{array}\\
w = {\sf +}(y,x);\\
\;\; {\sf In} \; w\}
\end{array} & \hspace{1cm} &
\{ \begin{array}[t]{l}
x = \{ \begin{array}[t]{l}
x = {\sf +}(w,w);\\
\;\; {\sf In} \; x \};
\end{array}\\
w = {\sf +}(y,x);\\
\;\; {\sf In} \; w\}
\end{array} 
\end{array} \] 
\noindent

\begin{definition}[Substitution operation]
Given a GRS term $M$, $y \in  (Variable \cup {\cal F}^0)$,
and $z \in  Variable$ such that
$\{ y,z \} \not\subseteq {\tt BV}(M)$,
the substitution of $y$ for each free occurrence of $z$ in $M$,
written as $M[y/z]$, is defined inductively as follows:
\begin{tightlist}
\item[(i)]
$z[y/z]=y$
\item[(ii)]
$x[y/z]=y$ , if $x \not\equiv z$
\item[(iii)]
$c[y/z] = c $
\item[(iv)]
$\Omega[y/z]=\Omega$ 
\item[(v)]
${\sf F}^k(y_1,\cdots,y_k)[y/z] = {\sf F}^k(y_1[y/z],\cdots,y_k[y/z]) $
\item[(vi)]
$\{ 
x_1=e_1; \cdots ;x_p=e_p; \; {\sf In} \; x \}[y/z] = 
\{ x_1=e_1[y/z]; \cdots ;x_p=e_p[y/z]; \; {\sf In} \; x[y/z] \} $
\end{tightlist}
\end{definition}

%Note that due to the variable convention the free variable 
%$y$ cannot get captured, and it must be the case that
%$\not\exists i, 1  \! \leq  \!i  \!\leq \! p, z  \equiv x_i$.


\subsection{Canonical forms of terms} 
\label{canonical}
\noindent
Consider the following terms:
\[ \begin{array}{lll}
\{\begin{array}[t]{l}
x = {\sf 8};\\
z = \{\begin{array}[t]{l}
y = x;\\
w = {\sf +}(x,y);\\
\;\; {\sf In} \; w \};
\end{array}\\
\; \; {\sf In} \; z \} 
\end{array} &
\{\begin{array}[t]{l}
x = {\sf 8};\\
y = x;\\
w = {\sf +}(x,y);\\
\; \; {\sf In} \; w \};
\end{array} &
\{ \begin{array}[t]{l}
w = {\sf +}(8,8);\\
\;\; {\sf In} \; w \}
\end{array} 
\end{array} \]
These terms have different syntactic structure,
however, we consider this difference merely {\it syntactic
noise}. While the following terms:
\[ \begin{array}{lll}
\{\begin{array}[t]{l}
w = {\sf +}(x,y);\\
\;\; {\sf In} \; w \};
\end{array} & \hspace{1cm} &
\{\begin{array}[t]{l}
w = {\sf +}(x_1,y_1);\\
\;\; {\sf In} \; w \}
\end{array} 
\end{array} \] 
which differ only in the reference to the free variables will not
be considered the same.
We also consider the following two terms to be distinct 
because $\Omega$ is not a ``substitutable value''.
$$\begin{array}{ll}
\{ \begin{array}[t]{l}
x  =  {\sf F}(y,z); \\
y  =  \Omega; \\
z  =  \Omega; \\
\;\; {\sf In} \; x \}
\end{array} & \hspace{2cm}
\{ \begin{array}[t]{l}
x  =  {\sf F}(y,y); \\
y  =  \Omega; \\
\;\; {\sf In} \; x \}
\end{array}
\end{array}$$

\noindent
We introduce the following rules to compute the
canonical form of a term. \\
%The meta-variables
%$B_i, BB_i$ range over the syntactic category {\it Binding}.\\

%\noindent
%{\bf Block Flattening rule:}
%\[\begin{array}{lll}
%\{ x \; = \;  \{ \; BB_1;\;BB_2;\;\cdots & & \;
%\{  x  \; = \; y\\
%\hspace{1.8cm}\;\;\;\;{\sf In}\;\; y \}; &
%\reduce{}{} & \;\; {BB_1} ; \; {BB_2} ; \cdots \;  \\
%\;\; B_1;\;\cdots \;\; B_n;\;  & & \;\; B_1; \; \cdots \;  \; B_n;\; \\
%\hspace{0.9cm}{\sf In} \;z \}  & & \hspace{0.9cm}{\sf In} \;z \} 
%\end{array} \]

\noindent
{\bf Block Flattening rule:}
\[\begin{array}{lll}
\{ x \; = \;  \{ \; y_1 = e_1'; \cdots  \;y_m = e_m'; & & \;
\{  x  \; = \; y\\
\hspace{1.8cm}\;\;\;\;{\sf In}\;\; y \}; &
\reduce{}{} & \;\; {y_1 = e_1'}; \cdots  {y_m=e_m'};  \\
\;\; x_1=e_1;\;\cdots \;\; x_n=e_n;\;  & & \;\; x_1=e_1; \; \cdots \;  \; x_n=e_n;\; \\
\hspace{0.9cm}{\sf In} \;z \}  & & \hspace{0.9cm}{\sf In} \;z \} 
\end{array} \]

\noindent
{\bf Substitution rules:}
\[ \begin{array}{llll}
\{ x_1 = e_1 ; \cdots x = c; \cdots  x_n=e_n; \;{\sf In} \; z \} &  \reduce{}{} &
\{ x_1=e_1[c/x]; \cdots x_n = e_n[c/x]; \; {\sf In} \; z[c/x] \} & \hspace{1cm} c \in {\cal F}^0\\
\{ x_n=e_n; \cdots x=y; \cdots x_n=e_n; \;{\sf In} \; z \} & \reduce{}{} &
\{ x_n=e_n[y/x]; \cdots x_n=e_n[y/x]; \; {\sf In} \; z [y/x]\}
& \hspace{1cm} x \not\equiv y\\
\{ x_n=e_n; \cdots x=x; \cdots x_n=e_n; \;{\sf In} \; z \} & \reduce{}{} &
\{ x_n=e_n[\mbox{{\bf $\odot$}}/x]; \cdots x_n=e_n[\mbox{{\bf $\odot$}}/x];
 \; {\sf In} \; z[\mbox{{\bf $\odot$}}/x] \}
\end{array} \]
where {\bf $\odot$} is a special constant.
These rules formalize the notion of a substitutable expression, and
say that only constants and variables (provided $x$ and $y$ are
distinct variables) can be substituted freely. Moreover, note that a
binding like $x=y$ or $x=c$ is deleted after the substitution.  If we
encounter a {\it degenerate binding} like $x=x$ then we substitute the
special constant {\bf $\odot$} for $x$. Disallowing such
bindings does not help because they can arise as a consequence of
doing a reduction.  In fact, as pointed out in Section \ref{crs},
given the rule $x={\sf I}(y) \reduce{}{} x=y$, the term $\{ x={\sf
I}(x); \; {\sf In} \; x \}$ will go to {\bf $\odot$}.

\begin{definition}[Canonical form]
Given a GRS term $M$, the canonical form of $M$ is computed
using the following two steps:
\begin{tightlist}
\item[1.]
Flatten all blocks in $M$ using the Block Flattening rule. Then apply
the Substitution rules to the term as
many times as they apply. Let the result be $\overline{M}$.
\item[2.] 
Eliminate the garbage, that is, the  subterms of
$\overline{M}$ that are
unreachable from the root of $M$.
Let the result be {\tt GC}($\overline{M}$).
\end{tightlist}
\end{definition}

\begin{proposition}
The canonical form of a GRS term  $M$ always exists and is unique.
\end{proposition}
\begin{proof}
Since there are only a finite number of blocks in $M$,
and an application of the Block Flattening rule eliminates
one block without creating a new one, the Block
Flattening rule can be applied only a finite number of times. 
The final flattened term is unique since the Block flattening rule
has the {\it diamond property}.

There are only a finite number of bindings of the form $x=y$ or $x=c$ or $x=x$
in the flattened term. Each of these bindings can be eliminated in one
substitution step without creating a new binding. Furthermore,
because of the third substitution rule (\ie the introduction
of {\bf $\odot$}),
the substitution rules also have the {\it diamond property}.
Hence $\overline{M}$ exits and is unique.

${\tt GC}(\overline{M})$ is unique by the definition
of garbage collection.
\end{proof}


\noindent
{\bf Renaming rule:}
\[ \begin{array}{c}
\{ x_1=e_1; \cdots ;x_p = e_p; \; {\sf In} \; x \}
\reduce{}{}
\{ x_1=e_1[x_j'/x_j]; \cdots ;x_j'=e_j[x_j'/x_j]; \cdots  ;x_p = e_p[x_j'/x_j] \;
{\sf In} \; x[x_j'/x_j] \} 
\end{array} \]
\noindent
where $x_j'$ is a new variable.  The renaming rule is similar to the
$\alpha$-renaming in the $\lambda$-calculus.

%\begin{proposition}
%The canonical form of a GRS term $M$ always exists and is unique.
%\end{proposition}

\begin{definition}[$\alpha$-equivalence]
\label{defalphaequiv}
Given GRS terms $M$ and $N$, $M$ and $N$ are said
to be $\alpha$-equivalent, written as $M \equiv_{\alpha} N$,
iff ${\tt GC}(\overline{M}) \equiv {\tt GC}(\overline{N})$
up to renaming.
\end{definition}

\noindent
The canonicalization rules plus renaming do
not affect the ``graph'' associated to a term, in other words, all
$\alpha$-equivalent terms will correspond to rooted isomorphic graphs.

%\begin{definition}[$\alpha$-function]
%Given two $\alpha$-equivalent GRS terms $M$ and $N$ in canonical form, the
%$\alpha$ function defines the variable in $N$ corresponding to a
%variable in a term $M$.
%\end{definition}

\subsection{GRS rules}

\begin{definition}[GRS rule]
A GRS rule $\tau$ is a set of preconditions, $x_1=e_1, \cdots, x_n=e_n$, and a
left-hand side, $l$, and a right-hand side,
$r$, and is written as:
\[ \frag{x_1=e_1 ; \cdots ; x_n=e_n}
{ x=l \;\; \reduce{}{}\;\;x=r }\] 
\noindent
where:
\begin{tightlist}
\item[(i)]
the pattern of rule $\tau$,
$\{x_1=e_1; \cdots x_n=e_n; \; x=l; \; {\sf In} \; x\}$,
is a block-term in canonical form, and $ l \not\equiv  \Omega$;
\item[(ii)]
$r$ is a term such that
${\tt FV}(r) \subseteq {\tt Var}(\{x_1=e_1;\cdots x_n=e_n;\;x=l; \;{\sf In} \; x \})$.
\end{tightlist}
The pattern of rule $\tau$ is denoted by ${\cal P}(\tau)$.
The term $r$ is called the right-hand side of the rule and is
denoted by ${\cal RHS}(\tau)$.
The free variables of the pattern of $\tau$ are called the meta-variables 
of rule $\tau$.
\end{definition}

\noindent
Notice that restriction $(i)$ makes it impossible to give a
GRS rule to rewrite a constant or a variable. 
In general, a GRS rule does not contain any $\Omega$s.

\begin{definition}[GRS]
A GRS is a structure $(A({\cal F} ), R)$, where $A({\cal F} )$ is the
set of GRS terms defined over signature ${\cal F}$,
and R is a set of GRS rules.
\end{definition}


\begin{definition}[Left-linear rule]
A GRS rule $\tau$ is said to be left-linear iff
$\forall y \in {\tt Var}({\cal P}(\tau))$, $y$ is referenced at most once in 
${\cal P}(\tau)$.
\end{definition}
%It will become clear shortly 
%that non left-linearity is interpreted as pointer equality.
%and not as tree-equivalence as in \cite{Farmer89}.

\begin{definition}[Left-acyclic rule]
A GRS rule $\tau$ is said to be left-acyclic iff
$ \forall y \in {\tt BV}({\cal P}(\tau))$, $y$ is not reachable from itself
in ${\cal P}(\tau)$. Otherwise the rule is said to be a left-cyclic rule.
\end{definition}

The rule, $x={\sf A}(x) \reduce{}{} x = {\sf 0}$,
is an example of a left-cyclic rule.
Notice that a left-cyclic rule is always non left-linear.


\subsection{Identifying redexes and $\omega$-ordering} 
\label{redexandordering}
There are subtle issues involved in identifying redexes in a term.
Consider the following two rules:
$$\begin{array}{lll}
\tau_1: \;\; \frag{ x_1  =  {\sf F}(0) ; \; x_2 = {\sf F}(0)}   
{ x={\sf G}(x_1, x_2 )\;\; \reduce{}{} \;\;  x={\sf 0} }
&  \hspace{1cm} &
\tau_2: \; \; \frag{ x_1  =  {\sf F}(0)}
{ x={\sf G}(x_1, x_1 )\;\; \reduce{}{} \;\;  x={\sf 0} }
\end{array}$$
and the following two terms:
$$\begin{array}{lll}
M \equiv \{ \begin{array}[t]{l}
t_1 = {\sf F}(0);\\
t_2 ={\sf F}({\sf 0});\\
t_3 = {\sf G}(t_1,t_2); \\
{\sf In} \; t_3 \}
\end{array} & \hspace{2cm}
N \equiv \{ \begin{array}[t]{l}
t_1 = {\sf F}(0);\\
t_2 = {\sf G}(t_1,t_1); \\
{\sf In} \; t_2 \}
\end{array} 
\end{array} $$

On the basis of the intuitive description given in Section
\ref{crs}, we can undoubtedly say that $\tau_1$ matches $M$, 
with substitution ``$x=t_3, x_1=t_1, x_2=t_2$'', and $\tau_2$ matches
$N$ with substitution ``$x=t_2,x_1=t_1$''.  Does rule $\tau_1$ applies
to $N$? or does rule $\tau_2$ applies to $M$? Rule $\tau_1$ does
indeed apply to the term $N$ by matching both the preconditions to the
same binding, that is, by the substitution
``$x_1=t_1,x_2=t_1,x=t_2$''.  However, there is no variable
substitution that can make $\tau_2$ applicable to $M$.  Thus, the
preconditions of a rule can be satisfied by overlapping bindings,
moreover, the left-hand side of a rule can also overlap its precondition, as
shown in the following example.  Consider the rule: $$ \frag{ x_1 =
{\sf G}(y) } {x={\sf G}\;(x_1)\;\; \reduce{}{} \;\; x={\sf 0} } $$ and
the term $M \equiv \{ t = {\sf G}(t);\;\;{\sf In} \; t \}$.  The
substitution ``$x=t,x_1=t, y=t$'' makes ${\sf G}(t)$ both a redex and
its precondition!
We can capture the notion of a redex in terms of an ordering on terms.


\begin{definition}[$\omega$-ordering: $\leq_{\sf \omega}$]
Given GRS terms $M$ and $N$ in
canonical form, $M \leq_{\sf \omega} N$ iff $\exists$ 
a function $\sigma:$
$${\tt Var}(M) \cup {\tt Constants}(M) 
 \rightarrow
{\tt Var}(N) \cup {\tt Constants}(N) $$
such that:
\begin{tightlist}
\item[(i)]
$\forall c \in {\tt Constants}(M)$, $\sigma(c)=c$;
\item[(ii)]
$\forall x \in {\tt FV}(M)$, $\sigma(x)=x$;
\item[(iii)]
$\forall x \in {\tt BV}(M)$,
if $x= {\sf F}^k(y_1,\cdots,y_k)$ in $M$ then 
$\sigma(x) \in {\tt BV}(N)$ and 
$\sigma(x)$ is bound to ${\sf F}^k(\sigma(y_1),\cdots,\sigma(y_k))$ in $N$;
\item[(iv)]
$\sigma({\tt Root}(M))={\tt Root}(N)$.
\end{tightlist}
$\sigma$ is called the substitution function 
induced by the ordering.
\end{definition}

\noindent
Notice that according to  condition $({\it iii})$
if $x$ is bound to $\Omega$ then $x$ can be mapped to any
variable or constant in $N$.
Intuitively, $M \leq_{\sf \omega} N$
if $N$ can be obtained from $M$ by replacing $\Omega$ with any other
term or by increasing the sharing in $M$.  This is a generalization of
the ordering on TRS terms introduced by Huet and L\'evy \cite{Huet2}.

\begin{proposition}
The $\omega$-ordering is a partial order with $\Omega$ as the least element.
\end{proposition}
\begin{proof}
See \cite{Zena93d}.
\end{proof}

The following examples may enhance the reader's
intuition about $\omega$-ordering.

Consider the following acyclic terms:
$$\begin{array}{l}
M_1 \equiv \{x_1 = {\sf G}(x_2,x_2); \; x_2 = {\sf F}(0);\; {\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_3 \equiv \{x_1 = {\sf G}(x_2,x_2); \; x_2 = \Omega; \; {\sf In} \; x_1\}\\
M_4 \equiv \{x_1 = {\sf G}(x_2,x_3);\;
x_2 = \Omega;\; x_3 = \Omega; \; {\sf In} \; x_1\}
\end{array}$$

Notice that $M_2 \leq_{\sf \omega} M_1$, $M_3 \leq_{\sf \omega} M_1$,
and $M_4$ is $\leq_{\sf \omega} M_1$, $M_2$ and $M_3$. 
However, $M_2$ and $M_3$ are not related.

Now consider the following cyclic terms:
$$\begin{array}{l}
N_1 \equiv \{x_1 = {\sf F}(x_1); \; {\sf In} \; x_1\} \\
N_2 \equiv \{x_1 = {\sf F}(x_2);\; x_2 = {\sf F}(x_1); \; {\sf In} \; x_1\} \\
N_3 \equiv \{x_1 = {\sf F}(x_2); \;
x_2 = {\sf F}(x_3); \; x_3 = {\sf F}(x_1); \; {\sf In} \; x_1\} \\
\end{array}$$

Notice that $N_2 \leq_{\sf \omega} N_1$ and $N_3 \leq_{\sf \omega} N_1$
but $N_2$ and $N_3$ are not related.


\blank
We use ${\sf \omega}$-ordering as follows in defining a redex.  We bind
all meta-variables of a rule to $\Omega$.
Such a term is called the {\it closure of a rule}. If term $p$ is the
closure of rule $\tau$ then a term $M$ is said to be a $\tau$-redex if
$p \leq_{\sf \omega} M$.

\begin{definition}[Closure of a rule]
Given a GRS rule $\tau$, where
${\cal P}(\tau) \equiv  \{ x_1=e_1;  \cdots x_n=e_n; \; x = l; \; {\sf In} \; x \}$,
the closure of $\tau$, written as ${\cal
C}l(\tau)$, is the term $\{ y_1=\Omega;\; \cdots y_m = \Omega;\;
x_1=e_1;  \cdots x_n=e_n; x = l; \; \; {\sf In} \; x \}$,
where $\{ y_1,\cdots, y_m \} =
{\tt FV}({\cal P}(\tau))$. 
\end{definition}

\begin{definition}[Subterm rooted at $x_i$]
Given a GRS term 
$M \equiv \{ x_1=e_1 ; \cdots x_p=e_p; \; {\sf In} \; x \}$ 
in canonical form, and $x_i \in {\tt BV}(M)$,
the subterm of $M$ rooted at $x_i$, written as $M @ x_i$, is 
the term ${\tt GC}(\{ x_1=e_1 ; \cdots x_p=e_p; \; {\sf In} \; x_i \})$.
\end{definition}


\begin{definition}[Redex]
\label{redexbyordering}
A redex in a GRS term $M$ in canonical form is a triple ($\tau,z,\sigma)$ such that:
\begin{tightlist}
\item[(i)]
$\tau$ is a GRS rule;
\item[(ii)]
$z \in {\tt BV}(M)$, such that
${\cal C}l(\tau) \leq_{\sf \omega} M @ z$;
\item[(iii)]
$\sigma$ is the substitution induced by
${\cal C}l(\tau) \leq_{\sf \omega} M @ z$.
\end{tightlist}
$z$ is said to be the root of the redex.
If $z ={\tt Root}(M)$ then $M$ itself is said to be a redex. \\
The set containing the roots of all
redexes in $M$ is denoted by $\Re(M)$.
\end{definition}

\noindent
For example, consider the following rule: 
$$\tau: \;\; x = {\sf G}(y,y) \reduce{}{} x = {\sf 0} $$
and the term $M \equiv \{ z = {\sf G}(z_1,z_1); \; z_1 = {\sf F}(0);\;
z_2 = {\sf H}(z);\; {\sf In}\; z_2 \}$ which has the following graph:
\vspace{-0.1in}
\begin{center}
%\epsf{../../../Bk/ps/sharingpattern.ps}
\epsffile{sharingpattern.ps}
\end{center}
\vspace{-0.2in}
$M @ z$ is a redex because ${\cal C}l(\tau) \equiv \{ y = \Omega;\; x
= {\sf G}(y,y);\;\; {\sf In} \; x \} \leq_{\sf \omega} M @ z$.

%\begin{definition}[Distinct Redexes]
%Two 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 are said to be
%distinct if $\tau_1 \neq \tau_2$, or $z_1 \neq z_2$, or 
%$\sigma_1 \neq \sigma_2$. 
%\end{definition}

\begin{definition}[Distinct Redexes]
Two 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 are said to be
distinct if $\tau_1 \neq \tau_2$ or $z_1 \neq z_2$.
\end{definition}

\subsection{Reduction}

We have explained informally, in Section \ref{crs}, that a GRS reduction
consists of first making a copy of the right-hand side of the rule,
and then replacing the root of the redex with that copy.  Therefore,
we introduce the notion of an {\it instance} of a term $M$ for a given
substitution $\sigma$, and the operation
of {\it replacement}. An instance of $M$ is created by substituting
$\sigma(x)$ for each free occurrence of variable $x$ in $M$, and
by renaming each bound variable of $M$.

\begin{definition}[Instance of a term]
Given a GRS term $M$ in canonical form and a substitution $\sigma$, an instance of $M$,
written as $M^\sigma$, is defined inductively as follows:
\begin{tightlist}
\item[(i)]
$x^\sigma=\sigma(x)$, where $x$ is either a constant or a variable;
\item[(ii)]
$\Omega^\sigma = \Omega$;
\item[(iii)]
${\sf F}^k(y_1,\cdots,y_k)^\sigma = {\sf F}^k(y_1^\sigma,\cdots,y_k^\sigma)$;
\item[(iv)]
$ \begin{array}[t]{lll}
\{ \begin{array}[t]{l}
x_1=e_1;\\
\;\;\;\vdots \\
x_p=e_p;\\
\;\;{\sf In} \; x \}^\sigma 
\end{array} & = & 
\{ \begin{array}[t]{l}
x_1'=(e_1[x_1'/x_1] \cdots [x_p'/x_p])^\sigma;\\
\;\;\;\vdots\\
x_p'=(e_p[x_1'/x_1] \cdots [x_p'/x_p])^\sigma;\\
\;\;{\sf In} \; (x[x_1'/x_1] \cdots [x_p' /x_p])^\sigma \}
\end{array}
\end{array}$\\
where $x_i', 1 \! \leq  \!i  \!\leq p$, are new variables.
\end{tightlist}
\end{definition}

The above definition does not depend on the order of the
substitutions because $x_i' \not\in {\tt Var}(M)$. \\

Given a rule $\tau$, and a redex $(\tau,z,\sigma)$ in $M$, the reduction
step consists of {\it replacing} the term bound to $z$ by 
$({\cal RHS}(\tau))^\sigma$ ( \ie an instance of the right-hand side of
$\tau$).

\begin{definition}[Replacement]
Given GRS terms $M$ 
and $N$, where $N$ is in canonical form and
${\tt BV}(N) \cap {\tt Var}(M) = \emptyset$,
the replacement of the term bound to $z$ in $M$ by $N$, written as
$M[z\leftarrow N]$, is defined as follows:
\begin{tightlist}
\item[(i)]
$M$, if $z \not\in {\tt BV}(M)$;
\item[(ii)]
$\{ x_1=e_1; \cdots ;z=N; \cdots ;x_n=e_n; \; {\sf In} \; x \}$,
if $M \equiv 
\{ x_1=e_1; \cdots ;z =e_i \cdots ;x_n=e_n; \; {\sf In} \; x \}$.
%\item[(iii)]
%$\{ x_1=e_1[z \leftarrow N]; \cdots ;
%x_n=e_n[z \leftarrow N]; \; {\sf In} \; x \}$,
%if $M \equiv
%\{ x_1=e_1; \cdots ;x_n=e_n; \; {\sf In} \; x \}$ and $z \not\in
%\{x_1,\cdots,x_n\}$.
\end{tightlist}
\end{definition}
Notice that no renaming occurs during the replacement, thus the free
variables of $N$ can get captured. 
Moreover, 
the bound variables of $M$, which are different from $z$, are not
affected by the replacement. \\

\noindent
{\sc Notation}:
{\it $M[{\cal Z} \leftarrow \Omega]$, where
${\cal Z}=\{z_1, \cdots, z_n \}$ will stand for $M[z_1 \leftarrow \Omega]
\cdots [z_n \leftarrow \Omega]$}. \\

\noindent
Now we state certain useful properties of replacement.

\begin{proposition}
\label{repl}
Given GRS terms $M,N_1$ and $N_2$ in canonical form
such that 
$({\tt BV}(N_1) \cap {\tt BV}(N_2))  = \emptyset$,
$({\tt BV}(N_1) \cup {\tt BV}(N_2)) \cap {\tt Var}(M)
= \emptyset$, and variables $z_1,z_2$ such that
$z_1 \not\equiv z_2$, and $
\{ z_1, z_2 \} \not\subseteq  {\tt BV}(N_1) \cup
{\tt BV}(N_2)$:
$$ M [z_1 \leftarrow N_1][z_2 \leftarrow N_2 ] \equiv 
 M [z_2 \leftarrow N_2][z_1 \leftarrow N_1 ].$$ 
\end{proposition} 
\begin{proof}
By cases on the existence of $z_1$ and $z_2$ in ${\tt BV}(M)$.
\end{proof}

The following proposition shows that under appropriate
circumstances the garbage collection step can be postponed.

\begin{proposition}
\label{garbage}
Given GRS terms $M$ and $N$, such that $N$ is in canonical form.
If ${\tt BV}(N) \cap {\tt Var}(M) =
\emptyset$ and 
${\tt FV}(N) \subseteq {\tt Var}({\tt GC}(\overline{M}))$ then
$$ {\tt GC}(\overline{{\tt GC}(\overline{M})[z \leftarrow N]}) \equiv 
{\tt GC}(\overline{\overline{M}[z \leftarrow N]}).$$
\end{proposition}
\begin{proof}
The garbage collection does not affect $N$. 
The condition ${\tt FV}(N) 
\subseteq  {\tt Var}({\tt GC}(\overline{M}))$
guarantees that the garbage not picked up by the
inner ${\tt GC}$ is not affected by $N$, and thus
is collected by the outer {\tt GC}.
\end{proof}

\begin{proposition}
\label{garbrepl}
Given GRS terms $M,N, P$ and $P'$ in canonical form, and variable
$z'$ such that
\begin{tightlist}
\item[(i)]
${\tt BV}(P) \cap {\tt Var}(M) = \emptyset$;
\item[(ii)]
$P' \equiv_\alpha P$;
\item[(iii)]
${\tt BV}(P') \cap {\tt Var}(N) = \emptyset$.
\end{tightlist}
If $M \leq_{\sf \omega} N$ let
$\sigma_{MN}$ be the substitution function induced by
the $\omega$-ordering,
$z$ be such that
$\sigma_{MN}(z) = z'$, and 
${\cal Z} = \{ s \mid s \in {\tt BV}(M), 
\sigma_{MN}(s) =  z', s \not\equiv z \}$,
then 
$${\tt GC}({\tt GC}(\overline{M [ z \leftarrow P]})[ {\cal Z} \leftarrow \Omega])
\leq_{\sf \omega} {\tt GC}(\overline{N[z' \leftarrow P']}).$$
\end{proposition}
\begin{proof}
We first show the following
$${\tt GC}(M[z \leftarrow \Omega][ {\cal Z} \leftarrow \Omega])
\leq_{\sf \omega} {\tt GC}(\overline{N[z' \leftarrow P']})$$
that is we want to show that  the function 
$\sigma_{MN}$ restricted to the domain of elements occurring in
$ {\tt GC}(M[z \leftarrow \Omega][{\cal Z} \leftarrow \Omega])$ is 
the substitution function induced by
${\tt GC}(M[z \leftarrow \Omega][ {\cal Z} \leftarrow \Omega])
\leq_{\sf \omega} {\tt GC}(\overline{N[z' \leftarrow P']})$.
Suppose it is not, then it must be the case
that for an element, say $x$, occurring in
$ {\tt GC}(M[z \leftarrow \Omega][{\cal Z} \leftarrow \Omega])$,
$\sigma_{MN}(x)$ does not occur in
${\tt GC}(\overline{N[z' \leftarrow P']})$.
This means that the replacement of the term
bound to $z'$ by $P'$ in $N$ has
removed the path to $\sigma_{MN}(x)$. However, this
means that the corresponding path in $M$ gets removed
also by setting to $\Omega$ $z$ and all the elements of ${\cal Z}$.
Contradiction, therefore it must be the case that
$\sigma_{MN}(x) $ occurs in
${\tt GC}(\overline{N[z' \leftarrow P']})$.

Moreover, 
for all elements $x$ in
${\tt BV}(P)$, let $x'$ be its renamed version.
The following function:
$$ \sigma' (x) = \left \{ \begin{array}{ll}
\sigma_{MN}(x) & 
x \in 
{\tt GC}({\tt GC}(\overline{M[z \leftarrow \Omega ]})[{\cal Z} \leftarrow \Omega] ) \\
x' & x \in {\tt BV}(P)
\end{array}
\right.$$
determines the ordering:
$${\tt GC}({\tt GC}(\overline{M[z \leftarrow P ]})[{\cal Z} \leftarrow \Omega] )
\leq_{\sf \omega} {\tt GC}(\overline{N[z' \leftarrow P' }])
\equiv N_1.$$
\end{proof}



\begin{definition}[Reduction]
Given a GRS term $M$ in canonical form and a rule $\tau$, $M$ reduces
to $N$ by doing the $\tau$-redex at $z$ in $M$, written as $M
\reduce{z}{\tau} N$, iff $(\tau,z,\sigma)$ is a redex in $M$, and 
$N \equiv
{\tt GC}(\overline{M[z \leftarrow ({\cal RHS}(\tau))^\sigma]})$.\\ 
The reflexive and transitive closure of $\reduce{}{}$ is denoted by 
$\reduces{}{}$.
\end{definition}
The redex $(\tau,z,\sigma)$ is often given the name $\rho$, and
sometimes we will also use the notation $M \reduce{\rho}{} N$ to show
the reduction of redex $\rho$.
Note that each replacement is followed
by a canonicalization step.


\subsection{Descendant of a redex}

%\begin{definition}[Descendant of a subterm, $\delta$]
%\label{descendant}
%Given GRS terms $M$, $M'$ and $N$ in canonical form, such that 
%$M' \equiv
%{\tt GC}(\overline{M[z \leftarrow N]})$,
%and ${\tt BV}(M) \cap {\tt BV}(N) =
%\emptyset$, the descendant function $\delta$ from $M$ to $M'$,
%$$\delta : {\tt Var}(M) \cup {\tt Constants}(M) \rightarrow
%{\tt BV}(M') \cup {\tt FV}(M') \cup {\tt Constants}(M') \}$$
%is a partial function and is defined as follows:
%\begin{tightlist}
%\item[(i)]
%$\forall x \in {\tt Constants}(M) \cup {\tt FV}(M)$, $\delta(x) = x$,
%if $x \in Constants(M') \cup FV(M')$;
%\item[(ii)]
%$\delta(z) = y$ if
%$N = \{y_1 = e_1 ; \cdots  {\sf In} \; y \}$;
%\item[(iii)]
%$\delta(z) = z$ if
%$N \equiv F^k(y_1, \cdots, y_k)$;
%\item[(iv)]
%$\forall x \in {\tt BV}(M)$, $x \neq z$, $\delta(x) = x$,
%\end{tightlist}
%\end{definition}


\begin{definition}[Descendant of a redex]
\label{descendantredex}
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, 
the descendant of $\rho_2$ with respect to
the reduction $M \reduce{\rho_1}{} M_1$ (written as 
$\rho_2 \setminus \rho_1$):
\begin{tightlist}
\item[(i)]
does not exist, if $z_2 \not\in {\tt BV}(M_1)$;
\item[(ii)]
is the triple 
$\rho_2'=(\tau_2,z_2,\sigma_2')$, if 
$z_2 \in {\tt BV}(M_1)$ and $\sigma_2'$ is:
$$\sigma_2'(x) =
\left \{ 
\begin{array}{ll}
\sigma_2(x) &  \sigma_2(x) \neq z_1 \\
{\tt Root}(r_1^{\sigma_1}) & \sigma_2(x) = z_1 \mbox{ and }
{\tt Root}(r_1^{\sigma_1}) \neq z_1 \\
\mbox{{\bf $\odot$}}
 & \sigma_2(x) = z_1 \mbox{ and }
{\tt Root}(r_1^{\sigma_1}) = z_1 \\
\end{array}
\right.$$
%
%where $\delta$ is the descendant function from $M$ to $M_1$ and $\sigma_2'$ 
%is defined as follows:
%$$
%\sigma_2'(x) = \delta(\sigma_2(x)), \;\;\; x \in {\tt Var}({\cal P}(\tau_2))
%\cup {\tt Constants}({\cal P}(\tau_2)).$$
\end{tightlist}
\end{definition}

The descendant of a redex 
does not necessarily exists,
and even if it exists, it is not necessarily a redex, as 
illustrated by the following example. 
Consider the following two rules:
\[ \begin{array}{l}
\tau_1: \;\; \frag{x_1={\sf G}(y)}{x={\sf F}(x_1) \reduce{}{} x = x_1}\\
\tau_2: \;\; x={\sf G}({\sf 0}) \reduce{}{} x = {\sf 0}
\end{array} \]
and the following reduction:
$$\begin{diagram}
& & \{ \begin{array}[t]{l}
t_1={\sf F}(t_2);t_2={\sf G}({\sf 0});\; {\sf In} \; t_1 \}
\end{array} & & & \\
& \SW^{\tau_2} & & \SE^{\tau_1} & & \\
\{ \begin{array}[t]{l}
t_1={\sf F}(0); \; {\sf In} \; t_1 \} 
\end{array} & & & & 
\{ \begin{array}[t]{l}
t_2={\sf G}({\sf 0}); \; {\sf In} \; t_2 \}
\end{array} 
\end{diagram}$$

\noindent
The two redexes in the above term are $\rho_1 = (\tau_1,t_1,\sigma_1)$,
where $\sigma_1 $ is  ``$x=t_1,\; x_1=t_2,\; y=0$'', and 
$\rho_2 = (\tau_2,t_2,\sigma_2)$, where $\sigma_2$ is ``$x=t_2$'', respectively.
$\rho_2 \setminus \rho_1$ is $(\tau_2,t_2,\sigma_2')$,
where $\sigma_2'$ is ``$x = t_2 $'', and is still a redex. On the other hand,
$\rho_1 \setminus \rho_2=(\tau_1,t_1,\sigma_1')$,
where $\sigma_1'$ is ``$x =t_1 ,\; x_1 = 0, \; y = 0$'', is no
longer a redex.

\begin{remark}
A GRS is non-duplicative,
that is, the descendant of a redex, if it exists, is unique.
\end{remark}


