\section{A Graph Model for GRS}
\label{equivalence}
We are interested in defining an equality on the set of terms,
such that the equality is useful in analyzing
the correctness of compiler optimizations.
If we want equal terms to be freely substitutable for each other, 
then the equality must be preserved by terms formed by putting 
equal terms in the same context,
which is defined as follows.

\begin{definition}[Context]
Let the definition of a GRS term (Definition \ref{grsterm})
be extended to include a special symbol $\Box$.
A context is then a GRS term containing $\Box$.
\end{definition}

\noindent
{\sc Notation}:
{\it We write $C[\Box]$ for an arbitrary context, such as
$\{ x_1 = e_1; \cdots x_n =e_n ; \; z = \Box; \;
{\sf In} \; x \}$, and
$C[M]$ for the term 
$\{ x_1 = e_1; \cdots x_n =e_n ; \; z = \Box; \;
{\sf In} \; x \}[z \leftarrow M] \equiv  
\{ x_1 = e_1; \cdots x_n =e_n ; \; z = M; \;
{\sf In} \; x \}$}. As in any replacement operation
${\tt BV}(M) \cap {\tt BV}(C[\Box]) = \emptyset$,
for $C[M]$ to be a legal term.
Observe that the free variables of a term $M$ 
can get bound in $C[M]$.

For a compiler a useful equality must have the
property $M= N \Longrightarrow \forall
C[\Box], C[M]=C[N]$.  This means that the equality has to be a {\it
congruence} with respect to the formation rules of terms. An optimization
will be considered correct if it preserves equality.


An example of an equivalence relation is {\it convertibility}. If two
terms $M_1$ and $M_2$ are convertible and the GRS is confluent, then
it follows that there will not be any context that can
distinguish between them.  Thus, convertibility is a congruence.  Therefore,
independent of the meaning or observations we associate to a term, a
minimal requirement that will have to be satisfied is that all terms
in the set $\{ M' \mid M \reduces{}{} M' \}$ have the same meaning.
It follows that all optimization rules drawn from the set of rewriting
rules will be automatically meaning preserving.  However, as pointed
out in \cite{Wadsworth}, convertibility makes too fine a distinction
to be interesting; it does not capture the computational behavior of a
term.  For example, consider the following two rules:
$$\begin{array}{ll}
\tau_1 : \;\; x = {\sf F}(y) \reduce{}{} x= {\sf F}(y) & \hspace{1cm}
\tau_2 : \;\; x= {\sf G}(y) \reduce{}{} x = \{
t= {\sf G}(t_1);
t_1 = {\sf G}(y);\; {\sf In} \;t \} 
\end{array}$$
and the terms
\[ \begin{array}{ll}
M \equiv \{ y = {\sf F}(z); \; {\sf In} \; y \} 
& \hspace{1cm}  N \equiv \{ y= {\sf G}(z); \; {\sf In} \; y \} \enspace .
\end{array} \]
\noindent
$M$ is not convertible to $N$ or vice versa. Yet
from a computational point of view,
we would like to consider them as producing no information.  We
may be tempted to extend convertibility by equating all terms without
normal form.  However, it has been shown by Wadsworth in
\cite{Wadsworth} that this will lead to an inconsistent theory.  For
example, if terms $M$ and $N$ do not have  normal forms,
then both the following terms in ${\sf SK}$-combinatory logic:

\[ \begin{array}{lll}
M_1 \equiv \{ \begin{array}[t]{l}
t = {\sf Ap}(x,{\sf K});\\
t_1 = M;\\
t_2 = {\sf Ap}(t, t_1);\\
\;\; {\sf In} \; t_2 \}
\end{array} & \hspace{1cm} &
N_1 \equiv \{ \begin{array}[t]{l}
t = {\sf Ap}(x,{\sf S});\\
t_1 = N;\\
t_2 = {\sf Ap}(t, t_1);\\
\;\; {\sf In} \; t_2 \}
\end{array} 
\end{array}  \]

\noindent
will not have normal forms either, and thus, will be equated.  However, by
plugging both of them in the context $\{ x = {\sf K};\; z = \Box;
\;{\sf In} \; z \}$ we can derive ${\sf K} = {\sf S}$. As
shown in \cite{Barendregt}, this will immediately lead to an inconsistent
theory, and will cause all terms to be equated.

The notion of {\it head normal form} (hnf) was introduced by Wadsworth
to syntactically characterize the class of terms that cannot be
equated.  Intuitively, a term does not have a head normal form if no
information can be extracted by reducing that term in any context,
that is, the term is totally undefined.  For example, the two terms
$M$ and $N$, introduced earlier, are totally undefined, while the
above terms $M_1$ and $N_1$ have some information contained in them. 
For example, we know that whichever term $M_1$ reduces to will have a
stable prefix of the form:
$\{ \begin{array}[t]{l}
t = {\sf Ap}(x,{\sf K});
t_1 = \Box ;
t_2 = {\sf Ap}(t, t_1);
\;\; {\sf In} \; t_2 \}.
\end{array}$
Similarly for $N_1$,
$\{t = {\sf Ap}(x,{\sf S});
t_1 = \Box ;
t_2 = {\sf Ap}(t, t_1);
\; {\sf In} \; t_2 \}$
constitutes a stable prefix.
Informally the hnf of a term embodies
its maximum stable prefix. Since the hnf's of $M_1$ and $N_1$ are
different they cannot be equated.  Furthermore, if two terms $M$ and
$N$ do not contain any information, \ie do not have hnf's, it
intuitively implies that the terms $C[M]$ and $C[N]$ will exhibit the
same behavior and thus, can be equated.  In this manner, we have
performed a further classification of the terms without normal forms
into ones that contain some information and those which contain
no information.  It is therefore legitimate to ask which terms in head
normal forms can be equated.  Convertibility may still be too
restrictive, as shown by the following example, where ${\sf Cons}$
is the usual list contructor:
\[ \begin{array}{lll}
M \equiv \{ \begin{array}[t]{l}
x = {\sf Cons}(y,z);\\
y = {\sf F}({\sf 0});\\
z = {\sf Cons}(w,{\sf Nil});\\
w = {\sf F}({\sf 0});\\
\;\; {\sf In} \; x \}
\end{array} 
& \hspace{1cm} &
N \equiv \{ \begin{array}[t]{l}
x = {\sf Cons}(y,z);\\
y = {\sf F}({\sf 0});\\
z = {\sf Cons}(y,{\sf Nil});\\
\;\; {\sf In} \; x \}
\end{array}
\end{array}  \]

\noindent
Graphs for $M$ and $N$ may be drawn as follows:
\begin{center}
\epsf{listexample1.ps}
\end{center}
\vspace{-0.2in}
\noindent
$M$ and $N$ are in normal form but clearly not inter-convertible.
However, if internal representation of lists is ignored by an observer
then both the terms represent the same unfolded list, ${\sf F}({\sf
0}):{\sf F}({\sf 0}):{\sf Nil}$.  If the GRS containing these terms
has a non-left-linear rule, it may be possible to distinguish between
such terms.  Thus, such terms cannot be equated without disallowing
non-left-linear rules.

We should also notice that  $M \leq_{\sf \omega} N$,
\ie $M$ has ``less sharing'' than $N$ in the above example.
Does it mean that $M$ is ``less defined'' than $N$ in the sense that
one can {\it compute less} with $M$ than with $N$?.  We would like to
answer the above question without delving into heavy duty model
theory.  We have carefully said ``compute'' to emphasize that we are
interested in studying what a term represents from an operational
point of view.  In particular, we are interested in observing the
gradual {\it syntactic building up of the final term}.

We introduce a function $\omega$ to compute the stable part of a term,
that is, the part of the term that will not change as more reductions
are performed on it.  The $\omega$ function captures what L\'evy has
called the {\it direct approximation} of a
$\lambda$-calculus term \cite{Levy78b},
and Welch has called 
the {\it instantaneous semantics} of a term \cite{Welch75}.
Take the following term:
\[ P \equiv \{ \begin{array}[t]{l}
t = {\sf Ap}({\sf Y},f);\\
\;\; {\sf In} \; t \}
\end{array} \]
\noindent
where the rule for the ${\sf Y}$
combinator is expressed as
$$ x = {\sf Ap}({\sf Y},f) \reduce{}{}
x = \{ t = {\sf Ap}(f,t_1); \; t_1 = {\sf Ap}({\sf Y},f); \;
{\sf In} \; t \} \enspace .$$
\noindent
Since ${\sf Ap}({\sf Y},f)$ occurring in
$P$ is a redex, we cannot predict what ${\sf Ap}({\sf Y},f)$
will produce without reducing it. Thus, without any prior knowledge of the
reduction, we will have to assert that no information is associated to $P$,
otherwise, a wrong assumption may lead to a situation
where we have to retract what was printed earlier.  Thus, we will say
that $\omega (P) = \Omega$, where $\Omega$
stands for no information.  Let's perform one-step reduction on $P$ to obtain the term: 
\[ P_1 \equiv \{ \begin{array}[t]{l}
t = {\sf Ap}(f,t_1);\\
t_1 = {\sf Ap}({\sf Y},f);\\
\;\; {\sf In} \; t \} \enspace .
\end{array}
\]
\noindent
At this point notice that all further reductions of $P_1$
will produce terms with context:
$\{ t = {\sf Ap}(f,\Box);\; {\sf In} \; t \}$. 
Thus, we can safely say that $\omega(P_1)$ is
\[\begin{diagram}
& & {\sf Ap} & & \\
& \SW & & \SE & \\
f & & & &  \Omega
\end{diagram} \]
\noindent
In general, we will have
$$ \begin{diagram}
\Omega  \;\;\;
\begin{array}[t]{lllll}
& & {\sf Ap} & & \\
& \SW & & \SE & \\
f & & & &  \Omega
\end{array} \;\;\;
\begin{array}[t]{lllllll}
& & {\sf Ap} & & & & \\
& \SW & & \SE & & & \\
f & & & & {\sf Ap} & & \\
& & & \SW & & \SE & \\
& & f & & & & \Omega
\end{array} \;\;\;
\cdots 
\end{diagram}
$$
\noindent
Notice that as more reductions are performed the stable part should
get larger, that is,
$\omega(P) \leq_{\sf \omega} \omega(P_1)
\leq_{\sf \omega} \omega(P_2) \cdots $.  We remind the reader that
$\leq_{\sf \omega}$ is the syntactic ordering on terms which captures
both the sharing and the fact that $\Omega$ is less than any other
term.  Assuming that this chain has a limit, then, even though
the term $P$ does not have a normal form, it may still have a precise
meaning.

We collect all the (stable) information gathered by reducing $P$ in a
set, called $W^*(P)$, and say that it represents the {\it information
content} of $P$. We can now formulate our original question regarding
the impact of sharing on a program's behavior as follows: {\it if $M$
has less sharing than $N$ then is $W^*(M)$ contained in $W^*(N)$}?  As
we shall see shortly, this is indeed the case in the absence of
interfering rules.

It is also interesting to analyze if $M$ ``less defined'' then $N$
implies that for all context $C[\Box]$, $C[M]$ is ``less defined''
than $C[N]$? That is, is the equality induced by $W^*$ a {\em congruence}? 
Later we will see that, in the absence of interfering rules, the
equality introduced by information content is also a congruence.
Thus, the collection of stable information contained in GRS terms does
indeed turn out to be a model for GRS without interfering rules. \\

We will need the following definition shortly.

\begin{definition}[Initial $\Omega$-form of a term, $M_\Omega$]
Given a GRS term $M$ in canonical form,
$M_\Omega$ is the term ${\tt GC}(M[ \Re(M)  \leftarrow \Omega])$.
\end{definition}

\subsection{Instant semantics}
\label{InstantandDynamicSemantics} 
The instant semantics of a GRS term $M$ is obtained by computing its
{\it stable part}, where stable part means
the part of $M$ which will not change
by further reductions.  A solution that comes to mind is to replace
each redex in a term by an $\Omega$, that is, to treat $M_\Omega$ as
stable. Intuitively, this seems right because a redex
can become any expression, and $\Omega$ is less than all expressions. 
Furthermore, it seems that if $M \rightarrow N$ then $M_\Omega
\leq_\omega N_\Omega$.  Unfortunately, this solution has a problem, as
shown by the following example.  Consider the rules

$$\tau_1: x={\sf F}(y,y) \reduce{}{} x={\sf 4} \hspace{1cm}
\tau_2: x={\sf I}(y) \reduce{}{} x = y $$

\noindent
and the following reduction:
\[ M \equiv 
\{ \begin{array}[t]{l}
t={\sf F}(t_1,t_2);\\
t_1={\sf A}({\sf 0});\\
t_2={\sf I}(t_1);\\
\;\; {\sf In} \; t \}
\end{array} \;\;\;
\reduce{t_2}{\tau_2} \;\;\; M_1 \equiv
\{ \begin{array}[t]{l}
t={\sf F}(t_1,t_1);\\
t_1={\sf A}({\sf 0});\\
\;\; {\sf In} \; t \}
\end{array} 
\]
\noindent
The only redex in $M$ is rooted at $t_2$, and thus, its stable
part is the following term $M_2$:
$$\begin{diagram}
& & {\sf F} & & \\
& \SW & & \SE & \\
{\sf A} & & & & \Omega\\
\downarrow & & & & \\
{\sf 0} & & & &
\end{diagram}$$

\noindent
However, since $M_1$ is a redex, $M_1$ does not contain any stable
information. Thus, the information contained in $M_1$ is less than the
information contained in $M$. This is contrary to our intuition that
the information should not decrease with reduction.  The problem is
due to the presence of rule $\tau_2$ which can introduce sharing.  If
we want to compute the instant semantics of a term without analyzing
the rhs of rules then we have to assume that the arc pointing to
$\Omega$ in $M_2$ can be redirected to point to the node of label
${\sf A}$, and thus making $M_2$ a $\tau_1$-redex.  In other words, we
should not treat $M_2$ as being in stable form. However, $M_\Omega$
does give the stable part of a term $M$ in a Recursive Program Schema (RPS)!

\subsubsection{Stable information in RPS and TRS}
We remind the reader that a Recursive Program Schema (RPS) is a TRS
which has a finite set of function symbols $\{ F_1, \cdots, F_n \}$
(the ``unknown'' or user-defined functions) where $F_i$ has arity
$m_i$, and a disjoint set of basic function symbols $\{G_1, \cdots,
G_m \}$ (the ``known'' functions), where $G_j$ has arity $l_j$.  The
rewrite rules of a RPS have the form ${\sf F}_i^{m_i}(x_1, \cdots,
x_{m_i}) \reduce{}{} t_i , 1 \leq i \leq n$, where all variables $x_i,
1 \leq i \leq m_i$, are pairwise distinct and $t_i$ is an arbitrary
term built from variables and functions, $F_i, \cdots, G_j, \cdots$. 
Furthermore, for each $F_i$ there is exactly one rule.

\begin{lemma}
For any RPS term $M$, $M_\Omega$ is the stable prefix of $M$.
\end{lemma}
\begin{proof}
If $M_\Omega = \Omega$ then $M_\Omega$ is obviously stable. If
$M_\Omega \neq \Omega$ then $\forall N$ such that $M_\Omega
\leq_\omega N$, $N$ cannot be a redex at the root, in other words,
$M_\Omega$ is stable.
\end{proof}

\blank
\noindent
However, $M_\Omega$ is not necessarily the stable prefix for a TRS
term M\footnote{Private communication with Jean-Jacques L\'evy.}.
Consider the following rules: 
$$\begin{array}{lll}
\tau_1:\;\;{\sf A}(x) & \reduce{}{} & {\sf B}(x) \\
\tau_2:\;\;{\sf F}({\sf B}(x)) & \reduce{}{} & {\sf 0}
\end{array}$$
and the reduction 
$$ M \equiv {\sf F}({\sf A}(x))
\reduce{}{} N \equiv {\sf F}({\sf B}(x)) $$
$M_\Omega$ is ${\sf F}(\Omega)$, while $N_\Omega$ is $\Omega$, and
$M_\Omega \not\leq_{\sf \omega} N_\Omega$.  Thus, we erroneously assumed that ${\sf
F}(\Omega)$ is a stable prefix. A TRS differs from a RPS in that
even though the TRS term $F({\Omega})$ is not a redex it can become one
by increasing its information, for example, by substituting ${\sf
B}(x)$ for $\Omega$.  This phenomena is called the {\it upward
creation of redexes}.  Reduction of a term in the $\lambda$-calculus
can also result in the upward creation of redexes.  To cope with this
problem in the $\lambda$-calculus, Wadsworth\cite{Wadsworth} and
L\'evy\cite{Levy78b} had introduced the notion of an $\omega$-rule,
which reduces any term that can become a redex (by upward
creation) to $\Omega$. The $\omega$-rule for the $\lambda$-calculus
is 
$$\Omega \; M \reduce{}{} \Omega \enspace .$$ 
The $\omega$-rule associated
to $\tau_1$ and $\tau_2$ will be ${\sf F}(\Omega) \reduce{}{} \Omega$.
However, in the presence of non-left-linear rules it is difficult
to generate $\omega$-rules for a TRS as shown by the following example.
We remind the reader that non-left-linearity in a TRS is interpreted
as tree equivalence on terms. Now consider the TRS rule ${\sf F}(y,y)
\reduce{}{} y $. Suppose we generate  the following $\omega$-rules:
\[ \begin{array}{lll}
{\sf F}(\Omega,y) \reduce{}{} \Omega \\
{\sf F}(y,\Omega) \reduce{}{} \Omega 
\end{array}\]
then the term $M \equiv {\sf F}({\sf A}({\sf 0}),{\sf A}(\Omega))$ 
will be in stable form. However, it should not be
because by replacing $\Omega$ by ${\sf 0}$, $M$ becomes a redex.

\subsubsection{$\omega$-redex}
Non-left-linear rules constitute a problem for a GRS also.  Since we
want to include them in our analysis, we abandon the idea of generating
$\omega$-rules, and instead introduce a new notion of redex, called
{\it $\omega$-redex} \cite{Huet1}.  A
$\omega$-redex captures our intuition about why a term should be
rewritten to $\Omega$. It consists of analyzing a term to see if it
can become a redex by either replacing $\Omega$ with some other term
or by increasing the sharing in the term.  The stable part of a term
$M$ will be computed by first replacing all redexes in $M$ by
$\Omega$, and then by reducing all $\omega$-redexes to $\Omega$ .

Notice that we have taken a conservative approach in determining which
terms can become redexes; we may reduce to $\Omega$ some terms,
which may never
become a redex.  However, we also need to guarantee that
not too much information is lost.  Since the stable part will be a
part of our criteria for equating terms, we may end up equating far
too many terms and lose congruence. Clearly if we reduce everything
to $\Omega$, all terms will get equated and we will immediately have
an inconsistent model.  As we will see in Section \ref{secequality}, a
way of guaranteeing that not too much information is lost is by
showing that the behavior of a term $C[M]$ can be inferred from the
observations about $M$.  Consider the rules
\[ \begin{array}{l} 
\tau_1: \;\;  x={\sf F}(y,y) \reduce{}{} x = {\sf 4} \\
\tau_2: \;\; \frag{x_1={\sf F}(0,1)}
{x={\sf G}(x_1) \reduce{}{} x = {\sf 3}}
\end{array}
\]
and terms $M \equiv {\sf F}(0,1)$ and $N \equiv {\sf F}(2,1)$. Suppose we
compute the stable information of term $M$ by applying the (incorrect)
rule: $x={\sf F}(y_1,y_2) \reduce{}{} x = \Omega$.
Then both $\omega(M)$ and $\omega(N)$ will be $\Omega$ and
as such they will be equated. Now consider 
the  context $C[\Box] \equiv 
\{ t_1 = {\sf G}(t_2);\;\;t_2 = \Box; \; {\sf In} \; t_1 \}$.
$C[M]$ produces ${\sf 3}$ as a possible observation, while
$C[N]$ does not.
Thus, we erroneously equate terms which are not ``extensionally equal''.
It seems that we cannot discard any information that can be 
used to build terms. By treating $\omega(M)$ as $\Omega$
we discard too much information as can be seen by the fact that 
by plugging the observations of $M$ in
$C[\Box]$ we will not be able to observe ${\sf 3}$.

\subsection{$\omega$-reductions and its properties}
\begin{definition}[$\omega$-redex]
A $\omega$-redex in a GRS term $M$ in canonical form
is a pair $(\tau,z)$ such that
\begin{tightlist}
\item[(i)]
$\tau$ is a rule;
\item[(ii)]
$z \in {\tt BV}(M)$ and $z$ is not bound to $\Omega$;
\item[(iii)]
${\cal C}l(\tau) \uparrow_{\sf \omega} M @ z$ and
${\cal C}l(\tau) \not\leq_{\sf \omega} M @ z$.
\end{tightlist}
z is called the root of the $\omega$-redex.  If z is also the root
of the term $M$ then $M$ is said to be a $\omega$-redex.\\
The set containing the roots of all $\omega$-redexes is denoted
by $\Re_\omega(M)$.

\end{definition}
Notice that because of condition $({\it iii})$, a $\omega$-redex
cannot be an ordinary redex.
For the example given at the 
beginning of Section \ref{InstantandDynamicSemantics}, we have
that ${\cal C}l(\tau_1)\not\leq_{\sf \omega} M_2$ and 
${\cal C}l(\tau_1) \uparrow_{\sf \omega} M_2$,
thus, $M_2$ is a $\omega$-redex, and will be reduced
to $\Omega$ in computing the stable part of $M_2$.

\begin{definition}[Distinct $\omega$-redexes]
Two $\omega$-redexes $\rho_1 = (\tau_1, z_1)$ and
$\rho_2 = ( \tau_2, z_2)$ in a GRS term $M$
in canonical form are said to be distinct if
either $\tau_1 \neq \tau_2$ or $z_1 \neq z_2$.
\end{definition}

\begin{proposition}
\label{compprop}
Given GRS terms $M_1$ and $M_2$ in canonical form,
if $M_1 \leq_{\sf \omega} M_2$ then
\begin{tightlist}
\item[(i)]
if $M_2$ is a $\omega$-redex then $M_1$ is either
a $\omega$-redex or $\Omega$;
\item[(ii)]
if $M_2$ is a redex
then $M_1$ is either a redex, a $\omega$-redex or $\Omega$.
\end{tightlist}
\end{proposition}
\begin{proof}
$(i)$ From the definition of $\omega$-redex we have that $\exists$
$\tau$ such that $M_2 \uparrow_{\sf \omega} {\cal C}l(\tau)$.
Therefore, if $M_1$ is not $\Omega$ it must be a $\omega$-redex.  Analogously for point $(ii)$.
\end{proof}


\begin{definition}[$\omega$-reduction]
Given a GRS term $M$ in canonical form, $M$ $\omega$-reduces to $N$ by
doing the $\tau$ $\omega$-redex at $z$, written as 
$M \reduce{z}{\tau}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  N$,
iff $(\tau,z)$ is a $\omega$-redex in $M$
and $N \equiv {\tt GC}(M[z \leftarrow \Omega])$. A term is said to be
in $\omega$-normal form when it has no $\omega$-redexes.
\end{definition}
Note that since $\Omega$ is not a substitutable value,
$M[z \leftarrow \Omega]$ is in canonical form. 


\begin{definition}[Descendant of a $\omega$-redex with respect to
$\omega$-reduction]
\label{descendantcompredex}
Given two distinct $\omega$-redexes $\rho_1=(\tau_1,z_1)$ and
$\rho_2=(\tau_2,z_2)$ in a GRS term
$M$ in canonical form, 
the descendant of $\rho_2$ with respect to
the reduction
$M \reduce{\rho_1}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  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 pair
$\rho_2'=(\tau_2,z_2)$, if 
$z_2 \in {\tt BV}(M_1)$. 
\end{tightlist}
\end{definition}

The following proposition shows that,
given two distinct $\omega$-redexes $\rho_1$ and
$\rho_2$, even in the presence of interfering rules
$\rho_2 \setminus \rho_1$ is an $\omega$-redex if it exists.

\begin{proposition}
\label{preservingCRs}
Given $\omega$-redexes $\rho_1=(\tau_1,z_1)$
and $\rho_2 = (\tau_2,z_2)$
in a GRS term $M$ in canonical form, if 
$M \reduce{\rho_1}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  M_1$ and
$z_2 \in {\tt BV}(M_1)$ then either
$\rho_2 \setminus \rho_1$ is an $\omega$-redex or 
$z_2$ is bound to $\Omega$ in $M_1$.
\end{proposition}
\begin{proof}
Since $M_1 \equiv {\tt GC}(M [z_1 \leftarrow \Omega])$,
$M_1 \leq_{\sf \omega} M $.
Therefore, if $z_2 \in {\tt BV}(M_1)$ then
$M_1 @ z_2 \leq_{\sf \omega} M @ z_2$. 
Therefore, by Proposition \ref{compprop}, $\rho_2 \setminus \rho_1$ is either a
$\omega$-redex or $\Omega$.
\end{proof}



\noindent
The stable part of a term $M$, \ie $\omega(M)$,
will then be computed by first replacing all distinct redexes occurring in $M$
by $\Omega$  and then computing the $\omega$-normal form of the
term so obtained.
Before giving the formal definition of the $\omega$-function
we introduce some properties of $\omega$-redexes and
$\omega$-reduction.


\begin{theorem}[Subcommutativity of
$\reduces{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}$]
\label{subcomm}
Given two distinct $\omega$-redexes $\rho_1$ and
$\rho_2$ in a GRS term $M$
in canonical form, if 
$M \reduce{\rho_1}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; M_1 $
and $M \reduce{\rho_2}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; M_2 $,
then $\exists$ $M_3$ such that
$M_2 \reduce{\rho_1 \setminus \rho_2}{0/1}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; M_3 $ and 
$M_1 \reduce{\rho_2 \setminus \rho_1}{0/1}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; M_3 $.
\end{theorem}
\begin{proof}
Let $\rho_1=(\tau_1,z_1)$, $\rho_2=(\tau_2,z_2)$, and
$M_1 \equiv {\tt GC}(M[z_1 \leftarrow \Omega])$, 
$M_2 \equiv {\tt GC}(M[z_2 \leftarrow \Omega])$.
If $z_1 \equiv z_2$ then $M_1 \equiv M_2 \equiv M_3$.
If $z_1 \not\equiv z_2$ then the proof,
analogous to Theorem \ref{commutative}, is by cases on the
existence of $\rho_1 \setminus \rho_2$ and
$\rho_2 \setminus \rho_1$. We show the first two cases only.
\begin{mycases}
\item {$\rho_2 \setminus \rho_1 = (\tau_2, z_2)$ and 
$\rho_1 \setminus \rho_2 = (\tau_1, z_1).$ }\\
By Proposition \ref{preservingCRs} $\rho_1 \setminus
\rho_2$ and $\rho_2 \setminus \rho_1$
must be $\omega$-redexes. Thus,
we want to show the following:
$$ {\tt GC}( M_1[z_2 \leftarrow \Omega])
\equiv 
{\tt GC}(M_2[z_1 \leftarrow \Omega]).$$

We have
$$\begin{array}{lll}
& {\tt GC}( M_1[z_2 \leftarrow \Omega]) \\
\equiv & {\tt GC} (
{\tt GC}   (M[z_1\leftarrow \Omega ])
                       [z_2\leftarrow \Omega ]) &
\mbox{(by Proposition } \ref{garbage}) \\
\equiv & {\tt GC} ( M[z_1\leftarrow \Omega ] [z_2\leftarrow \Omega ])  &
\mbox{(by Proposition } \ref{repl}) \\
\equiv & {\tt GC} ( M[z_2\leftarrow \Omega ] [z_1\leftarrow \Omega ]) 
& \mbox{(by Proposition } \ref{garbage}) \\
\equiv & {\tt GC} (
{\tt GC}   (M[z_2\leftarrow \Omega ])
                       [z_1\leftarrow \Omega ])   \\
\equiv & 
{\tt GC}   (M_2 [z_1\leftarrow \Omega ])   \\
\end{array}$$

\item {$\rho_1 \setminus \rho_2 = (\tau_1, z_1) $ 
\mbox{ and } $\rho_2  \setminus \rho_1$ does not exist.}\\
We need to show
$$M_1 \equiv
 {\tt GC}(M_2 [z_1 \leftarrow \Omega]) \enspace . $$

We have
$$\begin{array}{lll}
&  {\tt GC}(M_2 [z_1 \leftarrow \Omega]) \\
\equiv & 
{\tt GC}( {\tt GC}( M[z_2 \leftarrow \Omega]) [z_1 \leftarrow \Omega]) \\
\equiv &
 {\tt GC}({\tt GC}(M[z_1 \leftarrow \Omega]) [z_2 \leftarrow \Omega])
& \mbox{(following the argument in Case 1)} \\
\equiv &
 {\tt GC}( M[z_1 \leftarrow \Omega]) &
\mbox{(since } z_2 \not\in M_1 
\mbox{ and } {\tt GC} \mbox{ is idempotent}) \\
\equiv & M_1
\end{array}$$
\end{mycases}
\end{proof}

\begin{corollary}
\label{omegaconf}
$\reduces{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}$ is confluent.
\end{corollary}

\begin{proposition}
$\reduces{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}$ is 
strongly normalizing.
\end{proposition}
\begin{proof}
Suppose there are $n$ function symbols in a term $M$.  Each
$\omega$-reduction gets rid off one function symbol and does not
introduce any new ones. Thus, the lenght of $\omega$-reductions on $M$
is bounded by $n$.
\end{proof}

\blank
Since $\omega$-reductions are strongly normalizing and confluent we
can now define the $\omega$-function as follows.

\begin{definition}[$\omega$-function]
Given a GRS term $M$, $\omega(M)$ is the
$\omega$-normal form of $M_\Omega$.
\end{definition}


\subsection{Interaction of $\omega$-reductions and normal
reductions}
In the following, we analyze the effect of $\omega$-reductions and
normal reductions on $\omega$-redexes and redexes, respectively.

\begin{definition}[Descendant of a redex with respect to
$\omega$-reduction]
\label{descendantredexp}
Given an $\omega$-redex $\rho_1=(\tau_1,z_1)$ and a redex
$\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}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  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 \\
\Omega & \sigma_2(x) =  z_1 \\
\end{array}
\right. $$
\end{tightlist}
\end{definition}

The following proposition shows that 
an $\omega$-reduction cannot destroy a redex in the absence of
interfering rules.

\begin{proposition}
\label{preservingredex}
Given an $\omega$-redex $\rho_1=(\tau_1,z_1)$
and a redex $\rho_2 = (\tau_2,z_2, \sigma_2)$
in a GRS$_{\sf NI}$ term $M$ in canonical form, if 
$M \reduce{\rho_1}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  M_1$
and $z_2 \in {\tt BV}(M_1)$  
%$z_2$ is not bound to $\Omega$ in $M_1$
then $\rho_2 \setminus \rho_1$ is a redex. 
\end{proposition}
\begin{proof}
If $z_2 \in {\tt BV}(M_1)$, let
$\rho_2 \setminus \rho_1= (\tau_2, z_2, \sigma_2')$.
If $\exists x , \sigma_2(x) \neq \sigma_2'(x)$,
by non-interference it
must be the case that $x \not\in {\tt BV}({\cal P}(\tau_2))$.
Moreover, suppose $\exists x \in {\tt BV}({\cal P}(\tau_2)),
\sigma_2'(x)$ does not occur in $M_1$,
it means that all paths from $z_2$ to $\sigma_2'(x)$ go through
$z_1$.
This means that $z_1 \in \{ \sigma_2(y) \mid 
y \in {\tt BV}({\cal P}(\tau_2)) \}$.
We reached a contradiction; therefore,
$\forall x \in {\tt BV}({\cal P}(\tau_2)), \sigma_2'(x) $ occurs in $M_1$.
Since the new definition of $z_1$ and the garbage collection
do not affect the substitution $\sigma_2'$, $\rho_2 \setminus \rho_1$ is a redex.
%As in Proposition 4.7  $\rho_2 \setminus \rho_1$ may not be a redex
%because of the new definition of $z_1$ or 
%$\exists x \in {\tt BV}({\cal P}(\tau_2))$
%such that $\sigma_2(x) \not\in {\tt BV}(M_1)$.
%Due to non-interference it must be the case that
%$z \in {\tt FV}({\cal P}(\tau_2))$.
%Moreover, everything accessible to $z_2$ must occur in $M_1$.
%Therefore,  $\rho_2 \setminus \rho_1$ is a redex.
\end{proof}

\begin{definition}[Descendant of an $\omega$-redex with respect to
reduction]
\label{descendantomegaredex}
Given a redex $\rho_1$ and an $\omega$-redex
$\rho_2=(\tau_2,z_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 pair $\rho_2'=(\tau_2,z_2)$, if 
$z_2 \in {\tt BV}(M_1)$. 
\end{tightlist}
\end{definition}

A reduction, however, can destroy an
$\omega$-redex even in the absence of interfering rules,
as shown in the example below.
Consider the rules
$$\begin{array}{llll}
\tau_1: & x={\sf F}(y,y,y) & \reduce{}{} & x= y\\
\tau_2: & x={\sf G}(0) & \reduce{}{} & x= 1\\
\end{array}$$
and the reduction
$$ M \equiv \{ 
\begin{array}[t]{l}
t_1= {\sf F}(t_2,t_3,t_4);\\
t_2= {\sf G}(0);\\
t_3= {\sf G}(\Omega);\\
t_4= {\sf G}(0);\\
\;\;{\sf In}\; t_1 \}
\end{array}
\reduce{t_2}{}
M_1 \equiv \{ \begin{array}[t]{l}
t_1= {\sf F}(1,t_3,t_4);\\
t_3= {\sf G}(\Omega);\\
t_4= {\sf G}(0);\\
\;\;{\sf In}\; t_1 \}
\end{array}$$
Note that the $\omega$-redex rooted at $t_1$ in $M$ is no longer
an $\omega$-redex in $M_1$. However, it can get restored by reducing the
redex rooted at $t_4$ and the $\omega$-redex rooted at $t_3$.
Equivalently, by setting $t_3$ and $t_4$ to $\Omega$,
respectively.

Before stating the property that $\omega$-redexes can be restored 
we need the  following proposition.


%\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{proposition}
\label{garbrepl}
Given GRS terms $M$ and $N$ in canonical form. If 
$M \leq_{\sf \omega} N$, let
$\rho=(\tau,z,\sigma)$ be a redex
in $M$  and $\rho_1 = (\tau,z_1,\sigma_1)$ be a redex in $N$ such that
$\sigma_{MN}(z)=z_1$ then  
$${\tt GC}(\overline{M [ z \leftarrow {\cal RHS}(\tau)^{\sigma}]}
[{\cal Z} \leftarrow \Omega] )
\leq_{\sf \omega} {\tt GC}(\overline{N[z_1 \leftarrow {\cal RHS}(\tau)^{\sigma_1}]})$$
where ${\cal Z} = 
\{ s \mid \sigma_{MN}(s)=z_1, s \not\equiv  z  \}$.
%and ${\cal Z}_\omega = \{ s \mid s \in \Re_\omega(M), \sigma_{MN}(s)=z_1 \}$.
\end{proposition}
\begin{proof}
We first show that the function 
$\sigma_{MN}$ restricted to the domain of variables occurring in
$ {\tt GC}(M[z \leftarrow \Omega][{\cal Z}
\leftarrow \Omega])$  induces the ordering:
$${\tt GC}(M[z \leftarrow \Omega][ {\cal Z} \leftarrow \Omega])
\leq_{\sf \omega} {\tt GC}(\overline{N[z_1 \leftarrow {\cal RHS}(\tau)^{\sigma_1}]})
\enspace .$$
Suppose it is not, then it must be the case
that for an element, say $x$, occurring in
the left-hand side term,
$\sigma_{MN}(x)$ does not occur in the right-hand side term.
This means that the replacement of the term
bound to $z_1$ in $N$ by ${\cal RHS}(\tau)^{\sigma_1}$
has removed the path to $\sigma_{MN}(x)$. However, this
means that the corresponding path in $M$ also gets removed
by setting $z$ and all the elements of ${\cal Z}$ to $\Omega$.
Contradiction. Therefore it must be the case that
$\sigma_{MN}(x) $ occurs in
${\tt GC}(\overline{N[z_1 \leftarrow
{\cal RHS}(\tau)^{\sigma_1}]})$.

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

\begin{proposition}
\label{preservingomegaredex}
Given a redex $\rho_1=(\tau_1,z_1,\sigma_1)$
and an $\omega$-redex $\rho = (\tau,z)$
in a GRS$_{\sf NI}$ term $M$ in canonical form, if 
$M \reduce{\rho_1}{}  M_1$
and $z \in {\tt BV}(M_1)$  
%$z$ is not bound to $\Omega$ in $M_1$
then $\rho \setminus \rho_1$ is either 
an $\omega$-redex or it can become so after having 
perfomed some $\omega$-reductions
on ${M_1}_\Omega$.
%In other words, $\exists M_n,
%M_1 \reduce{\rho_2}{}
%%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  
%M_2 \reduce{\rho_3}{}
%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  
%M_3 \cdots
%\reduce{}{}
%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  
%M_{n-1}
%\reduce{\rho_n}{} M_n$, and
%$\rho \setminus 
%(\rho_1 \cup \rho_2 \cdots \rho_n)$ is an $\omega$-redex.
\end{proposition}
\begin{proof}
Since $\rho$ is an $\omega$-redex, $\exists N,
M \leq_{\sf \omega} N$
such that $\sigma_{MN}(z)$ is the root of a $\tau$-redex in $N$.
%where $\sigma_{MN}$ is the induced substitution function.
Let $z_1' = \sigma_{MN}(z_1)$ be the root
of the redex $(\tau_1,z_1',\sigma_1')$,
and let $N_1$ be such that $N \reduce{z_1'}{} N_1$.
Let ${\cal Z} =
\{ z' \mid  \sigma_{MN}(z') =z_1', 
z' \mbox{ is not bound to } \Omega, z' \not\equiv z_1 \}$.
%Let ${\cal Z}_\omega =
%\{ z' \mid
%z \in \Re_\omega(M), \sigma_{MN}(z') =z_1',
%z' \not\equiv z_1 \}$.
By Proposition \ref{garbrepl} we have
$${\tt GC}(M_1 [{\cal Z} \leftarrow \Omega])
%[ {\cal Z}_\omega \leftarrow \Omega])
\leq_{\sf \omega} 
{\tt GC} (\overline{N[z_1' \leftarrow {\cal RHS}(\tau_1^{\sigma_1'})] } )
\equiv N_1$$
Moreover, by Proposition
\ref{propinterf} the descendant of the redex rooted at $\sigma_{MN}(z)$
in $N$ must be a redex in $N_1$. Therefore,
by Proposition \ref{compprop}
we have that $\rho \setminus \rho_1$ must be either a redex,  an
$\omega$-redex or $\Omega$ in 
${\tt GC}(M_1 [{\cal Z} \leftarrow \Omega])$.
%[ {\cal Z}_\omega \leftarrow \Omega])$
By non-interference it follows that 
the only condition applicable is for
$\rho \setminus \rho_1$ to be an $\omega$-redex in
${\tt GC}(M_1 [{\cal Z} \leftarrow \Omega])$. The result then
follow from the fact that ${\cal Z} \subseteq 
\Re(M) \cup \Re_\omega(M)$.
%[ {\cal Z}_\omega \leftarrow \Omega])$,
%or equivalently in
%${M_1}_{\Omega}$.
%The result then follows from the fact that the term
%${\tt GC}(\overline{M_1 [{\cal Z} \leftarrow {\cal RHS}^{\sigma'}]}
%[ {\cal Z}_\omega \leftarrow \Omega])$
%can be obtained by performing a complete development of
%redexes in ${\cal Z}$ and by $\omega$-reducing the
%$\omega$-redexes in ${\cal Z}_\omega$.
\end{proof}


%\begin{proposition}
%\label{commomegared}
%Given an $\omega$-redex $\rho_1$ and a redex
%$\rho_2$ in a GRS$_{\sf NI}$ term $M$ in canonical form,
%if $M \;\; \reduce{\rho_1}{}
%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  
%M_1 $ and $M \reduce{\rho_2}{} N$, then
%$\exists N', P,
%N \reduces{}{} {\hspace{-0.9mm}\vspace{-0.6mm}_\omega} N'$,
%$N' \reduces{}{} P$ and
%%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  P$ and
%$M_1 \reduces{}{} P$.
%\end{proposition}
%\begin{proof}
%By cases on the existence of the descendant of 
%$\rho_1$ and $\rho_2$.
%\begin{mycases}
%\item {$\rho_1 \setminus \rho_2 = (\tau_1,z_1)$
%and $\rho_2 \setminus \rho_1 = (\tau_2, z_2, \sigma_2)$.}
%By Proposition \ref{preservingredex}, $\rho_2 \setminus \rho_1$ must be
%a redex. Therefore we will only consider the following cases:
%\begin{mysubcases}
%\item {$\rho_1 \setminus \rho_2$ is an $\omega$-redex  and
%$\rho_2 \setminus \rho_1$  is a redex}\\
%Similar argument as in Theorem \ref{commutative}.
%\item {$\rho_1 \setminus \rho_2$ is not an $\omega$-redex  and
%$\rho_2 \setminus \rho_1$  is a redex.}\\
%Follows from Proposition \ref{preservingomegaredex}.
%\end{mysubcases}
%\item {$\rho_1 \setminus \rho_2$ does not exist  and
%$\rho_2 \setminus \rho_1 = (\tau_2,z_2,\sigma_2)$. }
%Follows from Proposition
%\ref{preservingredex}.
%%\begin{mysubcases}
%%\item {$\rho_1 \setminus \rho_2$ is an $\omega$-redex} 
%%\item {$\rho_1 \setminus \rho_2$ is not an $\omega$-redex} 
%%\end{mysubcases}
%\item {$\rho_1 \setminus \rho_2=(\tau_1,z_1)$ and
%$\rho_2 \setminus \rho_1$ do not exist.} 
%Follows from Proposition 
%\ref{preservingomegaredex}.
%\item {$\rho_1 \setminus \rho_2$ and
%$\rho_2 \setminus \rho_1$ do not exist.} 
%As in Theorem \ref{commutative} this case cannot arise.
%\end{mycases}
%\end{proof}
%
%\begin{proposition}
%\label{commomegared1}
%Given a GRS$_{\sf NI}$ term $M$ in canonical form,
%if $M \reduces{}{}
%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;  
%M_1 $ and $M \reduces{}{} N$, then
%$\exists N', P,
%N \reduces{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} N'$, 
%$N' \reduces{}{}  P$ and
%$M_1 \reduces{}{} P$.
%\end{proposition}
%\begin{proof}
%By induction on the lenght of the reductions
%$M \reduces{}{}
%{\hspace{-0.9mm}\vspace{-0.6mm}_\omega} \;   M_1$ and 
%$M \reduces{}{} N$.
%\end{proof}
%
%
%

We now discuss two additional properties
of the $\omega$-function, that are, its  monotonicity with respect 
to $\leq_{\sf \omega}$, and with respect to reduction. These will be very
useful in later proofs.

\begin{proposition}[Monotonicity of $\omega$-function
with respect to $\leq_{\sf \omega}$]
\label{incnew}
Given GRS terms $M$ and $N$ in canonical form,
if $M \leq_{\sf \omega} N$ then 
$\omega(M) \leq_{\omega} \omega(N)$.
\end{proposition}
\begin{proof}
Let ${\cal Z}=\{ z \mid \sigma_{MN}(z) \in \Re(N) \cup \Re_\omega(N),
z \mbox{ is not bound to } \Omega \}$.
%, and
%${\cal Z}_\omega = \{ z \mid \sigma_{MN}(z) \in \Re_\omega(N),
%z \mbox{ is not bound to } \Omega \}$.
From Proposition \ref{garbrepl},
$$ {\tt GC}(M[{\cal Z} \leftarrow \Omega])
 \leq_{\sf \omega} \omega(N_\Omega) = \omega(N)
\enspace .$$


%%% ARVIND
%$( {\cal Z} \cup {\cal Z}' )  \subseteq (\Re(M) \cup \Re_\omega(M)$)
%by Proposition  \ref{compprop}. The descendants of redexes
%in $\Re(M) - {\cal Z}$ and $\omega$-redexes
%in $\Re_\omega(M) - {\cal Z}'$  can only be ``denoted'' to
%$\Omega$ or $\omega$-redexes in
%${\tt GC}(M[{\cal Z} \leftarrow \Omega][{\cal Z}' \leftarrow \Omega]$)
%by
%Propositions \ref{preservingCRs} and \ref{preservingCRs1},
%we have:
%$$\omega(M) \leq_{\sf \omega}
%{\tt GC}(M[{\cal Z} \leftarrow \Omega][{\cal Z}' \leftarrow \Omega])
%\leq_{\sf \omega} \omega(N).$$

By Proposition  \ref{compprop}, 
${\cal Z}   \subseteq (\Re(M) \cup \Re_\omega(M)$).
Therefore, we have
%by Proposition \ref{preservingCRs} we have:
$$\omega(M) \leq_{\sf \omega}
{\tt GC}(M[{\cal Z} \leftarrow \Omega])
\leq_{\sf \omega} \omega(N).$$
\end{proof}

\begin{proposition}[Monotonicity of $\omega$-function with respect
to reduction]
\label{monoreduction}
Given GRS terms $M$ and $N$ in canonical form,
if $M \reduces{}{} N$ then 
$\omega(M) \leq_{\omega} \omega(N)$.
\end{proposition}
\begin{proof}
The proof is by induction on the number  of reduction steps.
Suppose $M \reduce{\rho}{} N$, where
$\rho=(\tau,z,\sigma)$, then $N \equiv {\tt GC}(\overline{M[z \leftarrow P]})$, 
for some term $P$.
Since $\omega(M) = \omega({\tt GC}(M[z \leftarrow \Omega]))$
and ${\tt GC}(M[z \leftarrow \Omega])
\leq_{\sf \omega} {\tt GC}(\overline{M[z \leftarrow P]})$, 
then from the monotonicity of the $\omega$-function with respect
to $\leq_{\sf \omega}$
(Proposition \ref{incnew}) we have that
$\omega(M) \leq_{\sf \omega} \omega(N)$.  The result then follows 
by induction.
\end{proof}

%However, 
%the descendant of a $\omega$-redex with respect to
%a normal reduction is not necessarily a $\omega$-redex,
%for that to hold we need to impose the restriction of
%non-interference.
%\begin{proposition}
%\label{preservingomegaredex}
%Given a redex $\rho=(\tau,z)$ in a GRS$_{\sf NI}$
%term $M$ in canonical form, if 
%$M \reduce{\rho}{} \;  M_1$
%then $\forall$ $\omega$-redexes $\rho'=(\tau',z')$, $z' \neq z$,
%if $z' \in {\tt BV}(M_1)$ then 
%$\rho' \setminus \rho$ is a $\omega$-redex in $M_1$.
%\end{proposition}
%\begin{proof}
%If $\rho' \setminus \rho$ is not a $\omega$-redex, then
%it must be the case that the $\rho$-reduction can destroy a redex instead.
%Contradicting Proposition \ref{propinterf}.
%\end{proof}



\subsection{Meaning of a GRS term}
We collect all observable information about GRS terms
in a set called $\omega$-graphs. 

\begin{definition}[$\omega$-graphs: Set of observations]
Given a GRS, the set of all observations, called
$\omega\mbox{-}graphs$, is defined as:
$$\omega\mbox{-}graphs = \{ \omega(M) \mid \forall 
\mbox{ GRS terms } M \}.$$
\end{definition}

\noindent
We would like to define the meaning of a term $M$ as the limit of the set 
of our observations, that is, $\{\omega(M') \mid M \reduces{}{} M' \}$.
However, $\omega\mbox{-}graphs$
does not guarantee the existence of such a limit. 
Therefore, we apply the {\em ideal completion} method to turn
$\omega$-$graphs$ into a complete partial order \cite{Hennessy}.
Given a partial order $(A,\leq)$, a subset $D$ of $A$ is
an {\em ideal} iff $(i)$
$D$ is non-empty.
$(ii)$
$\forall a,b \in D, \exists c \in D,
a \leq c \mbox{ and } b \leq c $,
$(iii)$
$\forall c \in D,
\mbox{ if } \exists d \in A, d \leq c \mbox{ then }
d \in D$.

\begin{definition}[$\omega\mbox{-}graphs^\infty$:
Domain of observations]
Given a GRS, the domain of observations, called
$\omega\mbox{-}graphs^\infty$,
is the ideal completion of $\omega$-graphs, that is: 
$$\omega\mbox{-}graphs^\infty = \{ I \mid I \subseteq
\omega\mbox{-}graphs \mbox{ and } I \mbox{ is an ideal }\}.$$
\end{definition}

\noindent
To reflect this
change in our domain of observations, 
we include all $\omega\mbox{-}graph$ terms smaller than $\omega(M)$
in our observations as follows.

\begin{definition}[$W^*$: The information content of a GRS term]
Given a GRS term $M$ in canonical form, 
$W^*(M)= \{ a \mid a \in \omega\mbox{-}graphs,
a \leq_{\sf \omega} \omega(M'), M \reduces{}{} M' \}.$
\end{definition}


\noindent
We need to define under what conditions $W^*(M)$ is an element of
$\omega\mbox{-}graphs^\infty$, that is, $W^*(M)$ is an ideal.  

\begin{proposition}[$W^*(M)$ is an ideal for GRS$_{\sf C}$]
For all GRS$_{\sf C}$ terms $M$, $W^*(M)$ is in $\omega\mbox{-}graphs^\infty$.
\end{proposition}
\begin{proof}
\mbox{                                                             }
\begin{tightlist}
\item[(i)]
$W^*(M)$ is not empty since  it contains at least
$\Omega$;
\item[(ii)]
We show that $W^*(M)$ is a directed set,
that is, $\forall a,b \in W^*(M)$, $\exists c$, such that $a \leq_{\sf \omega} c $
and $b \leq_{\sf \omega} c$. 
If $a \in W^*(M)$, it means that $\exists M_1$, such that
$M \reduces{}{} M_1$ and $a \leq_{\sf \omega} \omega(M_1)$.
Analogously, $\exists M_2, M \reduces{}{} M_2$ and $b \leq_{\sf \omega}
\omega(M_2)$. 
Follows from the confluence of $\reduces{}{}$ that $\exists M_3$,
$M_1 \reduces{}{} M_3$ and $M_2 \reduces{}{} M_3$.
Moreover,
from the monotonicity of the
$\omega$-function with respect to $\reduces{}{}$ (Proposition
\ref{monoreduction}) we have
$$ a \leq_{\sf \omega} \omega(M_3)
\mbox{ and } b \leq_{\sf \omega } \omega(M_3) $$
that is, $\omega(M_3)$ is the element we were looking for.
\item[(iii)]
$W^*(M)$ is closed downwards by definition.
\end{tightlist}
\end{proof}

\blank
Let's now define a semantic ordering based on the information content.
\begin{definition}[$\sqsubseteq_{\sf g}$: Information ordering]
Given GRS terms $M$ and $N$ in canonical form, $M \sqsubseteq_{\sf g} N$ 
iff $W^*(M) \subseteq W^*(N).$ If $M \sqsubseteq_{\sf g} N$ and
$N \sqsubseteq_{\sf g} M$ then $M \equiv_{\sf g} N$. 
\end{definition}

\noindent
If we want $W^*$ to be our interpretation function, $W^*$ will have to
satisfy some properties, that is, the meaning will have to be
preserved by reduction, and it will have to be compositional.
In other words,

\[ \begin{array}{lllll}
{\bf Soundness:} & M \reduces{}{} N & \Longrightarrow & M \equiv _{\sf g} N \\
{\bf Congruence:} & M \equiv_{\sf g} N &  \Longrightarrow &
C[M]  \equiv _{\sf g} C[N]  \enspace .
\end{array}
\]

We will first show the soundness, and then later come back to a discussion of
congruence after a digression on the impact of sharing on the meaning 
function.

\begin{proposition}[Soundness of $\equiv_{\sf g}$]
\label{soundW}
Given GRS$_{\sf C}$ terms $M$ and $N$ in canonical form,
if $M \reduces{}{} N$ then $M \equiv_{\sf g} N$.
\end{proposition}
\begin{proof}
Trivially, $N \sqsubseteq_{\sf g} M$.  Next, we prove that 
$M \sqsubseteq_{\sf g} N$.  Let $P \in W^*(M)$, it means that 
$\exists M_1, M \reduces{}{} M_1$ and $P\leq_{\sf \omega} \omega(M_1)$.  
From the confluence of $\reduces{}{}$ we know that 
$\exists M_2, M_1 \reduces{}{} M_2$ and $N \reduces{}{} M_2$. 
From the monotonicity of the $\omega$-function with respect to reduction 
(Proposition \ref{monoreduction}), we have that 
$P \leq_{\sf \omega} \omega(M_1) \leq_{\sf \omega} \omega(M_2)$.
Since $\omega(M_2) \in W^*(N)$, then $P \in W^*(N)$ as well.
\end{proof}

\subsection{Impact of sharing on program behavior}
What is  
the impact of sharing on  program behavior, that is,
\[ M \leq_{\sf \omega} N \Longrightarrow M \sqsubseteq_{\sf g} N \; ? \]
It turns out that in the presence of interfering rules the above will
not hold. Consider the following GRS which has {\it confluent} but
interfering rules:
\[ \begin{array}{l}
\tau_1: \;\; \frag{x_1={\sf B}({\sf 0});  \;
x_2={\sf C}({\sf 0})}
{x= {\sf A}(x_1,x_2) \reduce{}{} x = {\sf 0}}\\
\tau_2: \;\; x={\sf C}({\sf 0}) \reduce{}{} x = {\sf B}({\sf 0})\\
\tau_3: \;\; x={\sf B}({\sf 0}) \reduce{}{} x = {\sf C}({\sf 0})
\end{array}
\]
and the following terms:
\[ \begin{array}{lll}
M \equiv \{ \begin{array}[t]{l}
t_1={\sf A}(t_2,t_3);\\
t_2={\sf B}({\sf 0});\\
t_3={\sf B}({\sf 0});\\
\;\; {\sf In} \; t_1 \}
\end{array} & \hspace{1cm}
N \equiv \{ \begin{array}[t]{l}
t_1={\sf A}(t_2,t_2);\\
t_2={\sf B}({\sf 0});\\
\;\; {\sf In} \; t_1 \}
\end{array}
\end{array} \]
then, it is easy to see that
$W^*(M)=\{\Omega, {\sf 0} \}$,
while $W^*(N)=\{\Omega, \{x_1=\Omega; \; x_2={\sf A}(x_1,x_1) ;
\; {\sf In} \; x_2 \}\}$. Therefore, $M \leq_{\sf \omega} N$ and 
$M \not\sqsubseteq_{\sf g} N $.
However, there is no such problem for a GRS without
interfering rules.

\begin{theorem}[Monotonicity of $\sqsubseteq_{\sf g}$ with respect
to $\leq_{\sf \omega}$]
\label{inc1}
Given GRS$_{\sf NI}$ terms $M$ and $N$ in canonical form,
if $M \leq_{\sf \omega} N$ then $M \sqsubseteq_{\sf g} N$.
\end{theorem}
\begin{proof}
We prove that if $M \reduces{}{} M'$, then $\exists N'$ such that
$N \reduces{}{} N'$ and $\omega(M') \leq_{\sf \omega} \omega(N')$.
The proof is by induction on the number of reduction steps of 
$M \reduces{}{} M'$.

Let $M \reduce{\rho}{} M_1$, where $\rho =(\tau,z,\sigma)$.  
Then
$\rho' = (\tau,z', \sigma')$,
where $z' = \sigma_{MN}(z)$, and 
$\sigma' = \sigma_{MN} \circ \sigma$, is a redex in $N$.
Let $N \reduce{\rho'}{} N_1$, and 
${\cal Z}=\{ s \mid \sigma_{MN}(s)=z', s \mbox{ not bound to } \Omega,
s \not\equiv z \}$.
That is, ${\cal Z}$ 
is the set of all variables in $M$, distinct from $z$,
which are 
mapped into $z'$.
From Proposition \ref{garbrepl}, 
$${\tt GC}(\overline{M[z \leftarrow {\cal RHS}(\tau)^\sigma]}[{\cal Z} \leftarrow \Omega] )
\leq_{\sf \omega} {\tt GC}(\overline{N[z' \leftarrow {\cal RHS}(\tau)^{\sigma'}]})
\equiv N_1.$$
%
%$${\tt GC}({\tt GC}(\overline{M[z \leftarrow \Omega ]})[{\cal Z}
%\leftarrow \Omega] ) \leq_{\sf \omega}
%{\tt GC}(\overline{N[z' \leftarrow r^{\sigma'}]})$$
%where $r = {\cal RHS}(\tau)$. 
%
%Moreover, 
%for all elements $x$ in
%${\tt BV}(r^\sigma)$, 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}(r^\sigma)
%\end{array}
%\right.$$
%determines the ordering:
%$${\tt GC}({\tt GC}(\overline{M[z \leftarrow r^\sigma]})[{\cal Z} \leftarrow \Omega] )
%\leq_{\sf \omega} {\tt GC}(\overline{N[z' \leftarrow r^{\sigma'}]})
%\equiv N_1.$$
%
By Proposition \ref{compprop}, ${\cal Z} \subseteq
\{ \Re(M) \cup \Re_\omega(M) \}$. 
Therefore, 
$$ \omega(M_1) =
\omega({\tt GC}(\overline{M[z \leftarrow {\cal RHS}(\tau)^\sigma]}[{\cal Z} \leftarrow \Omega])).$$
Therefore, by monotonicity of the $\omega$-function
with respect to $\leq_{\sf \omega}$ (Proposition \ref{incnew}) we have
$$ \omega(M_1) \leq_{\sf \omega} \omega(N_1).$$
Notice that any redex in $M_1$, that does not belong
to ${\cal Z}$, is a redex in 
${\tt GC}(M_1[{\cal Z} \leftarrow \Omega])$
(Proposition \ref{propinterf}), and
therefore it must be a redex in $N_1$.  The result then follows by induction.
\end{proof}


\blank
\noindent
This theorem leads to a simple but powerful result regarding
the behavior of terms obtained by plugging terms related by sharing
into any context.
\begin{corollary}
\label{monomega}
Given GRS$_{\sf NI}$ terms $M$ and $N$, if $M \leq_{\sf \omega} N$
then $\forall C[\Box]$, $C[M] \sqsubseteq_{\sf g} C[N].$
\end{corollary}
\begin{proof}
It follows from the fact that
if $M \leq_{\sf \omega} N$  then 
$C[M] \leq_{\sf \omega} C[N]$.
\end{proof}

\noindent
It will be shown later this result can be applied in a straightforward manner to show
the partial correctness of those compiler optimizations that simply
increase the sharing in a term.
%Examples of such optimizations
%include the common subexpression elimination, and the lifting of free
%expressions and loop invariants.


\subsection{Congruence}
\label{secequality}
Consider the rule
$$\tau: \;x= {\sf F} (y)  \reduce{}{} x= \{
t = {\sf F}(y) ;\; t_1={\sf Cons}(y,t);\;{\sf In} \; t_1 \}$$
and the following two terms:
$$\begin{array}{ll}
M \equiv \{ x =  {\sf Cons}(1, x); \;{\sf In} \; x \} 
& \hspace{2cm}  N \equiv \{ x = {\sf F}(1); \; {\sf In} \; x \}
\enspace . \\
\end{array}$$
Notice that $N \not\leq_{\sf \omega} M$, but given the chain: 
$$ N \reduce{}{} N_1 \reduce{}{} N_2 \reduce{}{} \cdots \reduce{}{}
N_i \reduce{}{} \cdots  $$
where $N_i \equiv
\{ t_0= {\sf F}(1);
t_1= {\sf Cons}(1,t_0);
\cdots ;
t_i= {\sf Cons}(1,t_{i-1}); \; {\sf In} \; t_i \}$,
we have that
$$\omega(N) \leq_{\sf \omega} 
\omega(N_1) \leq_{\sf \omega}  \cdots \leq_{\sf \omega} 
\omega(N_i) \leq_{\sf \omega} \cdots \leq_{\sf \omega} M. $$
In fact, using induction on $i$ we can show that $N \sqsubseteq_{\sf g} M$,
and one would correctly guess that 
$\forall C[\Box], \;\; C[N] \sqsubseteq_{\sf g} C[M]$. 
However, this does not follow from 
Corollary \ref{monomega}.
We need to show that 
$\sqsubseteq_{\sf g}$ is a congruence relation. 
Note that terms like $M$ and $N$
arise in the cyclic implementation of recursive rules,
such as the ${\sf Y}$-rule. 


%%%% ZENA THIS IS WITH SUBSTITUTION ALSO
%%%%\noindent
%%%%Notice that we require a substitution function also because
%%%%our context forming operation is not powerful enough.
%%%%In particular it does not allow a ground instantiation of a term,
%%%%the problem is due to our canonicalization procedure.
%%%%Consider, for example, the context:\\
%%%%\[ \{ \begin{array}[t]{l}
%%%%x = {\sf +}(3,3);\\
%%%%y = x ;\\
%%%%z = \Box \\
%%%%\;\; {\sf In} \; z \}
%%%%\end{array} 
%%%%\]
%%%%then by plugging ${\sf +}(y,y)$ in $C[\Box]$ we will obtain the
%%%%term:
%%%%\[ \{ \begin{array}[t]{l}
%%%%x = {\sf +}(3,3);\\
%%%%z = {\sf +}(y,y)\\
%%%%\;\; {\sf In} \; z \}
%%%%\end{array} 
%%%%\]
%%%%and not the term:
%%%%\[ \{ \begin{array}[t]{l}
%%%%x = {\sf +}(3,3);\\
%%%%z = {\sf +}(x,x)\\
%%%%\;\; {\sf In} \; z \}
%%%%\end{array} 
%%%%\]
%%%%\noindent
%%%%An example which clarifies why our context forming operation is
%%%%not sufficient to guarantee congruence, follows.
%%%%Consider the rules:
%%%%\[ \begin{array}{lll}
%%%%x={\sf F}({\sf 2}) & \reduce{}{} & x={\sf 3}\\
%%%%x={\sf F}(X) & \reduce{}{} & x= {\sf F}(X)\\
%%%%x={\sf G}({\sf 2}) & \reduce{}{} & x={\sf 4}\\
%%%%x={\sf G}(X) & \reduce{}{} & x= {\sf G}(X)\\
%%%%\end{array}\]
%%%%and the following terms:
%%%%\[ \begin{array}{ll}
%%%%M \equiv \{
%%%%\begin{array}[t]{l}
%%%%t = {\sf G}(x)\\
%%%%\;\; {\sf In} \; t \}
%%%%\end{array} & 
%%%%N \equiv \{ 
%%%%\begin{array}[t]{l}
%%%%t_1 = {\sf F}(x)\\
%%%%\;\; {\sf In} \; t_1 \}
%%%%\end{array} 
%%%%\end{array}  \]
%%%%then, we have:
%%%%$$ M \equiv_{\sf g} N \mbox{  and  }
%%%%\forall C[\Box], \; C[M] \equiv_{\sf g} C[N].$$
%%%%However, by letting $\sigma(x)={\sf 2}$ we obtain:
%%%%$$ M \not\equiv_{\sf g} N \mbox{  because  }
%%%%W^*(M)=\{\Omega,{\sf 4} \} \mbox{  and  }
%%%%W^*(N)=\{\Omega,{\sf 3} \}.\]
%%%%
%%%%%\noindent
%%%%%We will see that the proof of
%%%%%$$ M^\sigma \equiv_{\sf g}
%%%%%\bigsqcup \{ P^\sigma \mid P \in W^*(M) \}$$
%%%%%will be the same than for the context.
%%%%

A way of assuring that $\sqsubseteq_{\sf g}$ is a congruence is to show
that the behavior of $C[M]$, for any context $C[\Box]$, can be
inferred from the observations about $M$, that is, 
$$\forall C[\Box], \;\; C[M] \equiv_{\sf g}
\bigsqcup \{C[P] \mid  P \in W^*(M) \}.$$
In other words, the context should be a 
{\it continuous} operation with respect to our observations.
(Notice that $W^*(\bigsqcup \{C[P] \mid  P \in W^*(M) \}) =
\bigcup \{ W^*(C[P]) \mid P \in W^*(M) \}$.)

\blank
\noindent
We will first prove
$$ \forall C[\Box], \;\; \bigsqcup \{C[P] \mid  P \in W^*(M) \}
\sqsubseteq_{\sf g} C[M] $$
that is, by plugging the observations of $M$ in the context we do not
produce more information than the one contained in $C[M]$.

\begin{lemma}
\label{infoinM}
Given a GRS$_{\sf NI}$ term $M$
and context $C[\Box]$, $\bigsqcup \{C[P] \mid  P \in W^*(M)\}
\sqsubseteq_{\sf g} C[M].$
\end{lemma}
\begin{proof}
Suppose $M \reduces{}{} M'$, then $\forall P$,
$P \leq_{\sf \omega} \omega(M')$ we have
\[ \begin{array}{lll}
P & \leq_{\sf \omega}  M'  & \\
C[P] & \sqsubseteq_{\sf g}  C[M'] & \mbox{(by monotonicity of
$\sqsubseteq_{\sf g}$ with respect to $\leq_{\sf \omega}$}
\mbox{ (Corollary \ref{monomega}))} \\
& \equiv_{\sf g} C[M] & \mbox{(by soundness of  }\equiv_{\sf g}
\mbox{(Proposition \ref{soundW}))} \enspace .
\end{array} \]
\end{proof}

\noindent
The other direction
$$ \forall C[\Box], \;\; C[M] \sqsubseteq_{\sf g}
\bigsqcup \{C[P] \mid  P \in W^*(M) \} $$
requires some more machinery.  We want to show that each observation
of $C[M]$ can be obtained by first observing $M$ and then plugging
those observations instead of $M$ in the context.  The proof has
two basic steps.  First we show that each reduction sequence $C[M]
\reduces{}{} N$ can be reordered, such that, if the sequence contains any 
redexes that are descendants of redexes in $M$ then in the reordered
sequence these redexes are performed before all others. 
Second, we show that the $\omega$-function does
not lose too much information.  Since the $\omega$-function involves
two steps -- first computing $M_\Omega$ and then applying
$\omega$-reductions -- we will analyze the impact of these steps
separately.  

In the following, we will use the notation $M$ \ioreduces{{\cal Z}(M)} $N$, 
where ${\cal Z}(M) \subseteq \Re(M)$,
to mean that no descendant of
redexes in ${\cal Z}(M)$ is reduced. 

\begin{proposition}
\label{insidered}
Given a GRS$_{\sf NI}$ term $M$ in canonical form,
if $C[M] \reduces{}{} N$ then $\exists M'$,
$M \reduces{}{} M'$ and $C[M']$ \ioreduces{\Re(M')} $N$.
\end{proposition}
\begin{proof}
Let ${\cal Z}(M)$ be the set of redexes in  $M$
contracted during the reduction
$C[M] \reduces{}{} N$, that is,
$ {\cal Z}(M) =
\{ z \in {\tt BV}(M) \mid  
\exists i, C[M] \reduces{}{} N_i \reduce{z}{} N_{i+1} 
\reduces{}{} N \}$.
%where $\rho'$ is a descendant of $\rho$.
Then by the subcommutative property of GRS$_{\sf NI}$ (Theorem \ref{commutative}),
$\exists M', C[M] \reduce{cd({\cal Z}(M))}{} C[M']$ and 
$C[M']$ \ioreduces{\Re(M')} $N$, where $cd({\cal Z}(M))$ denotes a complete 
development with respect to ${\cal Z}(M)$.
\end{proof}

\begin{proposition}
\label{commuOmega}
Given a GRS$_{\sf NI}$ term $M$ in canonical form,
if $M$ \ioreduces{{\cal Z}(M)} $N$ then
${\tt GC}(M[{\cal Z}(M) \leftarrow \Omega])
\reduces{}{} {\tt GC}(N[{\cal Z}(M) \leftarrow \Omega])$.
%where redexes in ${\cal Z}'$ are the descendant of redexes in ${\cal Z}$.
\end{proposition}
\begin{proof}
Follows from Proposition \ref{propinterf}.
\end{proof}

%\begin{theorem}[Subcommutativity of $\reduce{}{} \cup
%\reduce{}{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}$]
%\label{subcommomega}
%Given a redex $\rho_1$ a $\omega$-redex $\rho_2$ in a GRS$_{NI}$ term $M$
%in canonical form, if 
%$M \reduce{\rho_1}{} \; M_1 $
%and $M \reduce{\rho_2}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; 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}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; M_3 $.
%\end{theorem}
%\begin{proof}
%By applying the same reasoning as in
%Theorems \ref{commutative} and \ref{subcomm}. 
%\end{proof}


\begin{proposition}
\label{omegamean}
Given GRS$_{\sf NI}$ terms $M$ and $N$, if
$M \reduces{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; N$ 
then $M \equiv_{\sf g} N$.
\end{proposition}
\begin{proof}
Since $N \leq_{\sf \omega} M$, and by monotonicity of $\sqsubseteq_{\sf g}$ 
with respect to $\leq_{\sf \omega}$
(Theorem  \ref{inc1}),
we have that $N \sqsubseteq_{\sf g} M$.
In order to prove the other direction let 
$M \reduces{}{} M_1$ by reducing redexes in ${\cal Z}$.
From  Proposition \ref{preservingredex},
$\omega$-reductions do not destroy redexes, therefore, 
$\exists N_1, N \reduces{}{} N_1$ by reducing the descendants of
redexes in ${\cal Z}$. The result then follows from
Proposition \ref{preservingomegaredex}.
%is still a redex in $N$. Thus, $\exists N_1, N \reduce{}{} N_1$.
%We then have that $\omega(M_1) \leq_{\sf \omega} \omega(N_1)$,
%since 
%from Proposition \ref{garbrepl} if $\rho_1 \setminus \rho$
%is no longer an $\omega$-redex, it can be
%restored by performing $\omega$-reductions on ${M_1}_\Omega$.
%
%From Propositions \ref{propinterf} and
%\ref{preservingomegaredex}
%the descendant of redex $\rho_1$ in $M_2$, if it exists, is still a redex.
%Analogously, for $\rho_2$ in $M_1$.
%Let us assume that these descendants exist. 
%%Therefore, $\rho_1'$ 
%%is still a redex in $M[z_2 \leftarrow \Omega]$, namely the redex
%%$(\tau,z_1',\sigma_1')$,  where $z_1'$ is the descendant of $z_1$ and
%%$\sigma_1'(x)$ = the descendant of $\sigma_1(x)$.
%%Analogously, $z_2'$, the descendant of $z_2$  will still be a $\omega$-redex
%%in $M[z_1 \leftarrow r^\sigma]$.
%The result then follows from the fact that
%$$ (M[z_2\leftarrow \Omega])[z_1 \leftarrow r^{\sigma_1}] \equiv
%(M[z_1\leftarrow r^{\sigma_1}])[z_2 \leftarrow \Omega ].$$
\end{proof}


\begin{lemma}
\label{iolemma}
Given GRS$_{\sf NI}$ terms $M$ and $N$, and context $C[\Box]$,
if $C[M] \mbox{ \ioreduces{\Re(M)} } N$
then $\omega(N) \sqsubseteq_{\sf g} C[\omega(M)]$.
\end{lemma}
\begin{proof}
%If we let $\Re\prime(M)$ be the set containing the root of  
%the descendants of redexes in $\Re(M)$ with respect to the
%the reduction $C[M] \mbox{ \ioreduces{} } N$.
By Proposition \ref{commuOmega},
\[ C[{\tt GC}(M[ \Re(M) \leftarrow \Omega])] \reduces{}{}
{\tt GC}(N[ \Re(M) \leftarrow \Omega]) \enspace . \]
Moreover, by the soundness of reduction 
(Proposition \ref{soundW}),
\[C[{\tt GC}(M[ \Re(M) \leftarrow \Omega])] \equiv_{\sf g}
{\tt GC}(N[ \Re(M) \leftarrow \Omega]) \enspace . \]
Since $\omega(N) \leq_{\sf \omega} 
{\tt GC}(N[ \Re(M) \leftarrow \Omega])$, from 
the monotonicity of
$\sqsubseteq_{\sf g}$ with respect to $\leq_{\sf \omega}$
(Proposition \ref{inc1}),
\[ \omega(N) \sqsubseteq_{\sf g}
{\tt GC}(N[ \Re(M) \leftarrow \Omega])
\equiv_{\sf g}
C[{\tt GC}(M[ \Re(M) \leftarrow \Omega])] \enspace . \]
Since $C[{\tt GC}(M[ \Re(M)\leftarrow \Omega])]
\reduces{}{}{\hspace{-0.9mm}\vspace{-0.6mm}_\omega}  \; 
C[\omega(M)]$, and by Proposition \ref{omegamean} $\omega$-reductions 
preserve the meaning
\[ C[{\tt GC}(M[ \Re(M) \leftarrow \Omega])]
\equiv_{\sf g} C[\omega(M)].\]
Therefore, $\omega(N) \sqsubseteq_{\sf g}
{\tt GC}(N[ \Re(M) \leftarrow \Omega]) \equiv_{\sf g}
C[{\tt GC}(M[ \Re(M) \leftarrow \Omega])]
\equiv_{\sf g}
C[\omega(M)]$.\\
Pictorially we have
$$\begin{diagram}
C[M] & \mbox{\ioreduces{\Re(M)}} & N  \\
\dArr & & \dDashto\\
C[{\tt GC}(M[ \Re(M) \leftarrow \Omega])] &
\rDashto  & {\tt GC}(N[ \Re(M) \leftarrow \Omega]) \\
\dArr_{\sf \omega} & & \dDashto_{\sf \omega}\\
C[\omega(M)] & \rDashto  & \omega(N)
\end{diagram}$$
\end{proof}

\begin{lemma}
\label{Mininfo}
Given a GRS$_{\sf NI}$ term $M$ and context $C[\Box]$,
$C[M] \sqsubseteq_{\sf g} \bigsqcup \{ C[P] \mid  P \in W^*(M) \}$.
\end{lemma}
\begin{proof}
Since $$ C[M] \equiv_{\sf g} \bigsqcup \{ Q \mid  Q \in W^*(C[M]) \}$$
we want to show that
$$\bigsqcup \{ Q \mid  Q \in W^*(C[M]) \} \sqsubseteq_{\sf g}
\bigsqcup \{ C[P]  \mid  P \in W^*(M) \} $$
that is, $\forall Q \in W^*(C[M]),
\exists P \in W^*(M) \mbox{ such that }
Q  \sqsubseteq_{\sf g} C[P].$
If $Q \in W^*(C[M])$ it means that $C[M] \reduces{}{} N$ and
$Q \leq_{\sf \omega} \omega(N)$, and, therefore, by
monotonicity of $\sqsubseteq_{\sf g}$ with respect to
$\leq_{\sf \omega}$
(Theorem \ref{inc1}), we have $Q \sqsubseteq_{\sf g} \omega(N)$.
By Proposition \ref{insidered},
given the reduction $C[M] \reduces{}{} N$,
$\exists M', M \reduces{}{} M'$ and $C[M']$ \ioreduces{\Re(M')} $N$.
Therefore, by Lemma \ref{iolemma} we have
\[ \omega(N) \sqsubseteq_{\sf g} C[\omega(M')] \enspace . \]
Since $\omega(M') \in W^*(M)$, by letting
$P \equiv \omega(M')$ we have that $Q \sqsubseteq_{\sf g} C[P]$.
\end{proof}

\begin{theorem}
\label{gcont}
Given a GRS$_{\sf NI}$ term $M$ and context $C[\Box]$, $C[M] \equiv_{\sf g}
\bigsqcup \{C[P] \mid  P \in W^*(M) \}$.
\end{theorem}
\begin{proof}
Follows from Lemma \ref{infoinM} and Lemma \ref{Mininfo}.
\end{proof}


\begin{theorem}[Congruence of $\equiv_{\sf g}$ with respect to
the context operation]
\label{theoremcongruence}
Given  GRS$_{\sf NI}$ terms $M$ and $N$, and context $C[\Box]$,
if $M \equiv_{\sf g} N$ then $C[M] \equiv_{\sf g} C[N].$
\end{theorem}
\begin{proof}

$\begin{array}[t]{lll}
C[M]  & \equiv_{\sf g} \bigsqcup \{C[P] \mid  P \in W^*(M)\}  &
\mbox{(by Theorem } \ref{gcont}) \\
& \equiv_{\sf g} \bigsqcup \{C[Q] \mid  Q \in W^*(N)\}
& \mbox{(by the hypothesis) }  \\
& \equiv_{\sf g} C[N] &  \mbox{(by Theorem } \ref{gcont})
\enspace . 
\end{array} $

\end{proof}

We stressed again that in the presence of interfering rules,
$\equiv_{\sf g}$ is not  guaranteed to be a congruence.
Consider the rules
\[ \begin{array}{ll}
\tau_1: & x={\sf A}(y) \reduce{}{} x = {\sf A}(y)\\
\tau_2: & x={\sf B}(y) \reduce{}{} x = {\sf B}(y)\\
\tau_3: & \frag{x_1={\sf A}(y)}
{x={\sf F}(x_1) \reduce{}{} x = {\sf 2}}\\
\tau_4: & \frag{x_1={\sf B}(y)}
{x={\sf F}(x_1) \reduce{}{} x = {\sf 3}}
\end{array}
\]
and the following two terms:
\[ \begin{array}{ll}
M \equiv \{ \begin{array}[t]{l}
t = {\sf A}(x);\\
\;\; {\sf In} \; t \}
\end{array} \hspace{0.5cm} & \hspace{0.5cm}
N \equiv \{ \begin{array}[t]{l}
t = {\sf B}(x);\\
\;\; {\sf In} \; t \}
\end{array}
\end{array}
\]
Notice that $M \equiv_{\sf g} N$, but the 
context
$\{
t_1 = {\sf F}(t_2); \; t_2 = \Box; \; {\sf In} \; t_1 \}$
can distinguish between $M$ and $N$. 


