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

\begin{document}

\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt


\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
\thanks{This work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300}
}
\maketitle




\newcommand{\delete}[1]{} % Comment out text.  
\newcommand{\suppress}[1]{} % Comment out text.  
\newcommand{\john}[1]{\{{\bf John:\sf #1}\}} % Highlight text.
%\newcommand{\zurab}[1]{{\bf\sf #1}} % Highlight text.
\newcommand{\zurab}[1]{#1} % Highlight text.

%\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}{\leq_L}
%\newcommand{\lles}{<_L}
\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}
\newcommand{\Lence}{L\'evy-equivalence}
\newcommand{\Lent}{L\'evy-equivalent}

 
\begin{abstract}
We prove a version of the \emph{Standardization Theorem} and the 
\emph{Discrete Normalization Theorem} in  \emph{stable 
Deterministic Residual Structures}, Abstract Reduction 
Systems with axiomatized notions of {\em residual\/}, which model 
orthogonal rewrite systems. The latter theorem gives a 
strategy for construction 
of reductions L\'evy-equivalent (or permutation-equi\-va\-lent) to a given, 
finite or infinite, \emph{regular} (or \emph{semi-linear}) reduction, 
based on the \emph{neededness} concept of 
Huet and L\'evy. This and other results of this paper add to the 
understanding of L\'evy-equivalence of reductions, and consequently, 
L\'evy's reduction space. \delete{The importance of the latter is already well-understood, and we substantiate it further by} We demonstrate
how elements of this space can be used to give denotational 
semantics to known functional languages in an abstract manner.  
\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, the \emph{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. This seminal work has been extended in many directions.


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. Kennaway and Sleep~\cite{[K.S.]} generalized the needed strategy to orthogonal Combinatory Reduction systems (CRSs) of Klop~\cite{[Kl.CRS]}. 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, the {\em
essential\/} strategy, for the $\lambda$-calculus~\cite{[colog]}, OTRSs \cite{[rta]}, and Orthogonal Expression Reduction Systems (OERS)~\cite{[caap]}, a form of higher-order rewriting similar to Klop's CRSs 
(which subsumes Term Rewriting and the $\lambda$-calculus)~\cite{[OCRS]}.
Sekar and Ramakrishnan~\cite{[SeRa]} study a normalizing strategy which in
each multi-step contracts a {\em necessary\/} set of redexes.
A different approach to normalization is developed in 
Kennaway~\cite{[Kenn]} and in
Antoy and Middeldorp~\cite{[AnMi]}. Antoy et al.~\cite{[Ant]} designed a needed
narrowing strategy.
Gardner~\cite{[Gar]} described a {\em complete\/} way of encoding
neededness information using a type assignment system, in the \lc.
Kennaway et al.~\cite{[K-tra]} studied needed strategies for infinitary OTRSs.

In~\cite{[ctrs]}, the present authors found     
natural conditions on a set $\stab$ of terms, in an OERS, 
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.   


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),
which 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. They proved the RN theorem for {\em
stable\/} DRS, for {\em regular\/} 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$ (which consists of terms to which $s$ is reducible) is
stable and {\em regular}, then the task can be reduced to
construction of a {\em minimal\/}, or rather a \emph{least} 
(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$-least -- we have $u\not\lleq v$, $v\not\lleq u$, and $u\not\leeqv
v$. 

 
A constructive approach is to develop a neededness theory relative to {\em
particular\/} reductions $P:t\doar s$ (constructed according to some strategy), 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.

 
In this paper we indeed develop a neededness theory relative 
to particular \emph{semi-linear}, or \emph{regular},
reductions, which enables us to characterize 
reductions in $\lclas{P}$ for any such
reduction $P:t\doar$, finite or infinite, in stable DRSs. (By an `infinite' reduction we mean a reduction of  length $\omega$.) 
We obtain two main 
results: the \emph{Standardization Theorem}, and the \emph{Discrete 
Normalization Theorem}. The first states that every finite semi-linear reduction 
$P$ can, in some canonical way, be transformed 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$. We also show
 that for infinite semi-linear
reductions $P$, standard reductions \Le-equivalent to $P$ need not exist. 
This concept of standardization is the best approximation to the 
outside-in left-to-right concept of 
standardization~\cite{[Bar],[Kl.CRS]}, since we do not 
have any nesting reduction imposed on redexes, unlike
ARSs of~\cite{[GLM]}, and there is no concept of `left' or `right' 
occurrences in DRSs. However, our standard 
reductions can be used successfully as canonical
representatives in their \Le-equivalence classes, without being unique representatives. The Discrete Normalization (DN)
theorem states that for any $P$, 
repeated simultaneous contraction of all 
$P$-erased redexes yields a reduction in $\lclas{P}$, and 
if $P$ is semi-linear and finite, then contraction of \emph{$P$-needed 
$P$-erased} redexes eventually terminates by constructing 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 does not have residuals in some later 
term of $P$. $P$ is semi-linear if its $P$-unneeded steps do not duplicate $P$-needed redexes. In orthogonal (acyclic) syntactic rewrite systems, all reductions are semi-linear.


Since every 
functional programming language is given by a (very often orthogonal) 
syntactic rewrite system $R$ and a \emph{deterministic} strategy $F$ 
(e.g. the lazy, call-by-name, and several eager strategies in the \lc), 
the \emph{value} of a term (program) $t$ is defined via its computation 
according to $F$. In semantics, values of 
terms are usually defined via some kind of finite or infinite trees, such as 
B\"ohm-trees~\cite{[Bar]},
constructed from symbols from the alphabet and a special constant 
$\bot$ to denote \emph{undefined} (in some sense) terms. The 
strategies $F$ compute these trees.  
So, our DN theorem characterizes computations of a term which 
converge to its value, where value can be defined in various 
ways. We will describe an abstract approach to semantics of 
orthogonal rewrite systems, showing how the conventional 
tree semantics of such 
systems can be recovered without any assumption of syntax, using 
L\'evy's reduction space which we study here.



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.  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.}. More details can be found in~\cite{[dndrs-rep]}.



\section{Deterministic Residual Structures}


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

A definition and a survey of results about ARSs can be found
in~\cite{[Kl.TRS]}. Our definition is slightly different, and 
follows that of Hindley~\cite{[Hin]}. 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\mapsto (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 $\mapsto(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$. (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+Q$ denotes the concatenation of $P$ and $Q$. $\,\,$ $P\leq Q$ denotes
that $P$ is an initial part of $Q$. 
\delete{
$\,\,\,\emptyset_t$ denotes the empty
reduction starting from $t$.
$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 descend from Stark's 
{\em Determinate Concurrent Transition
Systems} (DCTSs) \cite{[Sta]} and 
{\em Abstract Reduction Systems} of Gonthier et
al.~\cite{[GLM]}. Unlike DCTSs, the residual relation in DRSs may be 
duplicating, and unlike ARSs of~\cite{[GLM]},  we do
not have a nesting relation on redexes.  
Several refined concepts of abstract rewriting are studied in~\cite{[Oos.th],[Mel],[Raa.th]}.
DRS are intended to model all orthogonal term and graph 
rewrite systems, both first and higher-order, such as  \cite{[le80],[H.L.],[Kl.CRS],[OCRS],[Nip.b],[Lam],[Kath],[SPE],[Oos.th],[AL2],[Raa.th]}, 
and other conflict-free transition systems with a reasonable level of abstraction, while say ARSs of~\cite{[GLM]}
do not cover e.g., orthogonal term graph rewriting systems~\cite{[SPE]}.

 

\begin{deff}\em
\label{D.levy.str.}
(\cite{[rndrs]}) {\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

Note that [acyclicity] re-introduces some kind of `nesting' relation on 
redexes, but we do not even require this relation to be transitive.

As in~\cite{[le80],[H.L.],[Sta]},
the residual relation on redexes in a DRS $R$ is extended
to all co-initial finite 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 {\em L\'evy-} or {\em
permutation-equi\-va\-lence} 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$.
Intuitively, $P\leeqv Q$ means that $P$ can be obtained from $Q$ by a number of permutations of adjacent steps, therefore `$Q$ and $P$ do the same work'; and $P\lleq Q$ means that $P$ does less work than $Q$, the difference being $Q/P$, so  $P+Q/P\leeqv Q$. 
Unlike ~\cite{[le80],[H.L.]}, we do not consider complete developments of sets of residuals of a redex as multi-steps, so  $P/Q$ is only unique up to the choice of particular complete developments of such sets. (However, $P/Q$ is defined more precisely than up to $\leeqv$.) The above relations can
equivalently be defined also using Klop's method of commutative 
diagrams~\cite{[Kl.CRS],[Bar]}.
We will often use Klop's diagrams in proofs. 
 


\Le-equivalence extends to infinite reductions, denoted by
$t\doar\infty$, as follows. First, for any $u\subt t\dored{P}$, define $u/P=\emp$ if $u/P'=\emp$ for a finite initial part $P'$ of $P$. Now, for any $P,Q:t\doar$, define $P/Q=\emp$, or equivalently $P\lleq Q$, if for any redex $v$ contracted in $P$, say $P=P'+v+P''$, $v/(Q/P')=\emp$; and define $P\leeqv Q$ iff $P\lleq Q$ and $Q\lleq P$. $P/Q$ is only defined for finite $Q$, as the
reduction whose initial parts are residuals of initial parts of $P$ under~$Q$. 


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

\bd
\cite{[rndrs]} A DRS is \emph{stable}, SDRS, if the following axiom is satisfied: 
 
$\bullet$ [stability] Let $t\red{u}e$,
$t\red{v}s$, $u\not=v$, and let $u$ create $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$. 
\ed

\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}
}

 


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} {}\\
\dOnto<{Q_j}&            & &\dTo<{Q_j/P_i}&         & \dOnto     \\
s_j     &\rOnto^{P_i/Q_j}& & {}    & \rOnto^{U_{i,j}} & {}   \\
\dTo<{v_j}   &         & &\dOnto^{V_{i,j}} &             &  \dOnto   \\
s_{j+1}      &\rOnto      & &  {}       & \rOnto      & {}   \\
\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$. 
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)\}$.  

 

\bll{L.external.rem.ext.}
(\cite{[rndrs],[rndrs-rep]})
Let $P:t\doar s$ be external to a complete development $N$ of a set of redexes
 $U\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

As with the Stability Lemma, the following lemma extends the [acyclicity] property from one step external reductions to arbitrary finite external reductions.


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


 

 


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

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.

\delete{
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. 
We call $u$ {\em erased\/} in $P$ or {\em $P$-erased\/} if $u/P=\emp$, 
or equivalently, if $u/Q=\emp$ for any $Q\leeqv P$. 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.
\ed


Clearly, $P$-neededness, erasure, and essentiality do not depend
on the choice of a reduction in $\lclas{P}=\{Q\,\vert\,Q\leeqv P\}$. 
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: $P:t=f(g(x))\ar h(g(x),g(x))\ar h(x,g(x))$
Here $g(x)\subt t$ is $P$-needed, but not $P$-erased. 
Note also that $P$-essential redexes need not be $P$-needed. For:
$P:u=f(g(x))\ar f(x)$ 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, but the converse need not hold.

(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
Easy consequence of \Dr{D.red.need.ess.}. (Or see~\cite{[dndrs-rep]}.)
\eproof
\el



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


\delete{
It is easy to show that if $u\subt t\dored{P}$, then $u$ is $P$-erased 
iff every residual of $u$ along any $Q\leeqv P$ is either $Q$-needed or
$Q$-inessential (see~\cite{[dndrs-rep]}).
}
  

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


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]}.
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 $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 $UN_P(u,t)$. Then so is $v$.

(2) Let $UN_P(w,t)$ and let $v\subt e$ be its $u$-residual. Then $UN_P(v,e)$.

(3) Let $NE_P(v,t)$, and let $v\not= u$. 
Then $v$ has at least one $u$-residual $v'$, and if it is the only
$u$-residual of $v$, then $NE_P(v',e)$.

\bproof
(1) By \Lr{L.era.and.ess.im.ne.}.(3), $UN_P(u,t)\Rightarrow IE_P(u,t)$. 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$. Further, 
 $Q_e\leeqv P^*$. Hence $UN_P(v,e)$.
\begin{diagram}[height=1.8em,width=1.8em]
s   &\rOnto & & t          &\rTo^{u} & e & &\rOnto^{P^*}& P\\
{}  &       & &\dTo<{Q_t} &         &\dTo>{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$).  Further,
$Q_e=Q_t/u\leeqv P^*$. By
\Lr{L.external.rem.ext.} $Q_e$ is external to $v$. Thus $UN_P(v,e)$. 
 

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


The above proposition, as well as \Lr{L.nee.pres.one.ext.red.exis.}, is valid for $P$-(un)neededness replaced by $P$-(in)essentiality. We omit 
proofs (to be found in~\cite{[dndrs-rep]}) since 
the corresponding statements are 
not needed for the main results of this paper.

  
 

\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.lem.mult.}, 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


 

\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). Thus $v_0\subt t$ is $P$-needed.
\eproof 
\et

 
 

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



In orthogonal acyclic `syntactic' rewrite systems, if a redex $u$ erases or duplicates another redex $v$, then $v$ is `below' $u$, and $v$ cannot duplicate or erase $u$. Therefore, 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 does not 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).  We will only need the following slightly weaker (by \Lr{L.era.and.ess.im.ne.}) property:


\bdl{D.reg.red.}
We call $P:t\doar$, or equivalently $\lclas{P}$, \emph{regular} or \emph{semi-linear} if, for any $Q\leeqv P$, $P$-unneeded steps of $Q$ do not duplicate $P$-needed redexes.
\ed


Note that our [acyclicity] axiom is too weak to exclude irregular reductions from SDRSs. Consider simply the ARS given by the graph of a term $t$ containing two redexes $t\red{u}o$ and $t\red{v}s$, such that $v/u=\emp, u/v=\{u_1,u_2\}$, and contraction of $u_1$ and $u_2$ in either order 
yields $o$. Then, for $P=u$, $NE_P(u,t)$, $UN_P(v,t)$, but $v$ duplicates~$u$.


\suppress{
Below, unless otherwise stated, we only consider regular reductions in~SDRSs.
}


\bll{L.tai.reg.reg.}
Let $P$ be regular and let $Q\lleq P$, in a DRs. Then $P/Q$ is regular.

\bproof
Immediate, since for any redex in $\lclas{P/Q}$, $P$- and $P/Q$-neededness coincide.
\eproof
\el


\btl{L.qpp.nee.red.exi.}
Let $P:t\doar s$ be a non-empty regular reduction in a stable 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
regularity of $P$ 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 (canonical) 
$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

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


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

\bproof
Let $Q: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 regularity of $P$.\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.} 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 $P$-erased $P$-needed redex $v_j\in s_j$ along $Q'_j$ (see the figure).
(Note that
$P'_j\leeqv P$, so $P'_j$-neededness coincides with $P$-neededness.) Hence
$\err{P}{Q}\lleq Q$. \suppress{and the lemma follows.}

\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

\delete{
\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), 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{[Bar],[H.L.],[Kl.CRS],[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 (see~\cite{[ldrs]} for the use of self-essential standard reductions in an abstract optimality theory).
Therefore:


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


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

\bproof
By \Lr{L.pus.qp.ahe.}, $SE(P)\lleq P$ and is finite. Let 
$P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar t_n$ 
and $u_{i_0},\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}\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 diagram for \Lr{L.pus.qp.ahe.};  take $Q=P$).
Further, $s_k$ does not contain $P/SE(P)$-erased $P/SE(P)$-needed 
redexes by \Dr{D.ess.rel.red.}. By \Lr{L.tai.reg.reg.} and \Lr{L.pus.qp.ahe.}, 
$P/SE(P)$ is regular. By
\Tr{L.qpp.nee.red.exi.}, $P/SE(P)=\emp$, i.e., $P\leeqv SE(P)$. 
Hence $SE(P)$ is self-needed by \Lr{L.pus.qp.ahe.}, 
thus self-essential by \Cr{C.p-nee-p-ess.contr.}.
\eproof
\et

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

The following example shows that if $P$ is infinite, $P\leeqv SE(P)$ 
need not hold. Consider the OTRS $R=\{f(x)\ar g(h(x)), g(x) \ar f(h(x)),
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)$, it is the only $P$-essential reduction, but $P/Q\not=\emp$. 


This should not be understood as implying that needed reductions are 
not useful in the study of transfinite reductions in  
OTRSs~\cite{[K-tra]} -- needed-fair 
reductions \emph{strongly converge}  to infinite normal forms. The 
reduction $P$ above is divergent. In~\cite{[K-tra]},
reductions that do not converge strongly are considered meaningless,
while here we study normalization relative to \emph{any} reduction.
 
 

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


This section is devoted to proving the main result of the paper --
the Discrete Normalization Theorem. First a simple lemma, which is immediate from \Dr{D.red.need.ess.}.

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


\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.
\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.
Further, $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$). 
\delete{by CR for residuals.} 
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'}&   & P \\
\dOnto^{Q^*}  &             &   \dOnto>{Q'^*\ni w'}       &\\
 o         &  \rOnto^{\emptyset}     &     \,\,\, o\supseteq  W'   &   \\
\dOnto<{Q_1^*}     &             &   \dOnto>{Q_1^*}       &\\
 {Q}        &       & {Q'}             &   \\
\end{diagram}
\eproof
\el 


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

\bproof
Let $v/u=\{v_1,\ldots,v_k\}$, and suppose on the contrary that
$UN_P(v_i,P')$ for all $i=1,\ldots,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 $v_i$. $P'$ is regular by \Lr{L.tai.reg.reg.}. Hence,
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$, contradiction, since $P\leeqv u+SE(P')$ 
by the Standardization theorem, and $NE_P(v,t)$.  
\eproof
\el



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

\bproof
By \Lr{L.era.lle.}, $Q\lleq P$, hence $u+Q/u\lleq P$. Let
$Q:t=t_0\red{v_0}t_1\red{v_1}\ldots$ and 
$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
by \Lr{L.nee.pres.one.ext.red.exis.} $v_i$ has at least
one $P$-needed $u/Q_i$-residual, and $v_i/(u/Q_i)$ contracts at least
one $P$-needed redex. Suppose on the contrary that there are
 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, contradiction.
\delete{
\begin{diagram}[height=1.8em,width=1.8em]
t            &\rTo^{u}    & & e      &\rOnto     & s     \\
\dOnto<{Q_i} &            & &\dOnto           &         &       \\
t_i          &\rOnto^{u/Q_i}& & {}    & \rOnto         & {}   \\
\dTo<{v_i}   &           & &\dOnto_{v_i/(u/Q_i)} &             &   \\
t_{i+1}      &\rOnto     & &  {}       &           & {}  \\
\dOnto       &           & & \dOnto  &             &         \\
Q            &           & & Q/u        &          &  {}    \\
\end{diagram}
}
\eproof
\el


\btl{T.car.lev.eqv.drs.}
{\bf (Discrete Normalization)}  Let $P:t\doar$, in a stable DRS.

(1) $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 and semi-linear, then any reduction $t\doar$ that contracts
$P$-erased $P$-needed redexes eventually terminates;  the resulting reduction is
L\'evy-equivalent to $P$, even if a finite number of $P$-erased
$P$-unneeded redexes, and only such, are also contracted.

\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$. \suppress{The rest of (1) is immediate.}

(2) Let $P:t\red{u}o\doar s$. Suppose \suppress{on the contrary that} 
there is 
a $P$-erased reduction $Q:t\doar$ that contracts infinitely many 
$P$-needed redexes. By \Lr{L.pus.qp.ahe.} $SE_P(Q)$ is an infinite $P$-needed $P$-erased reduction, and by \Lr{L.pres.qp.pnee.}, 
$SE_P(Q)/u$ is a $P$-erased reduction with infinitely many $P$-needed steps, starting from $o$.
Similarly, one shows that there is an infinite $P$-erased $P$-needed, i.e., $\emp$-erased $\emptyset$-needed, reduction starting from $s$, 
contradiction.
\eproof
\et

 
\delete{
Finite standard reductions are not unique in their \Lence\ classes, but the DN theorem implies that there are only a finite number of them in every class. Further, since our standardization concept is the most liberal for acyclic orthogonal systems known in the literature, the DN theorem also implies termination of standardization algorithms (which transform finite reductions into standard ones) for such systems~\cite{[Bar],[H.L.],[Kl.CRS],[GLM],[Oos]}.
}


The DN theorem implies that $\lclas{P}$ contains only a finite number of standard reductions, for any finite semi-linear $P$. It also implies 
termination of known standardization algorithms (which transform finite 
reductions into standard ones) ~\cite{[Bar],[H.L.],[Kl.CRS],[GLM],[Oos]},
since our standardization concept is the most liberal one known in the literature.


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 the example demonstrating failure of standardization for 
infinite reductions 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 allowing self-neededly fair 
sequential reductions instead of
multi-step reductions.

Finally, note that, in a non-duplicating SDRS, for any finite 
semi-linear $P$, $SE(P)$ a shortest 
reduction in $\lclas{P}$.  To show this, let $SE(P)=u+P'$, $Q\leeqv P$,
and assume that $P'$ is shortest in $\lclas{P'}$.
Then $\vert Q/u\vert \leq\vert Q\vert -1$ since exactly
one residual of $u$ is contracted in $Q$, and
$\vert SE(P)\vert \leq \vert Q\vert$ follows from the induction assumption $\len{P'}\leq \len{Q/u}$.



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


Lisper~\cite{[Lis]} defined semantics for an ARS 
$A=(Ter,Red,\ar)$\footnote{More precisely, ARSs used in~\cite{[Lis]} 
are Klop's ARSs~\cite{[Kl.TRS]}.} 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 of 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$; 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],[A.O.]}) and Barendregt~\cite{[Bar]} (the
\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 
L\'evy defines meaningless to be $\lambda$-terms that do not 
have neither hnfs nor weak hnfs (which are simply abstractions 
$\lambda x t$). Reasonable concepts 
of meaningless terms in (infinitary) TRSs and the \lc\ are studied in~\cite{[KOV]}.


\delete{
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.  
}

  
Lisper's definition of abstract semantics allows one to describe all the above tree semantics, but 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)$ in $\cal C$. So the information increases 
(w.r.t. $\sqsubseteq$, in $\cal C$) as the 
computation progresses, and the whole history of the computation is taken 
into account. We define every $\sqsubseteq$-maximal element 
in the set $\{\sqcup f(P)\,\vert\,P:t\doar\}$ (which need not be 
$\sqsubseteq$-maximal in $\cal C$) to be a \emph{value} of $t$.
 We will call this semantics the \emph{maximal} semantics.

\Le's reduction space ${\cal L}=(L,\lleq)$, where $L$ is the set 
of all \Le-equivalence classes of reductions in a DRS $R$, is also a cpo
(the bottom element is irrelevant).
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 of the \lc. The Nivat, 
Boudol 
and \Le's semantics can be recovered similarly, by taking appropriate $R$
and $\ar_\bot$. 
\delete{It is easy to see that fair reductions compute the corresponding 
values in this case.
}
 


\delete{
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 all above four cases, there is (exactly one,
up to $\leeqv$) $\lleq$-minimal meaningful-fair reduction starting from a 
term $t$ (such reductions contract only meaningful redexes), and these 
reductions can be taken as representations of corresponding semantic trees. 
}


Alternatively, we can define 
all redexes inside meaningless redexes to be meaningless, and consider 
only ordinary \emph{meaningful-fair} reductions, i.e., reductions 
without $\bot$-steps in which no meaningful
redex has a meaningful residual in every subsequent term.
In all above four cases, there is (exactly one,
up to $\leeqv$) $\lleq$-minimal meaningful-fair reduction starting from a 
term $t$ (such reductions contract only meaningful redexes), and these 
reductions can be taken as representations of corresponding semantic trees. 


Note that,  unlike the maximal semantics, 
not-necessarily fair reductions are used to define denotational 
semantics in the latter case. And the DN theorem gives a characterization 
of reductions computing the values of terms in all the above cases.
 

\delete{
This reductions need not be fair, so unlike the maximal semantics, 
not-necessarily fair reductions are used to define denotational semantics, 
in this case.
}




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


We have proven an abstract Discrete Normalization theorem. It gives a
strategy for constructing reductions L\'evy-equivalent to a finite or
infinite reduction $P$ (which need not be normalizing or fair). 
We introduced a number of concepts and constructs, such as standardization,
which are technically interesting in their own rights. 


We have not addressed here the question of how to find
efficiently discretely needed redexes, and a syntactic theory 
similar to the strong
sequentiality theory~\cite{[H.L.],[KlMi]} needs to be developed for
discrete and relative normalization.    


One could try to develop a theory of normalization relative to 
\emph{regular stable} sets $\Pi$ of 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 regular stable 
sets $\stab$ of final
terms, or taking a L\'evy-equivalence class of regular reductions for $\Pi$, 
one would get the RN and DN theorems, respectively. 
 
Finally, development of a needed narrowing theory in~\cite{[Ant]} 
suggests that the abstract theory of neededness can be extended 
to cover narrowing and possibly other proof procedures. 
Non-deterministic systems must also be considered, and 
Boudol's work~\cite{[Bou]} 
extending \cite{[H.L.]} to non-orthogonal TRSs
can be used as the basis.

\vspace{.1in}
 
\begin{akn} 
We thank  J.R. Kennaway, V. Van Oostrom and M.R. Sleep for useful comments. The diagrams were drawn using P.~Taylor's diagram package.
\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[{AbOn93}]{[A.O.]}
Abramsky S., Ong C.-H. L. Full abstraction in the lazy lambda calculus. Inf.\& Comp., 105:159-267, 1993.


\bibitem[{AEH94}]{[Ant]} 
Antoy S., Echahed R., Hanus M. A needed narrowing
strategy. In: Proc. of POPL'94, Portland, Oregon, 1994.


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


 
\delete{
\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 \delete{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.
}

\delete{
\bibitem[{AsLa93}]{[AL]} 
Asperti A., Laneve C. Interaction Systems I: the
theory of optimal reductions.  MSCS, 11:1-48, 
Cambridge University Press, 1993.
} 

\bibitem[{AsLa96}]{[AL2]} 
Asperti A., Laneve C. Interaction Systems II: the practice of optimal reductions.  TCS, 159(2):191-244, 1996.


\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.
Inf.\& Comp., 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.
Cambr. 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 \delete{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 \delete{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, UEA, Norwich, 1994.
 
\delete{
\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[{GlKh96}]{[rndrs]}
Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic
residual structures. In~\cite{[Kir]},  p.~180-195.


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


\bibitem[{GLM92}]{[GLM]} 
Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract Standardisation
theorem. In: Proc. of LICS'92, IEEE Computer Society Press, 1992, p.~72-81.


\bibitem[{Hin64}]{[Hin]}
Hindley R.J. An abstract form of the Church-Rosser theorem I. JSL, 34(4):545-560, 1969.  


\delete{
\bibitem[{Hue80}]{[Hu80]} 
Huet G., Confluent reductions: Abstract properties and applications to term rewriting systems. JACM, 27(4):797-821,1980.  
}

\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[{Kat90}]{[Kath]}
Kathail V. Optimal Interpreters for Lambda-calculus based functional 
languages, PhD thesis, MIT, 1990.


\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, 
University of East Anglia, Norwich, 1989.

 
\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[{KOV96}]{[KOV]}
Kennaway J.R.,  van Oostrom V., de Vries F.J.
Meaningless terms in rewriting. In: Proc. of the 
$5^{th}$ International Conference on Algebraic and Logic
Programming, ALP'96, Aachen, 1996. To Appear.


\bibitem[{Kha88}]{[colog]} 
Khasidashvili Z. $\beta$-reductions and $\beta$-developments of
$\lambda$-terms with the least number of steps. In: Proc. of the
Int. 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 \delete{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 \delete{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[{KhGl96}]{[dndrs-rep]}
Khasidashvili Z., Glauert J.R.W. Discrete normalization and standardization
in stable deterministic residual structures.  Report SYS-C96-02, UEA, Norwich, 1996. 


\bibitem[{KhGl96a}]{[ldrs]}
Khasidashvili Z., Glauert J.R.W. Zig-zag and extraction families in 
non-duplicating stable Deterministic Residual Structures. Submitted for 
publication. (Available at {\sf ftp://ftp.sys.uea.ac.uk/pub/zurab/})


\bibitem[{CAAP'96}]{[Kir]}
Kirchner H., editor. Proc. of the $19^{th}$ International Colloquium on
Trees in Algebra and Programming, CAAP'96, Springer LNCS, vol.~1059, 1996.


\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 Comp. Science, vol.
II, Oxford Univ. 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[{Lam90}]{[Lam]}
Lamping J. An algorithm for optimal lambda calculus reduction. In: Proc. of POPL'90, 1990,~p.16-30.


\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.


\delete{
\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~\cite{[Kir]},  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[{Mel96}]{[Mel]}
Melli\`es P.-A. Description Abstraite des Syst\`emes de R\'e\'ecriture. 
Th\`ese de l'Uni\-versit\'e Paris 7, 1996. 

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

\delete{
\bibitem[{Ong88}]{[Ong]}
C.-H. L. Ong. The lazy lambda calculus: an investigation into 
the foundations of functional programming. Ph.D. Thesis, Imperial 
College, London, 1988.
}


\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. In: Proc. of
RTA'96. To appear.

\delete{
\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[{SPE93}]{[SPE]}
Sleep M.~R., Plasmeijer M.~J., van Eekelen M.~C.~J. D., eds. 
Term Graph Rewriting: Theory and Practice. John Wiley,
1993, p.141-156.

\bibitem[{Sta89}]{[Sta]} 
Stark E.~W. Concurrent transition systems. TCS,
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}
