\documentstyle[11pt]{article}
\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt

\textwidth   6.5in
\textheight  8.0 in
%\def \dred {\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\def \doar{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
%\documentstyle[fullpage,11pt,amssymbols]{article}
%\input{diagrams} % Paul Taylor's Macro Package
\begin{document}
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
%%%%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{proof}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\newcommand{\notation}{{\bf Notation }}
\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand \inputpic[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\newcommand{\vect}[1]{\mbox{$\overline{#1}$}}
\newcommand{\rpsim}{\mbox{$\stackrel{r}{\psim}$}}
\newcommand{\rpessim}{\mbox{$\stackrel{r}{\pessim}$}}
\newcommand{\ressim}{\mbox{$\stackrel{r}{\essim}$}}
\newcommand{\rsim}{\mbox{$\stackrel{r}{\sim}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\lclas}[1]{\mbox{$\langle{#1}\rangle_L$}}
\newcommand{\eclas}[1]{\mbox{$\langle{#1}\rangleÄ$}}
\newcommand{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\def\pessim{\prec\!\!\prec}
\def\steq{\approx_{st}}
\def\eq{\approx}
\def\essim{\approx}
\def\psim{\prec}
\def\orth{\perp}
\def\esorth{\perp_{es}}
\def\subt{\subseteq}
\def\subpc{\sqsubseteq}
%\def\lleq{\triangleleft}
%\def\lles{\triangleleft}
\def\lleq{\unlhd}
\def\lles{\lhd}
\def\leeqv{\approx_L}
\def\ind{\ddagger}
\def\hole{\circ}
\def\restr{\vert}
\def\exten{\updownarrow}
\def\zig{\simeq}



\title{On Relative Normalization in Orthogonal Expression Reduction Systems}
\author{John Glauert and Zurab Khasidashvili \\ School of Information Systems, UEA, Norwich NR4 7TJ England \\ 
jrwg@sys.uea.ac.uk,
zurab@sys.uea.ac.uk\thanks{This work was supported by the Science and Engineering Council of
Great Britain under grant GR/H 41300}}
\maketitle
\date{}

\section{Introduction}

Since a normalizable term, in a rewriting system, may have an infinite reduction, it is important to have a strategy that enables one to construct normilizing reductions. Such strategies are called {\em normalizing}. It is well known that the leftmost-outermost strategy is normalizing in the $\lambda$-calculus. For orthogonal Term Rewriting Systems (OTRSs), a general normalizing strategy, called the {\em needed} strategy, was found by Huet and L\'evy in~\cite{[H.L.]}. The needed strategy always contracts a {\em needed} redex -- a redex whose residual is to be contracted in any reduction to normal form. Huet and L\'evy showed that any term $t$ not in normal form has a needed redex, and that repeated contraction of needed redexes in $t$ leads to its normal form whenever there is one. They also defined the class of {\em strongly sequential} OTRSs where a needed redex can efficiently be found in any term.

Barendragt et al.~\cite{[B.K.K.S.]} generalized the concept of neededness to the $\lambda$-calculus. They studied neededness not only w.r.t. normal forms, but also w.r.t. head-normal forms -- a redex is {\em head-needed} if its residuals are contracted in each reduction to a head-normal form. The authors proved correctness of the two needed strategies for computing normal forms and head-normal forms, respectively. In Khasidashvili~\cite{[colog],[rta]}, a similar normalizing strategy, called the {\em essential} strategy, was defined for the $\lambda$-calculus and OTRSs. The strategy contracts {\em essential} redexes -- the redexes that have {\em descendants} under any reduction. The notion of descendant is a refinement of that of {\em residual} -- the descendant of a contracted redex is its contractum, while it does not have residuals. An advantage of the correctness proof of the essential strategy as in~\cite{[colog]} is that its generalization to all Orthogonal Combinatory Reduction Systems (OCRSs) is straightforward. Kennaway and Sleep~\cite{[K.S.]} used a generalization of L\'evy's labelling for the $\lambda$-calculus~\cite{[levy]} to adapt the proof from~\cite{[B.K.K.S.]} to the case of OCRSs.

In~\cite{[Mar]}, Maranget introduced a different notion of neededness, where a redex $u$ is needed if it has  a residual under any reduction that does not contract the residuals of $u$. This neededness notion makes sense also for terms that do not have a normal form. It was shown in~\cite{[rta]} that a redex is Maranget-needed iff it is essential. In~\cite{[Mar]}, Maranget studied also a strategy that computes a (`minimal') weak head-normal form of a term in an OTRS. Normalization w.r.t. another interesting set of `normal forms', that of constructor head-normal forms in constructor OTRSs, is studied by N\"ocker~\cite{[Nok.thi.]}. A question arises naturally: what are the properties that a set of terms must possess in order for the neededness theory of Huet and L\'evy still to make sense?

The main contribution of this paper is to provide a solution to that question.  We introduce the notion of {\em neededness} w.r.t. a set of reductions $\Pi$ or a set of terms $M$ so that each existing notion of neededness can be given by specifying $\Pi$ or $M$. We imposed natural conditions on $M$, called {\em stability}, that are sufficient and necessary for each term not in $M$-normal form (i.e., not in $M$) to have at least one $M$-needed redex, and repeated contraction of $M$-needed redexes in a term $t$ to lead to an $M$-normal form of $t$ whenever there is one. 
A set $M$ of terms is stable if it is {\em closed under permutation}: for any $t\not\in M$, any $P:t\doar o\in M$, and any $Q:t\doar e$, the final term of $P/Q$ is in $M$; and is {\em closed under unneeded expansion}: for any $e\red{u}o$ such that $e\not\in M$ and $o\in M$, a residual of $u$ is contracted in any reduction from $e$ to a term in $M$. 
We present a counterexample to show that in general the $M$-needed strategy is not {\em hypernormalizing} for every stable $M$.

Our relative neededness notion is based on tracing of {\em (open) components}, which are occurrences of contexts not containing {\em any} bound variable, rather than tracing of redexes or subterms. 
% We therefore introduce a notion of {\em descendant} for components and show that, for any co-initial reductions $P$ and $Q$, there are converging reductions $P'$ and $Q'$ such that the descendants of any subterm or a component of the initial term under $P+P'$ (the concatenation of $P$ and $P'$) and $Q+Q'$ are the same occurrences. 
We call a component of a term $t\not\in M$ {\em $M$-needed} if at least one descendant of it is `involved' in any $M$-normalizing reduction; a redex is {\em $M$-needed} if so is its pattern. This approach to defining the neededness notion is crucial from technical point of view, because a `non-standard' situation -- when a component under an $M$-unneeded component is $M$-needed -- may occur for some stable sets $M$. Also, components of a term in an OCRS enjoy the same `disjointness' property that subterms of a term in an OTRS possesses: descendants of disjoint components of a term in an OCRS remain disjoint, and this allows for simpler proofs.


\section{Preliminaries}
\label{S.CRS}


{\em Combinatory Reduction Systems} (CRSs) have been introduced in Klop~\cite{[Kl.CRS]} to provide a uniform framework for reductions in Term rewriting Systems (TRSs) and reductions with substitutions (referred to also as higher order rewriting) as in the $\lambda$-calculus. Several other interesting formalisms have been introduced later. We refer to  Klop et al.~\cite{[kor]} for further information. 


Our syntax, {\em Expression Reduction Systems (ERS)} (called CRSs in~\cite{[OCRS]}) is closer to the syntax of $\lambda$-calculus and First Order Logic. The alphabet contains (object) variables and function and quantifier symbols. Quantifiers may be {\em partial}, that is, they may bind variables only in some of the arguments. Patterns of left-hand and right-hand sides of rules in ERSs may have arbitrary shape, {\em object metavariables} must be bound, and right-hand sides may contain any number of, sometimes nested, {\em metasubstitutions}. For example, the $\beta$-rule is written as $\beta: Ap(\lambda aA,B)\ar(B/a)A,$ where $a$ is an object metavariable, to be instantiated by a variable, and $A$ and $B$ are term-metavariables, to be instantiated by terms.  The expression $(B/a)A$ is a metasubstitution, and its instance $(t/x)s$ denotes the result of substitution of the term $t$ for $x$ in $s$.


\notation We use $u,v,w$ for redexes, $t,s,e,o$ for terms, $P,Q$ for reductions; $+$ denotes concatenation of reductions; $P/Q$ denotes the {\em residual} of $P$ by $Q$ \cite{[levy],[H.L.]}; we write $t\subt s$ if $t$ is a subterm of $s$; $pat(u)$ denotes the pattern of $u$; $u$ will also denote the reduction that contracts the redex $u$.




We call a {\em component} an occurrence of a context that does not contain any bound variables (even if their binders are in the component). We use the letters used for terms to denote components as well. We write $s\subpc t$ if $s$ is a component of $t$. 

In Khasidashvili~\cite{[OCRS]} a notion of {\em descendant} is introduced to trace subterms during reductions in OERSs. The main difference with the notion of {\em residual} of redexes is that the descendant of a contracted redex is its contractum, while the redex does not have residuals. In the case when the pattern $pat(u)$ of $u\subt t$ does not overlap with a component $s\subpc t$, one can naturally define {\em $u$-descendants} of $s$ to be the descendants of the corresponding subterm $o=e[o_1,\ldots,o_n]$ with the `corresponding' descendants of $o_1,\ldots,o_n$ removed; the definition generalizes by transitivity to all $R$-reductions that are {\em external} to $s$, i.e., do not execute redexes whose patterns overlap with descendants of $s$ (see Definition~\ref{D.rel.need.}.(1)). The descendant relation for components can be defined also in the case of overlap between the pattern of the contracted redex and the traced component, but the definition has many cases and we leave it out; it anyway is not needed to prove the main result of the paper. We also show that OERSs have the following {\em strict Church-Rosser} property: for any co-initial $P$ and $Q$, the descendants of any component and any subterm of the initial term under $P+Q/P$ and $Q+P/Q$ are the same occurrences.








\section{Neededness, essentiality and unabsorbness}
\label{S. 3.}



Recall that a redex $u$ in $t$ is {\em Huet-L\'evy-needed}~\cite{[H.L.]} if in each reduction of $t$ to normal form (if any) at least one residual of $u$ is contracted; $u$ is {\em Maranget-needed}~\cite{[Mar]} if $u$ has at least one residual under any reduction starting from $t$ that does not contract residuals of $u$. Further, a subterm $s$ in $t$ is {\em essential} (written $ES(s,t)$) if $s$ has at least one descendant under any reduction starting from $t$ and {\em
inessential} (written $IE(s,t)$) otherwise~\cite{[rta]}. Finally, a subterm $s\subt t$ is {\em unabsorbed} in $P:t\doar e$ if none of the descendants of $s$ appear in redex-arguments of terms in $P$, and is {\em absorbed in} $P$ otherwise; $s$ is {\em unabsorbed in} $t$ if it is unabsorbed in any reduction starting from $t$ and {\em absorbed in} $t$ otherwise~\cite{[rta]}. (It is easy to see that a redex $u\subt t$ is unabsorbed iff $u$ is {\em external} \cite{[H.L.]} in $t$.) Obviously, unabsorbed redexes are essential and are both L\'evy- and Maranget-needed. % Note that L\'evy- and Maranget-neededness coincide for normalizable terms.

We show that every term $t$ not in normal form has an {\em eraser} -- a reduction that erases all inessential subterms of $t$. It is easy to show that, for example, {\em fair} reductions are erasers ($P:t\ar t_1\ar\ldots$ is {\em fair} if each redex $u_i\subt t_i$ is {\em secured} in $P$, i.e., there is $j>i$ such that $u_i$ does not have residuals in $t_j$). As in the case of OTRSs~\cite{[rta]}, we then show that Maranget-neededness (for redexes) coincides with our essentiality in OERSs as well. $(\Leftarrow$) is immediate. For ($\Rightarrow$), we first show that if one replaces any number of inessential subterms $s_{1},\ldots,s_{n}$ in a term $s$ with any terms $t_{1},\ldots,t_{n}$, then $t_{1},\ldots,t_{n}$ will be inessential in the obtained term $t$ --- one can construct an eraser of $t_{1},\ldots,t_{n}$ by a kind of simulation of an eraser of $s_{1},\ldots,s_{n}$. Now, if $IE(u,t)$, then any subterm $o$ not containing symbols occurring in redex-patterns is inessential when substituted for $u$ in $t$, and an eraser of $u$ that does not contract the residuals of $u$ can be constructed from any eraser of $o$; hence $u$ is not Maranget-needed. A side result is the existance of an essential redex in every term not in normal form. Existence of an unabsorbed redex in any term $t$ not in normal form can be proved exactly as in the case of OTRSs~\cite{[rta]}. 




%   The proofs of normalization of the needed strategy for OTRSs and the $\lambda$-calculus in~\cite{[H.L.],[le80]} are very difficult. A simple proof of normalization of the essential strategy for OTRSs in~\cite{[rta]} does not apply to the case of OERSs, but the proof for the $\lambda$-calculus in~\cite{[colog]} can easily be adapted for the case of OERSs. This proof is much simpler than the one in~\cite{[K.S.]}, which uses the difficult technique of L\'evy-labeling~\cite{[levy]}; the latter is a generalization of the proof in~\cite{[B.K.K.S.]} for the $\lambda$-calculus, which works for head-normal forms as well. Below we sketch a uniform proof that works for all `reasonable' classes of `normal forms', and is different from all the above proofs, although similar to all of them.  








\section{Relative notions of neededness}





\begin{deff}\em
\label{D.rel.need.}
(1) We call a reduction $P$ starting from a term $t$ in an OERS $R$ {\em external} to a  component $e\subpc t$ if there is no redex executed in $P$ whose pattern overlaps with a descendant of $e$. 


(2) We call a component $e\subpc t$ $P$-{\em unneeded} if $P$ is external to $e$ and call it $P$-{\em needed} otherwise.


(3) Let $\Pi$ be a set of reductions. We call $e\subpc t$ $\Pi$-{\em needed} if it is $P$-needed for every $P\in\Pi$ starting from $t$, and call $\Pi$-{\em unneeded} otherwise.


(4) Let $M$ be a set of terms in $R$, and let $\Pi_M$ be the set of {\em $M$-normalizing} reductions, i.e., reductions that end at a term in $M$. We call $e\subpc t$ {\em $M$-needed} ({\em $M$-unneeded}) if it is {\em $\Pi_M$-needed} ({\em $\Pi_M$-unneeded}). We say that $P$ {\em $M$-suppresses} $e$ if $P$ is $M$-normalizing and is external to $e$.


(5) If $o\subt t$, then we call $o$ ($P,\Pi,M$-){\em unneeded} ({\em needed}) if so is $Int(o)$, the component obtained from the subterm $o$ by removing {\em all} bound variables. However, if not otherwise stated, we say that a redex $u\subt t$ (which is a subterm) is $M$-{\em unneeded} ($M$-{\em needed}) if so is the pattern $pat(u)$ of $u$.

(6) We call a set $M$ of terms {\em stable} if: (a) $M$ is {\em closed under permutation}: for any $t\not\in M$, any $P:t\doar o\in M$, and any $Q:t\doar e$, the final term of $P/Q$ is in $M$; and (b) $M$ is {\em closed under unneeded expansion}: for any $e\red{u}o$ such that $e\not\in M$ and $o\in M$, $u$ is $M$-needed.


We write $NE_{(P,\Pi,M)}(e,t)$ ($UN(e,t)$) if $e$ is $(P,\Pi,M)$-needed (unneeded). Below $M$ will always denote a stable set of terms.
\end{deff}



If  $o\subpc t$ and $P:t\doar s$ is external to $o$, then we call the descendants of $o$ also the {\em residuals} of $o$. A component that does overlap with the pattern of a contracted redex does not have residuals. Note that if $u\subt t$, then $P:t\doar s$ is external to $pat(u)$ iff $P$ does not contract the residuals of $u$, because orthogonality of the system implies that if the pattern $pat(v)$ of a redex $v$ contracted in $P$ does overlap with a residual of $pat(u)$, then $pat(u)=pat(v)$. Hence $u$ is $M$-needed iff at least one residual of it is contracted in each reduction from $t$ to a term in $M$ (the intended notion of neededness).



The most appealing examples of stable sets for an OERS are the set of normal forms~\cite{[H.L.]}, the set of head-normal forms~\cite{[B.K.K.S.]}, and the set of constructor-head-normal forms for constructor TRSs~\cite{[Nok.thi.]}.  The graph $G_s$ of a term $s$ (which consists of terms to which $s$ is reducible) is closed under reduction, but need not be closed under unneeded expansion. For example, the graph $G_{I(x)}=\{I(x),\,x\}$ of $I(x)$ is closed under reduction but need not be closed under unneeded expansion: $I(I(x))$ can be reduced to $I(x)$ by reducing either $I$-redex. The set $M'$ of strongly normalizable terms (in some OERS) is closed under reduction, but need not be closed under unneeded expansion. For example, $t=Kz(Ky\omega)$ with $w=(\lambda x.xx)(\lambda x.xx)$ and $K=\lambda xy.x$ can be reduced to a strongly normalizable term (in this case, a variable) by contracting either $K$-redex. Note that {\em none} of the redexes in $t$ are $M'$-needed. Thus the closure of $M$ under unneeded expansion in a necessery condition for the normalization theorem. We show that closure of $M$ under permutation is also necessary. Indeed, consider $R=\{f(x)\ar g(x,x),\,a\ar b,\,b\ar a\}$ and $M=\{g(a,b)\}$. It is easy to show that $M$ is closed under unneeded expansion but is not closed under permutation; and in $R$ we have an $M$-needed infinite reduction  $f(a)\ar f(b)\ar f(a)\ar\ldots$ starting from an $M$-normalizable term.




Note that Huet-L\'evy-neededness (for redexes) coincides with neededness w.r.t. all normalizing reductions. We show that Maranget-neededness is neededness w.r.t. all fair reductions. Indeed, $(\Rightarrow)$ is immediate: if $u$ is Maranget-needed in $t$, then any fair $P$ starting from $t$ should contract a residual of $u$ to secure it. $(\Leftarrow)$ follows from the fact that, if $u$ is not Maranget-needed, then any reduction that secures $u$ without contracting its residuals can be extended to a fair one.














\section{The Uniform Normalization Theorem}



As for the case of subterms in OTRSs, descendants of non-overlapping components are non-overlapping components; due to this property everything works nicely. For example, one can show that if $P$ $M$-suppresses $pat(u_1),\ldots,pat(u_n)\subpc t$ and $t\red{u}e$, then $P/u$ $M$-suppresses the $u$-residuals of $pat(u_1),\ldots,pat(u_n)$. It follows that 

($\alpha$) residuals of $M$-unneeded redexes remain $M$-unneeded. \\
The fact that 

$(\gamma )$ each $M$-needed redex, if not contracted, has at least one $M$-needed residual \\
is not immediate, but can be proved, e.g., using the main theorem. One can show that for $M$-unneeded/$M$-needed components properties similar to the properties of inessential/essential subterms hold. For example, if  $u\subt t$ and $s\subpc pat(u)$, then $NE_M(u,t)$ iff $NE_M(s,t)$.  Note however that if a component $s$ is below a component $o$, then $UN_M(o,t)$ does not necessarily imply $UN_M(s,t)$, although inessentiality of the subterm corresponding to $o$ implies that of the subterm corresponding to $e$. Take for example $R=\{f(x)\ar g(x),\, a\ar b \}$, and take for $M$ the set of terms not containing occurrences of $a$.  Then $a$ is $M$-needed in $f(a)$, while $f(a)$ is not. But we still have the following crucial property, used in many proofs of normalization of needed strategy:

($\beta$) if $t\red{u}t'$, $UN_M(u,t)$, and $u'\subt t'$ is a new redex, then $UN_M(u',t')$. \\
This follows from the fact that if $P$ suppresses $pat(u)$, then $u+P/u$ suppresses $pat(u')$.


In Kennaway and Sleep~\cite{[K.S.]} a labelling is defined for OCRSs, based on the labelling system of Klop~\cite{[Kl.CRS]}, which is in turn a generalization of the labelling system for the $\lambda$-calculus introduced by L\'evy~\cite{[levy]}. To each labelled redex $u$ an {\em index} $Ind(u)$ is associated in such a way that: 
% the following  {\em decreasing labelling} property holds:

$(a)$ \cite{[K.S.]} If a step $t\red{u}s$ creates $v$, then $Ind(u)<Ind(v)$, and if $w\subt s$ is a residual of a redex $w'\subt t$, then $Ind(w)=Ind(w')$; and

$(b)$ \cite{[Kl.CRS]} Any reduction in which only redexes with a bounded redex-index are contracted is terminating.



\begin{thm}\em
\label{T.ex.M-need.}
({\bf Uniform Normalization}) Let $M$ be a stable set of terms in an OERS $R$.

(1) Any term $t$ in $R$ not in $M$-normal form contains at least one $M$-needed redex.

(2) A term $t$ in  $R$ has an $M$-normal form iff every $M$-needed reduction starting from $t$ is terminating.

\begin{proof}
(1) If $t$ does not have $M$-normal form, then (1) is clear. So let $P:t\doar s\red{u}e$ be an $M$-normalizing reduction with $s\not\in M$. By the stability of $M$, $u$ is $M$-needed. By ($\alpha$) and ($\beta$), it is either created by  or is a residual of an $M$-needed redex, and (1) follows by repeating the argument.

(2) Let $P:t\doar s$ be an $M$-normalizing reduction and $Q:t\red{u_0}t_1\red{u_1}\ldots$ be an $M$-needed reduction. Further, let $P_i=P/(u_0+\ldots +u_{i-1})$. By $(a)$, $Ind(P_i)\leq Ind(P)$ ($Ind(P)$ is the maximal index of redexes contracted in $P$). Since $Q$ is $M$-needed and $P_i$ is $M$-normalizing (by the closure of $M$ under permutation), at least one residual of $u_i$ is contracted in $P_i$. Therefore, again by $(a)$, $Ind(u_i)\leq Ind(P_i)$. Hence $Ind(Q)\leq Ind(P)$ and $Q$ is terminating by $(b)$.
\end{proof}
\end{thm}


One can show using $(\gamma )$ (e.g., as in~\cite{[K.S.]} or in~\cite{[colog]}) that, for any such stable set $M$ that $M$-unneeded redexes cannot duplicate or erase $M$-needed ones, the $M$-needed strategy is {\em $M$-hyper\-norma\-li\-zing}. That is, a term is $M$-normalizing iff it does not posses a reduction not containing terms from $M$ in which infinitely many times $M$-needed redexes are contracted. However, this is not the case for all stable $M$. Indeed, consider the OTRS $R=\{f(x)\ar h(f(x),f(x)),\,a\ar b\}$ and take for $M$ the set of terms not containing occurrences of $a$. Then $f(a)\ar h(f(a),f(a))\ar  h(f(b),f(a))\ar h(f(b),h(f(a),f(a)))\ar  h(f(b),h(f(b),f(a)))\ar\ldots$ contracts infinitely many $M$-needed redexes, while $f(a)\ar f(b)$ is $M$-normalizing.



%


\begin{thebibliography}{99}


% \bibitem{[AL]} Asperti A, Laneve C. Interaction Systems 1. The theory of optimal reductions. INRIA Rapport n. 1748, 1992.


%\bibitem{[Bar]} 
% Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.


\bibitem{[B.K.K.S.]} 
Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed Reduction and spine strategies for the lambda calculus. Information  and Computation, v. 75, no. 3, 1987, p. 191-231.

%\bibitem{[D.J.]} 
% Dershowitz  N.,  Jouannaud  J.-P.  Rewrite Systems. In: J. van Leeuwen  ed. Handbook of  Theoretical Computer Science, Chapter 6, vol. B, 1990, p. 243-320.

\bibitem{[H.L.]} 
Huet G., L\'evy J.-J. Computations in Orthogonal Rewriting  Systems. In: Computational Logic, Essays in Honour of Alan Robinson, ed. by J.-L. Lassez and G. Plotkin, MIT Press, 1991.
 
%

\bibitem{[K.S.]} 
Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in  regular combinatory reduction systems. Preprint, School of Information Systems, University of East Anglia, Norwich, 1989.



\bibitem{[colog]} 
 Z. Khasidashvili.  $\beta$-reductions and $\beta$-developments of $\lambda$-terms with the least number of steps. In Proc. of the International conference in Computer Logic ``COLOG 88'', Tallinn 1988, Springer LNCS, v. 417, 1990, p. 105--111.



\bibitem{[OCRS]} 
Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.



\bibitem{[rta]} 
Khasidashvili Z. Optimal normalization in orthogonal term  rewriting systems. In: Proc. of the fifth International Conference on Rewriting Techniques and Applications, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.


%\bibitem{[caap]} 
% Khasidashvili Z.  On higher order recursive program schemes.  In: Proc. of the $19^{th}$ International Colloquium on Trees in Algebra and Programming, CAAP'94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172-186.


\bibitem{[Kl.CRS]} 
Klop J. W.  Combinatory Reduction Systems. Mathematical Centre  Tracts  n. 127,  CWI, Amsterdam, 1980.

%\bibitem{[Kl.TRS]} 
% Klop J. W. Term  Rewriting Systems.  In:  S. Abramsky, D. Gabbay,  and T. Maibaum eds.  Handbook  of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1-116.

\bibitem{[kor]}
Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction Systems:
introduction and survey. In: To Corrado B\"ohm, J. of Theoretical
Computer Science 121, 1993, p. 279-308.


\bibitem{[levy]}
L\'evy J.-J. R\'eductions correctes et optimales dans le lambda-calcul, Th\`ese 
de l'Universit\'e de Paris VII, 1978.

%\bibitem{[le80]}
% L\'evy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalizm, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.


\bibitem{[Mar]}  
Maranget L.  La strat\'egie paresseuse, Th\`ese de l'Universit\'e de Paris
VII, 1992.


\bibitem{[Nok.thi.]}
N\"ocker E. Efficient Functional Programming. Compilation and Programming Techniques. Ph.~D. Thesis, Katholic University of Nijmegen, 1994.

\end{thebibliography}
\end{document}






