\section{Correctness of Optimizations}
\label{opti}
If we let $(A({\cal F}),R_{opt})$ be a GRS, where $A({\cal F})$ represents the set of terms over signature ${\cal F}$,
and $R_{opt}$ a set of optimization rules, then correctness
can be formulated as follows.

\begin{definition}[Total correctness]
An optimizer $(A({\cal F}),R_{opt})$
is  totally correct with respect to a GRS$_{\sf NI}$ $(A({\cal F}),R)$ iff
$\forall \; M \in  A({\cal F})$, if $M \reduces{}{} N$ using rules
in $R_{opt}$ then $M \equiv_{\sf g} N$.
\end{definition}

\noindent
In many situations it is acceptable if optimizations produce a more
defined program. 

\begin{definition}[Partial correctness]
An optimizer $(A({\cal F}),R_{opt})$
is partially correct with respect to a GRS$_{\sf NI}$ $(A({\cal F}),R)$ iff
$\forall \; M \in  A({\cal F})$, if $M \reduces{}{} N$ using rules in
$R_{opt}$ then $M \sqsubseteq_{\sf g} N$.
\end{definition}

%\noindent
%We can express the common subexpression elimination in terms
%of a GRS rule as follows:
%$$ \frag{y= {\sf +}(a,b)}{x={\sf +}(a,b) \reduce{}{} x =y} $$

\begin{fact}
If $M \reduce{}{} M_1$
by applying the common subexpression elimination rule then $M \leq_{\sf \omega} M_1$. 
\end{fact}

\begin{proposition}
The common subexpression elimination is partially correct
with respect to a GRS$_{\sf NI}$.
\end{proposition}
\begin{proof}
Directly from the above fact and Corollary \ref{monomega}.
\end{proof}

\blank
Let GRS$^{\sf Y}$ be a non-interfering GRS containing the following ${\sf Y}$-rule:
$$ {\sf Y}\mbox{-rule}: \hspace{1cm}
x ={\sf Ap}({\sf Y},f) \reduce{}{}
x = \{ \begin{array}[t]{l}
t = {\sf Ap}(f,t_1);\\
t_1= {\sf Ap}({\sf Y},f);\\
\;\;{\sf In} \; t \}
\end{array}$$
We can avoid the redex rooted at $t_1$ on
the right hand side of the above rule by using the following cyclic
${\sf Y}$-rule:
$$ {\sf Y_c}\mbox{-rule}: \hspace{1cm}
x ={\sf Ap}({\sf Y},f) \reduce{}{}
x={\sf Ap}(f,x)$$

\begin{proposition}
The cyclic ${\sf Y}$-rule is partially correct with respect to
a GRS$^{\sf Y}$. 
\end{proposition}
\begin{proof}
Suppose $M \reduce{}{} M_1$ using the 
$ {\sf Y}$-rule and 
$M \reduce{}{} M_2$ using the 
$ {\sf Y_c}$-rule. Then 
$M_1 \sqsubseteq_{\sf g} M_2$ and the result follows 
from Theorem \ref{theoremcongruence}.
\end{proof}

\blank
If we want to prove the total correctness of
the cyclic implementation of the ${\sf Y}$ rule or the
common subexpression elimination rule,
then we need to impose further restrictions on the GRS
rules. In particular, non-left-linear rules (which include left-cyclic rules)
will have
to be disallowed. Furthermore, sharing will have to be
ignored from the observations as well. The reader may refer to \cite{Zena93}, where such a 
term model based on B\"ohm trees is presented.

Surprisingly, the following algebraic rules:
$$\begin{array}{l}
{\sf *}(x,{\sf 0}) \reduce{}{} {\sf 0} \\
{\sf *}( x,{\sf 1} ) \reduce{}{} x
\end{array}$$
are not partially correct according to our model.
Consider the following reduction:
$$M_1 \equiv \{ x = {\sf G}({\sf 7});\;
y = {\sf *}(x,{\sf 1}); \; {\sf In} \; y \} 
\reduce{}{}
M_1' \equiv \{ x = {\sf G}({\sf 7});\; {\sf In} \; x \}.$$ 
As long as ${\sf G}({\sf 7})$ is a redex, 
$\omega(M_1) \leq_{\sf \omega} \omega(M_1')$.
However, 
if ${\sf G}({\sf 7})$ is not a redex, then there is no
relationship between $\omega(M_1)$ and $\omega(M_1')$.
Such situations can arise either because of {\it  type
errors} or {\it deadlocks}. We illustrate the
deadlock situation by the following
example:
$$M_2 \equiv \{ x= {\sf *}(y,{\sf 5});
y = {\sf *}(x,{\sf 1}); \; {\sf In} \; x \}
\reduce{}{}
M_2'  \equiv \{ x= {\sf *}(x,{\sf 5}); \; {\sf In} \; x \}.$$
Notice $M_2$ is type correct but it cannot produce
an integer as an answer. However, in our term model,
without the optimization $M_2$ will produce itself as an answer,
and with the optimization it will produce 
$M_2'$, which is not related to $M_2$.
We believe that cycles involving ``strict operators'' should not
be observable, that is, the observations of 
both $M_2$ and $M_2'$ should be $\Omega$.
