\documentstyle{llncs}
%\documentstyle[fullpage,10pt]{article}
%\documentstyle[fullpage,11pt,amssymbols]{article}
%\input{BoxedEPS}
%\HideDisplacementBoxes
%\SetOzTeXEPSFSpecial
\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt

\textwidth   6.0in
\textheight  8.5in

\input{diagrams} % Paul Taylor's Macro Package
\newcommand{\delete}[1]{} % Comment out text.
\newcommand{\john}[1]{\{{\bf John:\sf #1}\}} % Highlight text.
\newcommand{\zurab}[1]{\{{\bf Zurab:\sf #1}\}} % Highlight text.
\begin{document}
%\def \dred {\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\def \doar{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\newtheorem{nota}{Notation}[section]
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
%%%%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
%\newenvironment{proof}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\newcommand{\notation}{{\bf Notation }}
%\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\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}
\newcommand{\empt}{\emptyset}
\hyphenation{meta-var-ia-ble}
\newcommand{\len}[1]{\mbox{$\vert{#1}\vert$}}
\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{\err}[2]{\mbox{$SE_{{#1}}({#2})$}}

\newcommand{\pessim}[0]{\prec\!\!\prec}
\newcommand{\steq}[0]{\approx_{st}}
\newcommand{\essim}[0]{\approx}
\newcommand{\psim}[0]{\prec}
\newcommand{\orth}[0]{\perp}
\newcommand{\esorth}[0]{\perp_{es}}
\newcommand{\subt}[0]{\in}
\newcommand{\subts}[0]{\subseteq}
\newcommand{\contr}[0]{\hookrightarrow}
\newcommand{\fin}[0]{\in}
%\newcommand{\lleq}[0]{\triangleleft}
%\newcommand{\lles}[0]{\triangleleft}
\newcommand{\lleq}[0]{\unlhd}
\newcommand{\lles}[0]{\lhd}
\newcommand{\leeqv}[0]{\approx_L}
\newcommand{\hieqv}[0]{\approx_H}
\newcommand{\snpp}[0]{\approx_{sn}}
\newcommand{\inter}[0]{\ddagger}
\newcommand{\ind}[0]{\perp}
\newcommand{\hole}[0]{\circ}
\newcommand{\restr}[0]{\vert}
\newcommand{\exten}[0]{\updownarrow}
\newcommand{\fami}[0]{\simeq}
\newcommand{\zfami}[0]{\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{\lc}[0]{$\lambda$-calculus}
\newcommand{\ovl}[0]{\overline}
\newcommand{\unl}[0]{\underline}
\newcommand{\bd}[0]{\begin{deff}\em}
\newcommand{\bdl}[0]{\begin{deff}\em\label}
\newcommand{\bl}[0]{\begin{lem}\em}
\newcommand{\bll}[0]{\begin{lem}\em\label}
\newcommand{\bp}[0]{\begin{prop}\em}
\newcommand{\bpl}[0]{\begin{prop}\em\label}
\newcommand{\bt}[0]{\begin{thm}\em}
\newcommand{\btl}[0]{\begin{thm}\em\label}
\newcommand{\bel}[0]{\begin{ex}\em\label}
\newcommand{\bc}[0]{\begin{cor}\em}
\newcommand{\bcl}[0]{\begin{cor}\em\label}
\newcommand{\bproof}[0]{\begin{proof}}
\newcommand{\eproof}[0]{\end{proof}}
\newcommand{\ed}[0]{\end{deff}}
\newcommand{\el}[0]{\end{lem}}
\newcommand{\ep}[0]{\end{prop}}
\newcommand{\et}[0]{\end{thm}}
\newcommand{\ee}[0]{\end{ex}}
\newcommand{\ec}[0]{\end{cor}}
\newcommand{\setm}[0]{\setminus}
\newcommand{\crea}[0]{\vdash}
\newcommand{\emp}[0]{\emptyset}
\newcommand{\cfr}[0]{complete family-reduction\/}
\newcommand{\cfrs}[0]{complete family-reductions\/}
\newcommand{\qp}[0]{quasi-persistently}
\newcommand{\stc}[0]{strongly cofinal}
\newcommand{\suf}[0]{($\Rightarrow$)}
\newcommand{\nec}[0]{($\Leftarrow$)}
\newcommand{\nsuf}[0]{($\not\Rightarrow$)}
\newcommand{\nnec}[0]{($\not\Leftarrow$)}
\newcommand{\stab}[0]{{\cal S}}
\newcommand{\reg}[0]{{\cal R}}
\newcommand{\sls}[0]{}
\newcommand{\Le}{L\'evy}

\delete{
\title{Discrete Normalization and Standardization in Deterministic Residual
Structures}
\author{Zurab Khasidashvili and John Glauert  \\ School of Information
Systems, UEA\\
Norwich NR4 7TJ England \\
\sf{zurab@sys.uea.ac.uk, jrwg@sys.uea.ac.uk}\\
DRAFT, DO NOT DISTRIBUTE}
}

\title{Discrete Normalization and Standardization \\
in Deterministic Residual Structures}
\author{Zurab Khasidashvili and John Glauert}
\institute{School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
zurab@sys.uea.ac.uk, jrwg@sys.uea.ac.uk \\
Tel: +44 1603 59 26 71 \\
Fax: +44 1603 59 33 44
\thanks{This work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300}}

\maketitle

\begin{abstract}
We prove a version of the {\em Standardization Theorem\/} and the {\em
Discrete Normalization Theorem\/} in  {\em stable semi-linear Deterministic
Residual Structures}, which are {\em Abstract Reduction Systems\/} with
axiomatized {\em residual\/} relation. The latter theorem gives as a
corollary a Gross-Knuth style algorithm for construction of reductions
L\'evy-equivalent (or permutation-equivalent) to a given, finite or
infinite, reduction. This and other results of this paper add to the
understanding of L\'evy-equivalence of reductions, and consequently,
L\'evy's reduction space. \zurab{The importance of the latter is already
well-understood, and the substantiate it further by demonstrating
how elements of this space can be used to give denotational semantics
of known functional languages (based on rewrite systems) without reference
to the syntax.}
\end{abstract}


\section{Introduction}

Long ago, Curry and Feys~\cite{[C.F.]} proved that repeated contraction of
leftmost-outermost redexes in any normalizable $\lambda$-term eventually
yields its normal form, even if the term possesses infinite reductions as
well. The reason is that such redexes are {\em needed\/} in every
normalizable term $t$, i.e., they are contracted in every normalizing
reduction starting from $t$. Based on this observation, Huet and L\'evy
defined a general normalizing strategy, called the {\em needed} strategy,
for Orthogonal Term
Rewriting Systems (OTRSs). They showed that any
term $t$ not in normal form has a needed redex, and that repeated
contraction of needed redexes in $t$ leads to its normal form
whenever there is one.

Barendregt et al.~\cite{[B.K.K.S.]} studied neededness w.r.t. normal forms
as well as w.r.t. head-normal forms, in the $\lambda$-calculus, proving
correctness of the two needed strategies for computing normal
forms and head-normal forms, respectively. Maran\-get \cite{[Mar]}
studied a strategy that computes a weak head-normal form of a term in an
OTRS. Normalization w.r.t. another interesting set of `normal forms', that
of constructor head-normal forms in constructor OTRSs, is
studied by N\"ocker~\cite{[Nok.thi.]}.

Khasidashvili defined a similar normalizing strategy, called the {\em
essential\/} strategy, for the $\lambda$-calculus~\cite{[colog]} and
OTRSs~\cite{[rta]}. The strategy contracts {\em essential\/} redexes -- the
redexes that have {\em descendants\/} (not residuals) under any reduction.
Sekar and Ramakrishnan~\cite{[SeRa]} study a normalizing strategy which in
each multi-step contracts a {\em necessary\/} set of redexes -- a set at
least one member of which is contracted in every normalizing reduction. A
different approach to normalization in not-necessarily orthogonal rewrite
systems is developed in Kennaway~\cite{[Kenn]} and
Antoy\&Middeldorp~\cite{[AnMi]}. Antoy et al.~\cite{[Ant]} designed a needed
narrowing strategy.
\delete{Khasidashvili~\cite{[caap]} showed that in {\em Persistent\/} OERSs,
where redex-creation is limited, one can find {\em all\/} needed redexes in
any term.} Gardner~\cite{[Gar]} described a {\em complete\/} way of encoding
neededness information using a type assignment system.
Kennaway et al.~\cite{[K-tra]} studied needed strategy for infinitary OTRSs.

In~\cite{[ctrs]}, the present authors found
natural conditions on a set $\stab$ of terms, called {\em stability}, that are
necessary and sufficient for the following {\em Relative Normalization\/}
(RN for short) theorem to hold:  each $\stab$-normalizable term not in
$\stab$ (not in {\em $\stab$-normal form\/}) has at least one
$\stab$-needed redex, and repeated contraction of $\stab$-needed redexes in
a term $t$ will lead to an $\stab$-normal form of $t$ whenever there is
one.  Roughly,  $\stab$ is stable if it is closed under reduction (this
condition can be relaxed slightly)  and any step  $u$ entering $\stab$ is
$\stab$-needed.  This work is done in the context of orthogonal {\em
Expression Reduction Systems\/} (OERS)~\cite{[OCRS]}, a form of
higher-order rewriting which subsumes Term Rewriting and the
$\lambda$-calculus.

In~\cite{[rndrs]}, the authors further generalized the theory of relative
normalization by abstracting from the structure of terms. They study
relative normalization in {\em Deterministic Residual Structures} (DRSs),
and {\em Deterministic Family Structures} (DRSs). DRSs are {\em Abstract
Reduction Systems} (ARSs) where the residual relation on redexes is
axiomatized in a way that enables one to define permutation-equivalence on
reductions; DFSs are DRSs where in addition L\'evy's notion of {\em
redex-family\/} is also axiomatized. They proved the RN theorem for {\em
stable\/} DRS, for {\em regular\/} stable sets $\reg$ of final terms, and
for DFSs for {\em all\/} stable sets $\stab$ of final terms. Here a stable
set $\stab$ is {\em regular\/} if $\stab$-unneeded redexes cannot duplicate
$\stab$-needed ones.

Here we study reductions from a term $t$ to an arbitrary term $s$, assuming
such a reduction exists. If the set $\{s\}$ is stable, such as when $s$ is
a normal form, then existing theory can be applied. Otherwise,
if the reduction graph $G_s$ of $s$ is
stable and {\em regular}, then the task can be reduced to
construction of a {\em minimal\/} (w.r.t. L\'evy's ordering $\lleq$ on
reductions) $G_s$-normalizing reduction~\cite{[morn]}, since it must end at
$s$.
\delete{
But, for any pair of terms $(t,s)$, one might be interested to construct a
reduction from $t$ to $s$, whenever possible, and it might be the case that
the set $\{s\}$ is not stable. If the reduction graph $G_s$ of $s$ is
stable and {\em regular}, when the above task can be reduced to
construction of a {\em minimal\/} (w.r.t. L\'evy's ordering $\lleq$ on
reductions) $G_s$-normalizing reduction~\cite{[morn]}, since it must end at
$s$.
}
However, as we already know~\cite{[ctrs]}, $G_s$ need not be stable,
mainly because of {\em syntactic accidents}~\cite{[le80]}. For example, the
graph $\{I(x),\,x\}$ of $s=I(x)$, in the TRS with the rule $I(x)\ar x$, is
not stable, since $t=I(I(x))$ can be reduced to $s$ by contracting either
redex. Neither of the two redexes in $t$ is $G_s$-needed, and neither of
the two reductions $u:t\dored{I(I(x))}s$ and $v:t\dored{I(x)}s$ is
$G_s$-minimal -- we have $u\not\lleq v$, $v\not\lleq u$, and $u\not\leeqv
v$.

\delete{
form an
upper semi-lattice with L\'evy's embedding relation $\lleq$ as the
ordering.
}

A constructive approach is to develop a neededness theory relative to {\em
particular\/} reductions $P:t\doar s$, or more precisely, relative to
L\'evy-equivalence classes $\lclas{P}$ of reductions $P$, which
are elements of L\'evy's reduction space ordered by $\lleq$.
(Hence the name -- {\em discrete\/} normalization.)
We cannot aim at developing a needed strategy constructing  {\em a\/}
reduction from $t$ to $s$ because a redex in $t$ contracted in every
reduction from $t$ to $s$ may not exist, as is the case for the terms
$t=I(I(x))$ and
$s=I(x)$.\footnote{However, `normalization via necessary sets' approach
of~\cite{[SeRa]} may be useful here.} Furthermore, the task of construction
of a reduction L\'evy-equivalent to a given one makes sense also for
infinite reductions.


\zurab{In this paper we indeed develop a neededness theory relative
to particular
reductions, which enable us to characterize (and often construct)
reductions in $\lclas{P}$ for any
reduction $P:t\doar$, finite or infinite, in \emph{stable semi-linear
DRSs}. (Under an `infinite' reduction we mean a reduction of the length
$\omega$.)
We obtain two main
results: the \emph{Standardization Theorem}, and the \emph{Discrete
Normalization Theorem}. The first one states that every finite reduction
$P$ can, in some canonical way, be transferred into a \emph{standard} or
\emph{self-essential} reduction $SE(P)$ \Le-equivalent to $P$, where
self-essentiality means that `omission' of a step in $SE(P)$ would
yield a reduction no longer \Le-equivalent to $P$; and that for infinite
reductions $P$, standard reductions \Le-equivalent to $P$ need not exist.
This concept of standardization is the best approximation to the
left-to-right outside-in concept of
standardization~\cite{[Bar],[Kl.CRS]}, since we don't
have any nesting reduction imposed on redexes, differently from
ARSs of ~\cite{[GLM]}, and there is no concept of `left' or `right'
occurrences in DRSs. However, perhaps surprisingly, our standard
reductions can be used successfully as canonical
representatives in their \Le-equivalence classes. The second one (the DN
theorem) states that if $P$ is finite, then contraction of \emph{$P$-needed
$P$-erased} redexes eventually terminates by constructing a reduction in
$\lclas{P}$; and if $P$ is infinite, contraction of all $P$-erased redexes
in a term in parallel yields a reduction in $\lclas{P}$. Here a redex is
$P$-needed if at least one residual of it is contracted by any reduction in
 $\lclas{P}$, and is $P$-erased if it doesn't have residuals in some later
term of $P$.


The importance of this results is not only theoretical. Since every
functional programming language is given by a (very often orthogonal)
syntactic rewrite system $R$ and a \emph{deterministic} strategy $F$
(such as the lazy, call-by-name, and several eager strategies in the \lc),
the \emph{value} of a term $t$ is defined via its computation according
to $F$, i.e., is associated with the reduction
$P^{F}_t:t\ar F(t)\ar F(F(t))\ar\ldots$. In semantics, values of
terms are usually defined via some kind of finite or infinite trees,
constructed from symbols from the alphabet and a special constant
$\bot$ to define \emph{undefined} (in some sense) terms. And the reductions
$P^{F}_t$ are those that compute these trees. Examples of semantic trees
are Nivat's trees for Recursive Program Schemes~\cite{[Niv]}, and the
B\"ohm-trees~\cite{[Bar]} and L\'evy-Longo trees (called also
\emph{lazy-trees}~\cite{[le76],[Lon]}, in the \lc. Foe example,
the B\"ohm-tree of a $\lambda$-term $t$ is computed by the
strategy which first computes the head-normal-form (hnf) of $t$ using the
leftmost-outermost strategy $F_l$, then (if successful) continues in
the same manner in parallel in some subterms of the obtained term $t_1$,
and so on; the subterms where $F_l$ doesn't terminate at a hnf are
replaced by $\bot$.

So, our DN theorem characterizes computations of a term which
converge to the value of a term, where value can be defined in various
ways. And we will describe an abstract approach to semantics of
orthogonal systems, and show how the known (to us) semantics of orthogonal
systems can be recovered, \emph{without} any assumption of syntax, using
L\'evy's reduction space which we study here.
Similar considerations apply to several logic based programming
languages where operational semantics is also defined by deterministic
execution strategies. For \emph{narrowing}, a needed evaluation strategy is
already developed in~\cite{[Ant]}, and we expect that much of the theory
developed for DRSs can be extended to cover several proof procedures as
well.



The paper is organized as follows. In the next section, we recall the
definition of DRSs. In Section~\ref{S.drs.prop.}, we study relative
properties of discrete neededness, essentiality and erasure, and show
existence of $P$-needed redexes for any finite $P$ in a stable
DRS. \delete{Section~\ref{S.st.cof.fa.} relates fairness with strong
cofinality.} Section~\ref{S.sta.} is devoted to the standardization and
related results, which are used in Section~\ref{S.dis.no.} to prove the
Discrete Normalization Theorem, the main result of this paper.
Section~\ref{S.abs.sem.} is devoted to semantics of DRSs. Conclusions
appear in Section~\ref{S.concl.}.
}

\section{Deterministic Residual Structures}

In this section we recall {\em Deterministic Residual Structures} (DRSs),
introduced in \cite{[rndrs]} but largely based on ~\cite{[le80]}.
DRSs are {\em Abstract Reduction Systems\/} (ARSs) with axiomatized notions of
residual.

The definition and some results about ARSs can be found e.g.,
in~\cite{[Kl.TRS]}.
Our definition is slightly different. An ARS is a
triple $A$ = ({\em Ter},{\em Red},$\ar$)
where {\em Ter} is a set of {\em terms}, ranged over by
$t,s,o,e$; {\em Red} is a set of {\em redexes} (or {\em 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 {\em total\/} function, so one can identify $u$ with the
triple $t\red{u}s$.\footnote{Klop's ARSs are pairs $(Ter,\ar)$, and do not
allow one to distinguish transitions with the same source and target
terms.}
A {\em reduction} is a sequence
$t\red{u_1}t_2\red{u_2}\ldots$. 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$, and write $P:t\doar $ if $P$ denotes a (finite or infinite)
reduction starting from $t$. $\,\,\vert P\vert$ denotes the length of $P$.
$P\leq Q$ denotes
that $P$ is an initial part of $Q$. $\,\,\,\emptyset_t$ denotes the empty
reduction starting from $t$.
\delete{$Pu$ denotes a redex $u$ in the final term $ft(P)$ of $P$.
 $u$ also denotes the reduction that contracts $u$.} We use $U,V,W$ to
denote sets of redexes of a term.

DRSs are similar to Stark's {\em Determinate Concurrent Transition
Systems}~\cite{[Sta]}, to {\em Abstract Reduction Systems} of Gonthier et
al.~\cite{[GLM]},
and to van Oostrom's {\em Descendant Rewriting Systems}~\cite{[Oos.th]}.
The main difference from DCTSs is that Stark considers  a non-duplicating
residual relation (and we do not distinguish a {\em start state}). The
difference from ARSs of~\cite{[GLM]} is that we do
not have a nesting relation on redexes and the corresponding axioms, and
the stability axiom is modified accordingly. The
difference from van Oostrom's DRSs is that in the latter the notion of {\em
descendant} of any subterm/position of a term is formalized, not only the
notion of residual of redexes. \zurab{Several refined concepts of abstract
rewriting are introduced in~\cite{[Raa.th]}.}


\begin{deff}\em
\label{D.levy.str.}
{\bf (Deterministic Residual Structure)}  A {\em Deterministic Residual
Structure\/} (DRS) is a pair $R=(A, /)$, where $A$ is an ARS
and
$/$ is a {\em 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 {\em 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$ {\em duplicates\/} $v$.
If $v/u=\emptyset$, then $u$ {\em erases\/} $v$.
A redex of $s$
which is not a residual of any $v\subt t$ under $u$ is said to be
\delete{
{\em $u$-new\/} or
}
{\em created\/} by $u$.
The set of residuals of a
redex under any reduction is defined by transitivity.

A {\em development} of a set $U$ of redexes in a term $t$ is a reduction
$P:t\doar $ that only contracts residuals of redexes from $U$; the
development $P$ is {\em complete} if $U/P$, the set of residuals under $P$
of redexes from $U$, is empty $\emptyset$.
Development of $\emptyset$ is
identified with the empty reduction. $U$ will also denote a complete
development of $U\subts t$. The residual relation satisfies the following two
axioms, called {\em Finite Developments (FD)}~\cite{[GLM]} and {\em
acyclicity\/}~(which appears as axiom $(4)$ in~\cite{[Sta]}):

$\bullet$ [FD]  All developments are terminating; all co-initial complete
developments of the same set of redexes end at the same term; and residuals
of a redex under all complete co-initial developments of a set of redexes
are the same.

$\bullet$  [acyclicity] Let $u,v\subt t$, let $u\not= v$, and let
$u/v=\emp$. Then $v/u\not=\emp$.
\ed

The properties of the residual relation are all standard, and we refer
to~\cite{[H.L.],[levy],[le80],[Sta]} for details. Hence,
we assume that, in a DRS $R$,
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 $P/(Q_1+Q_2)=(P/Q_1)/Q_2$, and that {\em L\'evy-equivalence} or {\em
permutation-equivalence} is defined as the smallest relation on co-initial
reductions satisfying: $U+ V/U\leeqv V+U/V$ and $Q\leeqv Q'\,
\Rightarrow \, P+Q+N\leeqv P+Q'+N$, where $U$ and $V$ are complete
developments of redex sets in the same term. Further,
one defines $P\lleq Q$ iff $P/Q=\emptyset$, and
can show that $P\leeqv Q$ iff
$P\lleq Q$ and $Q\lleq P$; and $P\lleq Q$ iff $Q\leeqv P+N$ for some $N$.
The above relations can
equivalently be defined also using Klop's method of commutative diagrams.
We will often use Klop's diagrams in \delete{definitions and} proofs.
The method  is
well described in~\cite{[Kl.CRS],[Bar]}.


\zurab{
Note that [acyclicity] re-introduces some kind of `nesting' relation on
redexes, but we don't even require this relation to be transitive.
}

In practice, we are only interested in {\em stable} DRSs where a given
redex cannot arise from two unrelated sources:

\bd
\cite{[rndrs]} A DRS is {\em stable\/} if the following axiom is satisfied:
\delete{ (see Figure~\ref{berry-stab}):}

$\bullet$ [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 by $u/v$.
\begin{figure}
\begin{diagram}[height=2em,width=2em]
 t      & \rTo^u       & e             & \rTo^w           & {}  \\
 \dTo^v &              &  \dOnto_{v/u}  &                 &      \\
s       & \rOnto_{u/v} & o              & \rOnto_{w/(v/u)}   & {}  \\
\end{diagram}
%\caption{Berry's Stability}\label{berry-stab}
\end{figure}
\ed



The essence of stability is better understood via \Lr{L.disj.red.creat.} below
which expresses the preservation of {\em externality} during redex creation. For
syntactic systems externality is a natural concept relating to overlap between
components of terms involved in reduction steps. In an abstract setting it
expresses the absence of shared (residuals of) redexes.

\bdl{D.ext.reductions.}
(\cite{[rndrs]})
$\bullet$ Let $u\in U\subts t$ and $P:t\doar$. We call $P$ {\em external\/}
to $U$ (resp. $u$) if $P$ does not contract residuals of redexes in $U$
(resp. residuals of $u$).

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

\begin{diagram}[height=1.8em,width=1.8em]
t_0          &\rOnto^{P_i}& & t_i       &\rTo^{u_i}   & t_{i+1} & &\rOnto &{}\\
\dOnto<{Q'_j}&            & &\dTo<{Q_j/P_i}&         & \dOnto & & &     \\
{}       &\rOnto^{P_i/Q_j}& & {}    & \rOnto^{U_{i,j}} & {}     &  &   &{}\\
\dTo<{v_j}   &         & &\dOnto^{V_{i,j}} &             & \dOnto &  & &   \\
{}           &\rOnto      & &  {}       & \rOnto      & {}   & &   &{}\\
\dOnto       &            & &          &             &       & &  &   \\
{}           &        & & {}        &          &  {}   & &   &{}\\
\end{diagram}
\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$.
\zurab{
Note that a reduction $P$ 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$. So, externality is a subtle concept, and neededness
and essentiality notions which we introduce later employ that subtlety.
}

\delete{
\bdl{D.ext.reductions.}
(\cite{[rndrs]})
We call $P:t\doar s$ {\em external} to $Q:t\doar e$ if for every elementary
diagram $D(u,v)$ in a diagram $D(P,Q)$, whatever order of construction of
developments in the elementary diagrams is used, one has $u\not= v$. We
call $P$ external to a set of redexes $F\subts t$ if $P$ doesn't contract
residuals of redexes in $F$ (i.e., iff $P$ is external to the development
$F$). We will say that $P$ is external to $u\subt t$ if it is external to
$\{u\}$.
\ed
}

\bll{L.external.rem.ext.}
(\cite{[rndrs]})
Let $P:t\doar s$ be external to a complete development $N$ of $F\subts t$, in a
DRS, and let $Q:t\doar o$, then $P/Q$ is external to $N/Q$.
\el

\bll{L.disj.red.creat.}
{\bf (Stability Lemma)} (\cite{[rndrs]})
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$.
\el

It is easy to verify that the $\lambda$-calculus~\cite{[levy]}, orthogonal
TRSs~\cite{[H.L.]}, orthogonal higher-order
rewrite systems, such as \cite{[Kl.CRS],[OCRS],[Nip.b]}, and Orthogonal Term
Graph Rewriting Systems (OTGRSs) \cite{[KKSdV]} form DRSs; OTGRSs are
equivalent to Maranget's orthogonal DAG (Directed Acyclic Graph) rewriting
systems, defined via labelled orthogonal TRSs. \zurab{For Higher-Order
Rewriting Systems (HORSs)~\cite{[OR94],[Oos.th]}, which doesn't have a fixed
substitution calculus and thereby are more general than the ones listed above,
checking the DRS axioms need some effort~\cite{[Oos.th]}. All these are
stable, and can be shown so without using any notion of labelling.}

\delete{as can be checked just using an appropriate notion of descendant
which assigns the contractum to the contracted redex, as defined
in~\cite{[OCRS]} for ERSs -- labelling is not necessary. (The descendant
notion defined e.g., in~\cite{[B.K.K.S.]} is essentially the residual
notion, and is not useful for this purpose.)
}

We extend some of the earlier notions to infinite reductions, denoted by
$t\doar\infty$.

\bdl{D.inf.fres.rel.}
$\bullet$  Let $P:t\doar\infty$ and $Q:t\doar s$. Then $P/Q$ is the
reduction whose initial parts are residuals of initial parts of $P$ under
$Q$.

$\bullet$  If $u\subt t$, then $u/P=\emptyset$ if $u/P'=\emptyset$ for some
finite initial part $P'$ of $P$.

$\bullet$  If at least one of co-initial $N$ and $N'$ is infinite, then one
defines $N\lleq N'$ or equivalently $N/N'=\emptyset$ if, for any redex $v$
contracted in $N$,  $v/(N'/N_1)=\emptyset$, where $N=N_1+v+N_2$. $N$ and
$N'$ are L\'evy-equivalent, $N\leeqv N'$, if $N\lleq N'$ and $N'\lleq N$.
(One checks easily that $\lleq$ is a partial order, and $\leeqv$ is an
equivalence relation.)
\ed




\section{Existence of Discretely Needed Redexes}
\label{S.drs.prop.}

\zurab{In this section, we characterise some properties of a redex
with respect to
possible reductions in a DRS.
In particular, we define {\em $P$-needed\/}
redexes, for any reduction $P$, and then prove
existence of $P$-needed redexes for any finite $P$ in a stable DRS.}

Below we use the fact that L\'evy-equivalent reductions $P,Q:t\doar s$ are
{\em Hindley-equivalent}, written $P\hieqv Q$, i.e., for any $u\subt t$,
$u/P=u/Q$. We call this property \emph{CR for residuals}.



\subsection{Discrete Notions of Neededness and Essentiality}

We define {\em $P$-needed}, {\em $P$-essential},
and {\em $P$-erased\/} redexes, for any reduction $P$, and study their
(relative) properties.


\bdl{D.red.need.ess.}
$\bullet$  Let $P:t\doar $ and $u\subt t$, in a DRS. \delete{We call $P$
{\em external\/} to $u$ if $P$ doesn't contract residuals of
$u$~\cite{[ctrs]}.}  We call $u$ {\em erased\/} in $P$ or {\em
$P$-erased\/} if $u/P=\emp$. We say that $P$ {\em discards\/} $u$ if $P$ is
external to $u$ and erases it~\cite{[morn]}.

$\bullet$ We call $u$ {\em $P$-needed\/}, written $NE_P(u,t)$, if there is no
$Q\leeqv P$ that is external to $u$, and call it {\em $P$-unneeded\/},
$UN_P(u,t)$, otherwise. We call $u$ {\em $P$-essential\/}, $ES_P(u,t)$,
if there
is no $Q\leeqv P$ that discards $u$, and call it {\em $P$-inessential\/},
$IE_P(u,t)$, otherwise.

We extend these concepts to reductions co-initial with those containing
$u$ as a redex of one of its terms.

$\bullet$ Let $Q:t\doar$, $P:t\dored{P'}s\doar$, and $u\subt s$. We
say $NE_Q(u,s)$ if $NE_{Q/P'}(u,s)$.
We call $P$ {\em $Q$-needed\/} if so is every redex contracted in $P$.
We call $P$ {\em self-needed\/} if it is $P$-needed.
The other concepts above are extended
in the same way (though self-erasure is not a useful concept).
\ed

It is immediate from \Dr{D.red.need.ess.} that $P$-neededness,
$P$-erasure, and $P$-essentiality do not depend
on the choice of a reduction in the class $\lclas{P}$ of reductions
L\'evy-equivalent to $P$ -- so one can speak of $\lclas{P}$-neededness,
$\lclas{P}$-essentiality and $\lclas{P}$-erasure, respectively.

Note that $P$-needed redexes need not be $P$-erased in a DRS with a
duplicating residual relation.
We show this using an OTRS, an example of a DRS, defined using a rule set
$R=\{f(x)\ar h(x,x),\, g(x)\ar x\}$, with the usual
residual relation, and using subterms to label redexes.
Consider:
\begin{center}
$P:t=f(g(x))\ar h(g(x),g(x))\ar h(x,g(x))$
\end{center}
Here $g(x)\subt t$ is $P$-needed, but not $P$-erased.

Note also that $P$-essential redexes need not be $P$-needed. For:
\begin{center}
$P:u=f(g(x))\ar f(x)$
\end{center}
in $R=\{f(x)\ar x,\,g(x)\ar x\}$, redex $u$
is not $P$-needed , but
it is $P$-essential. However, for the redexes contracted in $P$ (not the
redexes whose residuals are contracted in $P$), $P$-neededness and
$P$-essentiality do coincide:


\bll{L.era.and.ess.im.ne.}
Let $u\subt t\dored{P}$, in a DRS.

(1) If $u$ is $P$-needed, then it is $P$-essential.

(2) If $u$ is $P$-erased and $P$-essential, then it is $P$-needed.

(3) If $P$ contracts a redex $v$, then $v$ is $P$-needed iff it is
$P$-essential.

\bproof
(1) If $u$ is $P$-inessential, then there is $Q\leeqv P$ that discards $u$;
thus $Q$ is external to $u$, and $u$ is $P$-unneeded -- a contradiction.
(2)~Suppose on the contrary that $UN_P(u,t)$, i.e., $\exists Q\leeqv P\!:$
$\,Q$ is external to $u$. Since $u/P=\emp$, we have $u/Q=\emp$, i.e., $Q$
discards $u$ -- a contradiction, since $ES_P(u,t)$.  (3)~It is enough
to consider the case when  $v$ is the first step in $P$.
\suf\ From (1). \nec\ From (2), since $v$ is erased in $P$.
\eproof
\el




%\bll{L.p-nee-p-ess.contr.}




\bcl{C.p-nee-p-ess.contr.}
A reduction $P$ in a DRS  is self-needed iff it is  self-essential.
\ec

\bll{L.char.p-erased.}
Let $u\subt t\dored{P}$. Then $u$ is $P$-erased iff ($\alpha$) every
residual of $u$ along any $Q\leeqv P$ is either $Q$-needed or
$Q$-inessential.

\bproof
\suf\ Let $u$ be $P$-erased, and suppose on the contrary that $u$ doesn't
satisfy ($\alpha$), i.e., there are $Q=Q'+Q''\leeqv P$ and $u'\in u/Q'$
such that $u'$ is $Q''$-unneeded and $Q''$-essential. Hence, there is
$Q^*\leeqv Q''$ that is external to $u'$ (since $u'$ is $Q''$-unneeded) and
$u'/Q^*\not=\emp$ (since  $u'$ is $Q''$-essential). Hence, by CR for
residuals, $u/P=u/(Q'+Q^*)\not=\emp$ -- a contradiction. \nec\  By
induction on the length of $P$. Obviously, $P$ cannot be empty, so let
$P=v+P'$. Since $u$ satisfies ($\alpha$), so does every $v$-residual of
$u$. By the induction assumption, $(u/v)/P'=\emp$. Hence $u/P=\emp$.
\eproof
\el


\delete{
\begin{rem}\em
Proposition 5.1 in~\cite{[morn]}, stating that a redex $u\subt t$ is
$\reg$-inessential iff it is $\reg$-unneeded and $\reg$-erased, for a
regular stable $\reg$, is a corollary of Lemmas~\ref{L.era.and.ess.im.ne.},
\ref{L.era.and.ess.im.ne.}.(1),, and \ref{L.ines.impl,eras.}.
\end{rem}
}


\subsection{Properties of Discrete Neededness and Essentiality}
\delete{\label{S.red.chai.}}


\zurab{We now embark on proving existence of $P$-needed redexes for any
finite $P:t\doar s$ in a stable DRS. The idea of our proof is simple,
and resembles
that for normalizing reductions~\cite{[rndrs]}; proofs are different.
We show that the last step
of $P$ is $P$-needed, and that any $P$-needed redex in a non-initial term
of $P$ is either a residual of such a redex in the preceding term, or is
created by contraction of a $P$-needed redex; therefore the redex in $t$
`responsible' for the last step of $P$ is needed.}


\delete{
When $P$ is infinite, we
show existence of a redex in $u\subt t$ which is responsible for at least
one redex in every term of $P$, and show that at least one such redex is
$P$-needed.
}


\bpl{P.prop.nee.cre.res.}
Let $P:s\doar t\red{u}e\dored{P^*}$, in a
stable DRS.

(1) Let $u$ create $v\subt e$, and let $u$ be $P$-unneeded (resp.
$P$-inessential). Then so is $v$.

(2) Let $v\subt e$ be a $u$-residual of $w\subt t$, and let $w$ be
$P$-unneeded (resp. $P$-inessential). Then so is~$v$.

(3) Let $v$ be $P$-needed (resp. $P$-essential), and let $v\not= u$.
Then $v$ has at least one $u$-residual $v'$, and it is the only
$u$-residual of $v$, then $v'$ is $P$-needed (resp. $P$-essential).

\bproof
(1) If $u$ is $P$-unneeded, then it is $P$-inessential by
\Lr{L.era.and.ess.im.ne.}.(3). Hence there is $Q_t\leeqv u+P^*$ that discards
$u$. By \Lr{L.disj.red.creat.}, $Q_e=Q_t/u$ is external to $v$, and
by \Dr{D.inf.fres.rel.} $Q_e\leeqv P^*$. Hence $v$ is
$P$-unneeded. In order to show that $v$ is $P$-inessential, it is enough to
show that $v/Q_e=\emptyset$. We will show that $v/Q'_e=\emptyset$,
where $Q'_e=Q'_t/u$ and $Q'_t\leq Q_t$ is finite and such that
$u/Q'_t=\emptyset$.
Indeed, if  on the contrary
$v/Q'_e\not=\emptyset$, then by \Lr{L.disj.red.creat.} the redexes in
$v/Q'_e$ must be created by $u/Q'_t$, which is not possible since
$u/Q'_t=\emptyset$.

\begin{diagram}[height=1.8em,width=1.8em]
s   &\rOnto & & t          &\rTo^{u} & e & &\rOnto^{P^*}& P\\
{}  &       & &\dTo<{Q'_t} &         &\dTo>{Q'_e} &\\
{}  &       & & {}         & \rOnto_{\emptyset} & {}     & \\
{}  &       & &\dOnto      &         & \dOnto  & \\
{}  &       & & Q_t        &         & Q_e     &   \\
\end{diagram}

(2) Since $w$ is $P$-unneeded, there is $Q_t\leeqv u+P^*$ that is external to
$w$ (see the picture for (1)).
Hence $u/Q_t=\emptyset$ (since $u/(u+P^*)=\emptyset$) and
$Q_e=Q_t/u\leeqv P^*$ by \Dr{D.inf.fres.rel.}. By
\Lr{L.external.rem.ext.} $Q_e$ is external to $v$. Thus $v$
is $P$-unneeded too. If moreover $w$ is $P$-inessential, then say
$Q_t\leeqv u+P^*$ discards it, and let $Q'_t\leq Q_t$ be finite and such that
$w/Q'_t=\emptyset$. Then
$v/(Q'_t/u)=\emp$ since $Q'_t\hieqv u+Q'_t/u$, i.e., $Q_e$
discards $v$, and $v$ is $P$-inessential.

(3)  If on the contrary $v/u=\emp$, then $P$ would discard $v$, contrary to
$NE_P(v,t)$ (resp. $ES_P(v,t)$). If $v'$ is the only $u$-residual of
$v$ then if $v'$ was $P^*$-unneeded ($P^*$-inessential),
there would be
$Q_e\leeqv P^*$ that is external to $v'$ (resp. that discards $v'$). Then
$u+Q_e$ would be external to (resp. would discard) $v$ -- a contradiction.
\eproof
\ep


\zurab{
We remark that, at this stage, we cannot prove that, in (3), $v$ always
has at least one $P$-needed (resp. $P$-essential) residual. This will be
shown in section~\ref{S.dis.no.}, using the standardization theorem.
}


%\bll{L.inf.punn.crea.punn.}
%\bll{L.inf.res.unn.uness.rema.}
%\bll{L.red.nee.cann.be.eras.}



\delete{
Now we define the notion of {\em redex-chains}, which enable us to trace
back the origins of redexes in earlier terms in a reduction:

\bdl{D.chain.}
let $P:t_0\dored{u_0}t_1\dored{u_1}\doar$ and let $v_i\subt t_i$ be such
that either $v_{i+1}$ is a $u_i$-residual of $v_i$, or $v_i=u_i$ and $u_i$
creates $v_{i+1}$. Then we call the sequence $\Gamma=v_0,v_1,\ldots$ a {\em
chain} in $P$ or a {\em $P$-chain} or a {\em $P$-chain of $v_0$}. We call
$v_j$ a {\em $(P-)$successor\/} of $v_i$ if there is at least one creation
in the chain $v_i, v_{i+1},\ldots, v_j$, i.e., $u_k=v_k$ for at least one
$i\leq k<j$. We call $v_i$ the {\em predecessor\/} of $v_j$ if $v_j$ is a
successor or a residual of $v_i$ (obviously, every redex in $t_j$ has
exactly one predecessor in every $t_i$ with $i<k$). The {\em degree\/} of
$\Gamma$, written $deg(\Gamma)$, is the number of creations in $\Gamma$.
\ed



\bll{L.pred. nee.ess.}
Let $\Gamma$ be a $P$-chain, in a stable DRS, and let $v\in\Gamma$ be
$P$-needed (resp. $P$-essential). Then so is every predecessor of $v$ in
$\Gamma$.

\bproof
By \Pr{P.prop.nee.cre.res.}.(1)-(2).
\eproof
\el



\bll{L.sta.m.ch.sta.}
Let $P:t\doar s$, and let $v\subt s$ be a $P$-successor of $u\subt t$, in a
stable DRS. Then  $u$ is $P$-needed.

\bproof
Let $v$ belong to a $P$-chain $\Gamma$ of $u$ with a positive degree, and
suppose on the contrary that there is $Q\leeqv P$ that is  external to $u$.
Let $P:t\dored{P'}o\red{w}e\dored{P^*}s$, where $w$ is the last member of
$\Gamma$ that is contracted in $P$ and creates the next member of $\Gamma$
(see the diagram). Since $Q$ is external to $u$, $Q'=Q/P'$ is external to
$w$ by \Lr{L.external.rem.ext.} and \Lr{L.disj.red.creat.}. By definition
of $w$, it creates a redex $v'\subt e$ whose residual is $v$. Since
$Q^*=Q/(P'+w)\leeqv P^*$ and therefore $v$ is $Q^*$-residual of $v'$ as
well, we have by \Lr{L.disj.red.creat.} that, along $Q'+w/Q'$, $v$ is
created by $w/Q'$. But this is impossible since $w/Q'=\emptyset$ -- a
contradiction.
\begin{figure}
\begin{diagram}[height=2em,width=2em]
 t    & \rOnto^{P'} & o  & \rTo   &  e    &  \rOnto^{P^*}    &  s     \\
 \dOnto^{Q}&     &  \dOnto^{Q'} &   &     \dOnto^{Q^*}   &   & \dOnto_{\empt} \\
s  & \rOnto_{\empt} & s  & \rOnto_{\empt}  & s &  \rOnto_{\empt} &   s   \\
\end{diagram}
%\caption{Preservation of External Reductions}\label{extern-red}
\end{figure}

\eproof
\el
}


\bll{L.ext.no.le.eqv.}
Let $u\subt t_0\dored{P}t_k$, and let $P$ be external to $u$, in a DRS.
Then $u\not\leeqv P$.

\bproof
Let $P:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_k$. We show that $P/u=\emp$
implies $u/P\not=\emp$ by induction on the number of elementary diagrams in
Klop's diagram $D(u,P)$ of $u$ and $P$. It follows from
\Dr{D.ext.reductions.} that the top and left edges of all sub-diagrams of
$D(u,P)$ are external reductions, therefore the induction principle is
sound. So let $P/u=\emp$. If $\vert P\vert=1$, i.e., $P=v_0$, we have
$u/v_0\not=\emp$ by [acyclicity]. So let $\vert P\vert >1$, let
$P:t_0\dored{Q}t_{k-1}\red{v_{k-1}}t_k$, and let $U=u/Q$ (see the diagram).
By the induction assumption, $U\not=\emp$. So let $U=U'+u'$, where $u'$ is
the last (non-empty) step of $U$, and let $V=v_{k-1}/U'$. Again by the
induction assumption, $u'/V\not=\emp$. Hence $u/P\not=\emp$.

\begin{figure}
\begin{diagram}[height=0.5em,width=2em]
 t_0   & & &  \rOnto^{Q}  & & & t_{k-1}          & \rTo^{v_{k-1}}    & t_k   \\
       & & &             & & &                  &                   &\dOnto \\
       & & &             & & &                  &                   &     \\
       & & &             & & &  \dOnto^{U'}     &                   &      \\
\dTo^u & & &             & & &  {}              &    \rOnto^{V}     &  {}  \\
       & & &             & & &  \dTo^{u'}       &                   &  \dOnto \\
  s    & & & \rOnto^\emp & & &    s             &  \rOnto^\emp      &  s   \\
\end{diagram}
\end{figure}
\eproof
\el




\bll{L.las.st.sel.nee.}
Let $P:t\doar s\red{u}o$, in a DRS. Then $u$ is $P$-needed.

\bproof
By \Lr{L.ext.no.le.eqv.}, there is no $Q:s\doar o$ such that $Q$ is
external to $u$ and $Q\leeqv u$. Hence $u$ is $u$-needed, i.e., $P$-needed.
\eproof
\el


\delete{
We turn to properties of infinite reductions.

\bll{L.inf.chain.}
For any infinite $P:t\doar\infty$ in a DRS, there is at least one $u\subt
t$ that has a chain of infinite degree along $P$.

\bproof
If every redex in $t$ had only chains of finite degrees, then there will be
a term $s$ in $P$ such that in the tail $P'$ of $P$ starting from $s$ there
will not be redex creation, i.e., $P'$ would be an infinite development  --
contradicting [FD].
\eproof
\el





\bll{L.inf.ch.pos.deg.need.}
Let $P:t\doar\infty$ and let $u$ have
an infinite $P$-chain $\Gamma$, in a
stable DRS. Then $ES_P(u,t)$. If moreover $deg(\Gamma)>0$, then
$NE_P(u,t)$.

\bproof
Suppose on the contrary that $IE_P(u,t)$. Then there is a $Q\leeqv P$ that
discards $u$. Hence there is a finite $Q'<Q$ that discards $u$. Thus there
are $P'<P$ and $N'$ such that $Q'+N'\leeqv P'$. Let $\Gamma'$ be the part
of $\Gamma$ corresponding to $P'$. If $deg(\Gamma')=0$, then $\Gamma'$
consists of residuals of $u$, and $Q'$ cannot discard $u$ since
$Q'+N'\leeqv P'$ and $u/P'\not=\emp$; and if $deg(\Gamma')>0$, $Q'$ cannot
discard $u$ since $u$ is $P'$-needed by \Lr{L.sta.m.ch.sta.} -- a
contradiction. Thus $ES_P(u,t)$. Now assume $deg(\Gamma)>0$. Then a
successor $v$ of $u$ in $\Gamma$ is contracted in $P$. As we have already
shown, $ES_P(v,t)$ since $v$ has an infinite chain as well. Hence, by
\Lr{L.era.and.ess.im.ne.}.(3), $v$ is $P$-needed, and $u$ is $P$-needed by
\Lr{L.pred. nee.ess.}.
\eproof
\el



\bll
Let $P:t\doar\infty$ and let $u$ has an infinite $P$-chain $\Gamma$ with
$deg(\Gamma')>0$, in a stable DRS. Then $NE_P(u,t)$.

\bproof
Since $deg(\Gamma)>0$, a successor $v$ of $u$ in $\Gamma$ is contracted in
$P$. By \Lr{L.inf.ch.any.deg.ess.}, $ES_P(v,t)$, since $v$ has an infinite
chain as well. But, by \Lr{L.era.and.ess.im.ne.}.(3), $v$ is $P$-essential iff
it is $P$-needed. Hence, $NE_P(u,t)$ by \Lr{L.pred. nee.ess.}.
\eproof
\el
}


\btl{T.exis.sel.nee.red.fin.cas.}
Let $P:t\doar s$ be a non-empty finite reduction in a stable DRS.
Then $t$ contains a $P$-needed redex.

\bproof
Let $P:t=t_0\red{u_0}t_1\red{u_1}\ldots \red{u_{n-1}}t_n=s$, and let
$v_0,\ldots, v_{n-1}$ be such that $v_i\in t_i$, $v_{n-1}=u_{n-1}$,
and either $v_i\not=u_i$ and $v_{i+1}$ is a $u_i$-residual of $v_i$,
or $v_i=u_i$ and $u_i$ creates $v_{i+1}$. By \Lr{L.las.st.sel.nee.},
$v_{i-1}$ is $P$-needed, and so are all $v_i$ by
\Pr{P.prop.nee.cre.res.}.(1)-(2).
\eproof
\et



\zurab{
Existence of $P$-needed redexes can be studied for infinite reductions
$P$ as well, but as we will demonstrate below, $P$-needed redexes for
infinite $P$ are not as useful as in the case of finite $P$, from the
point of view of Discrete Normalization.
}



\section{Standardization}
\label{S.sta.}

In orthogonal `syntactic' rewrite systems, if a reduction $P:t\doar s$
discards a redex $u\subt t$, then one easily constructs a $Q\leeqv P$ that
discards $u$ and doesn't contract redexes inside $u$ (see
e.g.,~\cite{[ctrs]}), and clearly such a $Q$ discards all redexes in the
arguments of $u$. In DRSs, where we do not have a nesting relation on
redexes, the above property can be approximated by saying that
`$P$-inessential redexes cannot duplicate $P$-essential ones' (obviously,
$P$-inessential redexes cannot erase $P$-essential ones). It follows from
\Lr{L.era.and.ess.im.ne.}.(3) that the [semi-linearity] axiom introduced below
and used essentially in our standardization procedure expresses the above
property of orthogonal rewrite systems, and is a slightly weaker condition.



\bdl{D.sem.lin.dr.}
We call a DRS $R$ {\em semi-linear\/} if it satisfies the following axiom:

$\bullet$ [semi-linearity] Let $P:t\red{u}s\doar$ in $R$. If $u$ is
$P$-unneeded, then $u$ does not duplicate $P$-needed redexes in $t$.
\ed


\delete{
$\bullet$ [semi-linearity] For any $P:t\doar$ in $R$, $P$-inessential
redexes in $t$ cannot duplicate $P$-essential ones.


Using results from~\cite{[ctrs]}, it is not difficult to show that
orthogonal ERSs are semi-linear. We believe that other DRSs mentioned above
are semi-linear as well. Obviously, linear systems are semi-linear too.
%Zurab: However, the axioms from~\cite{[GLM]} don't imply semi-linearity.
%need an example.
}

Below, if not otherwise stated, we only consider semi-linear stable DRSs.
Obviously, linear systems (having a non-duplicating residual relation) are
semi-linear.


\btl{L.qpp.nee.red.exi.}
Let $P:t\doar s$ be a non-empty finite reduction in a stable
semi-linear DRS. Then
$t$ contains a $P$-erased $P$-needed redex; for example, the $P$-needed
redex in $t$ whose residual is contracted first among residuals of
$P$-needed redexes in $t$.

\bproof
Let $P:t=t_0\red{u_0}t_1\red{u_1}\ldots\ar t_n=s$,
and let $u_i$ be the first among
the contracted residuals of $P$-needed redexes in $t_0$. By
Theorem~\ref{T.exis.sel.nee.red.fin.cas.}, $t_0$ contains a $P$-needed
redex,  and at least one residual of each $P$-needed redex in $t_0$ is
contracted in $P$; thus the redex $u_i$ as above exists. Let $u_i$ be the
residual of $v\subt t_0$. By \Pr{P.prop.nee.cre.res.}.(1)-(2), every $u_j$
with $j<i$ is $P$-unneeded. By
[semi-linearity] and \Pr{P.prop.nee.cre.res.}.(3), $u_i$ is the only
residual of $v$ in $t_i$, and is $P$-needed. Hence $v$ is $P$-erased (and
$P$-needed).
\eproof
\et


Note that for any finite $P:t\doar s$, $P$-needed redexes
all of whose
residuals along $P$ remain $P$-needed, are $P$-erased, since $s$ does not
contain $\emp$-needed redexes.




\bdl{D.ess.rel.red.}
(1) Let $P:t\doar $ and $Q\lleq P$. The {\em $P$-needed variant of $Q$},
written $\err{P}{Q}$, is defined as follows: let $v\subt t$ be such that it
is $P$-needed and its residual is contracted in $Q$ first among $P$-needed
residuals of $P$-needed redexes in $t$. Then $\err{P}{Q}=v+\err{P/v}{Q/v}$.
If there is no such a redex in $t$, then $\err{P}{Q}=\emp$.

(2) We call $\err{P}{P}$ the {\em self-needed variant of $P$\/} and denote
it by $SE(P)$.
\ed


Obviously, a reduction $P$ is self-needed iff $SE(P)=P$.


\bll{L.era.lle.}
Let $P,Q:t\doar$, in a DRS. Then $Q$ is $P$-erased iff $Q\lleq P$.

\bproof
Immediate from \Dr{D.red.need.ess.}.
\eproof
\el




\bll{L.pus.qp.ahe.}
Let $Q\lleq P$. Then $\err{P}{Q}$ is a $P$-erased $P$-needed reduction, and
its length coincides with the number of $P$-needed steps in $Q$. Further,
$\err{P}{Q}\lleq Q\lleq P$.

\bproof
Let $Q:t=t_0\dored{Q_i}t_i\red{u_i}t_{i+1}\dored{Q^*_{i+1}}$, and let
$u_{i_0}, u_{i_1},\ldots$ be all the $P$-needed steps in $Q$
($i_0<i_1<\ldots$). Since $u_{i_0}$ is the first $P$-needed step in $Q$, it
follows from \Pr{P.prop.nee.cre.res.}.(1)-(2)
that $u_{i_0}$ is a residual of some $P$-needed redex $v_0\subt t_0$, and
$u_{i_0}$ is the only residual of $v_0$ by [semi-linearity].\footnote{Here
we also use the fact that $Q\lleq P$, so that every finite initial part of
$Q$ can be considered as being an initial part of $P$, up to $\leeqv$, and
\Pr{P.prop.nee.cre.res.}.(1)-(2)
applies; recall that discrete neededness is invariant under $\leeqv$.} Hence
$v_0$ is $P$-erased. Thus $\err{P}{Q}=v_0+\err{P/v_0}{Q/v_0}$ where $v_0$
is $P$-needed and $P$-erased. Similarly, we show that
$SE_P(Q):t_0=s_0\red{v_0}s_1\red{v_1}s_2\doar$, where $u_{i_j}$ is the first
$P'_j$-needed step in $Q'_j=Q/(v_0+v_1+\ldots+v_{j-1})$, where
$P'_j=P/(v_0+v_1+\ldots+v_{j-1})$, and $u_{i_j}$  is the only residual of
some $P$-erased $P$-needed redex $v_j\in s_j$ along $Q'_j$. (Note that
$P_j\leeqv P$, so $P_j$-neededness coincides with $P$-neededness.) Hence
the lemma.

\begin{diagram}[height=1.5em,width=1.5em]
t_0=s_0    &\rOnto^{Q_{i_j}} & & & t_{i_j}   & \rTo^{u_{i_j}}& t_{i_j+1}  &
\rOnto^{Q^*_{i_j+1}} & & &  \,\,\,\,\, Q'_0=Q \\
\dOnto    &            & &  &\dOnto>{\emp} &\\
s_j    &\rOnto       & &  & t_{i_j}   & \rTo^{u_{i_j}}& t_{i_j+1}  &
\rOnto^{Q^*_{i_j+1}}  && &  Q'_j  \\
\dTo<{v_j} &          & &  &\dTo>{u_{i_j}}   &       &   \dOnto>{\emp}  \\
s_{j+1}  &\rOnto     & &  & t_{i_j}   & \rOnto^{\emp}& t_{i_j+1}  &
\rOnto^{Q^*_{i_j+1}}  & & & Q'_{j+1}  \\
\dTo<{v_{j+1}}     &           & &  &           &\\
 {}        &           & {}             &   \\
\end{diagram}
\eproof
\el



\bll{L.se.es.var.le.eq.orig.red.}
If $P$ is finite, then so is $SE(P)$, and $P\leeqv SE(P)$.

\bproof
By \Lr{L.pus.qp.ahe.}, $SE(P)\lleq P$. Let
$P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar t_n$
and let $u_{i_0}, u_{i_1},\ldots,u_{i_{k-1}}$ be all
$P$-needed steps
in $P$ ($i_0<i_1<\ldots$). Then, as
shown in the proof of \Lr{L.pus.qp.ahe.},
$SE(P):t_0=s_0\red{v_0}s_1\red{v_1}s_2\ldots\red{v_{k-1}}s_k$,
where $u_{i_j}$ is the first
$P'_j$-needed step in $P'_j=P/(v_0+v_1+\ldots+v_{j-1})$,
and $u_{i_j}$  is
a residual of $v_j$ along $P'_j$ (see also the above diagram;
take $Q=P$).
Further, $s_k$ does not contain $P/SE(P)$-erased $P/SE(P)$-needed
redexes by \Dr{D.ess.rel.red.}. Hence, by
\Tr{L.qpp.nee.red.exi.}, $P/SE(P)=\emp$. Thus $P\leeqv SE(P)$.
\eproof
\el


The following example shows that if $P$ is infinite, $P\leeqv SE(P)$
need not hold.

\bel{E.we.es.no.add.}
Consider the OTRS $R=\{ r_{1}: f(x)\ar g(h(x)), r_{2}: g(x) \ar f(h(x)),
r_{3}: h(x)\ar a \}$ and the reductions $P: f(x)\ar g(h(x))\ar g(a)\ar
f(h(a))\ar f(a)\ar g(h(a))\ar g(a)\ar\ldots$ and $Q:f(x) \ar g(h(x))\ar
f(h(h(x)))\ar g(h(h(h(x))))\ar\ldots$. Then it is easy to check that
$Q=SE(P)$, but $P/Q\not=\emp$.
\ee



\begin{rem}\em
\zurab{
This should not be understood as that needed reductions are
not useful in the study of transfinite reductions in orthogonal
TRSs~\cite{[K-tra]}. Indeed, it is shown in~\cite{[K-tra]} that,
for an appropriate notion of convergence of infinite reductions,
\emph{strong convergence}, needed-fair reductions do converge
to infinite normal forms. And the
reduction $P$ in \Er{E.we.es.no.add.} is divergent. In~\cite{[K-tra]},
reductions that do not converge (strongly) are considered meaningless,
while we study normalization relative to \emph{any} reduction.
}
\end{rem}


\bc
For any finite $P,Q$, $P\leeqv Q$ iff $SE(P)\leeqv SE(Q)$.
\ec

\delete{
Note that $Q$ in the \Er{E.we.es.no.add.} is not
even cofinal -- we have that $f(x)\ar g(h(x)) \ar g(a)$, but $g(a)$ can not
be reduced to terms in $Q$,  because each term in the graph of $g(a)$
contains an occurrence of $a$.
}


\bll{L.pnn.senee.}
Let $Q$ be $P$-needed and $Q\lleq P$. Then $Q$ is $Q$-needed.

\bproof
Suppose on the contrary that $Q$ has a $Q$-unneeded step, say $u$, and let
$Q=Q'+u+Q''$. By \Lr{L.era.and.ess.im.ne.}.(3), $u$ is $Q$-inessential, i.e.,
there is $N\leeqv u+Q''$ that discards $u$. Let $N'\leq N$ be finite and
discard $u$. Since $Q\lleq P$, it follows that $N\lleq P'$, where
$P'=P/Q'$. Hence $P'\leeqv N'+N''$ for some $N''$. This means that $u$ is
$P'$-inessential, hence $P$-inessential, and is $P$-unneeded by
\Lr{L.era.and.ess.im.ne.}.(1) -- a contradiction.
\eproof
\el

\bcl{C.pnee,sel.}
If $Q\lleq P$, then $SE_P(Q)$ is self-needed, and hence self-essential.

\bproof
By \Lr{L.pus.qp.ahe.}, $SE_P(Q)\lleq P$ and $SE_P(Q)$
is $P$-needed. Hence $SE_P(Q)$ is self-needed by \Lr{L.pnn.senee.}, and is
self-essential by \Cr{C.p-nee-p-ess.contr.}.
\eproof
\ec


It is easy to see that standard reductions, in the sense
of~\cite{[GLM]},
are self-essential. In fact, the notion of self-essential reduction is the
best approximation to the notion of standard reduction for DRSs, and it
captures the essence of standardization in many respects.
Therefore:


\bdl{D.stanndrs.}
We call a reduction in a DRS {\em standard\/} if it is self-essential.
\ed


Before proving the Standardization theorem, we need a simple characterization
of fair reductions.


\bdl{D.cof.str.cof.}
A reduction $P:t_0\ar t_1\ar\ldots$ in a DRS is {\em fair\/} if every redex
in any $t_i$ is $P$-erased~\cite{[Kl.TRS]}. We call $P$ {\em strongly
cofinal\/} if, for any $Q:t_0\doar$, $Q\lleq P$.
\ed


\bll{L.fa.pres.res.}
Let $u\subt t\dored{P}$ in a DRS. If $P$ is fair, then so is $P/u$.

\bproof
Since $P$ is fair, $u/P=\emp$, i.e., $u/P'=\emp$ for some finite $P'$
where $P=P'+P^*$.
Thus $P/u=P'/u+P^*$, and the lemma follows from the fact
that for any $N=N'+N^*$, $N$ is fair iff $N^*$ is also.
\eproof
\el



\bpl{L.fai.is.str.co.con.}
A reduction $P$ in a DRS is fair iff it is strongly cofinal.

\bproof
Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\dored{P^*_{i+1}}$ and
$Q:t_0=s_0\dored{Q_j}s_j\red{v_j}s_{j+1}\dored{Q^*_{j+1}}$. \suf\ We need
to show that $Q\lleq P$. Indeed, by \Lr{L.fa.pres.res.}, $P/Q_j$ is fair
(for all appropriate $j$), and hence $u_j/(P/Q_j)=\emp$, i.e., $Q\lleq P$.
\nec\ If $P$ is strongly cofinal, then $P_k+w_k\lleq P$ for any $w_k\subt
t_k$, i.e., $w_k\lleq P^*_k$. Thus every redex in $P$ is $P$-erased, and
$P$ is fair.
\eproof
\ep



\bd
Let $u\subt t$, in a DRS. We call $u$ {\em inessential\/} if there is
$P:t\doar$ that discards $u$ (i.e., $u$ is $P$-inessential),
and call it {\em essential\/} otherwise.
\ed


\zurab{
For example, consider $R=\{g(x)\ar b,\,h(x)\ar x,\, a\ar c\}$, take
$t=g(h(a))$, and take $Q:t\red{h(a)} g(a)$ and $P:t\red{t}b$. Then $a\subt
t$ is $Q$-essential, but it is inessential since $P$ discards it.
}

\bll{L.ess.ess.w.rt.stcof.re.}
In a DRS, $u\subt t$ is inessential iff it is $P$-inessential
for a strongly cofinal $P:t\doar$.

\bproof
($\Rightarrow)$ Since $u$ is inessential, there is $Q:t\doar s$ that
discards $u$. Hence, for any strongly cofinal $N:s\doar$, $Q+N$ discards
$u$ and is strongly cofinal. Hence $u$ is $P$-inessential (since $P\leeqv
Q+N$). $(\Leftarrow)$ Immediate.
\eproof
\el


\btl{L.fin.self.ese.var.}
{\bf (Standardization)} For any finite reduction $P$ in a stable
semi-linear DRS, $SE(P)$ is a standard reduction L\'evy-equivalent to $P$.
If $P$ is infinite, a standard reduction L\'evy-equivalent to it need not
exist.

\bproof
If $P$ is finite, then $P\leeqv SE(P)$ by \Lr{L.se.es.var.le.eq.orig.red.},
and  $SE(P)$ is self-essential by \Cr{C.pnee,sel.}. Now let $P$ be
infinite, and take $P$ and $Q$ as in \Er{E.we.es.no.add.}.
First note that $P$ is fair, hence is
strongly cofinal by \Pr{L.fai.is.str.co.con.}. Therefore, any
self-essential reduction L\'evy-equivalent to $P$ must be essential by
\Lr{L.ess.ess.w.rt.stcof.re.}, and must be infinite because $P$ is so. But
the argument  of any  redex in $R$ is inessential: the reduction $f(t) \ar
g(h(t)) \ar g(a)$ discards the argument $t$ of the $r_{1}$-redex $f(t)$,
hence  $IE(t,f(t))$;  and  similarly for  $r_{2}$- and $r_{3}$-redexes.
Therefore, $Q$ is the only infinite essential reduction in $R$. And we
already know that $P\not\leeqv Q$.
\eproof
\et





\delete{
\bcl{L.p.nee.p.nee.res.}
Let $u\subt t\dored{P}s$, in a \sls\ DRS, and let $NE_P(u,t)$. Then $P$
contracts at least one $P$-needed residual of $u$.

\bproof
If $P$ doesn't contract $P$-needed residuals of $u$, then $u$ must have a
$\emp$-needed $P$-residual in $s$ -- a contradiction.
\eproof
\ec
}





\section{Discrete Normalization}
\label{S.dis.no.}


This section is entirely devoted to proving the main result of the paper --
the Discrete Normalization Theorem.

\bdl{D.p.q.fair.}
Let $P,Q:t\doar$. We call $Q$ {\em $P$-fair\/} if $Q$ contracts only
$P$-erased redexes, and every $P$-erased redex in any term of $Q$ is erased
in $Q$ as well.    \delete{We call a redex $v\subt s$ {\em erased\/} if it
is erased in a \stc\ reduction starting from~$s$. }
\ed


\bll{L.res.fai.remfair.}
Let $P,Q:t\doar$, let $P=u+P'$, let $Q'=Q/u$, and let $Q$ be $P$-fair. Then
$Q'$ is $P'$-fair (see the diagram).

\bproof
Obviously $Q$ is $P$-fair implies $Q$ is $P$-erased.
By \Dr{D.inf.fres.rel.}, $P\lleq Q$ implies $P'\lleq Q'$. Hence $P'$ is
$Q'$-erased by \Lr{L.era.lle.}. It remains to show that any $P'$-erased
redex $w'$ in some term of $Q'$ is erased in $Q'$ too. Since $u$ is
$P$-erased, it is $Q$-erased by the assumption ($Q$ is $P$-fair). So let
$Q^*\leq Q$ be finite and erase $u$, let $Q=Q^* +Q_1^*$, and let
$Q'^*=Q^*/u$; hence $Q'=Q'^*+Q_1^*$. We can assume that $Q^*$ is chosen so
that $w'$ is in some term of $Q'^*$. Let $W'$ be the set of residuals of
$w'$ in the final term $o$ of $Q'^*$. Since $w'$ is $P'$-erased, so is $W'$
(i.e., $W'/(P'/Q'^*)=\emp$). Since $P/Q^*\leeqv P'/Q'^*$, $W'$ is
$P$-erased too. Since $Q$ is $P$-fair by the assumption, $W'$ is erased in
$Q$ as well, i.e., $W'/Q^*_1=\emp$. Hence $W'$ is erased in $Q'$, and so is
$w'$.

\begin{diagram}[height=1.5em,width=1.5em]
 {}         &\rTo^{u}    & {}             & \rOnto^{P'}&   & \\
\dOnto^{Q^*}  &             &   \dOnto>{Q'^*\ni w'}       &\\
 o         &  \rOnto^{\emptyset}     &     \,\,\, o\supseteq  W'   &   \\
\dOnto<{Q_1^*}     &             &   \dOnto>{Q_1^*}       &\\
 {Q}        &       & {Q'}             &   \\
\end{diagram}

\delete{
by \delete{Hindley-equivalence} $Q^*\leeqv u/(Q_1+v)+Q'^*$, every residual
of $w'$ in $ft(Q'^*)$ is $P'$ erased too.  But $ft(Q'^*)$ is a term in $Q$
too, i.e., $Q'=Q'^*+Q_1^*$, where $Q=Q^*+Q_1^*$; hence every residual of
$w'$ in $ft(Q'^*)$ is erased in $Q_1^*$, hence in $Q'$, since it is erased
in $Q$ (because $Q$ is $P$-fair). Thus $w'$ is erased in $Q'$.

\begin{diagram}[height=1.5em,width=1.5em]
 {}         &\rTo^{u}    & {}             & \rOnto^{P'}&   & \\
\dOnto<{Q_1} &               &\dOnto>{Q'_1} &\\
 {}        & \rOnto        & {}             &  \rOnto^{P'/Q'_1}     &   & \\
\dTo<{v} &             &\dOnto>{v/(u/Q_1)\ni v'}          &\\
 {}        &  \rOnto     & {}             &   \\
\dOnto^{Q^*}  &             &   \dOnto>{Q'^*\ni w'}       &\\
 {}        &  \rOnto^{\emptyset}     & {}             &   \\
\dOnto<{Q_1^*}     &             &   \dOnto>{Q_1^*}       &\\
 {Q}        &       & {Q'}             &   \\
\end{diagram}
}
\eproof
\el


\delete{
\bll{L.one.ext.self.ext.}
Let $P:t\doar s$ be external to $u\subt t$, in a \sls\ DRS. Then, for any
$Q\leeqv P$, $SE(Q)$ is external to $u$.

\bproof
By \Dr{D.ess.rel.red.}, $SE(Q)$ is $Q$-needed. But by
\Pr{P.prop.nee.cre.res.}.(2) all residuals of $u$ along $SE(Q)$ are
$Q$-unneeded. Hence $SE(Q)$ is external to $u$.
\eproof
\el
}

\bll{L.nee.pres.one.ext.red.exis.}
Let $P:t\red{u}t'\dored{P'}s$, let $v\subt t$, let $u\not=v$, and let $v$
be $P$-needed (resp. $P$-essential).  Then $v$ has at least one $P$-needed
(resp. $P$-essential) $u$-residual in $t'$.

\bproof
Suppose $v/u=\{v_1,\ldots,v_k\}$, and suppose on the contrary that
$UN_P(v_i,P')$ (resp. $IE_P(v_i,P')$) for all $1\leq i\leq k$ ($k\geq 1$ by
\Pr{P.prop.nee.cre.res.}.(3)). Thus, for every $i$, there is $P_i\leeqv P'$
that is external to (resp. that discards) $v_i$.
By \Lr{L.pus.qp.ahe.}, $SE(P')$ is $P'$-needed, and by
\Pr{P.prop.nee.cre.res.}.(2) all residuals of $v_i$ along $SE(P')$ are
$P'$-unneeded. Hence $SE(P')$ is external to all $v_i$, and
$u+SE(P')$ is external to $v$ (resp. and discards $v$ since $u+P_i\hieqv
u+P'$) -- a contradiction, since $P\leeqv u+SE(P')$ and $v$ is $P$-needed
(resp. $P$-essential).
\eproof
\el



\bll{L.pres.qp.pnee.}
Let $P:t\red{u} e\doar s$ \delete{be self-needed,} and let $Q:t\doar\infty$
be $P$-erased and $P$-needed. Then $u+Q/u\lleq P$ and it contracts
infinitely many $P$-erased $P$-needed redexes.

\bproof
We have $Q\lleq P$ by \Lr{L.era.lle.}, and $u+Q/u\lleq P$ follows. Let
$Q:t=t_0\red{v_0}t_1\red{v_1}\ldots$, and let
$Q_i:t=t_0\red{v_0}t_1\red{v_1}\ldots\ar t_i$. If $v_i\not\in u/Q_i$, then
it follows from \Lr{L.nee.pres.one.ext.red.exis.} that $v_i$ has at least
one $P$-needed $u/Q_i$-residual, and that $v_i/(u/Q_i)$ contracts at least
one $P$-needed redex. Suppose on the contrary that there is only a finite
number of such $i$. Then there is a $k$ such that
$t_k\red{v_k}t_{k+1}\red{v_{k+1}}\ldots$ is an (infinite)
$u/Q_k$-development. But this is impossible by [FD] -- a contradiction.
\eproof
\el


\btl{T.car.lev.eqv.drs.}
{\bf (Discrete Normalization)}
In semi-linear stable DRSs:

(1) Let $P,Q:t\doar$.  Then $P\leeqv Q$ iff $Q$ is $P$-fair. In particular,
any multi-step reduction $Q:t=t_0\doar t_1\doar\ldots$ that contracts in
parallel all $P$-erased redexes in every $t_i$ is L\'evy-equivalent to $P$.

(2) If  $P$ is finite, then any reduction $t\doar$ that contracts
$P$-erased $P$-needed redexes eventually terminates in a reduction
L\'evy-equivalent to $Q$, even if a finite number of $P$-erased
$P$-unneeded redexes, and only such, are also contracted.
\delete{
(3) If $Q$ contracts only $P$-erased $P$-needed redexes, and every such a
redex is erased in it, then $Q\lleq P$, but $P\leeqv Q$ need not hold when
$P$ is infinite.
}

\bproof
(1) ($\Rightarrow$) Let $P\leeqv Q$. Then $Q/P=\emp$, and $Q$ is $P$-erased
by \Lr{L.era.lle.}. For any $Q'< Q$, $P/Q'\leeqv Q''$, where
$Q:t\dored{Q'}s\dored{Q''}$. Hence any $P$-erased redex $u\subt s$ is
$Q$-erased too, i.e., $Q$ is $P$-fair. ($\Leftarrow$)   $Q/P=\emp$ follows
from \Lr{L.era.lle.}. So we have to show that $P/Q=\emp$. Let $P=u+P'$.
Then since every $P$-erased redex of $Q$ is erased in $Q$, we have that
$u/Q=\emp$.  By \Lr{L.res.fai.remfair.}, $Q'=Q/u$ is $P'$-fair. Hence, we
can show similarly that if $P'=u'+P''$, then $u'/Q'=\emp$, and so on. Thus
$P/Q=\emp$. The rest of (1) is immediate.

(2) Suppose on the contrary that there is a $P$-erased reduction $Q:t\doar
$ that contracts infinitely many $P$-erased $P$-needed redexes. Then, by
Lemmas~\ref{L.pus.qp.ahe.} and \ref{L.pres.qp.pnee.}, there is an infinite
$P$-erased $P$-needed reduction starting from $s$, i.e., an infinite
$\emp$-erased $\emptyset$-needed reduction starting from $s$ -- a
contradiction.
\delete{
(3) $Q\lleq P$ follows from \Lr{L.era.lle.}. \Er{E.we.es.no.add.} is a
counterexample for $P\lleq Q$.
}
\eproof
\et

\delete{
Obviously, the {\em Gross-Knuth\/} strategy which in each multi-step
contracts all the redexes in the term constructs fair, hence strongly
cofinal, reductions. Note also that if $t$ is normalizing, then any
strongly cofinal reduction starting from $t$ is normalizing as well.
Therefore, we have as a corollary the well known result stating that
Gross-Knuth strategy is normalizing. Also, note that if $P$ is a
normalizing reduction, then $P$-neededness is just  neededness,
$P$-neededness coincides with $P$-erased $P$-neededness, and we have the
Normalization Theorem as a corollary.
}


Let us call a reduction $P$ {\em self-neededly fair\/} if no redex in a term
of $P$ has a $P$-needed $P$-erased residual in every subsequent term. Then
it follows
from \Er{E.we.es.no.add.} that even
self-neededly fair $P$-needed $P$-erased reductions need not be
L\'evy-equivalent to $P$. So (1) of \Tr{T.car.lev.eqv.drs.} cannot be
improved by considering self-neededly fair sequential reductions instead of
multi-step reductions.

Finally, note that if the DRS is linear (i.e, non-duplicating), then the
self-needed variant $SE(P)$ of any finite reduction $P$ is an optimal
(i.e., shortest)
reduction L\'evy-equivalent to $P$.  To show this, let $P=u+P'$ be
self-needed, let $Q\leeqv P$, and assume that $P'$ is shortest in
its L\'evy-class. Then $\vert Q/u\vert \leq\vert Q\vert -1$ since exactly
one residual of $u$ is contracted in $Q$, and
$\vert P\vert \leq \vert Q\vert$ follows from the induction assumption.



\section{Denotational Semantics}
\label{S.abs.sem.}

\zurab{This section is new.}

Lisper~\cite{[Lis]} defined semantics for an ARS
$A=(Ter,Red,\ar)$\footnote{More precisely, ARSs used in~\cite{[Lis]}
are Klop's ARSs.} as follows: let ${\cal C}=(C,\sqsubseteq,\bot)$ be
a cpo and let $f:Ter\ar C$ be a \emph{monotone}
function, meaning that $t\ar s$
implies $f(t)\sqsubseteq f(s)$. Then \emph{semantics} of a term
$t\in Ter$ w.r.t. $f$ in $\cal C$ , $S(t,f,\cal C)$, is the set least
upper bounds $\sqcup f(P)$, such that there is no co-initial $Q$
such that $P<_m Q$ and $\sqcup f(P)\sqsubset \sqcup f(Q)$, where,
for any
$P:t\ar t_1\ar t_2\ar\ldots$, $f(P)=f(t), f(t_1),f(t_2),\ldots$,
and $\sqcup f(P)$ denotes the least upper bound of $f(P)$ in
$\cal C$ (the latter always exists by the monotonicity of $f$);
and $P<_m Q$ 
means that every term of $P$ can be reduced to a term in $Q$.  Elements of
$S(t,f,\cal C)$ are \emph{values} of $t$ in $\cal C$, w.r.t. $f$.


The most commonly used cpos as semantics for syntactic rewrite
systems are those of \emph{tree} cpos
${\cal T}=(T^{\infty}_{\bot},\preceq,\bot)$, where $T^{\infty}_{\bot}$
consists of finite and
infinite trees labelled by symbols from the rewrite alphabet and
the distinguished constant symbol $\bot$ which represents
\emph{undefined} or \emph{meaningless} terms; and $\preceq$ is the
ordering induced by $\bot\preceq s$ for any $s\in T^{\infty}_{\bot}$.
The tree cpo was first
defined for Recursive Program Schemes by Nivat~\cite{[Niv]}, and was
later extended to the \lc\ by \Le~\cite{[le76]} (the so called \Le-Longo
trees or Lazy-trees~\cite{[Lon]}) and Barendregt~\cite{[Bar]} (the so
called \emph{B\"ohm} trees); and to TRSs by Boudol~\cite{[Bou]}. In
Nivat's and Boudol's semantics, undefined are terms which cannot
be reduced to a \emph{root stable form} -- a term that cannot
be reduced to a redex. In B\"ohm semantics, $\lambda$-terms not
having a head-normal form (hnf) are considered meaningless, and
\Le\ defines meaningless to be whose $\lambda$-terms that do not
have neither hnfs nor weak hnfs (which are just abstractions
$\lambda x t$). So every notion of meaningless terms yields
corresponding concept of semantic tree. In~\cite{[AKKSV]}, the
authors study axioms on terms sets that yield reasonable concepts
of meaningless terms in (infinitary) TRSs and the \lc.

In~\cite{[Lis]}, an `abstract' description of tree cpos is given as
follows: Let $\pi$ assign a set of positions to terms so that $\pi(t)$
is prefix-closed. Define $f_\pi:T\ar T^{\infty}_{\bot}$ by:
$dom(f_\pi(t))=\bigcap_{t\doar t'}\pi(t')$, and $f_\pi(t)(p)=t(p)$ for all
positions $p\in Dom(f_\pi(t))$, where $t(p)$ is the symbol of $t$
at position $p$. As
observed in~\cite{[Lis]}, the above semantics in tree cpos, with
corresponding notions of undefined reduction $\ar_\bot$,
give the same semantics to RPSs,
\lc, and TRSs as originally defined in~\cite{[Niv],[Bar],[Bou]}, when
$\pi(t)$ is defined as the set of positions of $t$ not below any redex in
$t$; and the \emph{instant} semantics for graph
rewriting systems in Ariola and Arvind~\cite{[AriA]} can also be
recovered in this way.

The above definition of abstract semantics is not suitable for all
known interpretations,
and we generalize it slightly by taking $f$ to be a function from
the set of all reductions in $A$ to $C$. Such an $f$ is
\emph{monotone} if for any reduction $P:t\dored{P'}s\red{u}o$ in $A$,
$f(P')\sqsubseteq f(P)$. We define every $\sqsubseteq$-maximal element
in the set $\{\sqcup f(P)\,\vert\,P:t\doar\}$ to be a value of $t$.
 We will call this semantics the \emph{maximal} semantics.

\Le's reduction space ${\cal L}=(L,\lleq,\emptyset)$, where $L$ is the set
of all \Le-equivalence classes of reductions in a DRS $R$, is also a cpo.
And the interpretation $f$ on reductions in $R$ defined by $f(P)=\lclas{P}$
is obviously monotone. If we take $R=(A,/)$ where terms of $A=(Ter, Red,\ar)$
are (finite) $\lambda$-terms with constant $\bot$; $Red$ is the set of
$\beta$-redex occurrences; and $\ar$ is defined by: $t\red{u}_\beta s$ if
$u\in t$ is a $\beta$-redex having a hnf, and $t\red{u}_\bot s$
otherwise (where $t\red{u}_\bot s$ means that $s$ is obtained from $t$ by
replacing $u$ with $\bot$); and take as the residual relation the one
induced by that of the \lc, then the maximal semantics of $R$ in $\cal L$
(w.r.t. $f$ above) is exactly the B\"ohm semantics. The Nivat, Boudol
and \Le's semantics can be recovered similarly, by taking appropriate $R$
and $\ar_\bot$. It is easy to see that fair (or strongly cofinal)
reductions compute the corresponding values in this case.


Alternatively, we can specify the DRS $R$ as before, except define
all redexes inside meaningless redexes to be meaningless, and consider
only
\emph{meaningful-fair} reductions, i.e., reductions in which no meaningful
redex has a meaningful residual in every subsequent term in the reduction.
It is easy to prove that, in all above four cases, there is (exactly one,
up to $\leeqv$) $\lleq$-minimal meaningful-fair reduction (such reductions
contract only meaningful redexes), and these
reductions can be taken as representations of corresponding semantic trees.
This reductions need not be fair, so differently from the maximal semantics,
not-necessarily fair reductions are used to define denotational semantics,
up to an isomorphism, in this case.


This semantic consideration makes the purpose of the DN theorem clear: it
gives us a characterization of reductions computing the \emph{values}
of a term in a semi-linear stable DRS, where value can be defined in
\emph{any} useful way proposed in the literature (and we are familiar
with) for orthogonal rewrite systems. Further, our DN theorem can be
seen as an investigation into (sequential or multi-step) deterministic
strategies. For example, it is comparable to what Klop calls `relaxing'
strategies in~\cite{[Kl.TRS]}, and is more general. Finally, the discrete
normalization theorem can be considered as a refinement of transfinite
normalization theory, when the latter is restricted to terms with a finite
number of redexes and reductions of lengths at most $\omega$; indeed, the
latter studies only strongly convergent reductions, to which trees not
containing $\bot$ correspond, while we study normalization w.r.t. any
infinite reduction, which, as we have shown, can represent any tree in the
corresponding tree cpo.






\section{Conclusions and Future Work}
\label{S.concl.}

\zurab{This section has changed considerably.}

We have proved an abstract Discrete Normalization theorem which gives an
algorithm for constructing reductions L\'evy-equivalent to a finite or
infinite reduction $P$. The special cases
which have already been studied for syntactic orthogonal systems include
the cases when $P$ is normalizing, cofinal, or fair, and many others.
We introduce a number of concepts and constructs which are
technically interesting in their own rights. For example, we use the
Standardization theorem in~\cite{[ldrs]} to define abstract
\emph{extraction} process for linear stable DRSs and for showing that the
resulting extraction notion of family coincides with the zig-zag family and
does satisfy the family axioms of Deterministic Family
Structures~\cite{[rndrs]}. And our abstract standard reductions play
exactly the same role as left-to-right outside-in standard reductions in
the lambda-calculus~\cite{[le80]},
Interaction Systems~\cite{[AL]}, and orthogonal HRSs~\cite{[Oos]}.

Both the axiomatic approach to the study of syntax of rewriting and other
transition systems and the study of the theory of normalization by
neededness can be continued in many directions, some of which are already
mentioned in related papers~\cite{[ctrs],[rndrs],[morn]}. Here we mention
only very closely related problems.

\delete{
Secondly, from the point of view of axiomatization of syntactic systems, it
seems desirable to elaborate the semi-linearity axiom into smaller axioms
referring to one-step reductions only. This may help to extend our results
to wider classes of stable DRSs (although it already applies to all
orthogonal systems we are familiar with).
}

One could try to develop a theory of normalization relative to
\emph{stable} sets $\Pi$ of finite or infinite reductions which would
unify discrete normalisation
with the finitary relative normalisation of \cite{[rndrs]}. Thus
by taking the set of all $\stab$-normalizing reductions for stable
sets $\stab$ of final
terms, or taking a L\'evy-equivalence class of reductions for $\Pi$,
one would
get the Relative and Discrete Normalization theorems, respectively.
We expect strong connection between the concepts of stability for $\Pi$
(which is to be developed) and that of \emph{interpretations} in semantic
domains (see e.g.,~\cite{[B.L.]}). By extending the results
from~\cite{[morn]} concerning minimal relative normalization to the
infinitary abstract case, we could thereby obtain more general results
concerning minimal (or least) computations in interpretations,
extending those for Recursive Program Schemes in~\cite{[B.L.]}.


Also, we have not addressed here the question of how to find
efficiently $P$-needed $P$-erased redexes which are contracted in
reductions $Q\leeqv P$, and a syntactic theory similar to the strong
sequentiality theory~\cite{[H.L.],[KlMi]} needs to be developed for
discrete normalization, and in general for infinitary relative
normalization as described above.

Finally, development of needed narrowing theory in~\cite{[Ant]}
suggests that the abstract theory of neededness can be extended
to cover narrowing and possibly other proof procedures as well.
Non-deterministic systems must also be considered, and Boudol's work
extending that of Huet and \Le~\cite{[H.L.]} to non-orthogonal TRSs
can be used as the basis.



 \delete{
\begin{akn}
We thank  J.~R.~Kennaway, for useful comments.
\end{akn}
}



\begin{thebibliography}{99}

\delete{
\bibitem[{Abr89}]{[Abr]}
Abramsky S. The lazy lambda calculus. In. D.~Turner, ed. Research topics in
functional programming, addison Wesley, 1989, p.~65-116.

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

\bibitem[{AEH94}]{[Ant]} Antoy S., Echahed R., Hanus M. A needed narrowing
strategy. In: Proc. of the $21^{st}$ ACM Symposium on Principles of
Programming Languages, POPL'94, Portland, Oregon, 1994.


\bibitem[{AnMi94}]{[AnMi]} Antoy S. and Middeldorp A.
A Sequential Reduction Strategy. In  Proc.
of the $4^{th}$ International Conference on Algebraic and Logic
Programming, ALP'94, \delete{Madrid,} Springer LNCS,
vol.~850, p.~168-185, 1994.


\bibitem[{AA95}]{[AriA]}
Ariola Z.M., Arvind.


\bibitem[{AKKSV95}]{[AKKSV]}
Ariola Z.M., Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J.
Syntactic definitions of undefined: on defining the undefined.
In: Proc. of the $2^{nd}$ International Symposium on
Theoretical Aspects of Computer Software, TACS'94,  Springer LNCS,
v.~789, M.~Hagiya, J.~C.~Mitchell, eds. Sendai, 1994, p.~543-554.


\bibitem[{AsLa93}]{[AL]}
Asperti A., Laneve C. Interaction Systems I: The
theory of optimal reductions.  Mathematical Structures in Computer
Science, vol.~11, Cambridge University Press, 1993, p.~1-48.



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


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


\bibitem[{BeL\'e79}]{[B.L.]}
Berry G., L\'evy J.-J. Minimal and optimal computations of recursive
programs. JACM 26, 1979, p.~148-175.


\bibitem[{Bou85}]{[Bou]}
Boudol G. Computational semantics of term rewriting systems.
In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds.
Cambridge Univ. Press, 1985, p.~169-236.


\bibitem[{CuFe58}]{[C.F.]}
Curry H.~B., Feys R. Combinatory Logic. vol.~1, North-Holland, 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[{Gar94}]{[Gar]}
Gardner P. Discovering needed reductions using
type theory.  In: Proc. of the $2^{nd}$ International Symposium on
Theoretical Aspects of Computer Software, TACS'94,  Springer LNCS, v.~789,
M.~Hagiya, J.~C.~Mitchell, eds. Sendai, 1994, p.~555-574.


\bibitem[{GlKh94}]{[ctrs]}
Glauert J.R.W., Khasidashvili Z.  Relative Normalization in
Orthogonal Expression Reduction Systems. In: Proc. of the
$4^{th}$ International workshop on Conditional (and Typed) Term
Rewriting Systems, CTRS'94, Springer LNCS, vol.~968, N.~Dershowitz,
N.~Lindenstrauss, eds. Jerusalem, 1994, p.~144-165.


\bibitem[{GlKh94a}]{[morn]}
Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization
in Expression Reduction Systems. Report SYS-C94-06. University of East
Anglia, Norwich, 1994.
(Available as {\sf ftp://ftp.sys.uea.ac.uk/pub/glauert/MinOpt.ps.gz})

\bibitem[{GlKh96}]{[rndrs]}
Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic
residual structures. In: Proc. of the $19^{th}$ International Colloquium on
Trees in Algebra and Programming, CAAP'96, Springer LNCS, vol.~1059,
H.~Kirchner, ed. 1996,  p.~180-195.


\bibitem[{GLM92}]{[GLM]}
Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract Standardisation
theorem. In: Proc. of the $7^{th}$ Annual IEEE Symposium on Logic in
Computer Science, LICS'92, Santa Cruz, California, IEEE Computer Society
Press, 1992, p.~72-81.


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


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


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


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


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


\bibitem[{Kha88}]{[colog]}
Khasidashvili Z. $\beta$-reductions and $\beta$-developments of
$\lambda$-terms with the least number of steps. In: Proc. of the
International Conference on Computer Logic COLOG'88, Tallinn 1988, Springer
LNCS, v.~417, P.~Martin-L\"of and G.~Mints, eds. 1990, p.~105-111.


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



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


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

\bibitem[{KhGl96a}]{[ldrs]}
Khasidashvili Z., Glauert J.R.W. Zig-zag and extraction families in
linear stable Deterministic Residual Structures. Draft.
(Available as {\sf ftp://ftp.sys.uea.ac.uk/pub/zurab/LinZig.ps.gz})


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


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

\bibitem[{KlMi90}]{[KlMi]}
Klop J.W., Middeldorp A. Sequentiality in Orthogonal Term Rewriting
Systems. Journal of Symbolic Computation 12:161-195, 1991.


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


\bibitem[{L\'ev76}]{[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[{L\'ev78}]{[levy]}
L\'evy J.-J. R\'eductions correctes et optimales dans le
lambda-calcul, Th\`ese de l'Universit\'e de Paris VII, 1978.


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

\bibitem[{Lis96}]{[Lis]}
Lisper B. Computing in unpredictable environments: semantics, reduction
strategies, and program transformations. In: Proc. of the $19^{th}$
International Colloquium on Trees in Algebra and Programming, CAAP'96,
Springer LNCS, vol.~1059,  H.~Kirchner, ed. 1996,  p.~165-179.


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


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


\bibitem[{Nip93}]{[Nip.b]}
 Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc.
of the $1^{st}$ International Conference on Typed Lambda Calculus and
Applications, TLCA'93, Springer LNCS, vol.~664, Bazem M., Groote J.F., eds.
Utrecht, 1993, p.~306-317.


\bibitem[{Niv75}]{[Niv]}
Nivat M. On the interpretation of recursive polyadic program schemes.
Symposia Mathematica, 15:255-281, 1975.


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


\bibitem[{Oos94}]{[Oos.th]}
Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D.
Thesis, Free University of Amsterdam, 1994.

\bibitem[{Oos96}]{[Oos]}
Van Oostrom V. Higher order families. To appear in
RTA'96.

\bibitem[{OR94}]{[OR94]}
Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the
higher-order case. In: Proc. of the $3^{rd}$ International Conference on
Logical Foundations of Computer Science, `Logic at St.~Petersburg',
LFCS'94, Springer LNCS, vol.~813, Nerode A., Matiyasevich Yu.~V. eds.
St.~Petersburg, 1994. p.~379-392.


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


\bibitem[{SeRa93}]{[SeRa]}
Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond
Strong Sequentiality. Information and Computation, 104(1):78-109, 1993.

\bibitem[{Sta89}]{[Sta]}
Stark E.~W. Concurrent transition systems. Theoretical Computer Science,
64(3):221-270, 1989.


\delete{
\bibitem[{Win80}]{[Win]}
Winskel G. Events in Computation. Ph.D. Thesis, University of Edinburgh, 1980.
}
\end{thebibliography}
\end{document}



