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

\topmargin   0pt

\textwidth   6.5in
\textheight  8.5 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}


\begin{titlepage}



\thispagestyle{empty}

\title{On Relative Normalization in Orthogonal Expression Reduction Systems}
\author{John Glauert and Zurab Khasidashvili \\ School of Information Systems, UEA}
\maketitle

\thispagestyle{empty}


\begin{abstract}
We study reductions in orthogonal (left-linear and non-ambiguous) Expression Reduction Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. We introduce the notion of {\em neededness} with respect to 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$. For example, {\em L\'evy-neededness} is neededness w.r.t. the set of normal forms, {\em Maranget-neededness} is neededness w.r.t. all fair reductions, {\em head-neededness} is neededness w.r.t. the set of head-normal forms, etc. We find 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. 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 give a characterization of stable sets using {L\'evy-equivalence} of reductions. Finally, we relate notion of {\em essentiality} with the notion of neededness. 
\end{abstract}


\bigskip
\subsection*{Correspondence Address}

\begin{tabbing}
John Glauert \\
School of Information Systems \\
University of East Anglia \\
Norwich NR4 7TJ England \\
\\
Email: jrwg@sys.uea.ac.uk \\
Tel: +44 603 592671 \\
Fax: +44 603 507720
\end{tabbing} 

\end{titlepage}





\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,~\cite{[D.J.],[Kl.TRS]}) and reductions with substitutions (referred to also as higher order rewriting) as in the $\lambda$-calculus~\cite{[Bar]}. 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 the term $s$.  To express ``pure''
substitutions we use $S$-reduction rules $S^{n+1}a_{1}\ldots a_{n}A_{1}\ldots A_{n}A_0\ar(A_{1}/a_{1},\ldots,A_{n}/a_{n})A_0,\,\,\,n=1,2,\ldots$,
where $S^{n+1}$ is an {\em operator sign of substitution}, which binds free variables only in the last argument. 

We use $u,v,w$ for redexes, $t,s,e,o$ for $P,Q$ for reductions; $+$ denotes concatenation of reductions; 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$.


Any ERS $R$ can be split into a ``first order part'' $R_f$, which delays substitutions as $\undl{S}$-redexes, and a ``substitution part'' $\undl{S}$, which makes substitutions (underlining is only used to distinguish created $S$-redexes from other ones). For example, a $\beta$-reduction step $Ap(\lambda x\,t,s)\ar (s/x)t$ {\em refines} to a $\beta_f$-reduction step $(\lambda x\,t)s\ar\undl{S}x\,s\,t$ and an $\undl{S}$-step $\undl{S}x\,s\,t\ar (s/x)t$. 

Let $t\stackrel{u}{\ar} s$ be an $R_f$-reduction step and let $e$ be the contractum of $u$ in $s$.  For each argument $o$ of $u$ there are $0$ or more arguments of $e$. We call them ($u$-){\em descendants} of $o$. Correspondingly, subterms of $o$ have $0$ or more {\em descendants}.  By definition, the {\em descendant} of each pattern-subterm of $u$ is $e$. It is clear what is to be meant by {\em descendants} of a subterm that is not in $u$. In an $S$-reduction step $C[S^{n+1}x_1\ldots x_n\,t_1\ldots t_nt_0]\red{u}C[(t_1/x_1,\ldots,t_n/x_n)t_0]$, the argument $t_i$ and subterms in $t_i$ have the same number of descendants as the number of free occurrences of $x_i$ in $t_0$. All subterms of $t_0$, including free occurrences of
$x_1,\ldots,x_n$, have exactly one descendant. The descendant  of the contracted redex $u$ itself is its contractum. The notion of {\em descendant}  extends by transitivity  to arbitrary reductions in $R$. 




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 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$, for $R_f$ and $S$-steps, 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 call the co-initial reductions $P:t\doar s$ and $Q:t\doar e$ {\em strictly equivalent} (written $P\steq Q$) if $s=e$ and $P$-descendants and $Q$-descendants of any subterm or any component of $t$ are the corresponding occurrences in~$s$ and~$e$ (cf.~\cite{[OCRS]}). As in the case of the $\lambda$-calculus~\cite{[Bar]}, for any co-initial finite reductions $P$ and $Q$, one can define in orthogonal ERSs (OERSs) the notion of {\em residual of $P$ under $Q$}, written $P/Q$, due to L\'evy~\cite{[le80]} (the definition of {\em orthogonality} in ERSs is similar to the case of TRSs: the rules are left-linear and in no term redex-patterns can overlap); we write $P\lleq Q$ if $P/Q=\emptyset$ ($\lleq$ is the {\em L\'evy-embedding} relation);  $P$ and $Q$ are called {\em L\'evy equivalent} or {\em strongly equivalent} (written $P\leeqv Q$) if $P\lleq Q$ and $Q\lleq P$. We show that OERSs have the following {\em strict Church-Rosser} property: for any co-initial $P$ and $Q$, $P+Q/P\steq Q+P/Q$ (we actually use the weaker result that if $P$ and $Q$ are external to a component $e$, then the descendants of $e$ under $P+Q/P$ and $Q+P/Q$ are the same components). We will use the following definition below.


\begin{deff}\em
\label{D.fam.}
\cite{[le80]} (1) For any co-initial reductions $P$ and $Q$, the redex $Qv$ (read as $v$ {\em with history} $Q$), is called a {\em copy} of a redex $Pu$ if $P\lleq Q$, i.e.,  $P+Q/P\leeqv Q$, and $v$ is a $Q/P$-residual of $u$; the {\em (zig-zag) family} relation $\zig$ is the symmetric and transitive closure of the copy relation (cf.~\cite{[AL]}).

(2) For any $P:t\doar s$, a {\em family completion} of $P$, written $C(P)$, is a (finite) reduction obtained from $P$ by contracting redexes belonging to the families of redexes contracted in $P$.

(3) A reduction $P$ is called {\em $c$-complete} if $P=P_1+\ldots P_n$, where $P_i$ is a complete development of the maximal set of residuals of a single redex.
\end{deff}





\section{Essentiality and unabsorbness}
\label{S. 3.}



Recall that a redex $u$ in $t$ is {\em L\'evy-needed}~\cite{[H.L.],[le80]} 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.


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]}. However, existence of an essential redex in every such term $t$ follows immediately from existence of an {\em eraser} for $t$, that is, 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}~\cite{[Kl.TRS]} 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 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.




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 closed under reductions in $R$; 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.

%(2) Let $t$ be a term in $R$, and let $s\subpc t$. For any stable set $M$, we call $s$ $M$-{\em unneeded} (written $UN_M(s,t)$) if there is a reduction $P:t\doar e$ with $e\in M$ external to $s$; we say that $P$ {\em ($M$-)suppresses} $s$ in the latter case; we call $s$ $M$-{\em needed} (written $NE_M(s,t)$) otherwise. If $o\subt $, then we call $o$ $M$-{\em unneeded} (written $UN_M(o,t)$), resp. $M$-{\em needed} (written $NE_M(o,t)$), if so is $Int(o)$. 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$.
\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 (set of terms in the) graph $G_s$ of a term $s$ 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. Note that any set closed under reduction is the union of the graphs of a set of terms. 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.




Note that 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.






\begin{prop}\em
\label{L.stab.equiv.}
Let $M$ be a set of terms closed under reduction in an OERS. Then $M$ is stable iff, for any $t\not\in M$ and any $M$-normalizing $M$-needed $P,Q$ starting from $t$, $C(P)\leeqv C(Q)$ (see Definition~\ref{D.fam.}). 
\end{prop}



The above proposition is not used in the sequel, but we found it interesting to include; note that $M$-neededness of $P$ and $Q$ is crucial: if $M$ is the set of $\lambda$-terms in head-normal form, $u=(\lambda z.y)y'$, $w=(\lambda x.xx) (\lambda x.xx)$, and $t=\lambda x.u\omega$, then $P:t\red{u}\lambda x.y\omega$ and $Q:t\red{\omega}t\red{u}\lambda x.y\omega$, but $P\not\leeqv Q$. 
% The requirment that $M$ is closed under reduction is necessary as well. A counterexample can be given by taking as $M$ the set of normalizable terms exapt the graph of a normalizable term.









\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 using the strict Church-Rosser theorem that if $P$ $M$-suppresses $s_1,\ldots,s_n\subpc t$ and $t\red{u}e$, then $P/u$ $M$-suppresses the $u$-descendants of $s_1,\ldots,s_n$. It follows that 

($\alpha$) descendants of $M$-unneeded components remain $M$-unneeded. \\
The fact that 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 $e\subpc t$,  $o$ is a component with the same arity (i.e., the same number of holes), and $s$ is obtained from $t$ by replacing $e$ with $o$, then $NE(e,t)$ iff $NE(o,s)$; if $e\subpc s\subpc t$  and $NE_M(e,t)$, then  $NE_M(s,t)$; and 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 a,\, g(x,y)\ar h(x,y)\}$ with a typing that allows only terms with at most one occurrence of $f$, and take for $M$ the set of terms not containing occurrences of $f$; then in $t=g(f(x),y)$ $f$ is $M$-needed, while $g$ 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')$.





\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 it does not possess a reduction in which $M$-needed redexes are contracted infinitely many times.

\begin{prsk}
(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) One can easily transform an $M$-normalizing reduction (if any) starting from a term $t$ into a $c$-complete one $Q$. Now let $t\red{u}s$. It is easy to show that (a) if $NE_M(u,t)$, then  $\vert Q/u\vert_c<\vert Q\vert_c$ (since $Q$ contracts residuals of $u$), where  $\vert Q\vert_c$ denotes the number of maximal complete developments in  $Q$ (see Definition~\ref{D.fam.}), and (b) if $UN_M(u,t)$, then  $\vert Q/u\vert_F\leq\vert Q\vert_F$. Hence (2) follows from (1).
\end{prsk}
\end{thm}






\section{Conclusions and future work}

We have introduced a relative notion of neededness and proved the Uniform Normalization Theorem. Analogous questions arise for other strategies. For example, how can one construct reductions that avoid head-normal forms? Besides strong sequentiality for normal forms studied in Huet-L\'evy~\cite{[H.L.]}, strong sequentiality is studied w.r.t. head-normal forms in Kennaway~\cite{[Ken]}. Investigation of relative strong sequentiality and related to it strictness analysis (see e.g.,~\cite{[Nok.thi.]})  seems also as an interesting topic for future research.

\vspace{0.20cm}

\begin{akn} 
We thank  J. R. Kennaway and M. R. Sleep for useful discussions.
\end{akn}

%


\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{[Ken]}
Kennaway J. R. The conflict between call-by-need computation and parallelism. School of Information Systems, University of East Anglia, unpublished.


\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{[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. Ph. D. Thesis, Katholic University of Nijmegen, 1994.

\end{thebibliography}
\end{document}






