\documentclass{article}
\textwidth 130mm
\textheight 200mm
\renewenvironment{abstract}{\section*{Abstract}\small}{}
\newtheorem{definition}{Definition}
\newtheorem{example}[definition]{Example}
\newtheorem{application}[definition]{Application}
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{exercise}[definition]{Exercise}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{notation}[definition]{Notation}
\newtheorem{observation}[definition]{Observation}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{proposal}[definition]{Proposal}
\newtheorem{remark}[definition]{Remark}
\newtheorem{result}[definition]{Result}
\newtheorem{conjecture}[definition]{Conjecture}
\newtheorem{claim}[definition]{Claim}
\newtheorem{assumption}[definition]{Assumption}
\newtheorem{corollary}[definition]{Corollary}
\makeatletter
\renewcommand{\@begintheorem}[2]{ % not in italics
   \trivlist\item[\hskip\labelsep{\bf #1\ #2}]}
\renewcommand{\@opargbegintheorem}[3]{\trivlist
   \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}
\makeatother
\newtheorem{proof}{Proof}
\renewcommand{\theproof}{} % no numbers on proofs
% End of preamble
\usepackage{latexsym}
\input{diagrams} % Paul Taylor's Macro Package
\begin{document}
\bibliographystyle{plain}
\title{Stable Results and Relative Normalization}
\author{John Glauert \\
School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
J.Glauert@uea.ac.uk
\and
Richard Kennaway\\
School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
R.Kennaway@uea.ac.uk
\and
Zurab Khasidashvili   \\
Department of Mathematics and Computer Science \\
Bar-Ilan University, Ramat-Gan 52900, Israel \\
Khasidz@cs.biu.ac.il
\thanks{Part of this work was supported by the Engineering and 
Physical Sciences
Research Council of Great Britain under grant GR/H 41300.}
}

\date{}

\maketitle

\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}

\newcommand{\notationn}{\textbf{Notation}}
%\newcommand{\note}{\textbf{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}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\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{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\newcommand{\lc}{$\lambda$-calculus}
\newcommand{\pessim}{\prec\!\!\prec}
\newcommand{\steq}{\approx_{st}}
\newcommand{\steqc}{\approx_{st}^*}
\newcommand{\hyeq}{\approx_{H}}
\newcommand{\kleq}{\approx_{K}}
\newcommand{\eq}{\approx}
\newcommand{\essim}{\approx}
\newcommand{\psim}{\prec}
\newcommand{\orth}{\perp}
\newcommand{\esorth}{\perp_{es}}
\newcommand{\subt}{\subseteq}
\newcommand{\subpc}{\sqsubseteq}
\newcommand{\lleq}{\unlhd}
\newcommand{\lles}{\lhd}
%\newcommand{\lleq}{\leq_L}
%\newcommand{\lles}{<_L}
\newcommand{\leeqv}{\approx_L}
%\newcommand{\ind}{\ddagger} % occurs again below
%\newcommand{\zig}{\simeq}
\newarrow{Co}<--->
\newcommand{\snpp}{\approx_{sn}}
\newcommand{\inter}{\ddagger}
\newcommand{\ind}{\perp}
\newcommand{\hole}{\circ}
\newcommand{\restr}{\vert}
\newcommand{\exten}{\updownarrow}
\newcommand{\fami}{\simeq}
\newcommand{\zfami}{\simeq_z}

\newcommand{\Tr}[1]{Theorem~\ref{#1}}
\renewcommand{\Pr}[1]{Proposition~\ref{#1}}
\newcommand{\Cr}[1]{Corollary~\ref{#1}}
\newcommand{\Lr}[1]{Lemma~\ref{#1}}
\newcommand{\Dr}[1]{Definition~\ref{#1}}
\newcommand{\Er}[1]{Example~\ref{#1}}

\newcommand{\setm}{\setminus}
\newcommand{\crea}{\vdash}
\newcommand{\emp}{\emptyset}
\newcommand{\qprn}{quasi-persistently $\reg$-needed}
\newcommand{\qpmn}{quasi-persistently $\stab$-needed}
\newcommand{\das}{\downarrow_{\stab}}
\newcommand{\dar}{\downarrow_{\reg}}
\newcommand{\stab}{{\cal S}}
\newcommand{\reg}{{\cal R}}
%\newcommand{\stab}{{\twlmsb S}}
%\newcommand{\reg}{{\twlmsb S}}
\newcommand{\UN}{{\mbox{\it UN}}}
\newcommand{\NEED}{{\mbox{\it NE}}}
\newcommand{\FAM}{{\mbox{\it FAM}}}
\newcommand{\Card}{{\mbox{\it Card}}}
\newcommand{\Ind}{{\mbox{\it Ind}}}
\newcommand{\lab}{{\mbox{\it lab}}}

\newcommand{\Le}{L\'evy}

\begin{abstract}
In orthogonal expression reduction systems,
a common generalization of term rewriting and \lc,
we extend the concepts of normalization and needed reduction
by considering, instead of the set of normal forms,
a set {\cal S} of ``results''.
When {\cal S} satisfies some simple axioms,
we prove the corresponding generalizations of some fundamental
theorems: the existence of needed redexes,
that needed reduction is normalizing,
the existence of minimal normalizing reductions,
and L\'evy's optimality theorem.

\end{abstract}



\section{Introduction}

Since a normalizable term in a rewriting system may have an infinite
reduction, it is important to have a \emph{normalizing} strategy which
enables one to construct reductions to normal form. It is well known that
the leftmost-outermost strategy is normalizing in the
$\lambda$-calculus~\cite{[C.F.]}.

\subsection*{Normalization by Needed Reduction}

For Orthogonal Term Rewriting Systems (OTRSs), a general normalizing
strategy, called the \emph{needed} strategy, was found by Huet and L\'evy
in~\cite{[H.L.]}. The needed strategy always contracts a \emph{needed} redex
-- a redex with at least one
contracted \emph{residual} in
every reduction to normal
form. Huet and L\'evy show 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; we refer to this as the
\emph{Normalization Theorem}. They also define the class of \emph{strongly
sequential} OTRSs where a needed redex can be
found efficiently in any
term.

\subsection*{Extending the concept of Neededness}

Barendregt et al.~\cite{[B.K.K.S.]} generalize the concept of neededness
to the $\lambda$-calculus. They study neededness not only w.r.t.\ normal
forms, but also w.r.t.\ head-normal forms -- a redex is \emph{head-needed} if
its residuals are contracted in each reduction to a head-normal form. They
prove correctness of the two needed strategies for computing
normal forms and head-normal forms, respectively. Middeldorp~\cite{[Mid]}
studies normalization w.r.t.\ root-stable terms (which are terms that
cannot be rewritten to a redex). 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.]}.

The normalization by neededness theory has been extended in other
directions too, of which we mention a few. Khasidashvili   
defined the \emph{essential} strategy for the
$\lambda$-calculus~\cite{[colog]}, OTRSs~\cite{[rta]}, and \emph{Expression
Reduction Systems} (OERSs)~\cite{[caap]}. This strategy contracts
\emph{essential} redexes -- the redexes that have \emph{descendants} under
every reduction. The notion of descendant is a refinement of
\emph{residual} -- the descendant of a contracted redex is its contractum,
while it does not have residuals.\footnote{Note that descendants and 
residuals are sometimes treated as synonymous in the literature.} 
Essentiality makes sense for all subterms, not only redexes.
In~\cite{[Mar]}, Maranget introduces a different notion of neededness,
where a redex $u$ is needed if it has  a residual under any reduction that
does not contract residuals of $u$. This neededness notion makes sense
even for terms that do not have a normal form, and coincides with the
notion of essentiality.

Sekar and Ramakrishnan~\cite{[SeRa]} study a normalizing
strategy which in each multistep contracts a \emph{necessary} set of
redexes. Khasidashvili~\cite{[caap]} shows that in Higher Order
Recursive Program Schemes one can find all needed redexes in
any term, implying decidability of weak and strong normalization.
Khasidashvili and Piperno~\cite{[KP99]} designed an algorithm for 
statically finding all
inessential subterms (i.e., the garbage) in simply typeable $\lambda$-terms.
Gardner~\cite{[Gar]} described a complete way of encoding neededness
information, for the case of the \lc, using a type assignment system in the
sense that using the principal type of a term one
can find all the needed redexes in it. Antoy et al.~\cite{[Ant]} designed a
needed narrowing strategy. Kennaway et al.~\cite{[K-tra]} studied needed
strategies for infinitary OTRSs. Boudol~\cite{[Bou]} and
Melli\`es~\cite{[Mel]} extended the needed strategy to non-orthogonal
rewrite systems.  A different approach to normalization is developed by
Kennaway~\cite{[Kenn]} and by Antoy and Middeldorp~\cite{[AnMi]}.

\subsection*{The concept of Relative Neededness}

Since in the practice of Functional Programming one is interested in
terms of different shapes (weak-head-normal forms, 
constructor head-normal forms, etc.)) as the
results of computation, it is natural to ask what properties a set of 
terms must possess
in order for the neededness theory of Huet and L\'evy still to make sense.
Here we provide a comprehensive solution to that question.

We introduce the notion of \emph{neededness} w.r.t.\ a set of
reductions $\Pi$ so that each existing notion of
neededness can be given by specifying $\Pi$. 
Usually it is convenient to consider a set of terms $\stab$, and the induced
set of reductions $\Pi_{\stab}$ ending at a term in $\stab$.
For example, \emph{Huet and L\'evy-neededness}~\cite{[H.L.]} is
neededness w.r.t.\ the set
$NF$ of normal forms, \emph{Maranget-neededness}~\cite{[Mar]} is neededness
w.r.t.\ all fair reductions, \emph{head-neededness}~\cite{[B.K.K.S.]} is
neededness w.r.t.\ the set of head-normal forms,
\emph{root-neededness}~\cite{[Mid]} is neededness w.r.t.\ the set of
\emph{root-stable} forms, etc.

We impose a natural condition on $\stab$, \emph{stability}, which
guarantees that each term not in
$\stab$-normal form (i.e.,
not in $\stab$) has at least one $\stab$-needed redex,
such that repeated
contraction of $\stab$-needed redexes in a term $t$ will lead to an
$\stab$-normal form of $t$ whenever there is one.
A set $\stab$ of terms is stable if it is \emph{closed under
unneeded expansion}: for any $e\red{u}o$ such that $e\not\in \stab$ and
$o\in \stab$, a residual of $u$ is contracted in any reduction from $e$ to
a term in~$\stab$; and is \emph{closed under reduction}:
for any $t\ar o$ where $t\in \stab$, then $o\in \stab$.
\footnote{When the rewrite system is non-duplicating and non-erasing,
our concept of stability coincides with the concept of stability in event
structures~\cite{[Win89]}.}

We present a counterexample to
show that the $\stab$-needed strategy is not \emph{hypernormalizing} for
every stable $\stab$, i.e., an $\stab$-normalizable term may possess a
reduction contracting both $\stab$-needed and $\stab$-unneeded redexes
which never reaches a term in $\stab$ even though $\stab$-needed
redexes are contracted infinitely many times.
Therefore, \emph{multistep $\stab$-needed}
reductions, where every multistep contracts at least one $\stab$-needed
redex, need not be $\stab$-normalizing. This is  because a
`non-standard' situation may arise in what we will call
\emph{irregular} stable sets $\stab$, where $\stab$-unneeded redexes 
may contain
$\stab$-needed ones. However, for regular stable sets $\stab$,
the $\stab$-needed strategy is always hypernormalizing, and the
multistep $\stab$-needed strategy is normalizing.

Although we claim that our definition of stability is the most natural that
has been proposed, it is possible to weaken the conditions for stability and
still retain the concept of relative neededness. For example, an alternative
definition is explored in~\cite{[ctrs],[morn]}  where a stable set
$\stab$ is closed under unneeded expansion and 
\emph{closed under parallel moves}:
for any $t\not\in \stab$, any $P:t\doar o\in \stab$, and any $Q:t\doar e$
not containing terms in $\stab$, the final term of $P/Q$, the
\emph{residual} of $P$ under $Q$, is in $\stab$.

\subsection*{Minimal and Optimal Relative Normalization}

We further develop a theory of \emph{minimal} and
\emph{optimal} reduction in the framework of relative normalization, and
establish a relationship between them. While normal forms are unique in an
OERS, a term may have many $\stab$-normal forms. A reduction $P:t\doar s$
with $t\not\in \stab$ and $s\in \stab$ is said to be \emph{$\stab$-minimal}
if it does no more work than any other $\stab$-normalizing reduction
$Q:t\doar e$, i.e., the  residual $P/Q$ of $P$ under $Q$ is
empty. The final term in the $\stab$-minimal reduction is said to be a
\emph{minimal} $\stab$-normal form.


Minimal $\stab$-normal
forms are useful to compute since any other $\stab$-normal form is
accessible from the minimal one. Further, strategies
computing partial results (such as  head-normal-forms (hnfs) and weak hnfs,
in the \lc) usually compute minimal reductions, and it is natural to ask
whether optimality can be achieved while retaining minimality. The prime
example is the leftmost outermost strategy computing the so called
`principal' hnf and whnf of a $\lambda$-term, and used in constructions of
B\"ohm~\cite{[Bar]} and \Le-Longo~\cite{[le76],[Lon]} (also called
\emph{lazy}) trees, respectively. These trees represent the
values of the term according to different semantics -- B\"ohm semantics and
lazy semantics, respectively. Clearly this
property of minimality is not useful for full normal forms, but full normal
forms are rarely used in the practice of functional programming.


Our research on minimal
$\stab$-normalizing reductions was inspired by a result of
Maranget~\cite{[Mar]}, stating that \emph{standard} reductions are minimal
among reductions computing a `stable prefix' of a given term.
The earliest minimality result we are aware of was obtained by Berry and
L\'evy in~\cite{[B.L.]}, where existence of minimal reductions was shown
for any finite or infinite approximation of a possibly infinite value of
a term, for Recursive Program Schemes. Minimal reductions were used to
design optimal reductions, both finite and infinite, and minimality and
optimality of \emph{outermost complete family-reductions} were shown.
Minimal and optimal reductions were studied also in arbitrary
interpretations, not only for term (or Herbrand) models.

Here we restrict ourselves to finite reductions only, and study only
syntactic properties. We show that, for any stable and regular $\stab$, any
$\stab$-normalizable term not yet in $\stab$ possesses an $\stab$-needed
\emph{$\stab$-external} redex, and repeated contraction of
such redexes gives
$\stab$-minimal $\stab$-normalizing reductions. These redexes play the role of
\emph{standard} redexes w.r.t.\ $\stab$, since they are $\stab$-needed and
cannot be duplicated. We show that an $\stab$-normalizing reduction is
$\stab$-minimal iff it contracts \emph{$\stab$-erased} redexes, i.e., the
redexes that do not have residuals under any $\stab$-normalizing reduction.
We show also that $\stab$-minimal reductions need not exist if $\stab$ is
stable but is not regular.


Our study of optimal normalization w.r.t.\ stable sets $\stab$ is a
generalization of L\'evy's optimality theory~\cite{[le80]}, developed for
the $\lambda$-calculus. That is, we consider multistep reductions
contracting a number of redexes in the same \emph{family} in parallel, and
consider optimality w.r.t.\ the number of such multisteps. This is because
Barendregt et al~\cite{[BBKV]} showed that no one-step
optimal recursive $\beta$-reduction strategy
exists for the $\lambda$-calculus. We introduce a suitable labelling
system, allowing us to define a family relation in OERSs.
The generalization is then rather straightforward. We show that complete
$\stab$-needed
family-reductions, which contract all members of a family containing an
$\stab$-needed redex in a multistep, are optimal.

It is easy to see that $\stab$-needed complete family reductions, though
optimal, need not be $\stab$-minimal, because they may contract
$\stab$-unneeded redexes that are not $\stab$-erased. It is tempting to
think that contracting only the $\stab$-needed redexes of  $\stab$-needed
families could yield $\stab$-optimal reductions that are $\stab$-minimal at
the same time. We show however that this is not the case either in the
$\lambda$-calculus or in OTRSs.

\subsection*{Overview}

In the next section, we
review Expression Reduction Systems~\cite{[ERS],[OCRS],[pun-ic]}.  In
Section~\ref{S.rel.need.}, we introduce the relative notion of neededness.
In Section~\ref{S.labels}, we sketch some properties of our  labelling
system for OERSs needed to define a
family relation among redexes. We prove correctness of the $\stab$-needed
strategy for computing terms of $\stab$, for all stable $\stab$, in
Section~\ref{S.rel.normal.}, and prove hypernormalization of the
$\stab$-needed strategy w.r.t.\ regular stable sets $\stab$ in
Section~\ref{S.hyp.nr.}. In Section~\ref{S.min.}, we study
$\stab$-minimal reductions for regular stable sets $\stab$. In
Section~\ref{S.sta.} we establish a Relative Standardization Theorem. In
Section~\ref{S.un.opt.}, we prove the Relative Optimality
Theorem.  Finally, in Section~\ref{S.opt.vers.mnin.}, we relate relative
optimal and minimal reductions. The conclusions appear in
Section~\ref{S.conc.}. 

The concepts introduced in Section~\ref{S.rel.need.} build
on~\cite{[ctrs]}, but here the
definitions use only the residual concept while the earlier
definitions were based on a concept of descendants for subterms and
components. The stability concept is simpler, and hence slightly 
less general. The labelling system in Section~\ref{S.labels} 
extends unpublished work by Kennaway and Sleep~\cite{[K.S.]}.
The proofs in Sections~\ref{S.rel.normal.} and 
\ref{S.hyp.nr.} simplify analogous proofs  published as~\cite{[ctrs]}, 
and the remaining results are published in~\cite{[fsttcs]}. 
The results were first reported in~\cite{[morn]}.

\section{Orthogonal Expression Reduction Systems}
\label{S.CRS}


Klop introduced  \emph{Combinatory Reduction Systems}~(CRSs) in
\cite{[Kl.CRS]} to provide a uniform framework for reductions with
substitutions (also referred to as higher order rewriting) as in
the $\lambda$-calculus~\cite{[Bar]} and its extensions.
Restricted rewriting systems with
substitutions were first studied in Pkhakadze~\cite{[Pk]} and
Aczel~\cite{[Acz]}. Several interesting formalisms
have been introduced later~\cite{[OCRS],[Wol.th],[MN98],[OR94]}. We refer
to van Raamsdonk~\cite{[Raa.th]} for a survey.


\subsection*{Expression Reduction Systems}

Here we use \emph{Expression Reduction
Systems}~(ERSs),  defined in~\cite{[OCRS]} (under
the name of CRSs). The present formulation 
follows~\cite{[pun-ic]} and is simpler.



\begin{definition}
\label{D.1.}
Let $\Sigma$ be an \emph{alphabet} comprising \emph{variables}
$x,y,z,\ldots$; \emph{function symbols}, also called \emph{simple operators};
and \emph{operator signs} or \emph{quantifier signs}.  Each function symbol
has an \emph{arity} $k\in N$, and each operator sign $\sigma$ has an
\emph{arity} $(m,n)$ with $m,n\neq 0$ such that, for any sequence
$x_1,\ldots ,x_m$ of pairwise distinct variables, $\sigma x_1\ldots x_m$
is a \emph{compound operator} or a \emph{quantifier} with \emph{arity}
$n$. Occurrences of $x_1,\ldots,x_m$ in $\sigma x_1\ldots x_m$ are
called \emph{binding
variables}.  Each quantifier sign $\sigma$,  as well as any
corresponding quantifier $\sigma x_1\ldots x_m$ and binding variables
$x_1\ldots x_m$, have a \emph{scope indicator} $(k_1,\ldots ,k_{l})$ to
specify the arguments in which $\sigma x_1\ldots x_m$ binds all free
occurrences of $x_1,\ldots ,x_m$. \emph{Terms} are constructed from
variables by using functions and quantifiers in the usual way: variables
are terms, and if $t_1,\ldots,t_n$ are terms and $\delta$ is an $n$-ary
(simple or compound) operator, then $\delta(t_1,\ldots,t_n)$ is a term too.

\emph{Metaterms} are constructed similarly from \emph{terms}  and 
\emph{metavariables} $A, B,\ldots$ that range over terms, but with an 
extra operation: if $t_0,\ldots,t_n$ are metaterms, then so is 
$(t_1/x_1,\ldots,t_n/x_n)t_0$, also called a \emph{metasubstitution}, 
where the \emph{scope} of each $x_i$ is $t_0$. Metaterms without 
metasubstitutions are \emph{simple me\-ta\-terms}.
An \emph{assignment} maps each metavariable to a term over $\Sigma$. If $t$
is a metaterm and $\theta$ is an assignment, then the $\theta$-\emph{instance}
$t\theta$ of $t$ is the term obtained from $t$ by replacing
metavariables with their values under $\theta$, and by replacing
metasubstitutions ($t_1/x_1,\ldots ,t_n/x_n)t_0$, in right-to-left
order, with the result of substitution of terms $t_1,\ldots ,t_n$
for free occurrences of $x_1,\ldots,x_n$ in~$t_0$. The substitution 
operation may involve a \emph{renaming} of bound variables 
to avoid collision, and we assume that the set of variables in $\Sigma$ comes 
equipped with an equivalence relation, called renaming, such that any 
equivalence class of variables is infinite. We also assume that any variable 
can be renamed by any other variable in the corresponding equivalence 
class.\footnote{An equivalence class of variables can, for example, be 
the set of variables of the same type in a typed language.} 
Unless otherwise specified, the default renaming relation is the total 
binary relation on variables (a partial renaming relation may be useful 
for conditional systems).
\end{definition}

For example, a $\beta$-redex in the $\lambda$-calculus appears as
$Ap(\lambda x\;t,s)$ in our notation, where
$Ap$ is a function symbol of arity 2, and
$\lambda$ is an operator sign of arity (1,1) and scope indicator (1).
Integrals such as $\int_{s}^{t}f(x)\,dx$ can be represented as $\int\!\!
x\,s\,t\,f(x)$ using an operator sign $\int$ of arity (1,3) and scope
indicator (3).



\begin{definition}
\label{D.CRS.}
A \emph{Conditional Expression Reduction System} (CERS) is a pair 
$(\Sigma,R)$, where $\Sigma$ is an \emph{alphabet} described in 
Definition~\ref{D.1.} and $R$
is a set of \emph{rewrite rules} $r:t\ar s$, where $t$ and $s$ are closed
metaterms (i.e., no free variables) such that $t$ is a simple metaterm and
is not a metavariable, and each metavariable that occurs in $s$ occurs also
in~$t$. 

Furthermore, each  rule $r$ has a set of \emph{admissible assignments}
$AA(r)$ which, in order to prevent undesirable confusion of variable
bindings, must satisfy the following \emph{variable-capture-freeness}
condition: 

[vcf] for any  assignment  $\theta \in AA(r)$, any metavariable $A$ occurring
in $t$ or $s$, and any variable $x\in FV(A\theta)$, either every occurrence
of $A$ in $r$ is in the scope of some binding occurrence of $x$ in $r$, or
no occurrence is.

For any $\theta\in AA(r)$, $t\theta$ is an $r$-\emph{redex} or
an $R$-\emph{redex} (and so is any \emph{variant} of $t\theta$ obtained 
from it by renaming of bound variables), and $s\theta$ is the 
\emph{contractum} of $t\theta$.

If for any rule $r\in R$, $AA(r)$ is the maximal set of variable-capture 
free assignments, then the CERS is called an \emph{unconditional} 
Expression Reduction System, or simply an Expression Reduction System (ERS).
\end{definition}

For the sake of simplicity, we will restrict ourselves to 
\emph{variable-capture-free ERSs}, which are ERSs in which all
assignments are admissible for all rules. The results (and proofs)
are valid for the much larger class of \emph{fully-extended Context-sensitive 
CERSs}~\cite{[pun-ic]}. Roughly,
full extendedness means that an erasing step cannot turn a non-redex
instance of a left-hand side of a rule into a redex. For example, the
$\lambda\eta$-calculus is not fully extended because an erasing beta step
can create an $\eta$-redex above the contractum. It was first observed
by van Oostrom that the full extendedness restriction is necessary for many 
important results in the theory of higher-order rewriting, and since then
this restriction has been adopted in many recent 
works \cite{[Raa.th],[Oos],[HP96],[Oos97],[Oos99],[pun-ic]}.

We ignore questions relating to
renaming of bound variables. As usual, a rewrite step consists of
replacement of a redex by its contractum. Subterms of a redex corresponding
to metavariables are \emph{arguments} of the redex, and the rest is its
\emph{pattern}. Note that the use of metavariables in rewrite rules of ERSs is
not really necessary -- free variables can be used instead, as in TRSs,
since (free) variables in TRS rules play the role of metavariables in ERS
rules. We will indeed do so at least when giving TRS examples.


\subsection*{Examples}

Our syntax is similar to that of Klop's CRSs~\cite{[Kl.CRS]}, but 
has the attraction
that it is closer to the syntax of the $\lambda$-calculus. For
example, the $\beta$-rule is written as $Ap(\lambda xA,B)\ar
(B/x)A,$ where $A$ and $B$ can be instantiated by any terms; the
$\eta$-rule is written as $\lambda x(Ax)\ar A$ which requires that an
assignment $\theta$ is admissible iff $x\not\in (A\theta)$, otherwise an
$x$ occurring in $A\theta$ and therefore bound in $\lambda x(A\theta
x)$ would become free. A rule like $f(A)\ar\exists x(A)$ is also allowed,
but an assignment $\theta$ with $x\in A\theta$ is not. The $\mu$-recursor
rule is written as $\mu(\lambda x A)\ar (\mu(\lambda x A)/x)A$.
$\,\, \exists xA  \ar  (\tau x(A)/x) A$ and  $\exists !xA \ar \exists
xA\wedge\forall x\forall y (A\wedge (y/x)A\impl x=y)$ are rules
corresponding to familiar definitions.





\begin{notation}
We use $a,b, c,d$ for constants, $t,s,e,o$ for terms, $u,v,w$ for
redexes,  and $N,P,Q$ for reductions.  We write $s\ssq t$ if $s$ is a
subterm of $t$.  A one-step reduction contracting a redex
$u\subt t$ is written as $t\stackrel{u}{\ar} s$ or $t\ar s$ or just $u$.
We write $P:t\doar s$ if $P$ denotes a reduction of $t$ to $s$.
$P+Q$ denotes the concatenation of $P$ and $Q$. We write $U\subt t$ if
$U$ is a set of redexes in $t$.
\end{notation}



\subsection*{Orthogonality, Residuals, and L\'evy-equivalence}



The definition of \emph{orthogonality} in ERSs is similar to the case of
CRSs: all the rules are left-linear and in no term redex-patterns can
overlap~\cite{[Kl.CRS]}. The \emph{residual} relation on redexes in ERSs 
is defined as a combination of the residual relations in TRSs and the \lc, 
since any ERS step can be decomposed into a TRSs step followed by a number 
of substitution steps. Since the residual concept is so familiar both in 
TRSs and the \lc\, we do not reintroduce the concept here for ERSs, 
and instead refer to~\cite{[OCRS],[pun-ic]} for more details. 
\emph{Developments} of sets of redexes $U\subt t$ are defined in ERSs 
as usual~\cite{[Bar]}.


As in the case of the \lc~\cite{[Bar]} or OCRSs, for any co-initial 
reductions $P$ and $Q$, one can define in OERSs the notion of \emph{residual 
of $P$ under $Q$}, written $P/Q$, using Klop's method of commutative 
diagrams~\cite{[Kl.CRS]}. Klop's method is equivalent to L\'evy's original 
definition of the residual relation in the \lc~\cite{[levy],[le80]}; 
the latter is of more `algebraic' nature and uses multisteps rather than 
complete developments (multisteps contract a set of redexes in a term 
simultaniously; multisteps are well defined by the Finite Developments 
theorem).


We write $P\lleq Q$ if $P/Q=\emptyset$,
where $\lleq$ is the \emph{L\'evy-embedding} relation.  $P$ and $Q$ are
called \emph{L\'evy-equivalent}\footnote{or \emph{strongly-equivalent}, or
\emph{permutation-equivalent}}, written $P\leeqv Q$, if $P\lleq Q$
and $Q\lleq P$. It follows from the definition of $/$
that if $P$ and $Q$ are co-initial reductions in an OERS,
then $(P+P')/Q= P/Q+P'/(Q/P)$ and $P/(Q+Q')=(P/Q)/Q'$.

We will often be interested in residuals of single redexes written
$u/P$ where $u$ is a single-step reduction contracting $u$, a redex 
in the initial term of $P$. For example, $P\leeqv Q$ for finite $P$ and 
$Q$ implies that $P$ and $Q$ end at the same term and that $u/P=u/Q$ for 
all redexes, $u$, in the initial term.


The \emph{Strong Church-Rosser (confluence)}
property is established for OERSs in \cite{[OCRS],[pun-ic]}; the 
Finite Developments Theorem~\cite{[Bar],[Kl.CRS]} is proved first, from which 
strong confluence follows by a standard argument. Strong confluence for other
higher-order rewriting formats are obtained, among others,
in~\cite{[Kl.CRS],[OR94],[Oos.th],[Mel]}.


\begin{theorem}
\label{T.FD.}
(\textbf{Finite Developments}) All complete developments of a set of 
redexes in a term $t$, in an OERS,
end at the same term $s$, and the residuals in~$s$ of any redex in $t$ along
any complete development are the same.
\end{theorem}

\begin{theorem}
\label{T.CRst.oc.}
(\textbf{Strong Church-Rosser}) For any co-initial
reductions $P$ and $Q$ in an OERS, $P+Q/P\leeqv Q+P/Q$.
\end{theorem}




\section{Stability and Relative Notions of Neededness}
\label{S.rel.need.}


In this section, we introduce notions of neededness relative to a set of
reductions $\Pi$ and to a set of terms $\stab$; all existing
notions of neededness can be obtained by specifying $\Pi$ or $\stab$;
$\stab$-neededness is a special case of $\Pi$-neededness. We introduce
\emph{stability} of a set of terms in an OERS.
It is the aim of the Section~\ref{S.rel.normal.} to show that if
$\stab$ is stable, then a $\stab$-needed strategy is $\stab$-normalizing.

\subsection*{Relative Neededness}

\begin{definition}\label{D.exter.and.vanish.}

\begin{enumerate}
\item[(1)]  $P:t\doar o$ is \emph{external} to a redex $u\subt t$ 
if $P$ does not contract any residual of~$u$.

\item[(2)] $P:t\doar o$ is \emph{external} to a set of redexes
$U\subt t$ if $P$ is external to all $u\in U$.

\item[(3)] $P$ \emph{$\stab$-suppresses} $u$ if $P$ is
$\stab$-normalizing and is external to~$u$.

\item[(4)] $P$ \emph{erases} $u$ if $u/P=\emp$. Note that 
contracting a redex erases it.

\item[(5)] $P$ \emph{discards} $u$ if $P$ is external to $u$ and
erases it.
\end{enumerate}
\end{definition}


\begin{definition}
\label{D.rel.need.}
%\mbox{}
\begin{enumerate}
\item[(1)] Let $\Pi$ be a set of reductions in an OERS $R$. We call a redex
$u\subt t$ \emph{$\Pi$-needed} if in every reduction in $\Pi$ 
starting from $t$ at least one of its residuals is contracted (i.e., 
no reduction in $\Pi$ is external to $u$) and call it
\emph{$\Pi$-unneeded} otherwise. 

\item[(2)] Let $\stab$ be a set of terms in an OERS $R$. Let $\Pi_{\stab}$ 
be the set of all reductions that end at a term in $\stab$. These will be 
denoted \emph{$\stab$-normalizing} reductions. A term 
$t$ is denoted \emph{$\stab$-normalizing} if some $\stab$-normalizing 
reduction starts at $t$.
We call a redex $u$ \emph{$\stab$-needed}, written $\NEED_{\stab}(u,t)$, if
it is $\Pi_{\stab}$-needed, and call it $\stab$-unneeded,
written $\UN_{\stab}(u,t)$, otherwise.
\end{enumerate}
\end{definition}


Thus Huet and L\'evy neededness coincides with neededness w.r.t.\ the set
of normal forms. It is easy to see that Maranget's notion of
neededness~\cite{[Mar]}, where a redex is needed if it has a residual along
any reduction external to it, coincides with neededness w.r.t.\ the set of
fair reductions~\cite{[morn]}. 
(Recall that a reduction is fair if all redexes in any of
its terms are erased in it.) Obviously, any redex in a term that is not
$\stab$-normalizable is $\stab$-needed; we call such redexes
\emph{trivially $\stab$-needed}.


\subsection*{Stability}

\begin{definition}
A set $\stab$ of terms is \emph{stable} if:
\begin{enumerate}
\item[(a)] $\stab$ is \emph{closed under reduction}: if $t\in\stab$
and $t\ar s$, then $s\in\stab$; and

\item[(b)] $\stab$ is \emph{closed under unneeded expansion}: for any 
$e\red{u}o$
such that $e\not\in \stab$ and $o\in \stab$, $u$ is $\stab$-needed.
\end{enumerate}
\end{definition}



The most appealing examples of stable sets in an OERS are
normal forms~\cite{[H.L.]}, head-normal forms~\cite{[B.K.K.S.]},
weak-head-normal forms, constructor-head-normal
forms for constructor
TRSs~\cite{[Nok.thi.]}, and root-stable forms (terms
that cannot be rewritten to a redex)~\cite{[Mid]}.

Such sets are closed under reduction, which seems a natural condition for
stability. Closure under uneeded expansion is less intuitive, but without
it there will be $\stab$-normalizable terms with no $\stab$-needed redex.
For example, consider $R=\{I(x)\ar x\}$, and $\stab$ that contains $I(t)$,
but not $I(I(t))$, for some term $t$. There is no
$\stab$-needed redex in $I(I(t))$ as it can be
reduced to $I(t)$ by reducing either $I$ redex .

\subsection*{Weaker Stability Conditions}

A weaker definition of stability is studied
in~\cite{[ctrs]} where a set $\stab$ of terms is said to be
stable if it is closed under unneeded expansion and is 
\emph{closed under parallel moves}:

\begin{definition}
A set $\stab$ is \emph{closed under parallel moves} if for all $t\not\in \stab$,
and $P:t\doar o\in \stab$, then for any $Q:t\doar e$ that contains no term
in $\stab$, the final term of $P/Q$ is in $\stab$.
\end{definition}
Clearly, closure under reduction implies closure under parallel moves.
The $\stab$-needed strategy can also be proven to be $\stab$-normalizing
under these weaker conditions.
This rather technical definition ensures that if unneeded steps are
taken when  a normalizing needed reduction exists, it is still possible
to reach a term in $\stab$ by completing the residual of the normalizing
reduction.



\section{A Labelling for OERSs}
\label{S.labels}

We now introduce a labelling system for ERSs
which will be used to establish termination of certain reductions and
in section~\ref{S.un.opt.}
to define the concept of a redex \emph{family}.

\newcommand{\rulerewritesto}{\rightarrow}

Fix some OERS $R$.
For technical reasons, we assume that $R$ does not contain any rules
whose left-hand side consists of just an operator applied to variables 
and metavariables.
This is not a substantial restriction, since if the system includes
a rule of the form $f(x,y,z) \rulerewritesto \dots$,
we can replace the symbol $f(\dots)$ wherever it occurs by
$g(f(\dots))$, where $g$ is a new unary function symbol.
The new system will behave in all essential respects like the old
and will satisfy the restriction. A similar restriction is
adopted in~\cite{[Kl.CRS]}.

Let there be a set ${\cal L}_0$ of \emph{atomic labels},
and two  sets ${\cal C}$ and ${\cal C}'$ of \emph{label constructors} 
in $1-1$ correspondence with the set of subterms
of all the right-hand sides of the rules of the OERS, and in $1-1$ 
correspondence with the rules of the OERS, respectively.
The arity of each constructor in ${\cal C}'$ is the number of nodes in the 
left hand side of the rule which it
is associated with, excluding variable and metavariable nodes and the root.
And the arity of each constructor in $\cal C$ is $1$.
The set ${\cal L}$ of labels is the set of terms freely generated
by ${\cal L}_0$ and ${\cal C}\cup {\cal C}'$.
The \emph{height} of a label is its height considered as a tree.

We add all members of ${\cal L}$ to the OERS as new unary function
symbols.
By a \emph{labelled term} we mean any term which results from this
extension of the signature.
Every labelled term $t$ determines an unlabelled term $U(t)$ by simply
dropping the labels --- that is, by replacing every subterm of the form
$l(t')$ by $t'$, where $l$ is any label.
A labelling of a term is \emph{initial} if all its subterms are labelled
by different atomic labels.

Although for technical reasons we have introduced labels as new function
symbols, in writing terms down we shall indicate labels by superscripts.
A term $\alpha(\beta(\gamma(t)))$ would be written
$t^{\gamma\beta\alpha}$.
This suggests an alternative way of looking at labels, closer to the way
L\'evy and Klop use them: the labels are considered to be annotations
attached to the nodes of the syntax tree of the unlabelled term.

We now construct the set of \emph{labelled rules}.
Given any rule $s \rulerewritesto t$ of the unlabelled system,
and labellings $f$ of $s$ and $f'$ of $t$,
$s^f \rulerewritesto t^{f'}$ is a labelled rule provided that:
\begin{itemize}
\item
$f$ does not label the root of $s$, nor any occurrence of a metavariable.
\item
$f'$ attaches the label $c(c'(l_1,\dots,l_n))$ to each subterm of $t$,
other than metasubstitutions, where
$c$ is the label constructor corresponding to $t$, 
$c'$ is the constructor corresponding to the rule, and
$l_1,\dots,l_n$ are the labels present in $f(s)$, listed in depth-first
left-to-right order.
\end{itemize}
The choice of depth-first left-to-right ordering is not significant for
the theory; it is merely a convenient standard choice.
Note that $f'$ is completely determined by $f$, $s$, and $t$.
All nodes of $t^{f'}$ have distinct
labels, and different labellings of $s$ give different labellings of
$t$.
The reason for the restriction we made earlier is to ensure that
every left-hand side has at least one place to attach a label to.

The set of labelled rules constitutes the system ${\cal L}(R)$.
This is clearly an OERS.

As an example, consider the beta rule of lambda calculus.
In OERS notation, and writing the application operator explicitly, it is:
$$Ap( (\lambda x (A)), B ) \rulerewritesto (B/x)A$$
An example of a redex is
$$Ap( (\lambda y (Ap( y, y ))), (\lambda z(z)) )$$
A labelled version of this redex is:
$$(Ap( (\lambda y (Ap( y^\alpha, y^\beta))^\gamma)^\delta, 
(\lambda z(z)^\epsilon)^\zeta ))^\eta$$
This contains a redex of the labelled rule:
$$Ap( (\lambda x (A))^\delta, B) \rulerewritesto 
(B^{c(g(\delta))}/x)A^{d(g(\delta))}$$
where $g$ is the label constructor for the $\beta$-rule)
and it reduces to:
$$((Ap( ((\lambda z (z^\epsilon))^\zeta)^{c(g(\delta))},
((\lambda z (z^\epsilon))^\zeta)^{c(g(\delta))}))^{d(g(\delta))})^\eta.$$

For a redex $u$ in a labelled term, we define $\lab(u)$ to be
$c'(l_1,\ldots,l_n)$, where $c'$ is the constructor for the rule for $u$
and $(l_1,\ldots,l_n)$ is the tuple of labels in the left-hand side of 
the labelled rule for $u$. We call this the \emph{label} of the redex. The 
\emph{index} $\Ind(u)$ of $u$ is the height of
$lab(u)$. The \emph{index} $\Ind(P)$ of a
reduction $P$ is the maximal index of the redexes contracted in it.

This definition of labelling differs slightly from that of
Klop~\cite{[Kl.CRS]}. Klop combines multiple labels on a single term into
a single compound label, and thus for his definitions a term $t^\alpha$
is not a subterm of ${t^\alpha}^\beta$, whereas for us the term
$t^\alpha$ is a subterm of $(t^\alpha)^\beta$. He also represents
compound labels as flat strings, instead of structured terms, using
multiple underlining where we use multiple nesting.  In addition, our
use of label constructor symbols provides a greater generality which
allows us to simultaneously treat several variants of labelled rewrite
systems uniformly. (For example, in the case of the \lc, there are
two constructors in $\cal C$ corresponding to underlining and 
overlining~\cite{[le76],[levy]}. In the case of Interaction 
Systems~\cite{[AL]} the constructors in $\cal C$ replace
addresses in right-hand sides of rules. In the case of Klop's labelling
system~\cite{[Kl.CRS]}, all constructors are `empty'. Redex-labels 
occurring as the arguments in right-hand sides of rewrite rules correspond
to (constrained) labelled patterns in Maranget's labelling system for 
TRSs~\cite{[Mar91]}. And in his labelling system for HRSs, van 
Oostrom~\cite{[Oos]}
uses numbers where we use constructors in $\cal C$, and he uses rules where we
use label constructors in ${\cal C}'$.) 
However, our definitions are sufficiently close that
Klop's results for labelled systems carry over to the present setting.

The crucial properties of labelled reduction are given by the following 
propositions.

\begin{proposition}
\label{P.lab.nest.}
If a step $t\red{u}s$ in an OERS $R$ creates a redex $v\subt
s$, then, for any labelling $t^l$ of $t$, the corresponding step
$t^l\red{u^{l'}}s^{l''}$ in the corresponding labelled OERS $R^L$ creates a
redex $v^{l^*}$ whose label $l^*$ strictly contains the label
$l'$ of $u$. Thus
$\Ind(u^{l'})<\Ind(v^{l^*})$. If $w\subt s^{l''}$ is a residual of a redex
$w'\subt t^l$, then $w$ and $w'$ have the same labels, thus
$\Ind(w)=\Ind(w')$.

\begin{proof}
Easy from the definition of labelling.
Note that this is where we require the restriction on labelled
OERSs, that each left-hand side contain more than one function symbol.
\end{proof}
\end{proposition}


\begin{corollary}
\label{P.extr.cre.}
In an OERS, let $P$ and $Q$ be co-initial reductions such that $P$
creates a redex $u$ and $Q$ is external to every redex of $t$ having
a residual contracted
in $P$. Then every member of $u/(Q/P)$ is created by $P/Q$, and $Q/P$
is external to $u$.
\end{corollary}

\begin{proposition}
\label{P.BCT.}
In a labelled OERS, every reduction for which there is a bound on the
indexes of the redexes it reduces is terminating.

\begin{proof}
See~\cite{[Kl.CRS],[Mel],[Oos97]}.
\end{proof}
\end{proposition}



\section{The Relative Normalization Theorem}
\label{S.rel.normal.}


In this section, we present a uniform proof of correctness of the needed
strategy that works for all stable sets $\stab$ of `normal forms'. Our proof
differs from all known proofs because properties of needed and unneeded
redexes are different when arbitrary stable sets are considered. 
The main difference is that
$\stab$-unneeded redexes may replicate $\stab$-needed ones. However, the
termination argument we use is the same as in~\cite{[K.S.]} and
in~\cite{[Mar]}, and is based on Proposition~\ref{P.BCT.}. The main idea
and a proof in the same spirit is already in~\cite{[le80]}. As in most
earlier proofs, we use the fact that residuals of unneeded redexes remain
unneeded, and that unneeded steps cannot create needed redexes. However, in
order to prove that every needed redex has at least one needed residual
after contacting any other redex, we need first to show the existence of a
needed normalizing reduction.

In the rest of this section $\stab$ always denotes a stable set of terms.

\begin{lemma}\label{L.external.rem.ext.}
Let $P:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_n$ be external to
$U=\{u_1,\ldots,u_n\}\subt t_0$, and let $Q_0:t_0\doar o_0$. Then
$P'=P/Q_0$ is external to $U'=U/Q_0$. If $P$ is $\stab$-normalizing, then
so is $P'$.

\begin{proof}
Let $P_i:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_i$, $Q_i=Q_0/P_i$, and
$P'_{i+1}=v_i/Q_i$, $0\leq i<n$ (see the figure below). Since $P$ is
external to $U$, we have for each $i$ that $v_i\not\in U/P_i$. Therefore,
$v_i/Q_i\,\cap\, U/(P_i+Q_i)=\emptyset$ (since the residuals of different
redexes are different). Thus, by \Tr{T.CRst.oc.}, $v_i/Q_i\,\cap\,
U/(Q_0+P'_1+\ldots+P'_{i})=\emptyset$. Hence, $P'_{i+1}$ is external to
$U'/(P'_1+\ldots+P'_{i})$. This means that $P'$ is external to $U'$. If $P$
is $\stab$-normalizing, then so is $P'$, by the closure of $\stab$ under
reduction.


%\begin{figure}
\begin{diagram}
t_0  & \rTo^{v_0=P_1} & t_1  & \rOnto   & t_{n-1} &  \rTo^{v_{n-1}} & t_n   \\
\dOnto^{Q_0}&     &  \dOnto^{Q_1} &   &     \dOnto^{Q_{n-1}}   &   &
\dOnto_{Q_n}\\
o_0  & \rOnto_{P'_1} & o_1  & \rOnto  & o_{n-1} &  \rOnto_{P'_{n}} &   o_n   \\
\end{diagram}
%\caption{Preservation of External Reductions}\label{extern-red}
%\end{figure}
\end{proof}
\end{lemma}


\begin{corollary}
\label{T.3.1.c.}
For stable $\stab$, residuals of $\stab$-unneeded redexes
are $\stab$-unneeded.
\end{corollary}






\begin{lemma}
\label{L.4.1.c.}
Let $t\not\in \stab$, $t\red{u}t'$, $\UN_{\stab}(u,t)$,  and let $u'\subt
t'$ be a created redex. Then $\UN_{\stab}(u',t')$.
(Unneeded redexes cannot create needed redexes.)

\begin{proof}
$\UN_{\stab}(u,t)$ implies existence of $P:t\doar e$ that $\stab$-suppresses
$u$; thus $P$ is external to $u$. By Corollary~\ref{P.extr.cre.},
$P/u$ is external to $u'$. Also, $P/u$ is $\stab$-normalizing since $\stab$
is closed under reduction. Hence $u'$ is $\stab$-unneeded.
\end{proof}
\end{lemma}




We call  $P:t_0\ar t_1\ar\ldots$  \emph{$\stab$-(un)needed} if it
contracts only $\stab$-(un)needed redexes.

\subsection*{Relative Normalization}

\begin{theorem}
\label{T.ex.M-need.}
(\textbf{Relative Normalization}) Let $\stab$ be a stable set of terms in an
OERS~$R$.
\begin{enumerate}
\item[(1)] Every $\stab$-normalizable term $t\not\in\stab$ in $R$ contains an
$\stab$-needed redex.

\item[(2)] If $t\not\in\stab$ is $\stab$-normalizable, then any $\stab$-needed
reduction starting from $t$ eventually reaches a term in~$\stab$.
\end{enumerate}

\begin{proof}
\begin{enumerate}
\item[(1)] Let $P:t\doar s\red{u}e$ be an $\stab$-normalizing reduction that
does not contain terms in $\stab$ except for $e$. By the stability of
$\stab$, $u$ is $\stab$-needed. By Corollary~\ref{T.3.1.c.} and
Lemma~\ref{L.4.1.c.}, either it is a residual of an
$\stab$-needed redex in $t$, or it is created by an earlier step
$v$ of $t\doar s$ where $v$ is $\stab$-needed.
In the latter case the argument may be repeated.

\item[(2)] Let $P:t\doar e$ be an
$\stab$-normalizing reduction 
that does not contain terms in $\stab$ except for $e$, and let
$Q:t\red{u_0}t_1\red{u_1}\ldots$ be an $\stab$-needed reduction. Further,
let $Q_i:t\red{u_0}t_1\red{u_1}\ldots\red{u_{i-1}}t_i$ and $P_i=P/Q_i$,
$i\geq 1$ (see the figure). Let $R^L$ be the corresponding labelled OERS of
$R$, let $t$ have an initial labelling, and assume that $P$ and $Q$ are
reductions in $R^L$. By Proposition~\ref{P.lab.nest.}, $\Ind(P_i)\leq
\Ind(P)$. Since
$Q$ is $\stab$-needed and $P_i$ is $\stab$-normalizing (by the closure of
$\stab$ under reduction), at least one residual of $u_i$ is contracted 
in $P_i$. Therefore, again by Proposition~\ref{P.lab.nest.}, $\Ind(u_i)\leq
\Ind(P_i)$. Hence $\Ind(Q)\leq \Ind(P)$ and $Q$ is terminating by
Proposition~\ref{P.BCT.}.

\begin{diagram}[height=1.5em,width=4em]
t            & \rOnto^{P}   &   s     \\
\dOnto^{Q_i}   &              &     \dOnto \\
t_i           & \rOnto_{P_i}&  {}          \\
\dTo^{u_i}     &              &     \dOnto \\
t_{i+1}        & \rOnto_{P_{i+1}}&  {}    \\
\dOnto          &              &     \dOnto \\
{}          & \rOnto       &  {}         \\
\end{diagram}
\end{enumerate}
\end{proof}
\end{theorem}


\noindent\notationn
$\,\,\,t\!\das$ denotes that $t$ is
$\stab$-normalizable, i.e., reducible to a term in $\stab$.



\begin{lemma}
\label{L.pers.need.}
Let $t\!\das$ and let $t\red{u}s$. Then  any $\stab$-needed redex $v\subt
t$ different from $u$ has an $\stab$-needed residual.

\begin{proof}
Let $P:s\doar o$ be an $\stab$-needed $\stab$-normalizing reduction; there
is one by Theorem~\ref{T.ex.M-need.}. Then if all $u$-residuals of $v$ were
$\stab$-unneeded, $P$ would $\stab$-suppress them, and $u+P$ would
$\stab$-suppress $v$, a contradiction.
\end{proof}
\end{lemma}


We conclude this section by summarizing the neededness properties of
residuals and created redexes, established in \Cr{T.3.1.c.}, \Lr{L.4.1.c.},
and \Lr{L.pers.need.}, in the following proposition.



\begin{proposition}
\label{P.3.3.c.}
%\mbox{}
\begin{enumerate}
\item[(1)]  Residuals of $\stab$-unneeded redexes in a term $t\not\in\stab$ 
remain $\stab$-unneeded.

\item[(2)] Let $t\not\in \stab$, $t\red{u}t'$, $\UN_{\stab}(u,t)$,  and let
$u'\subt t'$ be a created redex. Then $\UN_{\stab}(u',t')$.

\item[(3)] Let $t\!\das$, $t\red{u}s$, $v\subt t$ be $\stab$-needed, and 
$v\not=u$. Then $v$ has an $\stab$-needed residual in $s$.
\end{enumerate}
\end{proposition}




\section{The Relative Hypernormalization Theorem}
\label{S.hyp.nr.}



In this section, we prove the Relative Hypernormalization Theorem for all
\emph{regular} stable sets of final terms in OERSs, and demonstrate that
the theorem fails for some irregular stable sets. Thus this theorem refines
the Relative Normalization Theorem, but is less general as it is restricted
to regular stable sets of results only. However, regularity is not a
restriction from a practical point of view, as all the sets of results that
have been used in practical programming languages are regular.  Moreover, it
allows for much simpler proofs. We do not need to consider termination
of reductions
with bounded index (\Pr{P.BCT.}), as the Finite Developments
Theorem is enough. We do not use the Standardization
Theorem~\cite{[H.L.],[Kl.CRS]} either.

\subsection*{Failure of Relative Hypernormalization for some stable sets}

For the case of normal forms, the needed strategy is
\emph{hypernormalizing}, that is, reductions starting from a normalizable
term that contract finite sequences of unneeded steps
in addition to needed redexes are still normalizing.

The following example shows that this need not be
the case for all stable sets $\stab$:

\begin{example}
\label{hyper.failure}
Consider $R=\{f(x)\ar h(x,f(x)),\,a\ar b\}$ and take
for $\stab$ the set of terms not containing occurrences of $a$. Then the
reduction $f(a)\ar h(a,f(a))\ar$ $h(b,f(a))\ar$ $h(b,h(a,f(a)))\ar$
$h(b,h(b,f(a)))\ar\ldots$ contracts
infinitely many $\stab$-needed redexes, while the reduction $f(a)\ar f(b)$ is
$\stab$-normalizing. This example shows also that multistep $\stab$-needed
reductions need not be $\stab$-normalizing:
group each pair of consecutive steps in the reduction above as a
multistep.
\end{example}


\subsection*{Regular Stable Sets}

For some stable $\stab$, $\stab$-unneeded redexes may
contain $\stab$-needed ones. Consider the simpler example
$R=\{f(x)\ar g(x),\, a\ar b\}$,
where $\stab$ is the set of terms not containing occurrences of $a$: we observe
that $a$ is $\stab$-needed in $f(a)$, but $f(a)$ is not.

Nesting of $\stab$-needed redexes within $\stab$-unneeded ones need
not cause problems; the failure of hypernormalization arises from duplication
of $\stab$-needed redexes by $\stab$-unneeded ones.
Hence we introduce the following definition:

\begin{definition}
We call a stable set $\reg$ \emph{regular} if, for any $t\not\in\reg$,
$\reg$-unneeded redexes cannot duplicate $\reg$-needed ones.
\end{definition}


Recall from~\cite{[le80]} that multistep needed reductions are normalizing
in the $\lambda$-calculus. The same holds for all regular
stable $\reg$; this follows immediately from hypernormalization of the
$\reg$-needed strategy, which we will prove in the rest of the section.

\subsection*{Canonical forms for Relative Reductions}


The proof uses the ability to transform any reduction into an equivalent
form where $\reg$-needed steps precede $\reg$-unneeded steps, while
conserving the number of $\reg$-needed steps.

\begin{definition}
\label{D.4.1.}
We call $P$ \emph{$\stab$-quasi-needed} if $\NEED_\stab \vert P\vert=\infty$,
where  $\NEED_\stab \vert P\vert$ denotes the number of  $\stab$-needed steps
in $P$. We call $P$ \emph{$\stab$-semi-needed} if it can be expressed as
$P=P_{N}+P_{U}$, where $P_N$ is $\stab$-needed and $P_U$ is
$\stab$-unneeded. In the latter case, we call $P_N$ the
\emph{$\stab$-needed part} of $P$, and call $P_U$ the
\emph{$\stab$-unneeded part} of $P$.
\end{definition}


In the following definition, we describe an algorithm that, for a
\emph{regular} stable $\reg$ in an OERS, transforms any finite reduction
$P$ into an $\reg$-semi-needed reduction L\'evy-equivalent to $P$, and any
$\reg$-quasi-needed reduction $Q$ into an infinite $\reg$-needed reduction.
The regularity of $\reg$ is essential for termination of the transformation
process, and for preservation of $\reg$-quasi-neededness of the reduction
under transformation. The latter property is crucial for our method of
proving the Relative Hypernormalization Theorem.



\begin{definition}
\label{D.4.2.}
Let  $Red$ be the set of all reductions in an OERS $R$, let $\reg$ be a
regular stable set of terms in $R$, and let $Red^{*}$ be the  set of
$\reg$-semi-needed reductions.  We will define a function $K:Red \ar Red^{*}$.
For any reduction $P$, with finite $\reg$-needed steps, we will denote
the $\reg$-needed part $K_{N}(P)$ and the $\reg$-unneeded part $K_{U}(P)$
so that $K(P)=K_{N}(P)+K_{U}(P)$.
$K$ is defined as follows:
\begin{enumerate}
\item[(a)] Let $P$ be a finite reduction. $K(P)$ is the $\reg$-semi-needed
reduction obtained from $P$ as follows: find in $P$ the
leftmost subreduction $P_1:t\red{u}s\red{v}o$ such that $\UN_\reg(u,t)$
and $\NEED_\reg(v,s)$. Let $P=P_0+P_1+P_2$. By \Pr{P.3.3.c.}.(2), $v$ is a
residual of a redex $v'\subt t$, which is $\reg$-needed by
\Pr{P.3.3.c.}.(1). Since $\reg$ is regular, $v$ is the only residual of
$v'$, hence $P_1$ and $P'_1=v'+u/v'$ are both complete developments of the
set $u,v'\subt t$. Now replace $P_1$ by $P'_1$ in $P$. Transform the
obtained reduction $P'$ in the same way, and so on, as long as possible.
Obviously, the number of $\reg$-unneeded steps in $P'$ preceding $v'$ is
less than the number preceding $v$ in $P$, and the number of $\reg$-needed
steps in $P$ and $P'$ coincide. Therefore, the procedure terminates.
The result is $K(P)$. Obviously, $P\leeqv K(P)$, and $K(P)\in
Red^{*}$.

\item[(b)] Let $\NEED_\reg \vert P\vert <\infty$ ($\vert P\vert =\infty$ is
possible). $P$ can be expressed as $P=P_1+P_2$, where $P_2$ is
$\reg$-unneeded  and the last step in  $P_1$ is $\reg$-needed. Then we take
$K(P)=K(P_1)+P_2$, which is possible since $P_1\leeqv K(P_1)$. Obviously,
$K(P)\in Red^{*}$ and $P\leeqv K(P)$.

\item[(c)] Let $\NEED_\reg \vert P\vert=\infty$.  Suppose that $P_i$ is 
the  initial
part of $P$ with  a length  $i$ and  $Q_{i}=K_{N}(P_{i})$. Let $\vert 
Q_i\vert =m_i$. We define $K(P)$ as the
reduction whose prefix of length $m_i$ is given by $Q_{i}$
($i=0,1,\ldots $). It follows from (a)-(b) that if $i<j$,  then $Q_{i}$ is
a prefix of $Q_{j}$, so $K(P)$ is defined consistently. Obviously,
$K(P)$ is $\reg$-needed and hence $K(P)\in Red^{*}$.
\end{enumerate}
\end{definition}


\begin{lemma}
\label{L.4.4.}
Let $P$ be a finite or infinite reduction in an OERS, and let $\reg$ be 
regular.
\begin{enumerate}
\item[(1)] If $P$ ends at a term in $\reg$, then $K_{N}(P)$
ends at a term in $\reg$ as well.

\item[(2)] If $\NEED_\reg\vert P\vert=\infty$, then $K(P)$ is $\reg$-needed, 
and is infinite.
\end{enumerate}


\begin{proof}
\begin{enumerate}
\item[(1)] follows from the stability of~$\reg$ --- $K(P)$ is 
$\reg$-semi-needed,
it ends at $\reg$, and the step of $K(P)$ entering $\reg$ is $\reg$-needed.

\item[(2)] follows immediately from Definition~\ref{D.4.2.}.
\end{enumerate}
\end{proof}
\end{lemma}


\begin{lemma}
\label{L.4.5.}
Let  $t_{0}$  have  an $\reg$-quasi-needed  reduction and $t_0\red{u}s_0$.
Then $s_0$ also has an $\reg$-quasi-needed reduction.

\begin{proof}
By Lemma~\ref{L.4.4.}, $t_{0}$ has an infinite $\reg$-needed reduction
$P:t_0 \red{u_{0}}t_{1}\red{u_{1}}\ldots$.  Let $U_{i}=u/(u_{0}+ \ldots
+u_{i-1})$,  $i=0,1, \ldots $. We can
construct the diagram below. It follows from finiteness of developments
that there  are infinitely  many numbers $k$ such that $u_{k}\not\in U_{k}$
(otherwise there should be a number $m$ such that
$t_m\red{u_m}t_{m+1}\red{u_{m+1}}\ldots$ is an infinite
$U_{m}$-development). By \Pr{P.3.3.c.}.(3), $u_{k} \not\in U_{k}$ and
$\NEED_\reg (u_{k},t_{k})$ imply that $u_{k}$ has at least one  $\reg$-needed
$U_{k}$-residual  in  $s_{k}$,  i.e. $u_k/U_k$ contains  at least  one
$\reg$-needed  step. Hence  $P/u$ is $\reg$-quasi-needed.
\end{proof}

\begin{diagram}
t_0    &   \rTo^{u_0}  &   t_1   &   \rTo^{u_1}  &   t_2    &  \rOnto  & {} \\
\dTo^{u=U_0}  &     & \dOnto^{U_1} &          & \dOnto^{U_2}&         &     \\
s_0    &   \rOnto_{u_0/U_0}  &   s_1   &   \rOnto_{u_1/U_1}  &   s_2   &
\rOnto  &   {} \\
\end{diagram}

\end{lemma}


\subsection*{Relative Hypernormalization}

\begin{theorem}
\label{T.4.2.}
(\textbf{Relative Hypernormalization}) Let $\reg$ be a regular stable set of
terms in an OERS $R$, and let $t\not\in \reg$ be a term in $R$. Then $t$
has an $\reg$-normal form  iff it does not possess a reduction in which
infinitely many times $\reg$-needed redexes are contracted.

\begin{proof}
($\Rightarrow$) Let $t\dored{P}s\in \reg$. Suppose on the contrary that
there is an $\reg$-quasi-needed $Q$ starting from $t$. Then by \Lr{L.4.5.}
$Q/P$ is $\reg$-quasi-needed as well. By closure of $\reg$ under 
reduction, $Q/P$ is in $\reg$ -- a contradiction,
since terms in 
$\reg$ do not contain
$\reg$-needed redexes. ($\Leftarrow$) By \Tr{T.ex.M-need.}.(1), one can
repeatedly contract $\reg$-needed redexes in $t$, unless a term in $\reg$
is reached; the latter is inevitable since $t$ does not have an infinite
$\reg$-needed reduction.
\end{proof}
\end{theorem}








\section{Minimal Relative Normalization}
\label{S.min.}

The theory of \emph{minimal} reduction in the framework of relative
normalization is based on reducing no more redexes than necessary when
computing $\stab$-normal forms. A reduction $P:t\doar s$ with $t\not\in
\stab$ and $s\in \stab$ is $\stab$-minimal if $P\lleq Q$ for all
$\stab$-normalizing $Q:t\doar e$. Minimal $\stab$-normal forms, such
as $s$ above, are useful to compute since any other $\stab$-normal form is
accessible from them. 

We define \emph{$\stab$-external}, \emph{persistently
$\stab$-needed}, and \emph{$\stab$-erased} redexes. We show that each
class is a strict subset of the next when $\stab$ is regular, and use
such redexes to build $\stab$-minimal reductions for regular $\stab$. We 
show that $\stab$-minimal reductions need not exist for irregular 
stable~$\stab$.


\subsection*{Persistently $\stab$-needed and $\stab$-erased redexes}


\begin{definition}
\label{D.qpn.}
%\mbox{}
\begin{enumerate}
\item[(1)] We call $u\subt t$ \emph{persistently $\stab$-needed} if 
all residuals of $u$ are $\stab$-needed.

\item[(2)] We call $u\subt t$ \emph{$\stab$-erased} if
$u$ does not have a residual under any $\stab$-normalizing reduction.

\item[(3)] We call a reduction \emph{$\stab$-erased} if it only
contracts $\stab$-erased redexes.
\end{enumerate}
\end{definition}


Note that $\stab$-erased redexes need not be $\stab$-needed
(e.g., when $\stab$ is the set of normal forms and the OERS has
an erasing rule, say $f(x)\ar a$). The following example illustrates the
introduced concepts using a simple OTRS.

\begin{example}\label{E.nne.per.sec.con.}
Consider an OTRS $R=\{f(x)\ar g(x,h(x)),\,h(x)\ar c,\,a\ar b\}$ and a
term (redex) $u=f(a)$:
\begin{diagram}[height=2em,width=3em]
f(a)   & \rTo^f &           &       & g(a,h(a)) &  &  & \rTo^h  & g(a,c) \\
\dTo^a &        &           & \ldTo^a  &     & \rdTo^a &  & \ruTo^h & \dTo_a \\
       &        & g(b,h(a)) &             &  &    & g(a,h(b)) &  &\\
       &        &           & \rdTo_a  \rdTo(6,2)^h &  & \ldTo_a &       &  & \\
f(b)   & \rTo_f &           &       & g(b,h(b))   &  &    & \rTo_h &  g(b,c)  \\
\end{diagram}
\noindent
Consider the following sets of terms in the reduction graph
of $u$, in  $R$: the set
${\cal S}_1 = \{g(b,c)\}$ of normal forms; the set
${\cal S}_2 = \{g(b,h(a)),$$g(b,h(b)),$$g(b,c)\}$ of terms not containing
a redex on the left-spine, i.e. not containing a redex with its head symbol
on the left-spine, when the term is considered as a tree; the set
${\cal S}_3 = \{f(b),$ $g(b,h(b)),$ $g(b,c)\}$
of terms not containing occurrences
of $a$; and the set ${\cal S}_4 =$ $\{g(a,h(b)),$ $g(a,c),$ $f(b),$ $g(b,h(b)),$ $g(b,c)\}$
of terms not containing $a$ on the right-spine. Then
${\cal S}_1$ and ${\cal S}_2$ are regular stable sets;
${\cal S}_3$ is stable but not regular (since ${\cal S}_3$-unneeded redex
$u$ duplicates the ${\cal S}_3$-needed redex $a$); and ${\cal S}_4$ is not
stable, and for the two redexes
$u$ and $a$ in $u=f(a)$, we have the following:

\begin{enumerate}
\item
$u$ is ${\cal S}_1$-needed, persistently ${\cal S}_1$-needed, and ${\cal
S}_1$-erased. $a\subt u$ is ${\cal S}_1$-needed but not persistently ${\cal
S}_1$-needed, since the second residual of $a$ in $g(a,h(a))$ is ${\cal
S}_1$-unneeded. Nevertheless, $a$ is ${\cal S}_1$-erased.

\item
$u$ is ${\cal S}_2$-needed, persistently ${\cal S}_2$-needed, and ${\cal
S}_2$-erased. $a\subt u$ is ${\cal S}_2$-needed but not persistently ${\cal
S}_2$-needed. $a$ is not ${\cal S}_2$-erased as it has a residual
along the ${\cal S}_2$-normalizing reduction $u\ar g(a,h(a))\ar g(b,h(a))$.

\item
$u$ is neither (persistently) ${\cal S}_3$-needed nor ${\cal S}_3$-erased.
$a\subt u$ is ${\cal S}_3$-needed but not persistently ${\cal S}_3$-needed
(since the second residual of $a$ in $g(a,h(a))$ is ${\cal S}_3$-unneeded);
still, $a$ is ${\cal S}_3$-erased.

\item
Both $u$ and $a$ are neither (persistently) ${\cal S}_4$-needed nor ${\cal
S}_4$-erased.
\end{enumerate}
\end{example}



\begin{lemma}\label{L.prs.m-nee.sec.}
Every persistently $\stab$-needed redex is $\stab$-erased, but an
$\stab$-erased redex, even if $\stab$-needed, need not be
persistently $\stab$-needed.

\begin{proof}
($\Rightarrow$) Let $u\subt t$ be persistently $\stab$-needed, and let
$P:t\doar s$ be $\stab$-normalizing. If $u/P$ was not empty, then every
$u'\in u/P$ (the set of $P$-residuals of $u$) would be
$\stab$-needed, which is not possible since $s\in \stab$. ($\Leftarrow$)
>From \Er{E.nne.per.sec.con.} (cases  $1$ and $3$).
\end{proof}
\end{lemma}





\subsection*{Minimal Relative Reduction}



\begin{definition}
\label{D.m-min.}
We call $P:t\doar s$ \emph{$\stab$-minimal}\footnote{We prefer
to use minimal rather than \emph{least} or \emph{smallest}.}
if  it is $\stab$-normalizing
and $P\lleq Q$ for any $\stab$-normalizing $Q:t\doar o$. When $P$ is
$\stab$-minimal,  we call $s$ a \emph{minimal} $\stab$-normal form
of~$t$.
\end{definition}

It follows immediately from Definition~\ref{D.m-min.} that if
$t\!\das$ and $t\not\in\stab$, then $t$ has
no more than one minimal
$\stab$-normal form $s$. For any other $\stab$-normal form $e$ of $t$, it
holds that $s\doar e$. Note that the latter property of minimal
$\stab$-normal forms cannot be taken as the definition, because in that
case an $\stab$-normalizable term could have many minimal
$\stab$-normal forms, due for example to a cycle in $\stab$, and some of
them may require more reduction to be reached than others. For example,
take $R=\{a\ar b,\,b\ar a,\,f(x)\ar x\}$ and regular stable set
${\stab} = \{a,b\}$. The term $t=f(a)$ has two $\stab$-normal forms,
$a$ and $b$,
and each is accessible from the other. However, any reduction from $t$ to $b$
must contract the $\stab$-unneeded redex $a$ and therefore no
reduction from $t$ to $b$ can be considered as $\stab$-minimal.





\begin{lemma}
\label{L.qpn<min.}
Every $\stab$-erased $\stab$-normalizing reduction is $\stab$-minimal.

\begin{proof}
Let $P:t_0\red{u_0}t_1\ar\ldots\ar t_n$ be an $\stab$-erased
$\stab$-normalizing reduction, let $P_i:t_0\red{u_0}\ldots\ar t_i$, and let
$Q:t_0\doar o\in \stab$. By stability of $\stab$, $Q_i=Q/P_i$ is
$\stab$-normalizing. Since $u_i$ is $\stab$-erased and
$Q_i$ is $\stab$-normalizing,  $u_i/Q_i=\emptyset$. Hence $P/Q=\emptyset$,
i.e., $P$ is $\stab$-minimal.
\end{proof}
\end{lemma}





\subsection*{Existence of Minimal $\stab$-normal forms}

Below, in the study of $\stab$-minimal reductions, we will restrict
ourselves to \emph{regular} stable $\stab$. The reason is that, as shown by
the following example, an $\stab$-normalizable term need not have an
$\stab$-minimal reduction when $\stab$ is irregular.


\begin{example}
\label{E.min.vers.irreg.}
Consider $R=\{f(x)\ar g(x,x),\,\,a\ar b\}$, with term $t=f(a)$, and
let $\stab=\{g(b,a),f(b),g(b,b)\}$, the set
of terms not containing $a$ on the left spine.
\begin{diagram}
f(a)  & \rTo &        &       & g(a,a) \\
\dTo  &      &        & \ldTo &        & \rdTo \\
     &      & g(a,b) &       &        &       & \mathbf{g(b,a)} \\
     &      &        & \rdTo &        & \ldTo \\
\mathbf{f(b)} & \rTo &  &     & \mathbf{g(b,b)} \\
\end{diagram}

\noindent
Obviously, $\stab$ is closed under unneeded expansion,
because the only $\stab$-needed redex in a term $s\not\in \stab$ is the
leftmost occurrence of $a$ in it, and $\stab$ is closed under
reduction. $\stab$ is not regular, because the outermost redex in $t$ is
$\stab$-unneeded, but duplicates the innermost one which
\emph{is} $\stab$-needed.

There are three candidates for $\stab$-minimal reductions starting from
$t$: $P:f(a)\ar f(b)$ and $Q:f(a)\ar g(a,a)\ar g(b,a)$ and
$N:f(a)\ar g(a,a)\ar g(a,b)\ar g(b,b)$. There are two more reductions that
continue $P$ and $Q$, but they clearly
cannot be $\stab$-minimal. We have $P\not\lleq Q$ as $P/Q=g(b,a)\ar g(b,b)$,
$Q\not\lleq P$ as $Q/P=f(b)\ar g(b,b)$,
and $N\not\lleq P$ as, again, $N/P=f(b)\ar g(b,b)$. Hence
none of the reductions is $\stab$-minimal.
\end{example}



\subsection*{$\stab$-external redexes}


We go on to show that, when $\stab$ is regular, an $\stab$-normalizing
reduction is $\stab$-minimal iff it is $\stab$-erased,  i.e. contracts only
$\stab$-erased redexes. However, $\stab$-erased reductions need not be
$\stab$-needed, and hence need not be $\stab$-normalizing, and again for
regular $\stab$, we show existence of
$\stab$-external $\stab$-normalizing reductions,
which are $\stab$-needed
$\stab$-minimal reductions.  


\begin{definition}
\label{D.F-red.}
Let $U\subt t$. We call $P$ an \emph{$U$-reduction} if it
contracts only residuals of redexes from $U$ and created redexes; we call
such redexes \emph{$U$-redexes}.  Below $U(t)$ will denote the set of all 
redexes of~$t$, and $U_{\stab}(t)$ will denote the set of $\stab$-needed 
redexes of $t$.
\end{definition}


\begin{definition}
\label{D.M-abs.}
%\mbox{}
\begin{enumerate}
\item[(1)] Let $U\subt t$. We call a redex $u\subt t$ 
$U$-\emph{external} (in $t$)
if $u\in U$ and, for any $U$-reduction $P$, none of the residuals of $u$
along $P$ appear in arguments of $U$-redexes. 

\item[(2)] We call $u\subt t$ \emph{external in $t$} if it 
$U(t)$-external, and \emph{$\stab$-external} if it is
$U_{\stab}(t)$-external. (Thus any
$\stab$-external redex is necessarily $\stab$-needed.)
We call a reduction $P$ \emph{$\stab$-external}
if each redex contracted in
it is.
\end{enumerate}
\end{definition}


\begin{example}\label{E.abs.una.}
Consider an OTRS $R=\{a\ar c,\,b\ar b',\,f(c,x)\ar c'\}$, and take a term
$t=g(f(a,b),a)$. Then both occurrences of $a$ in $t$ are external
in $t$, while $b$ is not external in $t$: we have $t\ar g(f(c,b),a)=s$,
and the residual of $b$ in $s$ is in an argument of the created redex
$f(c,b)$. If $U\subt t$ contains two redexes -- the first occurrence of $a$
in $t$ and the redex $b\subt t$, then only the first $a\subt t$ is
$U$-external in $t$. If the set of terms not having a left-spine redex
is taken for $\cal S$, then the first $a$ is the only $\cal S$-external
redex in $t$ (it is the only $\cal S$-needed redex too).
\end{example}


It is shown in~\cite{[H.L.],[rta],[pun-ic]}
that any term $t$ not in normal form contains an external redex
(such redexes are called \emph{unabsorbed in~\cite{[rta],[ctrs]}).
Now, if
one ignores all redexes in $t$ except those in $U\subt t$, it follows that,
for any $U\not=\emptyset$, $U$ contains an $U$-external redex.
And by taking $U_{\stab}(t)$ for $U$ ($U_{\stab}(t)\not=\emptyset$ by
\Tr{T.ex.M-need.}), we obtain the following proposition:}


\begin{proposition}
\label{L.exist.m.unabs.m.nee.}
Every term $t\not\in\stab$ contains an ($\stab$-needed)
$\stab$-external redex.
\end{proposition}


\begin{lemma}
\label{L.reg.f-unabs=>unabs.}
If a redex $u\subt t$ is $\reg$-external, then it need not be external
in $t$, but it cannot be replicated and is persistently $\reg$-needed.

\begin{proof}
Let $P:t\doar o$, not necessarily an $U_{\reg}(t)$-reduction. By
\Pr{P.3.3.c.}.(3), it is enough to show that if a residual $u'$ of
$u$ can appear inside an $\reg$-needed redex $w'\not= u'$, then $w'$ cannot
replicate $u'$; therefore $u$ has at most one residual in any term of $P$.
Suppose, on the contrary, that there is $P:t\doar o$ such that a residual
$u'$ of $u$ is inside an $\reg$-needed redex $w'$ such that $w'$
replicates $u'$; and assume that $P$ is a shortest such a reduction,
i.e., $u$ has exactly one residual in every term in $P$. By \Lr{L.4.4.},
there are $\reg$-needed $P'$ and $\reg$-unneeded $P''$ such that $P\leeqv
P'+P''$. Since $u'$ and $w'$ are $\reg$-needed and $P''$ is
$\reg$-unneeded, it follows from \Pr{P.3.3.c.}.(2) that there are
$\reg$-needed $u''$ and $w''$ in the final term of $P'$ such that $u'$ and
$w'$ are the only residuals of $u''$ and $w''$, respectively. Since $u$ is
$\reg$-external, $u''\not\in w''$. Hence $u''$ has exactly one
$w''$-residual, say $u^*$. By \Tr{T.CRst.oc.}, $w''+P''/w''$ replicates
$u''$, since $w'$ replicates $u'$. Thus $P''/w''$ replicates $u^*$ -- a
contradiction, since $P''/w''$ is $\reg$-unneeded by \Pr{P.3.3.c.}.(1), and
$\reg$ is regular.
\end{proof}
\end{lemma}


Note that if $\stab$ is irregular, then an $\stab$-external redex $u\subt
t$ need not be persistently $\stab$-needed or $\stab$-erased. Indeed, take
$R$, $\stab$, and $Q$ as in Example~\ref{E.min.vers.irreg.}. Then  $a$ in
$t$ is $\stab$-needed, so is its leftmost residual in $g(a,a)$, but the
rightmost residual is $\stab$-unneeded, and $a/Q=\emp$. Hence $a\subt t$ is
not persistently $\stab$-needed or $\stab$-erased. But $a\subt t$ is
$\stab$-external, since the only $U_{\stab}(t)$-reduction is
$N:f(a)\ar f(b)$, and $a$ is  $U_{\stab}(t)$-external in~$N$.


\subsection*{Characterizing $\reg$-minimal reductions}


\begin{proposition}
\label{P.min=qpn.}
An $\reg$-normalizing reduction is $\reg$-minimal iff it is $\reg$-erased.

\begin{proof}
$(\Leftarrow)$ From Lemma~\ref{L.qpn<min.}. $(\Rightarrow)$ Let
$P:t_0\red{u_0}t_1\ar\ldots\ar t_n$ be $\reg$-minimal, and let $Q:t_0 \doar
o$ be $\reg$-external, hence $\reg$-erased by
Lemmas~\ref{L.reg.f-unabs=>unabs.} and~\ref{L.prs.m-nee.sec.},
$\reg$-normalizing reduction; $Q$ exists by \Pr{L.exist.m.unabs.m.nee.}.
Further, let $P_i:t_0\red{u_0}\ldots\ar t_i$ and let $Q_i=Q/P_i$.
Since $Q$ is $\reg$-erased, so is $Q_i$, and
$Q_i$ is $\reg$-normalizing by the closure of $\reg$ under reduction.
Hence $Q_i$ is $\reg$-minimal by \Lr{L.qpn<min.}. Since $P$ is
$\reg$-minimal too, $u_i/Q_i=\emp$ for every $i$. But for every
$\reg$-normalizing reduction $Q'_i:t_i\doar o_i$, it holds that $Q_i\lleq
Q'_i$ (since $Q_i$ is $\reg$-minimal). Hence $u_i/Q'_i=\emp$, i.e., $u_i$
is $\reg$-erased, and $P$ is $\reg$-erased too.
\end{proof}
\end{proposition}


\subsection*{Minimal Relative Normalization}

\begin{theorem}\label{T.qpmn.gen.min.str.}
(\textbf{Minimal Relative Normalization})
Let $\reg$ be a regular stable set of terms in an OERS, and let
$t\!\dar$ where $t\not\in\reg$. Then repeated contraction of $\reg$-needed
$\reg$-erased redexes in $t$
yields an $\reg$-minimal $\reg$-normalizing reduction, even if a finite
number of $\reg$-unneeded $\reg$-erased, and only such, redexes are also
contracted. In particular, any $t\!\dar$ where $t\not\in \reg$ has an
$\reg$-external $\reg$-minimal reduction, which is $\reg$-needed.

\begin{proof}
By \Pr{L.exist.m.unabs.m.nee.}, any $t\dar$ where $t\not\in\reg$ has an
$\reg$-external redex, which is $\reg$-needed and
$\reg$-erased by \Lr{L.reg.f-unabs=>unabs.} and
\Lr{L.prs.m-nee.sec.}. It remains to apply \Tr{T.ex.M-need.} and
\Pr{P.min=qpn.}.

\end{proof}
\end{theorem}



\section{The Relative Standardization Theorem}
\label{S.sta.}


Recall that a reduction is \emph{standard} if redexes in it are contracted
in left-to-right outside-in order~\cite{[Bar],[H.L.],[Kl.CRS]}.
Maranget proved in~\cite{[Mar]} that standard reductions are minimal among
reductions computing a `stable prefix' of a term, in an OTRS.
Note that for regular $\reg$, in general,  $\reg$-normalizing standard
reductions need not be $\reg$-needed, according to the definitions
of~\cite{[Bar],[H.L.],[Kl.CRS]}, or according
to~\cite{[GLM]}, where left-to-right order of contracted redexes
is not required.

Take for example $R=\{f(x)\ar g(x,x),\, a\ar
b\}$, and take for $\reg$ the set of terms not containing a  redex on  the
right-spine; then $\reg$ is regular, $f(a)\ar g(a,a)\ar
g(b,a)\ar g(b,b)$ is standard and $\reg$-normalizing, but the
second step is $\reg$-unneeded and the final term is not a minimal
$\reg$-normal form.

Therefore, we should require that relative standard reductions are
$\reg$-minimal as in the following definition:

\begin{definition}
We call an $\reg$-normalizing reduction \emph{$\reg$-standard} if it is
outside-in and $\reg$-minimal.
\end{definition}


It is not difficult to check that $\reg$-external $\reg$-normalizing
reductions are then $\reg$-standard (see~\cite{[morn]}),
and the left-to-right order of contraction of $\reg$-external redexes can
also be arranged. Hence we have the following Relative Standardization
Theorem:


\subsection*{Relative Standardization}

\begin{theorem}
(\textbf{Relative Standardization}) Let $\reg$ be a regular stable set
of terms in an OERS, and let $t\!\dar$ where $t\not\in\reg$. Then $t$ has an
$\reg$-standard $\reg$-normalizing reduction. In particular,
$\reg$-external $\reg$-normalizing reductions are $\reg$-standard.
\end{theorem}





\section{The Relative Optimality Theorem}
\label{S.un.opt.}



In this section, we generalize
L\'evy's Optimality Theorem to the case of all  stable sets of
normal forms, in OERSs. The family concept we use is based on the labelling
system of Section~\ref{S.labels}.


\begin{definition}
\label{D.fam.}
For co-initial reductions $P:t\doar s$ and $Q:t\doar o$, redexes $u\in
s$ and $v\in o$ with \emph{histories} $P$ and $Q$, written $Pu$ and $Qv$,
are in the same \emph{(labelling-)family} if for any initial labelling of
$t$, they bear the same labels.
\end{definition}



\begin{definition}
A multistep reduction $P:t_0\dored{U_0}t_1\dored{U_1}\ldots\doar t_n$ is
called a \emph{family-reduction} if each $U_i$ is a set of redexes belonging
to the same family ($t_i\dored{U_i}t_{i+1}$ is the multistep
corresponding to complete
developments of $U_i$). $\Vert P\Vert$ will denote the number of multisteps
in $P$. The family-reduction $P$ is \emph{complete} if each $U_i$ is
a maximal set of redexes of $t_i$
belonging to the same family. A family-reduction $P$ is called
\emph{$\stab$-needed} if each $U_i$ contains at least one $\stab$-needed
redex.
\end{definition}



\noindent\notationn Below $\FAM(P)$ will denote the set of families
(whose member redexes are) contracted in $P$. $\Card(\FAM(P))$ will
denote the number of families in $\FAM(P)$.



\begin{lemma}
\label{L.fam.compl.}
Every family is contracted at most once in a complete
family-reduction.

\begin{proof}
Let $P_n:t_0\dored{U_0}t_1\dored{U_1}\ldots \dored{U_{n-1}}t_n$
be a complete family-reduction. We show by induction on $n=\Vert
P\Vert$ that $(a)_n$: all families contracted in $P_n$ are
different; and $(b)_n$: there is no redex in $t_n$ whose family
has been contracted in $P_n$. So let us assume that $P_n$ is a
labelled reduction with $t_0$ having an initial labelling. The
case $n=0$ is clear. Further, $(a)_n$ follows immediately from
$(a)_{n-1}$ and $(b)_{n-1}$. Again by $(a)_{n-1}$ and
$(b)_{n-1}$, and by completeness of $P_n$, all redexes in $t_n$ that are
residuals of redexes
of $t_{n-1}$ are in families that have not been contracted
before. The label of any new redex in $t_n$ must contain $\lab(U_{n-1})$.
A redex with the same label cannot
occur in $t_0,\ldots, t_{n-1}$ since $t_0$ has an initial
labelling and, by the induction assumption,
$\lab(U_{n-1})\not=\lab(U_{i})$, for all $i<n-1$. Thus $(b)_n$ is
also valid.
\end{proof}
\end{lemma}


\subsection*{Relative Optimality}

\begin{theorem}
\label{T.unif.opt.}
(\textbf{Relative Optimality})
Let $\stab$ be a stable set of terms in an OERS $R$, and let $t\!\das$.
Then any $\stab$-needed complete family-reduction starting from $t$ is
$\stab$-optimal in the sense that it reaches an $\stab$-normal form of $t$
in a minimal number of
family-reduction steps.

\begin{proof}
Similar to the proof of the optimality theorem for the
$\lambda$-calculus in~\cite{[le80]}. Let $P:t\doar s$ be an
$\stab$-normalizing family-reduction and $Q:t\dored{U_0}t_1\red{U_1}\ldots$
be an  $\stab$-needed complete family-reduction. Further, let
$Q_i:t\dored{U_0}t_1\red{U_1}\ldots\doar t_i$ and $P_i=P/Q_i$. By
\Pr{P.lab.nest.}, $\FAM(P_i)\ssq \FAM(P)$.  Since $Q$ is
$\stab$-needed, at least one residual of some $u_i\in U_i$ is contracted in
$P_i$ ($P_i$ is $\stab$-normalizing by the closure of $\stab$ under
reduction). Hence, again by \Pr{P.lab.nest.}, $\FAM(Q)\subseteq \FAM(P)$.
Hence, by Lemma~\ref{L.fam.compl.}, $\Vert Q\Vert=\Card(\FAM(Q))\leq
\Card(\FAM(P))\leq\Vert P\Vert$.
\end{proof}
\end{theorem}




\section{Relative optimal versus minimal reductions}
\label{S.opt.vers.mnin.}

It is easy to see that any $\reg$-needed family-reduction that in
each step contracts all the $\reg$-needed redexes of some family, but does
not necessarily contract its $\reg$-unneeded members, is still optimal.
We will call this an $\reg$-needed \emph{semi-complete} family-reduction.
It follows from \Pr{P.min=qpn.} that such a reduction
is $\reg$-minimal as well iff every $\reg$-needed redex contracted in
it is $\reg$-erased.

For example, consider $R=\{g(x)\ar f(x,x),\,\,a\ar b\}$,
where $\reg$ is the set of terms not
containing left-spine redexes. Then $g(a)\ar f(a,a)\ar f(b,a)$ is both
$\reg$-minimal and a $\reg$-optimal semi-complete family-reduction, whereas
complete family reductions would lead to $f(b,b)$ which is not the minimal
$\reg$-normal form.

However, the following example shows that a
term in an OERS need not possess an
$\reg$-minimal $\reg$-optimal semi-complete family-reduction:


\begin{example}
\label{E.ers.min.opt.}
For the OERS $R=\{\sigma x A B\ar \delta x
(((A/x)B/x)A),\,\, f(A)\ar g(A,A)\}$, let $\reg$ be the set of terms
not containing left-spine redexes. Then $\reg$ is closed under unneeded
expansion because for any $t\not\in \reg$ such that $t\red{u}s\in \reg$,
$u$ must be the outermost left-spine redex. Also, $\reg$ is closed under
reduction -- no redex
can be created or put on the left-spine without contracting a
left-spine redex, which does not exist in terms from $\reg$. Thus $\reg$
is stable. $\reg$ is moreover regular, since if there is $u$ such that
$\UN_{\reg}(u,t)$, then the reduction $P:t\doar s\in\reg$ that contracts
outermost left-spine redexes is $\reg$-needed, and is external to $u$, and
each residual of $u$ along $P$ that is placed on the left-spine is
discarded by contraction of a left-spine redex above it. But so do the
residuals of redexes that are in $u$, and hence they cannot be
$\reg$-needed. That is, no $\reg$-unneeded redex can contain 
(or duplicate) a $\reg$-needed one.

Now let us consider the term $t=\sigma x(f(x),x)$. There are two
$\reg$-needed semi-complete family-reductions starting from
$t$: 
$$P:t\ar \delta
x(f(f(x)))\doar \delta x (g(g(x,x),g(x,x)))$$ (since both occurrences of $f$
in $\delta x(f(f(x)))$ are $\reg$-needed) and $$Q:t\ar\sigma
x(g(x,x),x)\ar \delta x (g(g(x,x),g(x,x))),$$ but neither reaches
the $\reg$-minimal $\reg$-normal form $\delta x (g(g(x,x),f(x)))$ of
$t$, obtainable by the reduction $t\ar\delta x(f(f(x)))\ar \delta
x (g(f(x),f(x)))\ar\delta x (g(g(x,x),f(x)))$.
\end{example}

The reason why the above counterexample works is that redexes
of the
same family are nested. However the following examples show that, even if
there is a `hierarchy' of nesting of redexes of different families, the
term still need not have $\reg$-minimal $\reg$-optimal family-reductions.


\begin{example}
Consider the OTRS $R=\{f(x) \ar g(x,x),\,g(b,x) \ar h( x,x),\,\penalty0 
a \ar b\}$,
and again take for $\reg$ the set
of terms not containing left-spine redexes (e.g. $\{h(b,a),h(b,b)\}$).
\begin{diagram}
f(a)  & \rTo &        &       & g(a,a) \\
\dTo  &      &        & \ldTo &        & \rdTo \\
     &      & g(a,b) &       &        &       & g(b,a) & \rTo     & h(a,a) \\
     &      &        & \rdTo &        & \ldTo &        & \ldTo    & \dTo \\
f(b)  & \rTo &        &       & g(b,b) &       & \mathbf{h(b,a)} & & h(a,b) \\
     &      &        &       &        & \rdTo & \dTo   & \ldTo    \\
     &      &        &       &        &       & \mathbf{h(b,b)} \\
\end{diagram}

By the same argument as
in Example~\ref{E.ers.min.opt.}, we can show that $\reg$ is a regular
stable set.
Now $P:f(a) \ar g(a,a) \ar g(b,a) \ar h(a,a) \ar h(b,a)$
is an $\reg$-minimal reduction, but $h(b,a)$ is not reachable by an
$\reg$-needed
semi-complete family reduction. If the first step reduces $a$
then we reach the $\reg$-normal form $h( b,b)$ which is not $\reg$-minimal.
Hence, in order to reduce $f(a)$ to $h( b,a)$, one should delay contraction
of the $\reg$-needed occurrences of $a$ (which all belong to the same
family). So
$f(a) \ar g(a,a)$ must be the first step. In $g(a,a)$, both
occurrences of $a$ are $\reg$-needed, but their contraction
makes $h( b,a)$ unreachable. Thus there is no $\reg$-minimal reduction
that is $\reg$-optimal at the same time.
\end{example}


\begin{example}
Take for $\reg$ the set of $\lambda$-terms in head-normal form,
which is regular, and take $t=(\lambda x.xx)u$, where $u=(\lambda y.\lambda
z.zvz)w$, and $y,z,v$ and $w$ are different variables. Then
$P:t\ar uu\ar (\lambda z. zvz) u\ar uvu\ar (\lambda z.
zvz)vu\ar vvvu=e$ is an $\reg$-minimal reduction. In order to
reach $e$ from $t$ by a semi-complete $\reg$-needed family reduction,
one should delay contraction of $\reg$-needed redexes in the family of
$u$. So the outermost redex in $t$ must be contracted first. In the
obtained term $o=uu$, both occurrences of $u$ are $\reg$-needed, and
their contraction would make $e$ unreachable -- there is no
occurrence of $w$ in $(\lambda z. zvz)(\lambda z. zvz)$.
\end{example}

Obviously, if reductions are non-duplicating, then every $\reg$-optimal
reduction is $\reg$-minimal too, and every $\reg$-needed $\reg$-normalizing
reduction is both $\reg$-minimal and $\reg$-optimal at the same time. This
suggests that there may not be conflict between minimality and optimality
when graph rewriting is concerned.



\section{Conclusions}
\label{S.conc.}




We have investigated properties which a set $\stab$ of `final terms' or
`(partial) results' should possess in order for the
normalization-by-neededness theory still to make sense. We introduced
appropriate notions of neededness, defined stability and regularity of sets
of terms, and proved a Normalization Theorem relative to stable sets of
`normal forms', and a Hypernormalization Theorem relative to regular stable
sets of `normal forms'. We have also studied minimal and optimal
normalization relative to regular stable sets $\reg$  of final terms, and
have showed that $\reg$-normalizing reductions that are both minimal and
optimal need not exist for any $\reg$-normalizable term $t$, despite the
fact that $t$ possesses minimal as well as optimal $\reg$-normalizing
reductions.

The abstract content of the relative normalization and optimality
results has  been analyzed by introducing \emph{stable Deterministic 
Residual Structures (SDRSs)}
and \emph{Deterministic Family Structures}, respectively~\cite{[rndrs]}.
SDRSs axiomatize the residual relation in orthogonal systems, and DFSs
are SDRSs with an axiomatized family relation. And our minimality 
results hold in such
SDRSs where every set $U$ of redexes in a term has an 
element that has at most one residual under any $U$-reduction (for
example, $U$-external redexes in OERSs are such).
Since this work was first presented, Melli\`es~\cite{[Mel98]} has also 
established minimality results for his axiomatic rewrite systems.

\vspace{0.20cm}

\section*{Acknowledgments}

We thank  J.-J.~L\'evy, L.~Maranget, P.-A.~Melli\`es, V.~van
Oostrom, F.~van Raamsdonk, and M.~R.~Sleep for useful comments and
discussions. The referees provided valuable suggestions.
The diagrams were drawn using P.~Taylor's diagram package.

%

\bibliography{GlaKenKha}

\end{document}