\documentstyle[twocolumn]{article}
%\input{amssym.def}
%\input{amssym}
\pagestyle{empty}
\setlength{\textheight}{8.75in}
\setlength{\columnsep}{2.0pc}
\setlength{\textwidth}{6.8in}
\setlength{\footheight}{0.0in}
\setlength{\topmargin}{0.25in}
\setlength{\headheight}{0.0in}
\setlength{\headsep}{0.0in}
\setlength{\oddsidemargin}{-.19in}
\setlength{\parindent}{1pc}
%\makeatletter

\input{diagrams} % Paul Taylor's Macro Package

%\usepackage{latexsym}

\begin{document}
%\date{}

%\documentclass{elsart}

%\input{diagrams} % Paul Taylor's Macro Package
%\usepackage{latexsym}

%\begin{document}


\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}% [section]
\newtheorem{cor}[thm]{Corollary}% [section]
\newtheorem{ex}[thm]{Example}% [section]
\newtheorem{rem}[thm]{Remark}% [section]
\newtheorem{nota}[thm]{Notation}% [section]
\newtheorem{prop}[thm]{Proposition}% [section]
\newtheorem{deff}[thm]{Definition}% [section]
\newtheorem{conv}[thm]{Convention}% [section]


%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf Proof }}{}
\newenvironment{poll}[1]{\noindent{\bf Proof of Lemma~\ref{#1}}}{}
\newenvironment{potl}[1]{\noindent{\bf Proof of Theorem~\ref{#1}}}{}
\newenvironment{popl}[1]{\noindent{\bf Proof of Proposition~\ref{#1}}}{}
\newenvironment{pocl}[1]{\noindent{\bf Proof of Corollary~\ref{#1}}}{}

\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
%\newcommand{\suppress}[1]{} % Comment out text.
%\newcommand{\suppress}[1]{\{\{{\sf #1}\}\}} % Highlight text.
\newcommand{\incl}[1]{#1} % include text.
%\newcommand{\incl}[1]{} % exclude text.


\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{\lc}{$\lambda$-calculus}
\newcommand{\ovl}{\overline}
\newcommand{\unl}{\underline}
\newcommand{\bd}{\begin{deff}}
\newcommand{\bdl}[1]{\begin{deff}\label{#1}}
\newcommand{\bl}{\begin{lem}}
\newcommand{\bll}[1]{\begin{lem}\label{#1}}
\newcommand{\bp}{\begin{prop}}
\newcommand{\bpl}[1]{\begin{prop}\label{#1}}
\newcommand{\bt}{\begin{thm}}
\newcommand{\btl}[1]{\begin{thm}\label{#1}}
\newcommand{\bel}[1]{\begin{ex}\label{#1}}
\newcommand{\bc}{\begin{cor}}
\newcommand{\bcl}[1]{\begin{cor}\label{#1}}
\newcommand{\bproof}{\begin{pruuf}}
\newcommand{\eproof}{\end{pruuf}}
%\newcommand{\bproof}[0]{\bproof}
%\newcommand{\eproof}[0]{\eproof}
\newcommand{\ed}{\end{deff}}
\newcommand{\el}{\end{lem}}
\newcommand{\ep}{\end{prop}}
\newcommand{\et}{\end{thm}}
\newcommand{\ee}{\end{ex}}
\newcommand{\ec}{\end{cor}}


%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newcommand{\notation}{{\bf Notation }}
%\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}

\newcommand{\ben}{\begin{description}}
\newcommand{\een}{\end{description}}
\newcommand{\bit}{\begin{description}}
\newcommand{\eit}{\end{description}}
\newcommand{\bds}{\begin{description}}
\newcommand{\eds}{\end{description}}


\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\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{\imply}{\,\Rightarrow\,}



\newcommand{\sleq}{\unlhd_{\stab}}
\newcommand{\sleqr}{\unlhd_{\stab_{red}}}
\newcommand{\sles}{\lhd_{\stab}}
\newcommand{\seqv}{\approx_{\stab}}

\newcommand{\oleq}{\unlhd_{\Omega}}
\newcommand{\oles}{\lhd_{\Omega}}
\newcommand{\ileq}{\unlhd_{\stab_{\mathcal I}}}
\newcommand{\iles}{\lhd_{\stab_{\mathcal I}}}

\newcommand{\bleq}{\unlhd_{\stab_{\mathcal B}}}
\newcommand{\bles}{\lhd_{\stab_{\mathcal B}}}
\newcommand{\beqv}{\approx_{\stab_{\mathcal B}}}

\newcommand{\snp}[1]{\mbox{$[{#1}]_{\stab}$}}
\newcommand{\sunp}[1]{\mbox{$[{#1}]_{\stab}^-$}}


\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{\sclas}[1]{\mbox{$\langle{#1}\rangle_S$}}
\newcommand{\stclas}[1]{\mbox{$\langle{#1}\rangle_{ST}$}}
\newcommand{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\newarrow{Co}<--->
\newcommand{\pessim}{\prec\!\!\prec}
\newcommand{\steq}{\approx_{st}}
\newcommand{\essim}{\approx}
\newcommand{\psim}{\prec}
\newcommand{\orth}{\perp}
\newcommand{\esorth}{\perp_{es}}
%\newcommand{\subt}{\subseteq}
\newcommand{\subt}[0]{\in}
\newcommand{\subts}[0]{\subseteq}


\newcommand{\contr}{\hookrightarrow}
\newcommand{\zcontr}{\hookrightarrow_z}
\newcommand{\scontr}{\hookrightarrow_s}
\newcommand{\contre}{\underline{\hookrightarrow}}
\newcommand{\zcontre}{\underline{\hookrightarrow}_z}

\newcommand{\fin}{\in}
\newcommand{\con}[1]{\mbox{$\lceil{#1}\rceil^{\leq}$}}

\newcommand{\extrr}[1]{\mbox{$\stackrel{#1}{\rightharpoonup}$}}
\newcommand{\lextrr}[1]{\mbox{$\stackrel{#1}{\leftharpoonup}$}}
\newcommand{\extr}{\mbox{$\rightharpoonup$}}
\newcommand{\lextr}{\mbox{$\rightharpoonup$}}
\newcommand{\staeq}{\approx_{STA}}
\newcommand{\leng}[1]{\mbox{$\vert{#1}\vert$}}
%\newcommand{\doextr}{\mbox{$\rightharpoonup^*$}}
\newcommand{\doextr}{\mbox{$\,\ \rightharpoonup\kern-0.7em\rightharpoonup\ $}}
\newcommand{\err}[2]{\mbox{$ST_{{#1}}({#2})$}}


%\newcommand{\lleq}{\leq_L}
%\newcommand{\lles}{<_L}
%\newcommand{\lles}{\triangleleft}
\newcommand{\lleq}{\unlhd_L}
\newcommand{\lles}{\lhd_L}
\newcommand{\leeqv}{\approx_L}
\newcommand{\snpp}{\approx_{sn}}
\newcommand{\hieq}[0]{\approx_H}

\newcommand{\lmeet}{\sqcap_L}

\newcommand{\inter}{\ddagger}
\newcommand{\ind}{\perp}
\newcommand{\hole}{\circ}
\newcommand{\restr}{\vert}
\newcommand{\exten}{\updownarrow}

\newcommand{\stan}{STA}
\newcommand{\stav}[1]{STV(#1)}

\newcommand{\fami}{\simeq}
\newcommand{\zfami}{\simeq_z}
\newcommand{\sfami}{\simeq_s}

\newcommand{\zleq}{\unlhd_z}
\newcommand{\zles}{\lhd_z}
\newcommand{\zgeq}{\unrhd_z}
\newcommand{\zgre}{\rhd_z}

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


\newcommand{\suf}{($\Rightarrow$)}
\newcommand{\nec}{($\Leftarrow$)}
\newcommand{\setm}{\setminus}
\newcommand{\crea}{\vdash}
\newcommand{\emp}{\emptyset}
\newcommand{\cfr}{complete family-reduction}
\newcommand{\cfrs}{complete family-reductions}
\newcommand{\qp}{quasi-persistently}
\newcommand{\stc}{strongly cofinal}
\newcommand{\rn}{RN}
\newcommand{\trnt}{the Relative Normalization theorem}
%\newcommand{\qp}{quasi-persistently}
%\newcommand{\stc}{strongly cofinal}
\newcommand{\pmn}{persistently $\stab$-needed}
\newcommand{\qprn}{quasi-persistently $\reg$-needed}
\newcommand{\qpmn}{quasi-persistently $\stab$-needed}
\newcommand{\das}{\downarrow_{\stab}}
\newcommand{\dar}{\downarrow_{\reg}}
\newcommand{\stab}{{\mathcal {S}}}
\newcommand{\reg}{{\mathcal {S}}}
\newcommand{\era}{\triangleright}

\newcommand{\fcC}{\mathcal {L(C)}}
\newcommand{\pc}{permutation-equivalence}
\newcommand{\pt}{permutation-equivalent}
\newcommand{\Lc}{\Le-equivalence}
\newcommand{\Lt}{\Le-equivalent}

\newcommand{\lin}[1]{\mbox{${#1}_I $}}
\newcommand{\calF}{\mathcal {F}}
\newcommand{\calR}{\mathcal {R}}
\newcommand{\calS}{\mathcal {S}}


\newcommand{\ip}[2]{\mbox{$\lceil{#1}\rceil^{{#2}}$}}
%\newcommand{\ms}[2]{\mbox{$\lceil{#1}\rceil^{({#2})}$}}
\newcommand{\fp}[2]{\mbox{$\lceil{#1}\rceil_{{#2}}$}}


\newcommand{\john}[1]{\{{\bf John:~\sf #1}\}} % Highlight text.
\newcommand{\zurab}[1]{\{{\bf Zurab:~\sf #1}\}} % Highlight text.
\newcommand{\delete}[1]{} % Comment out text.
\newcommand{\excl}[1]{} % exclude text.
%\newcommand{\excl}[1]{\{#1\}} % include text.




\title{An Abstract  B\"ohm-normalization}


\author{John Glauert \\
School of Information Systems, UEA \\
Norwich NR4 7TJ, UK\\
\texttt{jrwg@sys.uea.ac.uk} \\
\\
Zurab Khasidashvili   \\
%Department of Computer Science\\
%Bar-Ilan University, Ramat-Gan 52900, Israel  \\
Department of CS, Bar-Ilan University \\
Ramat-Gan 52900, Israel \\
\texttt{khasidz@cs.biu.ac.il}
}

\date{}
\maketitle
%\thispagestyle{empty}




\begin{abstract}
In this paper, we study \emph{normalization by neededness} with respect to  
`infinite results', such as B\"ohm-trees, in an abstract framework of 
\emph{Stable Deterministic Residual Structures} (SDRS). We formalize 
the concept of `infinite results' as suitable sets of infinite reductions, 
and prove an abstract infinitary normalization theorem with respect to such 
sets.  We also give a sufficient and necessary condition for
existence of \emph{minimal} normalizing reductions.

\end{abstract}


\section{Introduction}




A normalizable term in a rewriting system may have an
infinite reduction, so it is important to have a \emph{normalizing}
strategy which enables one to construct reductions to normal
form. For example, it is well known that the leftmost-outermost strategy is
normalizing in the $\lambda$-calculus~\cite{[C.F.]}. For Orthogonal TRSs, a
general normalizing strategy, called
the \emph{needed} strategy, was found by Huet and L\'evy~\cite{[H.L.]}. The
strategy always contracts a \emph{needed} redex --
one whose residual has to be contracted in
any reduction to normal form. Huet and L\'evy showed that any
term not in normal form has a needed redex, and that repeated
contraction of needed redexes leads to its normal form
whenever there is one. (They also defined \emph{strongly sequential}
orthogonal TRSs where a needed redex can be computed effectively in every
reducible term. We will not discuss this topic here.)



This fundamental work on neededness has been extended in several directions.
Barendregt et al.~\cite{[B.K.K.S.]}, Maranget~\cite{[Mar]},
N\"ocker~\cite{[Nok.thi.]} and Middeldorp~\cite{[Mid]} studied neededness
w.r.t. head-normal forms, weak head-normal forms, constructor head-normal
forms, and root-stable forms, respectively.
Sekar and Ramakrishnan~\cite{[SeRa]} studied normalization via
\emph{necessary sets} of redexes.  Kennaway et al.~\cite{[K-tra]} studied a
needed strategy for infinitary orthogonal TRSs. A different approach to
normalization is developed in Kennaway~\cite{[Kenn]} and Antoy and
Middeldorp~\cite{[AnMi]}. Antoy et al.~\cite{[Ant]} designed a needed
narrowing strategy.
Gardner~\cite{[Gar]} described a \emph{complete} way of encoding
neededness information using a type assignment system.
Khasidashvili~\cite{[colog],[rta]} introduced a refinement
of the needed strategy which is based on a concept of descendant
which refines that of residual. Melli\`es~\cite{[Mel2]} and van 
Oostrom~\cite{[Oos99]} extended the needed and essential strategies, 
respectively, to some non-orthogonal systems.


In~\cite{[rel-glc]}, the present authors addressed the question of
normalization relative to a desired set of final terms,
considering the properties that a set $\stab$ of terms must
possess in order for the neededness theory of Huet and L\'evy
still to make sense. This work is done in the context of orthogonal
\emph{Expression Reduction Systems} (ERSs), a formalism
for rewriting which subsumes Term Rewriting and the $\lambda$-calculus.
Natural conditions were imposed on $\stab$, called \emph{stability}, that are
sufficient for the following \emph{Relative Normalization}
(RN) theorem to hold:  each $\stab$-normalizable term not in
$\stab$ (that is, not in \emph{$\stab$-normal form}) has at least one
$\stab$-needed redex, and repeated contraction of such redexes always leads
to an $\stab$-normal form. It is shown also that if a stable $\stab$ is
\emph{regular}, i.e., if $\stab$-unneeded redexes cannot duplicate
$\stab$-needed ones, then the $\stab$-needed strategy is hypernormalizing
as well, and \emph{minimal} (w.r.t. the L\'evy-embedding relation)
$\stab$-normalizing reductions exist.


In \cite{[rndrs]}, we further generalized the theory by abstracting from the 
structure of terms. We studied relative normalization in Deterministic 
Residual Structures (DRSs), which are abstract reduction systems with an 
axiomatized residual relation. Despite their highly abstract nature, a 
counterpart of the \emph{stability} property of Berry~\cite{[berry]} and
Winskel~\cite{[Win89]} enabled us to prove the \rn\ theorem for all
\emph{regular}
stable sets $\stab$. (We actually prove  the Relative Hypernormalization
theorem.)  We show that without this stability axiom the theorem fails. The
proof method employed is similar to that in~\cite{[colog],[rta]}, and is 
based on the fact that $\stab$-needed steps in a reduction can be pushed before
$\stab$-unneeded steps without affecting the number of $\stab$-needed
steps. In~\cite{[dndrs]}, we studied \emph{discrete normalization} in SDRSs, 
which is normalization relative to particular (finite or infinite) reductions.


Here we extend the concepts of stability and regularity from sets
of terms (which represent `finite' results, or values, such as head normal 
forms) to sets of reductions, to represent the concepts of `infinite' values, 
such as B\"ohm trees. Throughout the paper, we  restrict ourselves to finite 
terms -- terms can contain only a finite number of redexes. For regular
stable sets $\stab$ of finite or  infinite results and an 
$\stab$-normalizable term $t$, in an SDRS, we show that all $\stab$-needed 
fair reductions starting from $t$ are $\stab$-normalizing, and if $t$ has 
a finite $\stab$-normalizing reduction, then any $\stab$-needed reduction 
starting from $t$ eventually normalizes $t$ in a finite number of steps.
This result unifies the Relative Hypernormalization theorem with the 
Discrete Normalization theory.  \zurab{We also show that for $\stab$-minimal 
reductions to exist, for regular stable sets of finite results $\stab$,
every  $\stab$-normalizing term must posses an 
$\stab$-needed $\stab$-erased redex (where a redex is $\stab$-erased if it 
does not have a residual under $\stab$-normalizing reductions).}


The paper is organized as follows. In the next section, we recall
SDRSs and present some fundamental lemmas concerning (mutually)
\emph{external} reductions. In section~\ref{S.meet.}, we give a 
construction of the meet operation with respect to Le\'vy's ordering on 
reductions. In Section~\ref{S.st.res.}, we introduce
the concept of stability for sets of reductions, and give examples.
In Section~\ref{S.rn.sdrs.}, we prove the \rn\
theorem for regular stable sets of reductions in SDRSs, \zurab{and present . 
the minimality resuls.} Conclusions appear in Section~\ref{S.concl.}.




\section{Deterministic Residual Structures}


In this section we recall \emph{Deterministic Residual Structures} (DRSs)
which are \emph{Abstract Reduction Systems} (ARSs) satisfying certain
properties concerning \emph{residuals}. Residuals of redexes were first
introduced and studied by Church and Rosser in the $\lambda
I$-calculus~\cite{[C.R.]}. The study of abstract systems with 
residuals started from Hindley~\cite{[Hin]}.

The definition and some results about ARSs can be found e.g.,
in~\cite{[Klo92],[Hu80]}. Our definition is slightly different.

\bd
An ARS is a
triple $A$ = (\emph{Ter},\emph{Red},$\ar$)
where \emph{Ter} is a set of \emph{terms}, ranged over by
$t,s,o,e$; \emph{Red} is a set of \emph{redexes} (or \emph{redex occurrences}),
ranged over by $u,v,w$; and
$\ar:Red\ar (Ter\times Ter)$ is a function such that for any $t\in Ter$
there is only a finite set of $u\in Red$ such that $\ar(u)=(t,s)$,
written $t\red{u}s$. This set will be known as the redexes of term $t$, where
$u\subt t$ denotes that $u$ is a member of the redexes of $t$ and $U\subts
t$ denotes that $U$ is a subset of the redexes. Note
that $\ar$ is a \emph{total} function, so one can identify $u$ with the
triple $t\red{u}s$. (Klop's ARSs~\cite{[Klo92]} are pairs $(Ter,\ar)$, and
do not allow one to distinguish transitions with the same source and target
terms.) A \emph{reduction} is a sequence $t\red{u_1}t_2\red{u_2}\ldots$. 
\delete{Reductions are denoted by $P,Q,N$. We write
$P:t\doar s$ or $t\dored{P}s$ if $P$ denotes a reduction (sequence) from
$t$ to $s$. $\,\,\vert P\vert$ denotes the length of $P$.
$P+Q$ denotes composition (or concatenation) of $P$ and $Q$. We use $U,V,W$ to
denote sets of redexes of a term.}
\ed


\begin{nota}
Reductions are denoted by 
$P,Q,N$. We write $P:t\doar s$ or $t\dored{P}s$ if $P$ denotes a reduction 
(sequence) from $t$ to $s$. $Q:t\doar$ may be finite as well as infinite. 
$P+Q$ denotes the concatenation of $P$ and $Q$.  $u$ also denotes the 
reduction that contracts $u$.  Further, for any reduction $Q$, $\ip{Q}{k}$ 
will denote the initial part of $Q$ of length $k$, provided $k\leq \leng{Q}$ 
(the length of $Q$), and $\fp{Q}{k}$ will denote the tail of $Q$ starting 
from the $(k+1)$th step; thus $Q=\ip{Q}{k}+\fp{Q}{k}$. Finally, we write 
$P\leq Q$ if $P$ is an initial part of~$Q$.
\end{nota}


\bdl{D.levy.str.}
{\bf (Deterministic Residual Structure)} A \emph{Deterministic Re\-sidual
Structure} (DRS) is a pair $\calR=(A, /)$, where $A$ is an ARS and
$/$ is a \emph{residual} relation on redexes relating redexes in the source
and target term of every reduction $t\red{u}s\in A$, such that
for $v\subt t$, the set $v/u$ of \emph{residuals of $v$ under $u$} is a
set of redexes of $s$; a redex in $s$ may be a residual of only one redex
in $t$ under $u$, and $u/u=\emptyset$. If $v$ has more than one
$u$-residual, then $u$ \emph{duplicates} $v$.
If $v/u=\emptyset$, then $u$ \emph{erases} $v$, and if moreover $v\not=u$,
then $u$ \emph{discards} $v$. A redex of $s$
which is not a residual of any $v\subt t$ under $u$ is said to be
\emph{$u$-new} or \emph{created} by $u$. The set $v/P$ of residuals of $v$ 
under any finite reduction $P$ is defined by transitivity.

A \emph{development} of $U\subts t$ is a reduction $P:t\doar $ that only
contracts residuals of redexes from $U$; it is \emph{complete} if it
is finite and $U/P=\cup_{u\in U}\,u/P=\emptyset$. Development of $\emptyset$ is
identified with the empty reduction.  The residual relation satisfies the 
following two axioms:
\bds
\item[{\rm [FD]}] (\emph{Finite Developments}~\cite{[GLM]}) All
developments are terminating; all complete developments of $U\subts t$ end
at the same term; and residuals of a redex $v\subt t$ under all complete
developments of $U$ are the same. Below $U$ will also denote a complete
development of $U\subts t$.

\item[{\rm [weak acyclicity]}] (\cite{[Sta]}) Let $u,v\subt t$, $u\not= v$,
and $u/v=\emp$. Then $v/u\not=\emp$.\footnote{This axiom is called
[acyclicity] in~\cite{[rndrs]}, and is axiom~(4) in~\cite{[Sta]}.}
\eds
We call a DRS $\calR$ \emph{stable} (SDRS) if
the following axiom is satisfied:
\bds
\item[{\rm [stability]}] If $u,v\subt t$ are different redexes, $t\red{u}e$,
$t\red{v}s$, and $u$ creates a redex $w\subt e$, then the redexes in
$w/(v/u)$ are not $u/v$-residuals of redexes of $s$, i.e.,  they are
created along $u/v$.
%\begin{figure}
\begin{diagram}[height=1.5em,width=1.5em]
 t      & \rTo^u       & e             & \rTo^w           & \cdot  \\
 \dTo^v &              &  \dOnto_{v/u}  &                 &      \\
s       & \rOnto_{u/v} & o              & \rOnto_{w/(v/u)}   & \cdot  \\
\end{diagram}
%\caption{Berry's Stability}\label{berry-stab}
%\end{figure}
\eds
\ed


DRSs are closely related to \emph{Determinate Concurrent Transition Systems} 
(DCTS) of Stark~\cite{[Sta]}, and to \emph{Abstract Reduction Systems} (ARSs) 
of Gonthier et al.~\cite{[GLM]}. The main difference from DCTSs is that Stark 
requires a non-duplicating residual relation. Unlike
ARSs of~\cite{[GLM]}, we do not have a nesting relation on redexes and the
corresponding axioms, and the stability axiom is modified accordingly.
Instead, we study properties of conflict-free transition and reduction
systems based on the duplication and erasure effect of executed transitions
on the others, and develop a theory that is applicable to systems with
nested transitions too.  Other related abstract
reduction systems are studied in~\cite{[Mel.th],[Oos.th],[Raa.th]}.


One can verify that all orthogonal (first or fully extended higher-order,
see e.g.,~\cite{[Raa.th]})  term rewriting systems, such as the
$\lambda$-calculus,  form DRSs. These systems are stable, and can be shown
so just using an appropriate notion of descendant which assigns the
contractum to the contracted redex -- labelling is not necessary. Further,
orthogonal Term Graph Rewriting Systems~\cite{[KKSdV]} are DRSs but
they do not satisfy all the nesting axioms of~\cite{[GLM]}.  


The properties of the residual relation in orthogonal systems are all
standard~\cite{[H.L.],[levy],[B.L.],[le80],[Bou],[Sta],[Mel.th]}, and we
only review quickly the main constructions used in this paper. In a DRS
$\calR$, \emph{L\'evy-equivalence} or \emph{permutation-equivalence} is 
defined as the smallest relation on co-initial
finite reductions satisfying: $U+ V/U\leeqv V+U/V$ and $Q\leeqv Q'\,
\imply \, P+Q+N\leeqv P+Q'+N$, where $U$ and $V$ are sets of redexes in the
same term. The residual relation on redexes is extended to all co-initial
reductions as follows: $(P_1+P_2)/Q=P_1/Q+P_2/(Q/P_1)$ and
$Q/(P_1+P_2)=(Q/P_1)/P_2$. The \emph{L\'evy-embedding} relation on
co-initial finite reductions, $\lleq$, is defined by: $P\lleq Q$ iff
$P/Q=\emptyset$. One can show that $P\leeqv Q$ iff
$P\lleq Q$ and $Q\lleq P$ and that $P\lleq Q$ iff $Q\leeqv P+N$ for some $N$.
Intuitively, $P\lleq Q$ expresses that $Q$ does more work than $P$,
and $Q/P$ is the part of $Q$ that remains after $P$ has been done. Further, one
can prove the following \emph{strong Church-Rosser} theorem for DRSs: For
all co-initial finite reductions $P$ and $Q$ in a DRS, $P\sqcup Q\leeqv
Q\sqcup P$, where $P\sqcup Q$ abbreviates $P+Q/P$. \zurab{And finally, we will 
also need the following \emph{Cube Lemma}: for any finite co-initial 
reductions $P,Q$ and $N$, $N/(P\sqcup Q)= N/(Q\sqcup P)$.}


L\'evy-equivalence extends to infinite reductions as follows. First,
for any $u\subt t \dored{P}$, define $u/P=\emptyset$ if $u/P'=\emptyset$ for
some finite $P'\leq P$ (we say $u$ is \emph{erased} in $P$).
Now, for any co-initial $P,Q$, define $P/Q=\emptyset$, or equivalently,
$P\lleq Q$, if for any redex $v$ contracted in $P$, say $P=P'+v+P''$,
$v/(Q/P')=\emptyset$ (see the diagram); and define $P\leeqv Q$ iff 
$P\lleq Q$ and $Q\lleq P$.
\begin{diagram}[height=1.5em,width=1.5em]
{}  & \rOnto^{P'} & {}          & \rTo^v  & {}       & \rOnto^{P''}  
	  &  &  P   \\
\dOnto^{Q} &            & \dOnto_{Q/P'}&   
		&   &                       \\
  {} &     & {}         & {} &   &  & \\
\end{diagram}
Finally, $P/Q$ is only defined for finite $Q$, as the reduction whose initial 
parts are residuals of the initial parts of $P$ under~$Q$.


The [stability] axiom is not used in the above constructions.
Intuitively, stability means that a
redex cannot arise from two unrelated sources.  This property has
a natural extension to many-step reductions, where `unrelated'
is formalized by the notion of \emph{external} which captures
the concept that two
external reductions do not contract redexes that have common residuals
(although the contracted redexes may have `inessential' common ancestors).

\bdl{D.ext.reductions.}
\bit
\item[\labelitemi]  Let $u\in U\subts t$ and $P:t\doar o$.
We call $P$ \emph{external}
to $U$ (resp. $u$) if $P$ does not contract residuals of redexes in $U$
(resp. residuals of~$u$). 

\item[\labelitemi]  Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar t_n$
and $Q:t_0=s_0\dored{Q_j}s_j\red{v_j}s_{j+1}\doar s_m$.
Let $U_{i,j}=u_i/(Q_j/P_i)$ and $V_{i,j}=v_j/(P_i/Q_j)$ (see diagram).
We call $P$ \emph{external} to $Q$ if for any $i,j$,
$U_{i,j} \cap V_{i,j}=\emp$.

\begin{diagram}[height=1.5em,width=1.5em]
t_0          &\rOnto^{P_i}& & t_i       &\rTo^{u_i}   & t_{i+1} \\
\dOnto<{Q_j}&            & &\dOnto<{Q_j/P_i}&         & \dOnto     \\
s_j     &\rOnto^{P_i/Q_j}& & \cdot    & \rOnto^{U_{i,j}} & \cdot   \\
\dTo<{v_j}   &         & &\dOnto^{V_{i,j}} &             &  \dOnto   \\
s_{j+1}      &\rOnto      & &  \cdot       & \rOnto      & \cdot   \\
\end{diagram}
\eit
\ed


Obviously, $P$ is external to the set $U$ iff it is external to any
development of $U$, and is external to a redex $u$ iff it is external to
the reduction contracting $u$. Note that a reduction external to one
complete development of $U$ need
not be external to all developments of $U$, and in general, externality is
not invariant under $\leeqv$. For, consider a TRS $R=\{a\ar a',
\,f(x)\ar b,\, g(x)\ar c\}$, a term $t=f(g(a))$, and reductions
$P:t\red{a}f(g(a'))\red{f}b$, $Q:t\red{a}f(g(a'))\red{g}f(c)$, and
$N:t\red{g}f(c)$. Then we have $Q\leeqv N$, $P$ is external to $N$,
but not to $Q$; and $P$ is not external to $U=\{a,\,g(a)\}$.

\zurab{
Recall from \cite{[H.L.]} that in conreate orthigonal rewrite systems,
a redex is called \emph{external} if its residuals never appear inside 
arguments of other redexes. It should be clear from the context to which 
concept of external we are referring to.
}


\bll{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\}\subts t_0$, and let $Q_0:t_0\doar o_0$. Then
$P'=P/Q_0$ is external to the set $U'=U/Q_0$.

\el



We conclude this section by presenting two fundamental lemmas, which
generalize the [weak acyclicity] and [stability] axioms to many-step
reductions~\cite{[rndrs]}.


\bll{L.ext.lem.mult.} %%%%% {L.ext.no.le.eqv.}
{\bf (Weak Acyclicity)}
Let $P,N$ be co-initial finite reductions in a DRS, and let $P$ be external
to $N$. Then $N\not\leeqv P$.

\el


\bll{L.disj.red.creat.}
{\bf (Stability)}
Let $P:t\doar s$ be external to
$Q:t\doar e$, in a stable DRS, and let $P$
create redexes $W\subts s$. Then the residuals $W/(Q/P)$ of redexes in $W$
are created by $P/Q$, and $Q/P$ is external to~$W$.
\begin{diagram}[height=2em,width=2em]
t       & \rOnto^{P}   &    s \supseteq W                 \\
 \dOnto^Q &              &    \dOnto_{Q/P}            \\
e       & \rOnto_{P/Q} &    o  \supseteq W/(Q/P)           \\
\end{diagram}

\el




\section{Construction of the $\lleq$-meet operation}
\label{S.meet.}

In this section we give a construction of the $\lleq$-meet operation (to be used
in the subsequent sections) and prove its correctness. 
This implies that $\lleq$ is a complete lattice on L\'evy-equivalence
classes of reductions. This lattice was first constructed by 
Berry and L\'evy~\cite{[B.L.]}, for the case of Recursive Program 
Schemes (RPSs), as the ideal completion 
of the upper semi-lattice on L\'evy-equivalence
classes of finite reductions.




Below, in our construction of $\lleq$-meets, $\Phi$ denotes a set 
of co-initial reductions in a DRS. Further, for
example, we write $P\lleq\Phi$ iff $\forall Q\in\Phi . \,Q\lleq P$;
$\ip{\Phi}{k}$ denotes the set of initial parts, of length $k$, of
reductions in $\Phi$; etc.



\bdl{D.mj.}
{\bf ($\lleq$-meet)} Let $\Phi$ be a set of reductions starting from $t$, 
in a DRS. Then the \emph{$\lleq$-meet} of reductions in $\Phi$, written
$\lmeet \Phi$, is defined as follows: Let $U\ssq t$ be the maximal subset
such that $U\lleq \Phi$, and let $t\dored{U}s$ be a complete $U$-development
(or the multi-step contracting $U$). Then $\lmeet \Phi=U+\lmeet (\Phi/U)$.
\ed


\btl{T.int.glb.}
Let $\Phi$ be a set of co-initial reductions in a DRS. Then
$\lmeet\Phi$ is a (unique up to $\leeqv$) $\lleq$-meet of~$\Phi$.

\bproof
Let $\lmeet\Phi=Q: t_0\dored{U_0}t_1\dored{U_1}t_2\doar\ldots$. It is 
immediate from the construction that $\lmeet\Phi\lleq \Phi$. Thus we
need to show that for any $P:t_0\doar$ such that $P\lleq\Phi$, $P\lleq Q$,
that is, for any $n< \leng{P}$, $\ip{P}{n}\lleq Q$. We show this by
induction on $n$. The case $n=0$ (i.e., $P=\emp$) is clear. So let $n=k+1$,
and let $\ip{P}{k}\lleq Q$. Then $\ip{P}{k}\lleq \ip{Q}{l_k}$ for some $l_k$.
We can assume that $\ip{Q}{l_k}$ ends at $t_m$ for some $m$. Thus
$\ip{Q}{l_k}\leeqv \ip{P}{k}+Q'_k$ for some finite $Q'_k$, and
$\Phi/\ip{Q}{l_k}$ consists of $Q'_k$-residuals of reductions in
$\Phi/\ip{P}{k}$, up to $\leeqv$. Let $v$ be the $(k+1)$th step of $P$.
Since $P\lleq\Phi$, $v\lleq \Phi/\ip{P}{k}$, thus by the Cube Lemma,
$(v/Q'_k)\lleq \Phi/\ip{Q}{l_k}$, and therefore $v/Q'_k\ssq U_m$ by
\Dr{D.mj.}. This means that $\ip{P}{n}\lleq Q$. Thus $P\lleq Q$, and
$\lmeet\Phi$ is a $\lleq$-meet of~$\Phi$.
\begin{diagram}[height=2.2em,width=2.2em]%
{}  &        &{}  &                & {} &        & {}  \\
    &        &    & \ruTo(2,2)^{v} &       &\ruOnto(2,2)^{v/Q'_k}  &      \\
t_0 &\rOnto^{\ip{P}{k}} & \cdot & \rOnto^{Q'_k} & t_m &\rOnto^{U_m} &\cdot \\
\dOnto_{N\in\Phi} & &\dOnto_{N/\ip{P}{k}} & & \dOnto_{N/\ip{Q}{l_k}} & &  \\
{}&     &{}   & \    & {}  &\     &{}  \\
\end{diagram}
\eproof
\et





\section{Stable sets of finite or infinite results}
\label{S.st.res.}




In this section, we will introduce the concepts of stability, regularity and
superstability of sets of 
reductions, to cover usual concepts of infinite results, such as 
B\"ohm-trees. From this definition, our earlier concepts of stability
and regularity for 
sets of finite results~\cite{[rndrs],[rel-glc]}  can be obtained
as a special case. Moreover, to any reduction $P$ we will associate a
stable set $\stab_P$ of reductions, which will allow us to infer Discrete
Normalization and Standardization results~\cite{[dndrs]} from our
normalization results in the next section.



We start by recalling the concepts of relative neededness, and of stability  
and regularity of sets of terms~\cite{[rndrs],[rel-glc]}, and 
introduce superstability. The latter will
allow us to extend our results concerning minimal relative 
normalization~\cite{[rel-glc]} to the abstract framework of SDRSs.



\bdl{D.rel.need.}
Let $\stab$ be a set of terms in a DRS $\calR$.
\ben
\item[(1)] We call a redex $u\subt t$
\emph{$\stab$-needed} if at least one residual of
it is contracted in any reduction from $t$ to a term in $\stab$, and call
$u$ \emph{$\stab$-unneeded} otherwise.

\item[(2)] We call $\stab$ \emph{stable} iff:
\ben
\item[\textrm{[RC]}] $\stab$ is \emph{closed under reduction}: 
if $t\in\stab$ and $t\ar s$, then $s\in\stab$, and

\item[\textrm{[CUE]}] $\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.
\een

\item[(3)] Further, we call a stable set $\stab$ \emph{regular} iff:
\ben
\item[\textrm{[Reg]}] In no term can an $\stab$-unneeded redex duplicate an 
$\stab$-needed one.
\een

\item[(4)] Finally, we call a regular stable set $\stab$ 
\emph{superstable} iff:
\ben
\item[\textrm{[Min]}] For any $\stab$-normalizable term $t$, the set of all
$\stab$-normalizing reductions starting from $t$ contains a unique,
up to $\leeqv$, $\lleq$-minimal element. Such a reduction will be called
\emph{$\stab$-minimal}.
\een
\een
\ed




Examples of stable sets are normal forms~\cite{[H.L.]}, head normal
forms in the \lc~\cite{[B.K.K.S.]}, weak head normal
forms in the \lc~\cite{[A.O.]}, constructor head normal forms for constructor
TRSs~\cite{[Nok.thi.]}, and root stable forms in orthogonal
TRSs~\cite{[Mid]}.  All the above sets are
regular. Other examples include weak-head-normal forms (up
to garbage-collection, modulo a congruence) in Yoshida's $\lambda f$-calculus
(an environment calculus)~\cite{[Yos]}, the set of \emph{answers} in the
\emph{call-by-need} $\lambda$-calculus of Ariola et al.~\cite{[A.F.]}, and
flexible generalized head normal forms in the
$\lambda_{hd}^v$-calculus of Xi~\cite{[Xi]}; all
are conditional rewrite systems. 


Although all normalizing reductions are minimal w.r.t. the set of normal forms,
this is not so for other concepts of results. For example, for the set of
head-normal form, only the reductions L\'evy-equivalent to the 
leftmost-outermost head-normalizing reductions are minimal. Head-minimal 
reductions compute the principal head-normal forms~\cite{[Bar]}, 
from which all other head-normal forms are accessible.


An example of an irregular stable set is given in~\cite{[rndrs]}.
The next example exhibits a regular stable set which is not superstable:

\begin{ex}\em
\label{E.nohyp.}
Consider the SDRS given by the following diagram
\begin{diagram}[height=0.9em,width=0.9em]
t    & &       &\rTo^u  &   &   &  &    & t_2 &  & {} \\
  &      &   & & & &   &\ldTo(2,4)^{v_1} & &\rdTo(2,4)^{v_2} & \\
       &   &     &  &   &  &   &    &  &  & {} \\
 \dTo^v      & & & & & & & & & & \\
        &   &    &  &   &  & o_1 &    &  &  & o_2 \\
      & & & & & & &\rdTo(2,4)^{v'_2} & &\ldTo(2,4)_{v'_1} &  \\
       &   &     &  & s_1  &  &  &    &  &  & {} \\
     & & &\ruTo(4,2)^{u_1} & &\rdTo(4,2)_{u'_2} & & & & &  \\
t_1      &   &    &  &  &  &  &    & t' &  & {} \\
      &\rdTo(4,2)_{u_2} & & & & & &\ruTo(4,2)_{u'_1} & & &  \\
{}        &   &   &  & s_2  &  &  &    &  &  & {} \\
\end{diagram}
where $u/v=\{u_1,u_2\}$, $v/u=\{v_1,v_2\}$, $v_1/v_2=\{v'_1\}$,
$v_2/v_1=\{v'_2\}$, $u_1/u_2=\{u'_1\}$, $u_2/u_1=\{u'_2\}$, and let
${\stab}=\{o_2,s_2,t'\}$. Then $\stab$ is regular stable but not superstable,
as one can easily verify that there is no $\stab$-minimal reduction
starting from $t$.
\end{ex}





\bd
Given a set $\stab$ of reductions in a DRS $\calR$ and a term $t$ in 
$\calR$, we call $t$ \emph{$\stab$-normalizable} if $\stab$ contains a 
reduction $P$ starting from $t$; $P$ is then called $\stab$-normalizing. 
\delete{
Further, $\stab(t)$ will denote the set of all reductions in $\stab$ that 
start from $t$. Thus $t$ is $\stab$-normalizable iff $\stab(t)\not=\emp$, 
and $\stab$ consists of all $\stab$-normalizing reductions.
}
\ed


\bdl{D.rel.ord.}
Let $\stab$ be a set of reductions in a DRS.
\ben
\item[(1)]  We call $u\subt t$ \emph{$\stab$-unneeded} if there is a 
reduction $Q\in\stab$ staring from $t$ that is external to $u$, and call 
it \emph{$\stab$-needed} otherwise.

\item[(2)] Let $P,Q$ be co-initial reductions. If $P$ and $Q$ are both 
finite, then we define $P\sleq Q$ if $P/Q$ is $\stab$-unneeded. Otherwise,  
$P\sleq Q$ if for any finite $P'\leq P$ there is a finite $Q'\leq Q$ such 
that $P'\sleq Q'$. Further, $P\seqv Q$ iff $P\sleq Q$ and $Q\sleq P$. We 
call $\sleq$ and $\seqv$ respectively $\stab$-\emph{embedding} and 
$\stab$-\emph{equivalence}. 
\delete{$\sclas{P}$ denotes the $\seqv$-equivalence 
class of $P$ (we will show below that $\seqv$ is an equivalence relation). 
We write $\sclas{P}\sleq\sclas{Q}$ if $P\sleq Q$.}
\een
\ed




It is immediate from the definition that $\lleq \ssq \sleq$.

\bll{L.leeq.imp.seqv}
Let $P,Q$ be co-initial reductions in a DRS. Then $P\lleq Q$ implies 
$P\sleq Q$ and $P\leeqv Q$ implies $P\seqv Q$.
\el




\bdl{D.clo.reduc.sets.}
Let $\stab$ be a set of reductions in a DRS.
\ben
\item[(1)]  We call $\stab$ \emph{stable} iff:

\ben
\item[\textrm{[CS]}] \emph{$\stab$ is suffix-closed}: if $P'\not\in\stab$, then
$P'+P''\in\stab$ implies $P''\in\stab$.

\item[\textrm{[CE]}] \emph{$\stab$ is closed under $\stab$-embedding}: $P\in\stab$
and $P\sleq Q$ implies $Q\in\stab$.

\item[\textrm{[CN]}] \emph{$\stab$ is closed under neededness}: every non-empty
$P\in\stab$ contracts at least one $\stab$-needed redex.
\een

\item[(2)] Furthermore, we call $\stab$ \emph{regular} iff:

\ben
\item[\textrm{[Reg]}]  In no term can an $\stab$-unneeded redex duplicate an 
$\stab$-needed one.
\een

\item[(3)] Finally, we call $\stab$ \emph{superstable} iff:

\ben
\item[\textrm{[Min]}] For any $\stab$-normalizable term $t$, $\stab$ contains 
a unique, up to $\leeqv$, $\lleq$-minimal element starting from $t$.  
Such reductions will be called $\stab$-minimal.
\een
\een
\ed



Note that, for a set of terms $\stab_{ter}$ in a DRS,  stability of 
$\stab_{ter}$ follows easily from stability of the \emph{corresponding}
set $\stab_{red}$ of $\stab_{ter}$-normalizing reductions --
(possibly infinite) reductions starting outside $\stab_{ter}$ and entering
it. Indeed, [CE] (for $\stab_{red}$) implies [RC] (for $\stab_{ter}$). 
And [CN] implies
[CUE] (since any step entering $\stab_{ter}$ is an $\stab_{red}$-normalizing
reduction, thus is $\stab_{red}$-needed and therefore $\stab_{ter}$-needed
too).  

Conversely, if $\stab_{ter}$ is stable, then $\stab_{red}$ is stable as well:
[CS] is immediate, [CN] follows from [CUE], and [CE] follows from [CUE] and
[RC]. (Indeed, to prove [CE], let $P\in\stab_{red}$ and
$P\sleqr Q$. Further, let $P'\leq P$ be finite and 
$P'\in\stab_{red}$. Then there is a finite $Q'\leq Q$ such that
$P'\sleqr Q'$. i.e., $P'/Q'$ is $\stab_{red}$-unneeded, hence 
$\stab_{ter}$-unneeded. By [RC], $P'/Q'$ ends in $\stab_{ter}$.
And by [CUE], $Q'$ too ends in $\stab_{ter}$. Hence $Q\in \stab_{red}$,
and [CE] is proved.)

Now it is immediate that $\stab_{ter}$ is regular, resp. superstable,
iff so is $\stab_{red}$. Furthermore, $\stab$-neededness and related
concepts are not affected if we view $\stab_{ter}$ as the corresponding 
set $\stab_{red}$ of reductions. Therefore, in the following, we will
often tacitly identify $\stab_{ter}$ with $\stab_{red}$.



Given a reduction $P$ in an SDRS $\calR$, we can also construct its 
corresponding stable set $\stab_P$ as follows. Let $\calR_P$ be an 
SDRS whose terms are L\'evy-equivalence classes $\lclas{Q}$ of finite 
initial parts of reductions in $\lclas{P}$, whose redexes are pairs 
$\lclas{Q}\ar \lclas{Q+u}$, where $u$ is a redex in the final 
term of $Q$, and the residual relation is the induced one:
If $\lclas{Q}\red{u^*} \lclas{Q+u}$ and
$\lclas{Q}\red{v^*}\lclas{Q+v}$ in $\calR_P$, then for any
$v'\in v/u$, $\lclas{Q+u}\red{v'^*}\lclas{Q+u+v'}$
is a $u^*$-residual of $v$. (This definition is sound since 
$Q+u+v'\lleq P$.) $\calR_P$ is an SDRS since its reduction graph is 
isomorphic to 
$\lclas{P}$, and in addition, $\calR_P$ is acyclic. Now $\stab_P$
is defined as the set of all suffixes of reductions in $\calR_P$ 
corresponding to reductions in $\lclas{P}$ (hence reductions in $\stab_P$
are `maximal' in some sense). Hence $\stab_P$ is suffix-closed, 
and it satisfies [CE] since all co-initial reductions in $\calR_P$ are
L\'evy-equivalent (because of the above `maximality' property).
 When $P$ is finite, the last step of any (non-empty)
reduction in $\stab_P$ is $\stab_P$-needed by \Lr{L.ext.lem.mult.}, implying
[CN] and thus stability of $\stab_P$. 

When $P$ is infinite, [CN] 
does not hold in general (in SDRSs), as can be seen from the diagram
below (only a finite part of the infinite reduction graph is shown). 
Each non-empty horizontal step creates its next horizontal step,
and similarly for vertical steps; every redex has at most one residual
on the opposite side of each elementary diagram, and erasure is indicated 
by empty steps $\emp$. The SDRS axioms are not violated. Further, the 
infinite reductions $u_0+u_1+\ldots$ and $v_0+v_1+\ldots$ are L\'evy-equivalent
but they contract different, hence unneeded, redexes. Clearly, no 
normalization-by-neededness theory can be developed for such reductions.
\begin{diagram}[height=1.6em,width=1.8em]
\cdot     &\rTo^{u_0}    &  \cdot    &\rTo^{u_1}    &\cdot  & &  \\
\dTo^{v_0} &        &\dTo   &        & \dTo_{\emp}    &  &      \\
\cdot   &\rTo  & \cdot & \rTo^{u'_1}  & \cdot &\rTo^{u_2} & \cdot \\
\dTo^{v_1}  & &\dTo^{v'_1} & & \dTo & & \dTo_\emp  \\
\cdot  &\rTo_{\emp} & \cdot &\rTo  &\cdot  & \rTo^{u'_2}   & \cdot \\
      &       &\dTo^{v_2}  &       & \dTo^{v'_2}  &      &  \\
{}  &  & \cdot     &\rTo_{\emp}  &\cdot  &     & \rdOnto\\
\end{diagram}

Let us recall concepts related to neededness w.r.t. particular reductions 
$P$, or discrete neededness, from~\cite{[dndrs]}.

\bdl{D.red.need.ess.}
\bit
\item[\labelitemi]   Let $P:t\doar $ and $u\subt t$, in a DRS.    
We call $u$ \emph{$P$-needed} if there is no
$Q\leeqv P$ that is external to $u$, and call it \emph{$P$-unneeded}
otherwise.

\item[\labelitemi] Let $Q:t\doar $, $P:t\dored{P'}s\doar $,
and $u\subt s$, in a DRS. We
say that $u$ is $Q$-needed, or more precisely, $P'u$ is $Q$-needed, if $u$
is $Q/P'$-needed. We call $P$ \emph{$Q$-needed} if every redex contracted
in $P$ is $Q$-needed. We call $P$ \emph{self-needed} or \emph{standard} if 
it is $P$-needed.
\eit
\ed


It is easy to verify that $P$-neededness of redexes occurring in terms
of reductions in $\lclas{P}$ coincides with $\stab_P$-neededness,
and in particular standard reductions $P$ are simply $\stab_P$-needed
reductions. Hence the stability concept for sets of reductions allows 
to unify the existing relative and discrete normalization theories (as far
as normalization-by-neededness is concerned). 



It is easy to check that for example the sets of reductions
`computing' B\"ohm-trees~\cite{[Bar]} or
L\'evy-Longo-trees~\cite{[le76],[Lon]} or Berarducci-trees~\cite{[Ber96]}
are stable and regular. 
To make this precise, let us consider the B\"ohm-tree
semantics of the \lc. Recall that  the \emph{immediate syntactic value}
$\omega(t)$ of a $\lambda$-term $t$ is defined by: 
$\omega(t)=\bot_{\mathcal B}$
if $t$ is not a head normal form, and $\omega(t)=\lambda x_1\ldots x_m .
y\omega(t_1)\ldots\omega(t_n)$ if $t=\lambda x_1\ldots x_m . y t_1\ldots t_n$,
where $\bot_{\mathcal B}$ is a special constant which denotes the `undefined'.
Then the \emph{B\"ohm-tree} or \emph{B\"ohm-normal-form} $BT(t)$ of $t$,
which is the \emph{value} of $t$ according to \emph{B\"ohm-semantics}, is
defined by $BT(t)=\oleq\!\!-lub\{\omega(t)\,\vert\,t\doar_\beta s\}$,
where $\oleq$ is the minimal context-closed ordering on
$\lambda$-$\bot_{\mathcal B}$-terms (i.e., $\lambda$-terms possibly 
containing occurrences of $\bot_{\mathcal B}$) generated by 
$\bot_{\mathcal B}\oleq t$ for any $\lambda$-$\bot_{\mathcal B}$-term $t$.


Now let us define the \emph{B\"ohm-approximant computed by
$P:t_0\ar t_1\ar\ldots$}, written $\omega(P)$, by
$\omega(P)=\oleq\!\!-lub\{\omega(t_i)\,\vert,\,i=0,1.\ldots\}$. It is well
known that $t\doar s$ implies $\omega(t)\oleq\omega(s)$, thus in particular
for a finite $P:t_0 \doar t_k$, $\omega(P)=\omega(t_k)$. Now we can define
that $P:t_0\doar$ \emph{computes} $BT(t_0)$ iff $\omega(P)=BT(t_0)$.  Let
us call a subterm of $t$ an $\bot_{\mathcal B}$-subterm if its corresponding
occurrence in $\omega(t)$ is $\bot_{\mathcal B}$. Recall that the standard way
to approximate $BT(t_0)$ sequentially is to construct `iterated
head-reductions' $P:t_0\dored{P_0} t_1\dored{P_1}\ldots$, where $P_i$ is
the head-reduction computing the principal head normal form of one of the
$\bot_{\mathcal B}$-subterms of $t_i$ having a head normal form. In order 
to compute $BT(t_0)$, $P$ must be `fair', i.e., every $\bot_{\mathcal B}$ 
subterm of every $t_i$ having a head normal form must eventually be dealt 
with in $P$; we call such reductions $P$ \emph{canonical B\"ohm-reductions}.


Regularity and stability of the set $\stab_{\mathcal B}$ of reductions 
computing B\"ohm-trees follow easily from the top-down manner of 
construction of
B\"ohm-trees: [CS] is immediate; [CN] follows from the fact that head
redexes of $\bot_{\mathcal B}$-subterms of any $\lambda$-term $t$ are
$\stab_{\mathcal B}$-needed; and [CE] follows from a simple observation that
$Q\in\stab_{\mathcal B}$ iff $P\bleq Q$ for some canonical B\"ohm-reduction 
$P$. The axiom [Reg] follows from the fact that if a $\beta$-redex $u\subt t$ 
is nested in an $\stab_{\mathcal B}$-unneeded $\beta$-redex $v$, then for any
canonical B\"ohm-reduction $P:t\doar$, $P$ does not contract residuals of $v$,
and therefore it does not contract residuals of $u$ as any residual of $u$ is
nested inside a residual of $v$. Finally,  [Min] follows from the fact that 
$P\lleq \lmeet \stab_{\mathcal B}^*$ for 
any canonical B\"ohm-reduction $P$, where $\stab_{\mathcal B}^*$ is the subset
of reductions in $\stab_{\mathcal B}$ that are co-initial with $P$ (note that, 
since $P\in\stab_{\mathcal B}$, $P\lleq \lmeet \stab_{\mathcal B}^*$ implies
$P\leeqv \lmeet \stab_{\mathcal B}^*$). To prove 
$P\lleq \lmeet \stab_{\mathcal B}^*$, assume $P:t=t_0\red{u_0}t_1\red{u_1}\ldots$
and $\lmeet \stab_{\mathcal B}:t=s_0\dored{U_0}s_1\dored{U_1}\ldots$. Since
$u_0$ is external, it must be contracted by any reduction in
$\stab_{\mathcal B}$, hence $u_0\in U_0$ and hence $u_0/U_0=\emptyset$.
Further, $P/U_0$ remains external, and we can prove similarly that the first
contracted redex in $P/U_0$ must belong to $U_1$, and so on. This means that,
$P/\lmeet \stab_{\mathcal B}=\emptyset$, that is, $P\lleq \stab_{\mathcal B}$.



Note that $N\bleq Q$ implies $\omega(N)\oleq \omega(Q)$, but $N\bles Q$ need
not imply $\omega(N)\oles \omega(Q)$. This is because the ordering $\bleq$
is more subtle than $\oleq$ and can take into account (or observe) parts of
computations that occur in the $\bot_{\mathcal B}$-subterms, while
$\omega(t)=\bot_{\mathcal B}$ for any $t$ not in head normal form, 
irrespectively of `how far' is $t$ from being a head normal form. For 
example, let $t=Ix(Ix)$ and $N:t\red{I} (Ix)x$; then  $\emp\bles N$ but
$\omega(\emp)=\omega(N)=\bot_{\mathcal B}$.
\delete{The set of approximants $\{\omega(s)\,\vert\,t\doar s\}$ of $BT(t)$
is in $1-1$ correspondence with the set of $\seqv$-classes $\sclas{P}$ of
`iterated head-reductions' $P:t\doar$ described above.}
Thus $\bleq$, defined on reductions rather than on terms, can be seen as a
refinement of the classical B\"ohm topology on trees~\cite{[Bar]}. 


Thus stability
of sets of reductions is a natural generalization of stability for sets of
finite results. It is also consistent with the definition of stability of
sets of configurations in prime event structures with erasure
in~\cite{[mfcs],[mfcs-tcs]}.





\section{Relative Normalization in SDRSs}
\label{S.rn.sdrs.}


In this section, we will generalize the Relative Hypernormalization theorem 
to regular stable sets of finite or infinite reductions, in stable DRSs 
$\calR$. We then show how $\stab$-minimal reductions can be constructed 
in $\calR$. 


We begin by showing that, for finite or infinite results $\stab$, 
$\stab$-unneeded redexes cannot
create $\stab$-needed ones, and that residuals of $\stab$-unneeded
redexes remain unneeded. When $\stab$ is regular, this enables us to
construct an $\stab$-needed variant of any
$\stab$-normalizing reduction, in any SDRS.


\bll{P.cre.res.need.}
Let $\stab$ be a set of reductions satisfying [CE] and [CS], in an SDRS
(in particular, $\stab$ may be regular), and let 
$P:t\red{u}s\doar\in\stab$. Further:
\ben
\item[(1)] Let $v'$ be a $u$-residual of $v\subt t$, and let $v$ be 
$\stab$-unneeded. Then so is $v'$.

\item[(2)] Let $u$ create  $v\subt s$, and let $u$ be $\stab$-unneeded. 
Then so is $v$.
\een

\bproof
\ben
\item[(1)] Since $v$ is $\stab$-unneeded, there is $Q:t\doar\in\stab$ that is 
external to $v$. Then $Q/u$ is external to $v'$ by 
\Lr{L.external.rem.ext.}, and $Q/u\in\stab$ by [CE], 
\Lr{L.leeq.imp.seqv} and [CS] (indeed, $Q\in \stab \wedge Q\lleq 
u+Q/u$ implies $u+Q/u\in\stab$ implies $Q/u\in\stab$). 
Hence $v'$ is $\stab$-unneeded.

\item[(2)] Since $u$ is $\stab$-unneeded, there is $Q:t\doar\in\stab$ that is 
external to $u$. By \Lr{L.disj.red.creat.}, $Q/u$ is external to $v$, 
and $Q/u\in\stab$ by [CE] and [CS] (see the proof of (1)). Thus $v$ is 
$\stab$-unneeded.
\een
\eproof
\el


\bdl{D.can.sn.}
Let $\stab$ be a set of reductions in an SDRS $\calR$. 
\ben
\item[(1)] We call $P$  \emph{$\stab$-(un)needed} if it contracts only
$\stab$-(un)needed redexes. We call $P$ \emph{$\stab$-quasi-needed} if it
contracts infinitely many $\stab$-needed redexes.

\item[(2)] The \emph{$\stab$-needed part of $P:t\doar$}, written $\snp{P}$, 
is a finite or infinite reduction defined by: $\snp{P}=u+\snp{P/u}$, where 
$u\subt t$ is the redex whose residual along $P$ is contracted first among 
$\stab$-needed steps in $P$, if any.

\item[(3)] We call $P:t_0\ar t_1\ar\ldots$ \emph{$\stab$-needed fair} if
for any $\stab$-needed redex $v\in t_i$, $v_i\sleq \fp{P}{i}$.
\een
\ed


It follows immediately from \Lr{P.cre.res.need.} that $\snp{P}$ is 
$\stab$-needed. Note that $\snp{P}$ is not defined uniquely as its 
$(k+1)$th step depends on the particular sequentializations of multi-steps 
(i.e., complete developments of redex sets) in $P/\ip{\snp{P}}{k}$, but this 
does not cause any difficulties.
 


\bll{L.4.4.1.}
Let $P$ be a finite or infinite reduction in an SDRS $\calR$, and let 
$\stab$ be a regular stable set of reductions in $\calR$. Then $\snp{P}$ 
is an $\stab$-needed reduction whose length coincides with the number of 
$\stab$-needed steps in $P$, and $P\seqv \snp{P}$.

\bproof
Immediate from the fact that, in the notation of \Dr{D.can.sn.}, $u$ has at
most one residual along $P$ (by the regularity of $\stab$), and one of the 
residuals of $u$ is contracted in~$P$ (see the diagram, where all horizontal
steps are $\stab$-unneeded and all vertical ones are $\stab$-needed).
\begin{diagram}[height=1.4em,width=1.8em]
\cdot         &\rOnto & & \cdot       &    & &      &    &   & \\
\dTo     &        &  &\dTo    &        &  &   &           & &  \\
\cdot    &\rOnto   &  & \cdot   &  \rOnto  &&  \cdot   & &  & \\
\dTo &        & &    &         & & \dTo &           & &  \\
\cdot         &\rOnto  & &       &   & & \cdot     & &
& \\
\dOnto^{\snp{P}}     &       &  &   &        &  & & \rdOnto(3,2)^P  &  &  \\
         &   & &     &    & &      &  & &   & & {} \\
\end{diagram}
\eproof
\el


Next we show that, unless it is contracted, an $\reg$-needed redexes has at
least one $\reg$-needed residual. Therefore, residuals of
$\reg$-quasi-needed reductions remain so. It follows that
an $\reg$-normalizable term $t$ cannot possess an
$\reg$-quasi-needed reduction if at least one $\reg$-normalizing reduction
starting from $t$ is finite.


\bll{P.ne.re.sta.reg.}
Let $\stab$ be a regular stable set of reductions in an SDRS $\calR$, and let
$P:t\red{u}s\dored{P'}\in\stab$. Further, let $u\not=v\subt t$, and let
$v$ be $\stab$-needed. Then $v$ has at least one $\stab$-needed residual
in $s$.

\bproof
Since $P\in \stab$ and $v$ is $\stab$-needed, $v/u=V\not=\emp$. Suppose on
the contrary that none of the redexes in $V$ is $\stab$-needed. By [CS] and
\Lr{L.4.4.1.}, $\snp{P'}\in\stab$, and since $\snp{P'}$ is $\stab$-needed,
it is external to $V$ by \Lr{P.cre.res.need.}.(1). Hence $u+\snp{P'}$ is
external to $v$, and $u+\snp{P'}\in\stab$ by [CE], contradicting
$\stab$-neededness of~$v$.
\eproof
\el



\bll{L.4.5.}
Let $\stab$ be a regular stable set of reductions in an SDRS, let $t_{0}$  
have an $\reg$-quasi-needed reduction, and let $t_0\red{u}s_0$.
Then $s_0$ also has an $\reg$-quasi-needed reduction.

\bproof
By \Lr{L.4.4.1.}, $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 $ (see 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 Lemma~\ref{P.ne.re.sta.reg.}, $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.
%
%\begin{figure}
\begin{diagram}[height=1.4em,width=1.4em]
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}
%\caption{Preservation of Quasi-needed Reductions}\label{Di.ess.}
%\end{figure}
\eproof
\end{lem}

The following theorem justifies the stability concept for sets of
reductions:


\btl{ne.fa.norm.reg.}
Let $\stab$ be a regular stable set of reductions in an SDRS $\calR$, and 
let $t$ be $\stab$-normalizable. 
\ben
\item[(1)] Any $\stab$-needed fair reduction starting from $t$
is $\stab$-normalizing.

\item[(2)] If $\stab$ contains a finite reduction starting from $t$,
then $t$ does not possess a reduction in
which $\reg$-needed redexes are contracted infinitely many times.
\een

\bproof
\ben
\item[(1)]
By \Lr{L.4.4.1.}, there is an $\stab$-needed reduction $P:t\doar\in\stab$. 
Let $Q$ be $\stab$-needed fair. By [CE], it is enough to  prove that 
$P\sleq Q$, which requires proving that $\ip{P}{k}\sleq Q$ for every finite 
initial part $\ip{P}{k}$ of $P$. Suppose $\ip{P}{k}\sleq Q$, and let us prove 
$\ip{P}{k+1}\sleq Q$. Then $\ip{P}{k}/\ip{Q}{l_k}$ is $\stab$-unneeded 
for some $l_k$. Let $v$ be the $(k+1)$th step of $P$. If $v$ has an 
$\stab$-needed $\ip{Q}{l_k}/\ip{P}{k}$-residual $v'$, then by 
\Lr{P.cre.res.need.} $v'$ must be a residual of some $\stab$-needed 
redex $v''$ in the final term $t_{l_k}$ of $Q_{l_k}$ (see the diagram), 
and $v''\sleq\fp{Q}{k}$ since $Q$ is $\stab$-needed fair. Thus, by the 
Cube Lemma and \Lr{P.cre.res.need.}, 
$v'\sleq\fp{Q}{l_k}/({\ip{P}{k}/\ip{Q}{l_k}})$, and we are done.
\begin{diagram}[height=1.5em,width=1.5em]
t_0          &\rOnto^{\ip{P}{k}}& &  \cdot       &\rTo^{v}   & {} {} \\
\dOnto<{\ip{Q}{l_k}}&            & &\dTo   &         &      \\
t_{l_k}     &\rOnto^{\ip{P}{k}/\ip{Q}{l_k}}& & \cdot    & \rTo^{v'} & {}  \\
\dOnto<{\fp{Q}{l_k}}   &         & &\dOnto   &             &     \\
{}      &      & & {}      &       &  {}  \\
\end{diagram}

\item[(2)] Let $P:t\doar s$ and $P \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 -- a contradiction, since $P\in\reg$ implies that
$Q/P$ is $\reg$-unneeded.
\een
\eproof
\et


\zurab{Based on the result in Section{S.meet.}, we will now  give 
a sufficient and necessary condition
for superstability of regular stable sets of finite results.
}


\bdl{D.qpn.}
Let $\stab$ be a set of reductions in a DRS.
\ben
\item[(1)] We call $u\subt t$ \emph{$\stab$-erased} if
$u$ does not have a residual under any $\stab$-normalizing reduction.

\item[(2)] We call a reduction \emph{$\stab$-erased} if it only
contracts $\stab$-erased redexes.
\een
\ed


Clearly, a reduction $P$ is $\stab$-erased iff $P\lleq Q$ for every 
$Q\in\stab$. Note that $\stab$-erased redexes need not be $\stab$-needed
(e.g., when $\stab$ is the set of normal forms and the OTRS has
an erasing rule, say $f(x)\ar a$). However, any reducible normalizable 
term $t$ in an orthogonal (first or higher-order) term rewriting system 
has an \emph{external} redex~\cite{[H.L.]}. And such redexes are both 
erased and 
needed w.r.t. to the regular stable sets considered in the literature.




\btl{T.min.fin.}
Let $\stab$ be a regular stable set of terms, in an SDRS.
Then $\stab$ is superstable (i.s, satisfies [Min]) iff any $\stab$-normalizable
term $t\not\in \stab$ contains an $\stab$-erased $\stab$-needed redex.

\bproof
Let $\stab_{red}$ be the set of all $\stab$-normalizing reductions 
starting from $t$, and let $\lmeet \stab_{red}: t=t_0\dored{U_0}
t_1\dored{U_1}\ldots$.

\nec\  By the assumption and the construction of $\lmeet \stab_{red}$,
every multi-step of $\lmeet \stab_{red}$ contracts
an $\stab$-needed redex. Hence $\lmeet \stab_{red}\in \stab_{red}$
by \Tr{ne.fa.norm.reg.} and $\lmeet \stab_{red}$
is $\stab$-minimal by \Tr{T.int.glb.}, which imply~[Min].

\suf\ Since, by [Min], $\lmeet \stab_{red}$ is $\stab$-normalizing, 
it contracts a $\stab$-needed redex by [CUE]. Let $i$ be the smallest 
number such that $U_i$ contains an $\stab$-needed redex, say $v_i$. 
Suppose on the contrary that $i\not=0$. Then, by \Lr{P.cre.res.need.}, 
$t_{i-1}$ contains a $\stab$-needed redex $v_{i -1}$ for which 
$v_i$ is the unique residual (since by the minimality of $i$, all redexes
in $U_{i-1}$ are $\stab$-unneeded). But $v_{i-1}$ is erased along 
$\lmeet \stab_{red}$ since $v_i$ is, and by the $\stab$-minimality of 
$\lmeet \stab_{red}$, $v_{i-1}$ is $\stab$-erased. Hence we must have
$v_{i-1}\in U_{i-1}$ -- a contradiction. 
\eproof
\et

This theorem gives a more `local' definition of superstability
for regular stable sets of finite results.
By combining this with the Relative Hypernormalization theorem,
we get the following corollary:


\bcl{T.qpmn.gen.min.str.}
({\bf Minimal Relative Normalization})
Let $\reg$ be a superstable set of terms in an SDRS, and let
$t$ be an $\reg$-normalizable term 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. 
\ec


\delete{

\begin{rem}\em
\label{R.depth.}
Similarly to the case of regular stable sets of
results~\cite{[rel-glc],[Mel98]}, for any finite $P$, $\sclas{P}$ contains
a $\lleq$-minimal element.  This result is a counterpart of Berry's stability
theorem and the stability property in event structures, but somewhat
strengthened, since as we have already discussed, $\bleq$ is a refinement
of the classical B\"ohm topology.  However, to extend this result to
infinite $P$ as well, one will need SDRSs equipped with a metric associating
a \emph{depth} to every redex, and to restrict the reduction space to
\emph{strongly convergent} reductions only~\cite{[Ken96]}. This goes beyond
the scope of this paper. Restriction to strongly convergent reductions seems
also necessary to insure stability of  sets of co-initial fair reductions
(cf.~\cite{[mfcs-tcs]}).
\end{rem}
}





\section{Concluding remarks}
\label{S.concl.}


We have formalized a concept of `infinite results', and proved a 
normalization theorem relative to such results, in an abstract framework
of SDRSs. We also studied minimal relative normalization in SDRSs. 
These results unify and extend several earlier results on relative and 
discrete normalization. Furthermore, concepts of stable sets of results
and corresponding orderings introduced in this paper allow SDRSs to be viewed
as semi-distributive domains, or `domains with duplication'~\cite{[stable]}. 





\begin{thebibliography}{99}


\bibitem{[A.O.]}
S. Abramsky and C.-H. L. Ong, Full abstraction in the lazy lambda calculus,
\emph{Information and Computation} {\bf 105} (1993) 159-267.


\delete{
\bibitem{[Acz]}
Aczel P. A general Church-Rosser theorem. Preprint, University of
Manchester, 1978.
}


\bibitem{[Ant]}
S. Antoy, R. Echahed and M. Hanus, A needed narrowing
strategy, in: \emph{Proc. 21st ACM Symp. on Principles of
Programming Languages} (1994) 268-279.


\bibitem{[AnMi]}
S. Antoy and A. Middeldorp, A Sequential Reduction Strategy,
\emph{Theoret. Comput. Sci.} {\bf 165(1)} (1996) 75-95.


\bibitem{[A.F.]}
Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, P.A. Wadler, A
call-by-need lambda calculus, in: \emph{Proc. 22nd ACM Symp. on Principles
of Programming Languages} (1995) 233-246.

\delete{
\bibitem{[AL]}
A. Asperti and C. Laneve, Interaction systems I: The
theory of optimal reductions,  \emph{Mathematical Structures in Computer
Science} {\bf 11} (1993) 1-48.


\bibitem{[AL2]}
A. Asperti and C. Laneve, Interaction systems II: The practice of optimal
reductions,  \emph{Theoret. Comput. Sci.} {\bf 159(2)} (1996) 191-244.


\bibitem{[A.M.]}
A. Asperti and H. Mairson, Parallel beta reduction is not elementary
recursive, in: \emph{Proc. 25th ACM Symp. on Principles of Programming
Languages} (1998).


\bibitem{[A.G.]}
A. Asperti and S. Guerrini, \emph{The Optimal Implementation of Functional
Programming Languages} (Cambridge Tracts in Theoretical Computer Science 
{\bf 45}, Cambridge University Press, 1998). 
}

\bibitem{[Bar]}
H. P. Barendregt, \emph{The Lambda Calculus, Its Syntax and Semantics}
(North-Holland, Amsterdam, 1984).


\delete{
\bibitem{[Bar.76]}
H.P. Barendregt, J.A. Bergstra, J.W. Klop and H. Volken, Some notes on
lambda-reduction, in: Degrees, reductions, and representability in the
lambda calculus, Preprint no. 22, University of Utrecht, Department of
mathematics, 1976, 13-53.
}

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


\bibitem{[Ber96]}
Berarducci A. Infinite lambda-calculus and non-sensible models. 
Logic and Algebra, Lecture Notes in Pure and Applied Mathematics 180, 
Marcel Dekker Inc., 1996, p.~339-378.


\bibitem{[berry]}
G. Berry, Mod\'eles compl\'etement ad\'equats et stables des
$\lambda$-calculs typ\'es, Th\`ese de l'Universit\'e
de Paris VII, 1979.

\bibitem{[B.L.]}
G. Berry and J.-J. L\'evy,  Minimal and optimal computations of recursive
programs, \emph{J. of the Association for Computing Machinery} {\bf 26}
(1979) 148-175.


\bibitem{[Bou]}
G. Boudol, Computational semantics of term rewriting systems.
in: M.~Nivat and J.C.~Reynolds, eds., \emph{Algebraic methods in semantics}
(CUP, 1985) 169-236.

\bibitem{[C.R.]}
A. Church and J.B. Rosser, Some properties of conversion,
\emph{Transactions of American Mathematical Society} {\bf 39} (1936)
472-482.

\delete{
\bibitem{[C.K.]}
D. Clark and J.R. Kennaway, Event structures and non-orthogonal term graph
rewriting, \emph{Mathematical Structures in Computer Science} {\bf 6}
(1996) 545-578.
}

\bibitem{[C.F.]}
H.B. Curry and R. Feys, \emph{Combinatory Logic, Vol.~1}  (North-Holland,
Amsterdam, 1958).


\delete{
\bibitem[{DeJo90}]{[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{[Gar]}
P. Gardner, Discovering needed reductions using
type theory,  in: \emph{Proc. TACS'94}, Lecture Notes in Computer Science,
vol~789  (Springer, Berlin, 1994) 555-574.

\delete{
\bibitem{[ctrs]}
J.R.W. Glauert and Z. Khasidashvili, Relative normalization in
orthogonal expression reduction systems, in: \emph{Proc. CTRS'94}, Lecture
Notes in Computer Science, vol.~968  (Springer, Berlin, 1994) 144-165.


\bibitem{[morn]}
J.R.W. Glauert and Z. Khasidashvili, Minimal and optimal relative
normalization in orthogonal expression reduction systems, Technical Report
SYS-C94-06, UEA Norwich,~1994.
}

\bibitem{[rndrs]}
J.R.W. Glauert and Z. Khasidashvili, Relative normalization in deterministic
residual structures, in: \emph{Proc. CAAP'96}, Lecture Notes in Computer
Science, vol.~1059 (Springer, Berlin, 1996) 180-195.

\delete{
\bibitem{[rndrs-rep]}
J.R.W. Glauert and Z. Khasidashvili, Relative normalization in stable
deterministic residual structures, Technical Report SYS-C96-05, UEA
Norwich,~1996.
}


\bibitem{[rel-glc]}
J.R.W. Glauert, J.R. Kennaway  and Z. Khasidashvili, Stable results and 
relative normalization, \emph{Journal of Logic and Computation} 
{\bf 10(3)}, Special Issue: Type Theory and Term Rewriting, 
F.~Kamareddine and J.W.~Klop, eds. Oxford University Press (2000)
323-348.



\delete{
\bibitem{[GAL]}
G. Gonthier, M. Abadi and J.-J. L\'evy,  The geometry of optimal lambda
reduction,   in: \emph{Proc. 19th ACM Symp. on Principles of Programming
Languages} (1992) 15-26.
}

\bibitem{[GLM]}
G. Gonthier, J.-J. L\'evy and P.-A. Melli\`es, An abstract standardisation
theorem, in: \emph{Proc. 7th IEEE Symp. on Logic in Computer Science}
(1992) 72-81.

\delete{
\bibitem{[Gue.th]}
S. Guerrini, Theoretical and practical issues of optimal implementations of
functional languages, Ph.D. Thesis, University of Pisa,~1996.
}

\bibitem{[Hin]}
R.J. Hindley,  An abstract form of the Church-Rosser theorem I,
\emph{Journal of Symbolic Logic} {\bf 34(4)} (1969) 545-560.

\delete{
\bibitem{[H.P.]}
B. Hoffmann and D. Plump, Implementing term rewriting by jungle evaluation,
\emph{Theoretical Informatics and Applications} {\bf 25} (1991) 445-472.
}

\bibitem{[Hu80]}
G. Huet, Confluent reductions: Abstract properties and applications to term
rewriting systems, \emph{J. of the Association for Computing Machinery}
{\bf 27(4)} (1980) 797-821


\bibitem{[H.L.]}
G. Huet and  J.-J. L\'evy,  Computations in Orthogonal Rewriting  Systems,
in: J.-L.~Lassez and G.~Plotkin, eds., \emph{Computational Logic, Essays in
Honor of Alan Robinson}  (MIT Press, 1991) 394-443.


\delete{
\bibitem{[Kath]}
V. Kathail, Optimal interpreters for lambda-calculus based functional
languages, Ph.D. Thesis, MIT, 1990.
}

\bibitem{[Kenn]}
J.R. Kennaway, Sequential evaluation strategy for
parallel-or and related reduction systems, \emph{Annals of Pure and
Applied Logic} {\bf 43} (1989) 31-56.


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

\bibitem{[KKSdV]}
J.R. Kennaway, J.W. Klop, M.R. Sleep and F.-J. de Vries,  Event structures and
orthogonal term graph rewriting, in: M.R.~Sleep, M.J.~Plasmeijer,
M.C.J.D.~van Eekelen, eds., \emph{Term Graph Rewriting: Theory and
Practice} (John Wiley,
1993) 141-156.


\bibitem{[K-tra]}
J.R. Kennaway, J.W. Klop, M.R. Sleep and F.-J. de Vries, Transfinite
reductions in orthogonal term  rewriting systems, \emph{Information and
Computation} {\bf 119(1)} (1995) 18-38.


\bibitem{[colog]}
Z. Khasidashvili, $\beta$-reductions and $\beta$-developments of
$\lambda$-terms with the least number of steps, in: \emph{Proc. COLOG'88},
Lecture Notes in Computer Science, Vol.~417 (Springer, Berlin, 1990)
105--111.

\delete{
\bibitem{[OCRS]}
Z. Khasidashvili, The Church-Rosser theorem in orthogonal combinatory
reduction systems, Report 1825, INRIA Rocquencourt, 1992.
}

\bibitem{[rta]}
Z. Khasidashvili, Optimal normalization in orthogonal term  rewriting
systems, in: \emph{Proc. RTA'93}, Lecture Notes in Computer Science,
Vol.~690 (Springer, Berlin, 1993) 243-258.

\bibitem{[stable]}
Z. Khasidashvili, Stable computational semantics of conflict-free rewrite
systems. \zurab{(Available on request.)}


\bibitem{[dndrs]}
Z. Khasidashvili and J.R.W. Glauert, Discrete normalization and
standardization in deterministic residual structures, in: \emph{Proc.
ALP'96}, Lecture Notes in Computer Science, vol.~1139 (Springer, Berlin,
1996) 135-149.

\delete{
\bibitem{[dndrs-rep]}
Z. Khasidashvili and J.R.W. Glauert, Discrete normalization and
standardization in stable deterministic residual structures,  Technical Report
SYS-C96-06, UEA Norwich,~1996.


\bibitem{[azdfs]}
Z. Khasidashvili and J.R.W. Glauert, Zig-zag, extraction and separable
families in  non-duplicating stable deterministic residual structures,
Technical Report IR-420, Free University, Amsterdam,~1997.
}

\delete{
\bibitem{[icalp]}
Z. Khasidashvili and J.R.W. Glauert, The geometry of orthogonal reduction
spaces, in: \emph{Proc. ICALP'97}, Lecture Notes in Computer Science, vol.~1256
(Springer, Berlin, 1997) 649-659.
}

\delete{
\bibitem{[icalp-rep]}
Z. Khasidashvili and J.R.W. Glauert, The geometry of conflict-free
reduction spaces,  Technical Report
SYS-C98-04, UEA Norwich,~1998.
}

\delete{
\bibitem{[geo-tcs]}
Z. Khasidashvili and J.R.W. Glauert, The conflict-free reduction geometry.
(Extended version of~\cite{[icalp]}, submitted for publication.)
\zurab{Available on request.}
}

\bibitem{[mfcs]}
Z. Khasidashvili and J.R.W. Glauert,  Relating conflict-free stable
transition and event models (extended abstract), in: \emph{Proc. MFCS'97},
Lecture Notes in Computer Science, vol.~1295 (Springer, Berlin, 1997)
269-278.


\bibitem{[mfcs-tcs]}
Z. Khasidashvili and J.R.W. Glauert,  Relating conflict-free stable
transition and event models via redex families. Special issue dedicated 
to MFCS'97 conference, P.~Ru\v{z}i\v{c}ka, ed. Theoretical Computer 
Science (to appear). Available at
{\tt http://www.cs.biu.ac.il/\~{}khasidz}.

\delete{
\bibitem{[acoi-rep]}
Z. Khasidashvili and J.R.W. Glauert, An abstract concept of optimal
imple\-men\-ta\-tion, Technical Report SYS-C97-01, UEA Norwich,~1997.
}


\delete{
\bibitem{[Kl.CRS]}
J.W. Klop, \emph{Combinatory reduction systems} (Mathematical Centre Tracts
no.~127,  Amsterdam, 1980).
}

\bibitem{[Klo92]}
J.W. Klop, Term  rewriting systems,  in:  S.~Abramsky, D.~Gabbay  and
T.~Maibaum, eds.,  \emph{Handbook  of Logic in Computer Science, Vol.~2}
(Oxford University Press, 1992) 1-116.

\delete{
\bibitem{[Laf]}
Y. Lafont, Interaction nets, in: \emph{Proc. 17th ACM Symp. on Principles
of Programming Languages} (1990) 95-108.


\bibitem{[Lam]}
J. Lamping, An algorithm for optimal lambda calculus reduction,
in: \emph{Proc. 17th ACM Symp. on Principles of Programming Languages}
(1990) 6-30.
}

\bibitem{[le76]}
L\'evy J.-J. An algebraic interpretation of the
$\lambda\beta K$-calculus; and an
application of a labelled \lc. TCS 2(1):97-114, 1976.


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


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

\bibitem{[Lon]}
Longo G. Set theoretic models of lambda calculus: theories, expansions
and isomorphisms. Annals of Pure and Applied Logic, 24:153-188, 1983.

\delete{
\bibitem{[Mar91]}
L. Maranget, Optimal derivations in weak $\lambda$-calculi and in orthogonal
term rewriting systems, in: \emph{Proc. 18th ACM Symp. on Principles of
Programming Languages} (1991) 255-269.
}

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


\bibitem{[Mel.th]}
P.-A. Melli\`es,  Description Abstraite des Syst\`emes de R\'e\'ecriture,
Th\`ese de l'Uni\-versit\'e Paris VII, 1996.

\bibitem{[Mel2]}
P.-A. Melli\`es, Axiomatic rewriting theory II: The $\lambda\sigma$-calculus
enjoys finite normalization cones, \emph{Journal of Logic and Computation} 
{\bf 10(3)}, Special Issue: Type Theory and Term Rewriting, 
F.~Kamareddine and J.W.~Klop, eds. Oxford University Press (2000)
461-487.

\delete{
\bibitem{[Mel98]}
P.-A. Melli\`es, Axiomatic rewriting theory IV: A stability theorem in
rewriting theory, in: \emph{Proc. 14th IEEE Symp. on Logic in Computer
Science} (1998).
}

\bibitem{[Mid]}
A. Middeldorp, Call by need computations to root-stable form, in:
\emph{Proc. 24th ACM Symp. on Principles of Programming Languages} (1997)
94-105.


\delete{
\bibitem{[NPW]}
M. Nielsen, G. Plotkin and G. Winskel, Petri nets, event structures and
domains, Part 1, \emph{Theoret. Comput. Sci.} {\bf 13} (1981) 85-108.
}

\bibitem{[Nok.thi.]}
E. N\"ocker, Efficient functional programming: Compilation and
programming techniques, Ph.D. Thesis, Katholic University of
Nijmegen, 1994.


\delete{
\bibitem{[OD]}
M. O'Donnell, Reduction strategies in subtree replacement systems, Ph.D.
thesis, Cornell University, Ithaca, N.Y., 1976.
}

\bibitem{[Oos.th]}
V. van Oostrom, Confluence for abstract and higher-order rewriting, Ph.D.
Thesis, Free University, Amsterdam,~1994.

\delete{
\bibitem{[Oos]}
V. Van Oostrom, Higher order families, in: \emph{proc. RTA'96}, Lecture
Notes in Computer Science, vol.~1103 (Springer, Berlin, 1996) 392-407.
}

\delete{
\bibitem{[Oos97]}
V. Van Oostrom, Finite family developments, in: \emph{proc. RTA'97},
Lecture Notes in Computer Science, vol.~1232 (Springer, Berlin, 1997)
308-322.
}

\bibitem{[Oos99]}
V.~van Oostrom, Normalisation in weakly orthogonal rewriting,
in: \emph{proc. RTA'99}, Lecture Notes in Computer Science, vol.~1631 
(Springer, Berlin, 1999) 60-74.


\delete{
\bibitem{[Plo75]}
G. Plotkin,  Call-by-name, call-by-value and the $\lambda$-calculus,
\emph{Theoret. Comput. Sci.} {\bf 1} (1975) 125-159.
}

\bibitem{[Raa.th]}
F. van Raamsdonk, Confluence and normalisation for higher-order rewriting,
Ph.D. Thesis, Free University, Amsterdam,~1996.


\delete{
\bibitem{[Ros]}
B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, \emph{J.
of the Association for Computing Machinery} {\bf 20} (1973) 160-187.
}

\delete{
\bibitem{[Sch]}
G. Schied, On relating rewrite systems and graph grammars to event
structures, in: \emph{Proc. GTCS'94}, Lecture Notes in Computer Science,
vol.~776 (Springer, Berlin, 1994) 326-340.
}

\bibitem{[SeRa]}
R.C. Sekar and  I.V. Ramakrishnan, Programming in equational logic: Beyond
strong sequentiality, \emph{Information and Computation} {\bf 104(1)}
(1993) 78-109.

\bibitem{[Sta]}
E.W. Stark, Concurrent transition systems, \emph{Theoret. Comput. Sci.}
{\bf 64(3)} (1989) 221-269.

\delete{
\bibitem{[Wad]}
P.C. Wadsworth, Semantics and pragmatics of the lambda-calculus, Ph.D.
thesis, University of Oxford, 1971.


\bibitem{[Win]}
G. Winskel, Events in computation, Ph.D. Thesis, Edinburgh University, 1980.
}

\bibitem{[Win89]}
G. Winskel, An introduction to event structures, in: \emph{Proc. Linear
time, branching time and partial order in logics and models of
concurrency}, Lecture Notes in Computer Science, vol.~354 (Springer,
Berlin, 1989) 364-397.

\bibitem{[Xi]}
H. Xi, Evaluation under lambda abstraction,  in: \emph{proc. PLILP'97},
Lecture Notes in Computer Science, vol.~1292 (Springer, Berlin, 1997)
259-274.

\bibitem{[Yos]}
N. Yoshida, Optimal reduction in weak \lc\ with shared environments, in:
\emph{Proc. ACM Conference on Functional Programming Languages and Computer
Architecture} (1993) 243-252.

\end{thebibliography}
\end{document}
%% End LaTeX Document