\documentstyle{elsart}



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

\begin{document}


\begin{frontmatter}

\title{An Abstract Theory of Optimal Evaluation\thanksref{EPCRC}}
\thanks[EPCRC]{Part of this work was supported by the Engineering and
Physical Sciences Research Council of Great Britain under grant GR/H
41300.}

\author{Zurab Khasidashvili}
\address{NTT Basic Research Laboratories \\
Atsugi, Kanagawa, 243-01, Japan \\
\emph{zurab@theory.brl.ntt.co.jp}}
\author{John Glauert}
\address{School of Information Systems, UEA \\
Norwich NR4 7TJ, UK\\
\emph{jrwg@sys.uea.ac.uk}}



\begin{abstract}
This paper generalizes the Huet and L\'evy theory of normalization by
neededness and L\'evy's optimality theory to an abstract setting. We define
\emph{Stable Deterministic Residual Structures} (SDRS) and
\emph{Deterministic Family Structures} (DFS) by axiomatizing the
\emph{residual} relation in an \emph{Abstract Reduction System}. We present
two proofs of the \emph{Relative Normalization Theorem}, one for SDRSs for
\emph{regular stable} sets, and another for DFSs for all \emph{stable} sets
of desirable `normal forms', and prove a Relative Optimality Theorem for
DFSs. We further introduce and study a concept of \emph{implementation} of
DFSs. We show that for any DFS, its implementation  is a non-duplicating
DFSs with zig-zag as the family relation, and optimal family-reductions in
the former are implemented by needed reductions in the latter. (Zig-zag is
simply the symmetric and transitive closure of the residual relation on
redexes with histories.) We show that sharing formalized by our concept of
a family is compositional: the sharing in a DFS can be decomposed into a
weaker sharing (such as zig-zag) and a (proper) sharing in the
implementation of the latter. These results require study of the
family relation in non-duplicating SDRSs. We show that zig-zag forms a
family-relation in every non-duplicating SDRS, and that it is the only
\emph{separable} family relation in such SDRSs. To prove this, we needed to
develop an abstract \emph{extraction} procedure, and to show that the
family concepts defined via zig-zag and via extraction yield the same
relation.
\end{abstract}

\end{frontmatter}

\maketitle



\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
%\newcommand{\john}[1]{} % Comment out text.
%\newcommand{\zurab}[1]{} % Comment out text.
\newcommand{\john}[1]{\{{\bf John: \sf #1}\}} % Highlight text.
\newcommand{\zurab}[1]{\{{\bf Zurab: \sf #1}\}} % Highlight text.
\newcommand{\delete}[1]{} % Comment out text.
\newcommand{\suppress}[1]{} % Comment out text.
%\newcommand{\suppress}[1]{\{\{{\sf #1}\}\}} % Highlight text.
\newcommand{\incl}[1]{#1} % include text.
%\newcommand{\incl}[1]{} % exclude text.
%\newcommand{\excl}[1]{} % exclude text.
\newcommand{\excl}[1]{\{#1\}} % include text.


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

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


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

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


\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand{\inputpic}[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\newcommand{\imply}{\,\Rightarrow\,}


\newcommand{\vect}[1]{\mbox{$\overline{#1}$}}
\newcommand{\rpsim}{\mbox{$\stackrel{r}{\psim}$}}
\newcommand{\rpessim}{\mbox{$\stackrel{r}{\pessim}$}}
\newcommand{\ressim}{\mbox{$\stackrel{r}{\essim}$}}
\newcommand{\rsim}{\mbox{$\stackrel{r}{\sim}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\lclas}[1]{\mbox{$\langle{#1}\rangle_L$}}
\newcommand{\sclas}[1]{\mbox{$\langle{#1}\rangle_S$}}
\newcommand{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\newarrow{Co}<--->
\newcommand{\pessim}{\prec\!\!\prec}
\newcommand{\steq}{\approx_{st}}
\newcommand{\essim}{\approx}
\newcommand{\psim}{\prec}
\newcommand{\orth}{\perp}
\newcommand{\esorth}{\perp_{es}}
%\newcommand{\subt}{\subseteq}
\newcommand{\subt}[0]{\in}
\newcommand{\subts}[0]{\subseteq}


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

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

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


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


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

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

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

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

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


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

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

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






\section{Introduction}



In order to achieve optimal evaluation of $\lambda$-terms, L\'evy
introduced a notion of \emph{redex-family} to capture the concept of
redexes of the `same origin'. The hope was that it would be possible to mimic
multi-step reductions which contract whole families in a term by reduction
of some graph representation, in which every multi-step would be
represented by contraction of a single graph redex~\cite{[levy],[le80]}.
There was no other way as Barendregt et al~\cite{[Bar.76]} showed that there
does not exist a
one-step optimal recursive $\beta$-reduction strategy on $\lambda$-terms.
Such an implementation has indeed been achieved by Lamping~\cite{[Lam]} and
Kathail~\cite{[Kath]}, reviving interest in optimal graph reduction.
Maranget~\cite{[Mar91]} generalized \Le's optimality theory to orthogonal
Term Rewriting Systems (TRSs), Gonthier et al~\cite{[GAL]} simplified
Lamping's technique, and Asperti and Laneve generalized both L\'evy's
optimality theory and Gonthier's implementation to Interaction
Systems, which cover most of the languages  with a constructor-destructor
discipline~\cite{[AL],[AL2]}. More recently, van Oostrom generalized the
optimality theory to the whole class of orthogonal Higher-Order Rewriting
Systems (HORSs)~\cite{[Oos]}, and Guerrini developed a general theory of
sharing-graph rewriting~\cite{[Gue.th]}.

\Le\ introduced the family concept in three different ways: via an
appropriate
notion of \emph{labelling}, via \emph{extraction}, and by \emph{zig-zag}.
He showed that they all yield the same
concept, in the \lc. The same holds for all orthogonal HORSs $R$ if all
three family concepts are defined in the refinement of $R$ which decomposes
every original $R$-step into first-order or TRS-step and a number of
substitution
steps~\cite{[Oos]}. However, the zig-zag family can be defined directly in
$R$, and this yields a different, weaker, family concept~\cite{[AL]}.
Independently and much earlier, Kennaway and Sleep~\cite{[K.S.]} defined
a concept of labelling for orthogonal Combinatory Reduction Systems (CRSs),
improving Klop's original labelling system for CRSs~\cite{[Kl.CRS]},
which covers orthogonal TRSs and Interaction Systems. Their labelling is
different from both Maranget's labelling for orthogonal TRSs~\cite{[Mar91]} and
Asperti-Laneve's labelling for Interaction Systems~\cite{[AL]}.



This variety of family concepts, and development of alternative graph
rewriting algorithms for optimal implementation of orthogonal rewriting
systems, such as Term Graph Rewriting~\cite{[KKSdV]}, Jungle
Rewriting~\cite{[H.P.]}, and many others, inspired by Wadsworth's pioneering
work on graph-based implementation of the \lc~\cite{[Wad]}, created the
need to develop an abstract notion of family general enough to cover all the
existing notions, and refined enough to enable proof of normalization and
optimality results. Usefulness and feasibility of such a theory was already
pointed out by Berry and L\'evy:`Thus a unifying or axiomatized point of
view should be adopted to preserve the syntactic results of this paper.
This seems possible along the lines of O'Donnell~\cite{[OD]} and
Rosen~\cite{[Ros]}. Furthermore, the axiomatized approach should include
the \lc\ where much of the syntactic part of this paper is
valid'~\cite{[B.L.]}.




This work is the first step towards developing an axiomatic theory of
optimality. We define a \emph{Deterministic Family Structure} (DFS) as a
\emph{Deterministic Residual Structure} (DRS) with an axiomatized
\emph{family} and \emph{contribution} relations. The family relation in a
DFS is simply an
equivalence relation containing zig-zag, and the \emph{contribution}
relation expresses causal dependencies among families and is formalized in
terms of creation of redexes. All existing definitions of family relation
in the
literature~\cite{[levy],[Kl.CRS],[K.S.],[Mar],[AL],[Oos]} satisfy our DFS
axioms. A DRS in turn is an \emph{Abstract Reduction Systems} (ARSs) which
has a \emph{residual} relation
between redexes in the source and target terms of each transition $t\red{u}s$.
Redexes of $t$ may be erased by reduction of $u$, new redexes may be
introduced in $s$, while other redexes of $s$ are considered \emph{residuals} of
redexes in $t$, as specified by the residual relation.
Further, the residual relation is generalized to all (many-step) reductions, and
\emph{permutation-equivalence} on reductions, referred to below as
\emph{L\'evy-equivalence}, and \emph{L\'evy-embedding relation}, is
introduced, as is done for the \lc\  in~\cite{[levy],[le80]}. Sufficient
conditions needed to define permutation equivalence in an abstract setting
were stated by Stark~\cite{[Sta]} (for the case when the residual relation
is non-duplicating, independently from L\'evy~\cite{[levy],[le80]}) and by
Gonthier et al.~\cite{[GLM]}.


\suppress{
In~\cite{[Sta]}, Stark defines \emph{Concurrent Transition Systems} (CTSs)
and uses them to develop a model of concurrent computation,
studying ways of building machine networks with concurrent machines as
basic objects. On the other hand, Gonthier et al.~\cite{[GLM]} were
interested in studying more syntactic properties, such as standardization,
of orthogonal rewrite systems in an abstract setting. The way
standardization is understood in that paper requires a \emph{nesting}
relation on redexes in a term, and some axioms giving its important
properties. Standard reductions then become some kind of outside-in
reductions. However, the \cite{[GLM]} axioms are rather restrictive, and we
do not impose a nesting relation on redexes.  Unlike CTSs, our residual
relation may be duplicating. Despite their highly abstract nature, a
counterpart of the \emph{stability} property of Berry~\cite{[berry]} and
Winskel~\cite{[Win89]} enables us to develop a large part of normalization
and optimality theory of L\'evy~\cite{[levy],[le80],[B.L.].[H.L.]} in the
framework of stable DRSs and DFSs.
}



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



This fundamental work has been extended in several directions.
Barendregt et al.~\cite{[B.K.K.S.]}, Maranget~\cite{[Mar]},
N\"ocker~\cite{[Nok.thi.]} and Middeldorp~\cite{[Mid]} studied neededness
w.r.t. head-normal forms, weak head-normal forms, constructor head-normal
forms, and root-stable forms, respectively.
Sekar and Ramakrishnan~\cite{[SeRa]} studied normalization via
\emph{necessary} set of redexes.  Kennaway et al.~\cite{[K-tra]} studied a
needed strategy for infinitary orthogonal TRSs. A different approach to
normalization is developed in Kennaway~\cite{[Kenn]} and Antoy and
Middeldorp~\cite{[AnMi]}. Antoy et al.~\cite{[Ant]} designed a needed
narrowing strategy.
Gardner~\cite{[Gar]} described a \emph{complete} way of encoding
neededness information using a type assignment system.


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


Here we further generalize the theory by
abstracting from the structure of terms. We study relative normalization in
DRSs. Despite their highly abstract nature, a counterpart of the
\emph{stability} property of Berry~\cite{[berry]} and
Winskel~\cite{[Win89]} enables us to prove the \rn\ theorem for all
\emph{regular}
stable sets $\stab$. (We actually prove  the Relative Hypernormalization
theorem.)  We show that without this stability axiom the theorem fails. The
proof method employed is similar to that in~\cite{[colog],[rta]} (it was
discovered by the author independently from~\cite{[H.L.]}), and is based on
the fact that $\stab$-needed steps in a reduction can be pushed before
$\stab$-unneeded steps without affecting the number of $\stab$-needed
steps.


Since for \emph{irregular} stable $\stab$, $\stab$-unneeded redexes can
duplicate $\stab$-needed ones, the above proof method does not apply for all
DRS; for the same reason, the $\stab$-needed strategy is no longer
hypernormalizing. However, the DFS axioms (in particular, a strong
termination axiom [FFD]) insure that any $\stab$-normalizing reduction can
be transformed into an $\stab$-needed $\stab$-normalizing one by pushing
$\stab$-needed steps forward, and that all $\stab$-needed reductions are
eventually terminating (at a term in $\stab$).
Furthermore, for DFSs we show that a strategy that contracts, in an
arbitrary order, redexes that belong to $\stab$-needed families, but which
need not be
$\stab$-needed themselves, is still $\stab$-normalizing. As a corollary,
any \emph{$\stab$-needed complete family-reduction}, which in any term
contracts all members of a family containing an $\stab$-needed redex in a
multi-step, is
eventually $\stab$-normalizing. Using the same method as in~\cite{[le80]},
we show that the latter reductions are also optimal in the sense that they
reach $\stab$ in a least number of family-reduction steps.


In order to provide an abstract criterion for \emph{correctness} of a graph
implementation of complete-family reductions, we introduce an abstract
concept of \emph{L\'evy-implementation}: With a DFS we associate a
\emph{non-duplicating} DRS, called its implementation, whose steps exactly
correspond to complete family-reduction steps in the original DFS. For
example, implementation DRSs can model sharing-graph implementation of
L\'evy's complete family-reductions in the \lc\ (modulo `book-keeping'
steps which in general can be prohibitively expensive~\cite{[A.M.]}). It is
not difficult to show that needed (w.r.t. a stable set of results)
reductions in
the implementation DRS correspond exactly to needed complete
family-reductions in the original DFS, implying that the former DRS indeed
implements optimal computations in the latter DFS, in the sense of
L\'evy~\cite{[levy],[le80]}.



Further, we show that the family relation in the implementation DRS induced
by the original DFS coincides with zig-zag, which is the weakest family
sharing (by our definition of families). Note that a family relation in a
(non-duplicating or duplicating) DRS need not coincide with zig-zag. An
example is Asperti and Laneve's concept of family for Interaction
Systems~\cite{[AL]}, where unlike the \lc\ a single redex can create more
than one members of a family which cannot be related by zig-zag (without
employing the internal structure of reduction steps). In non-duplicating
DRSs, we call such families \emph{non-separable.}


Actually, we show that the sharing concept formalized in DFSs is
\emph{compositional}: any sharing can be decomposed into a weaker sharing
and a non-separable sharing in the non-duplicating DRS implementing that weaker
sharing. To this end, we investigate the family relation in non-duplicating
DFSs. We show that zig-zag forms a family-relation in every non-duplicating
SDRS, and that it is the only separable family relation in such SDRSs.
These results are obtained by defining an abstract extraction procedure for
non-duplicating SDRSs and
showing that zig-zag coincides with our extraction-family relation. The
technical contribution here is the simplicity of our construction which
avoids irrelevant syntactic complications, such as those related to the
top-down and left-to right nature of the conventional concept of
standardization.




The paper is organized as follows. In the next section, we introduce stable
DRSs and prove some fundamental lemmas concerning (mutually)
\emph{external} reductions. In Section~\ref{S.rn.sdrs.}, we prove the \rn\
theorem for regular stable sets $\stab$ in an SDRS $R$, and demonstrate
that if $R$ is not stable, then the theorem fails. In
Section~\ref{S.rn.fs.}, we introduce DFSs, compare them
with stable DRSs, and prove the Relative Normalization and Optimality
theorems for any stable set $\stab$ of results. Section~\ref{S.zi.ext.}
gives a
characterization of zig-zag relation via extraction in non-duplicating
SDRSs, used in Section~\ref{S.li.zi.fa.} to prove that, in
every non-duplicating SDRS, zig-zag is a family relation, and moreover, is
the unique separable family-relation.  In Section~\ref{S.impl.drs.} we
define and study implementation DRSs, and show the compositionality of
sharing. Conclusions appear in Section~\ref{S.concl.}.



The results of this paper have been reported
in~\cite{[rndrs-rep],[azdfs],[acoi-rep]} and published as~\cite{[rndrs]}.
Some results are taken from~\cite{[dndrs],[dndrs-rep]}



\section{Deterministic Residual Structures}


In this section we define \emph{Deterministic Residual Structures} (DRSs)
which are \emph{Abstract Reduction Systems} (ARSs) satisfying certain
properties concerning residuals.

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

\bd
An ARS is a
triple $A$ = (\emph{Ter},\emph{Red},$\ar$)
where \emph{Ter} is a set of \emph{terms}, ranged over by
$t,s,o,e$; \emph{Red} is a set of \emph{redexes} (or \emph{redex occurrences}),
ranged over by $u,v,w$; and
$\ar:Red\ar (Ter\times Ter)$ is a function such that for any $t\in Ter$
there is only a finite set of $u\in Red$ such that $\ar(u)=(t,s)$,
written $t\red{u}s$. This set will be known as the redexes of term $t$, where
$u\subt t$ denotes that
$u$ is a member of the redexes of $t$ and $U\subts
t$ denotes that $U$ is a subset of the redexes. Note
that $\ar$ is a \emph{total} function, so one can identify $u$ with the
triple $t\red{u}s$.
A \emph{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$. $\,\,\vert P\vert$ denotes the length of $P$.
$P+Q$ denotes concatenation of $P$ and $Q$.
\delete{$P\leq Q$ denotes
that $P$ is an initial part of $Q$. $\,\,\,\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.
\ed

DRSs are similar to \emph{Determinate Concurrent Transition
Systems} (DTCS) of Stark~\cite{[Sta]}, to \emph{Abstract Reduction Systems}
(ARSs) of Gonthier et al.~\cite{[GLM]}, and to van Oostrom's
\emph{orthogonal
Descendant Rewriting Systems}~\cite{[Oos.th]}.
The main difference from DCTSs is that Stark requires a
non-duplicating residual relation, and distinguishes a start state. Unlike
ARSs of~\cite{[GLM]}, we do not have a nesting relation on redexes and the
corresponding axioms, and the stability axiom is modified accordingly.
Instead, we study properties of conflict-free transition and reduction
systems based on the duplication and erasure effect of executed transitions
on the others, and develop a theory that is applicable to systems with
nested transitions too. The
difference from van Oostrom's orthogonal DRSs is that in the
latter the notion of \emph{descendant} of any subterm/position of a term is
formalized, not only the notion of residual of redexes; and the acyclicity
axiom below is not required there. Closely related, but more syntactically
oriented, abstract reduction systems are studied
in~\cite{[Mel.th],[Raa.th]}.



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

A \emph{development} of $U\subts t$ is a reduction $P:t\doar $ that only
contracts residuals of redexes from $U$; it is \emph{complete} if
$U/P=\cup_{u\in U}\,u/P=\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:
\bds
\item[{\rm [FD]}] (\emph{Finite Developments}~\cite{[GLM]}) All
developments are terminating; all complete developments of $U\subts t$ end
at the same term; and residuals of a redex $v\subt t$ under all complete
developments of $U$ are the same.

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


One can verify that all orthogonal (first or higher-order, see
e.g.,~\cite{[Raa.th]})  term rewriting systems, such as the
$\lambda$-calculus,  form DRSs. These systems are stable, and can be shown
so
just using an appropriate notion of descendant which assigns the contractum
to the contracted redex -- labelling is not necessary.
Further, orthogonal Term Graph Rewriting Systems~\cite{[KKSdV]}, which are
equivalent to orthogonal DAG (Directed Acyclic Graphs) rewriting systems
defined via labelled orthogonal TRSs~\cite{[Mar91],[Mar]}, are DRSs but
they do not verify all nesting axiomsof~\cite{[GLM]}.  Similarly,
Interaction Nets~\cite{[Laf]} form DRSs (when restricted to finite nets),
and they do not have or need any nesting order on redexes (as nets are
undirected, possibly cyclic, graphs).



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



To show that the above definitions are sound, it is convenient to consider
\emph{multi-step} reductions, where a multi-step contracts
\emph{simultaneously}, or in \emph{parallel}, a set of redexes in a term;
thus a multi-step can be seen as a complete development of a set of
redexes, and it is conventional to switch freely between multi-steps and
complete developments. Now for example correctness of the above definition
of residuals for reductions can be proved by induction on the number of
multi-steps in $P_1,P_2$ and $Q$, where steps in these reductions are
viewed as multi-steps contracted singleton sets of redexes. These induction
is equivalent to induction on \emph{multi-diagrams}, which are diagrams of
the form:
\begin{diagram}[height=1.6em,width=1.8em]
\cdot     &\rTo    &  \cdot    &\rTo    &\cdot  &\rTo        & \cdot &\rTo
& \cdot\\
\dTo   &        &\dTo   &        & \dTo    &  & \dTo  &  & \dTo  \\
\cdot   &\rTo  & \cdot & \rTo  & \cdot &\rTo & \cdot &\rTo   & \cdot \\
\dTo  & &\dTo  & & \dTo & & \dTo & &\dTo  \\
\cdot  &\rTo & \cdot &\rTo  &\cdot  & \rTo   & \cdot &\rTo   & \cdot\\
\dTo   &       &\dTo  &       & \dTo  &      & \dTo & &\dTo \\
\cdot     &\rTo  & \cdot     &\rTo  &\cdot  & \rTo    & \cdot &\rTo   & \cdot\\
\end{diagram}
where each arrow represents a multistep, and each inner square is yielded
by the equation $U+V/U\hieq V+U/V$, where $U$ and $V$ as well as $U/V$ and
$V/U$ are multi-steps. Here $\hieq$ is \emph{Hindley-equivalence}, which is
defined for finite co-initial reductions as follows: $P\hieq P'$ iff they
end at the same term and for any redex $u$ in the initial term, the
residuals of $u$ under $P$ and under $P'$ are the same redexes. The
induction principle is then to infer a property for such a multi-diagram
from properties of its proper sub-diagrams. For example, the correctness of
definitions $(P_1+P_2)/Q=P_1/Q+P_2/(Q/P_1)$ and $Q/(P_1+P_2)=(Q/P_1)/P_2$
can be inferred from the following multi-diagram:
\begin{diagram}[height=2em,width=2em]
\cdot      & \rOnto^{P_1}       & \cdot           & \rOnto^{P_2}
& \cdot  \\
 \dOnto^Q &              &  \dOnto_{Q/P_1}  &             &
\dOnto_{Q/(P_1/P_2)}   \\
\cdot & \rOnto_{P_1/Q} & \cdot    & \rOnto_{P_2/Q/P_1)}   & \cdot  \\
\end{diagram}


However, it is not necessary to switch to multi-steps in order to provide a
sound induction principle for definitions and proofs involving many-step
reductions. (Otherwise, the `trick' to use multi-step reductions would not
be sound!) \emph{Klop's commutative diagrams} can be used
instead~\cite{[Kl.CRS]}. Klop's diagrams are constructed using developments
rather than multi-steps, and this involves `splitting' of elementary (or
one-step) diagrams. The following is a simple example of a Klop-diagram:
\begin{diagram}[height=1.6em,width=1.8em]
\cdot     &\rTo    &      &    & \cdot  &  \rTo      &   &      & \cdot\\
\dTo   &        &    &        & \dTo    &  &    &  & \dTo  \\
    &   &   &    & \cdot &\rTo & \cdot &\rTo   & \cdot \\
   & &  & & \dTo & & \dTo & &\dTo  \\
\cdot  &  &   &\rTo  &\cdot  & \rTo   & \cdot &\rTo   & \cdot\\
\end{diagram}
where now arrows represent reduction steps, not multi-steps, and each inner
square is again yielded by the equation $U+V/U\hieq V+U/V$ where $U$ and
$V$ as well as $U/V$ and $V/U$ are now complete developments of respective
sets of redexes. Both multi-step and Klop's diagrams use empty (multi-)
steps to retain the rectangular shape of the diagrams. Construction of a
Klop-diagram need not terminate in general, but it always does for
reductions in DRSs, by virtue of the axiom [FD]. Construction of Klop's
diagrams is well described also in~\cite{[Bar]}, for the case of the \lc.
We will often use Klop's diagrams in proofs. In that case, say $P/Q$ is
considered as a reduction rather than a multi-step reduction, thus is only
unique up to the particular sequentializations of corresponding
multi-steps. (However,  $P/Q$ is defined more precisely than up to
$\leeqv$.)  In conclusion, let us note that, in the definition of DRSs, we
could instead of [FD] equivalently require only termination of developments
and the following strong local commutativity property: for any co-initial
redexes $u$ and $v$, $u\sqcup v\hieq v\sqcup u$. That is why Klop's
diagrams are equivalent to multi-diagrams.


The [stability] axiom is not used in the above constructions. Intuitively,
stability means that a
redex cannot arise from two unrelated sources.  This property has
a natural extension to many-step reductions, where `unrelated'
is formalized by the notion of \emph{external}. For
syntactic systems, externality of two co-initial reductions is a natural
concept relating to overlap between
components of terms involved in the reduction steps. In an abstract setting it
expresses that the two reductions do not contract redexes that have common
residuals.


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

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

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


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



\bll{L.external.rem.ext.}
Let $P:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_n$ be external to
$U=\{u_1,\ldots,u_n\}\subts t_0$, and let $Q_0:t_0\doar o_0$. Then
$P'=P/Q_0$ is external to the set $U'=U/Q_0$.

\bproof
Let $P_i:t_0\red{v_0}t_1\red{v_1}\ldots\ar t_i$, $Q_i=Q_0/P_i$, and
$P'_{i+1}=v_i/Q_i$, $(0\leq i<n)$ (see the figure).
Since $P$ is external to $U$, we have
for each $i$ that $v_i\not\in U/P_i$. Therefore, $v_i/Q_i\cap
U/(P_i+Q_i)=\emptyset$ (since the residuals of different redexes are
different). Thus \delete{by \Pr{L.perm.equiv.}.(3),} $v_i/Q_i\cap
U/(Q_0+P'_1+\ldots+P'_{i})=\emptyset$. Hence, $P'_{i+1}$ is external to
$U'/(P'_1+\ldots+P'_{i})$. This means that $P'$ is external to $U'$.
\begin{diagram}[height=2em,width=2em]
 t_0  & \rTo^{v_0=P_1} & t_1  & \rOnto   & t_{n-1} &  \rTo^{v_{n-1}} & t_n   \\
 \dOnto^{Q_0}&     &  \dOnto^{Q_1} &   &     \dOnto^{Q_{n-1}}   &   &
\dOnto_{Q_n}\\
o_0  & \rOnto_{P'_1} & o_1  & \rOnto  & o_{n-1} &  \rOnto_{P'_{n}} &   o_n   \\
\end{diagram}
\eproof
\el

We conclude this section by proving two fundamental lemmas, which
generalize [weak acyclicity] and [stability] axioms to many-step
reductions, and are used repeatedly throughout the paper


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

\bproof
We show that $P/N=\emp$ implies $N/P\not=\emp$ by induction on the number
of elementary diagrams in a
Klop diagram $D(P,N)$ of $P$ and $N$. It follows from
\Dr{D.ext.reductions.} that the top and left edges of all sub-diagrams of
$D(P,N)$ are external reductions, therefore the induction is
sound. So let $P/N=\emp$. If $\vert P\vert=\vert N\vert=1$, we have
$N/P\not=\emp$ by [weak acyclicity]. Otherwise, let say $\vert P\vert >1$, let
$P:t\dored{Q}e\red{v}o$, and let $N^*=N/Q$ (see the figure).
By the induction assumption, $N^*\not=\emp$. So let $N^*=N'+w$, where $w$ is
the last (non-empty) step of $N^*$, and let $V=v/N'$. Again by the
induction assumption, $w/V\not=\emp$. Hence $N/P\not=\emp$.
\begin{diagram}[height=1.0em,width=2em]
 t       & \rOnto^{Q}  & e                & \rTo^{v}          & o    \\
         &             &                  &                   &\dOnto \\
         &             &                  &                   &     \\
         &             &  \dOnto^{N'}     &                   &      \\
\dOnto^N &             &  \cdot           &    \rOnto^{V}     &  \cdot  \\
         &             &  \dTo^{w}        &                   & \dOnto \\
  s      & \rOnto_\emp &    s             &  \rOnto_\emp      &  s   \\
\end{diagram}
\eproof
\el


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

\bproof
By induction on the number $n$ of elementary diagrams in Klop's diagram
$D(P,Q)$ of $P$ and $Q$. The case $n=1$ is the axiom [stability].
It follows from
\Dr{D.ext.reductions.} that the top and left edges of all sub-diagrams of
$D(P,Q)$ are external reductions, therefore we can assume the lemma is
proved for all subdiagrams of $D(P,Q)$. Let $W^*=W/(Q/P)\not=\emp$.

If $\vert P\vert=1$ and $\vert Q\vert>1$, say $Q=v+Q'$, then
$W'=W/(v/P)\not=\emp$, and by [stability] redexes in $W'$ are created by
$P/v$. By the induction assumption, redexes in $W^*$ are created by $P/Q$
and $Q'/(P/v)$ is external to $W'$, implying that $Q/P=v/P+Q'/(P/v)$ is
external to $W$.

\begin{diagram}[height=2em,width=2em]
 t      & \rTo^v       & \cdot           & \rOnto^{Q'}           & e  \\
 \dTo^P &              &  \dOnto_{P/v}  &             & \dOnto_{P/Q}   \\
W\ssq s & \rOnto_{v/P} & s' \ni W' & \rOnto_{Q'/(P/v)}   & \cdot  \\
\end{diagram}
Now it remains to consider the case when $\vert P\vert>1$, i.e., $P=u+N$
with $\vert N\vert>0$ (see the figure below). Then
$W=W_u/N\cup W_N$, where $W_u$ is the set of
redexes created by $u$, and $W_N$ is the set of redexes created by (i.e.,
along) $N$. By the induction assumption, $Q/u$ is external to $W_u$, and
the redexes in $W_u/(Q/u)$ are created by $u/Q$. By
\Lr{L.external.rem.ext.}, $Q/P=(Q/u)/N$ is external to the set $W_u/N$. By the
induction assumption, $Q/P=(Q/u)/N$ is external to $W_N$ and redexes in
$W_N/(Q/P)$ are created by $N/(Q/u)$. Hence $Q/P$ is external to $W$, and
since $W/(Q/P)=W_N/(Q/P)\cup W_u/((Q/u)\sqcup N)$, redexes in $W/(Q/P)$ are
created by $P/Q$.
\begin{diagram}[height=2em,width=2em]
  t            & \rOnto^{Q}   &   e     \\
 \dTo^{u}      &              &     \dOnto_{u/Q} \\
 W_u\in o      & \rOnto^{Q/u} & o' \ni W_u/(Q/u) \\
\dOnto^{N}     &              &     \dOnto_{N/(Q/u)} \\
 W\in s        & \rOnto_{(Q/u)/N}&  s'\ni W^*    \\
\end{diagram}
\eproof
\el





\section{Relative Normalization for regular stable sets}
\label{S.rn.sdrs.}


In this section, we prove that, for any \emph{regular} stable
set of terms $\stab$ in a
stable DRS $R$, an $\stab$-normal form of an
$\stab$-normalizable term can be found by contracting $\stab$-needed
redexes in it, even if every $\stab$-needed step is preceded by a finite
number of $\stab$-unneeded steps. We show that without the assumption of
stability for $R$, this result breaks down.



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

\item[(2)] We call $\stab$ \emph{stable} if:
\ben
\item[$(a)$] $\stab$ is \emph{closed under parallel moves}: \\
for any $\stab$-early $t$, any $P:t\doar o\in \stab$, and any $\stab$-early
$Q:t\doar e$, the final term of $P/Q$ is in $\stab$; and

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


A stable set need not be closed under reduction --
$Q/P$ in the definition above may contain terms not in $\stab$,
but closure under
parallel moves requires that the final term is.
Stability and regularity coincide in non-duplicating systems.
Below $\stab$ will usually denote a stable
set of terms in some DRS.  $\reg$ will denote a regular stable set.
For simplicity, we only consider stable sets
that are closed under reduction; obviously, closure
under reduction implies closure under parallel moves.

The most appealing examples of stable sets are
normal forms~\cite{[H.L.]}, head-normal
forms in the \lc~\cite{[B.K.K.S.]}, weak-head-normal
forms in an orthogonal TRS (a partial result is in~\cite{[Mar]}),
constructor-head-normal forms for constructor
TRSs~\cite{[Nok.thi.]}, root-stable forms in (weakly) orthogonal
TRSs~\cite{[Mid]}, and flexible generalized-head-normal forms in the
$\lambda_{hd}^v$-calculus~\cite{[Xi]}.  All the above sets are closed under
reduction, and are regular. Other examples include weak-head-normal forms
(up
to garbage-collection, modulo a congruence) in Yoshida's $\lambda f$-calculus
(an environment calculus)~\cite{[Yos]} and the set of \emph{answers} in
\emph{call-by-need} $\lambda$-calculus of Ariola et al.~\cite{[A.F.]}; both
are conditional rewrite systems. An example of an orthogonal TRS with an
irregular stable $\stab$ is given in Remark~\ref{R.irreg.no.hyper.}.




We begin the proof by showing that $\stab$-unneeded redexes cannot
create $\stab$-needed ones, and that residuals of $\stab$-unneeded
redexes remain unneeded. When $\stab$ is regular, this enables us to
construct a $\stab$-needed variant of any
$\stab$-normalizing reduction.


\bll{T.3.1.c.}
For any stable $\stab$, residuals of $\stab$-unneeded redexes of a term $t$
under any reduction $P:t\doar s$ remain $\stab$-unneeded.

\bproof
Let $u\in t$ be $\stab$-unneeded, and let $v$ be a $P$-residual of $u$.
Then there is an $\stab$-normalizing reduction $Q:t\doar o$ that is
external to $u$. By \Lr{L.external.rem.ext.}, $Q/P$ is external to $v$,
thus $v$ is $\stab$-unneeded (as $Q/P$ is $\stab$-normalizing by stability
of $\stab$).
\eproof
\el




\begin{lem}\em
\label{L.4.1.c.stab.}
Let $\stab$ be stable, let $t\not\in \stab$, let $t\red{u}e$, let $u$ be
$\stab$-unneeded, and let $w\subt e$ be a redex created by $u$, in a stable
DRS. Then $w$ is $\stab$-unneeded.

\bproof
If $e\in \stab$, then every redex in $e$ is $\stab$-unneeded; so suppose
$e\not\in \stab$. Since $u$ is $\stab$-unneeded, there is an
$\stab$-normalizing $P:t\doar s$ that does not contract residuals of $u$.
By \Lr{L.disj.red.creat.}, $P/u$ does not contract residuals of $w$. Also,
$P/u$ is $\stab$-normalizing since $\stab$ is closed under parallel moves.
Hence $w$ is $\stab$-unneeded.
\eproof
\end{lem}



The following example shows that, in the above lemma, stability of the DRS
is necessary.


\bel{E.nec.of.stab.for.norm.the.}
Let terms in the DRS $R$ be $t=I(I(x))$, $s=I(x)$, and $e=x$; redexes in
$t$ be $u=t$ and $v=I(x)$, $s$ contain the only redex $w=s$, and $x$
does not contain a redex; let the reduction relation be given by
$Red=\{t\red{u}s, \,t\red{v}s, \,s\red{w}x\}$, let the residual relation be
empty except for empty reductions, for which the residual relation is
identity, and let $\stab=\{x\}$. (Obviously, this is not, and cannot be,
the usual residual relation for orthogonal TRSs.) Then $\stab$ is stable
and regular, both $u$ and $v$ are $\stab$-unneeded, and both create the
redex $w\subt s$ that is $\stab$-needed. Note also that the Relative
Hypernormalization theorem (proved below) is not valid for $(R,\stab)$
since $t\not\in \stab$ is $\stab$-normalizable but does not contain an
$\stab$-needed redex.
\ee



\begin{defn}\em
\label{D.4.1.}
We call  $P:t_0\ar t_1\ar\ldots$  \emph{$\stab$-(un)needed} if it contracts only
$\stab$-(un)needed redexes. We call $P$ \emph{$\stab$-quasi-needed} if it
contracts infinitely many $\stab$-needed redexes, and  call it
\emph{$\stab$-semi-needed} if it can be expressed as $P=P_{1}+P_{2}$  where
$P_1$ is $\stab$-needed and $P_2$ is $\stab$-unneeded. In the latter case,
we call $P_1$ the \emph{$\stab$-needed part} of $P$ ($P_1$ can be infinite,
in which case $P_2=\emptyset$).
\end{defn}


We now describe an algorithm that, for a \emph{regular} stable
$\reg $ in a DRS $R$, transforms any finite or infinite reduction $P$ into
an $\reg $-semi-needed reduction $K(P)$. The algorithm is as follows: find
in $P$ the leftmost subreduction $P_0:t\red{u}s\red{v}o$ such
that $u$ is $\reg$-unneeded and $v$ is $\reg$-needed. Let $P=P_1+P_0+P_2$. By
Lemma~\ref{L.4.1.c.stab.}, $v$ is a residual of a redex $v'\subt t$, which
is $\reg$-needed by \Lr{T.3.1.c.}. Since $\reg$ is regular, $v$
is the only residual of $v'$, hence $P_0$ and $P'_0=v'+u/v'$ are both
complete developments of the set $u,v'\subt t$, thus $P_0\leeqv P'_0$. Now
replace $P_0$ by $P'_0$ in $P$. Transform the obtained reduction $P'$ in
the same way, and so on, as long as possible. Obviously, by regularity of
$\reg$, the number of $\reg$-unneeded steps in $P'$ preceding $v'$ is less
than the number preceding $v$ in $P$, and the number of $\reg$-needed steps
in $P$ and $P'$ coincide.


The regularity of $\reg $ is essential for termination of the
transformation process, and for preservation of $\reg $-quasi-neededness of
the reduction under transformation. The latter property is crucial for our
method for proving termination of an $\reg$-needed reduction starting from
an $\reg $-normalizable term.




\begin{lem}\em
\label{L.4.4.}
Let $P$ be a finite or infinite reduction in an SDRS, and let $\reg$ be regular.
\ben
\item[(1)] If $P$ ends at a term in $\reg$, then $K(P)$ is a finite
$\stab$-semi-needed reduction whose $\stab$-needed part ends at a term in
$\reg$ as well.

\item[(2)] If $P$ is $\stab$-quasi-needed, then $K(P)$ is an infinite
$\stab$-needed reduction.
\een

\bproof
\ben
\item[(1)] Since the transformation does not change the number of  $\reg$-needed
steps in $P$, it follows that $K(P)$ is $\reg$-semi-needed, and it ends at
$\reg$ since $K(P)\leeqv P$. The step of $K(P)$ entering $\reg$ is the last
$\reg$-needed step of $K(P)$ by stability of $\reg$.

\item[(2)] Immediate from the construction of $K(P)$.
\een
\eproof
\end{lem}



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


\begin{lem}\em
\label{L.pers.need.}
Let $\reg$ be a regular stable set of terms in a DRS $R$, and let
$t\red{u}s$. Then any $\reg$-needed redex $v\subt t$ different from $u$ has
an $\reg$-needed residual.

\bproof
If $t$ is not $\reg$-normalizable, then neither is $s$, and all redexes in
$t$ and $s$ are $\reg$-needed. So suppose $t$ is $\reg$-normalizable
($t\not\in \reg$ since $t$ contains an $\reg$-needed redex), and suppose on
the contrary that each residual $v_i$ of $v$ in $s$ is $\reg$-unneeded. By
closure of $\reg$ under parallel moves, $s$ is $\reg$-normalizing too. By
\delete{\Cr{T.4.1.}} \Lr{L.4.4.}.(1), there is an $\reg$-needed
$\reg$-normalizing reduction $P:s\doar o$. Since by \Lr{T.3.1.c.} all
residuals of each $v_i$ along $P$ are $\reg$-unneeded, $P$ is external to
all $v_i$. Therefore, $u+P$ is external to $v$ and is $\reg$-normalizing --
a contradiction, since $v$ is $\reg$-needed.
\eproof
\end{lem}








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

\bproof
By Lemma~\ref{L.4.4.}, $t_{0}$ has an infinite $\reg$-needed reduction
$P:t_0 \red{u_{0}}t_{1}\red{u_{1}}\ldots$.  Let $U_{i}=u/(u_{0}+ \ldots
+u_{i-1})$,  $i=0,1, \ldots $ (see the diagram below). It follows from
finiteness of developments that
there  are infinitely  many numbers $k$ such that $u_{k}\not\in U_{k}$
(otherwise there should be a number $m$ such that
$t_m\red{u_m}t_{m+1}\red{u_{m+1}}\ldots$ is an infinite
$U_{m}$-development). By Lemma~\ref{L.pers.need.}, $u_{k}$ has at least one
$\reg$-needed $U_{k}$-residual in  $s_{k}$,  i.e. $u_k/U_k$ contains  at
least  one  $\reg$-needed  step. Hence  $P/u$ is $\reg$-quasi-needed.
%
%\begin{figure}
\begin{diagram}[height=2em,width=2em]
t_0    &   \rTo^{u_0}  &   t_1   &   \rTo^{u_1}  &   t_2    &  \rOnto  &
\cdot \\
 \dTo^{u=U_0}  &     & \dOnto^{U_1} &          & \dOnto^{U_2}&         &      \\
s_0    &   \rOnto_{u_0/U_0}  &   s_1   &   \rOnto_{u_1/U_1}  &   s_2    &
\rOnto  &   \cdot \\
\end{diagram}
%\caption{Preservation of Quasi-needed Reductions}\label{Di.ess.}
%\end{figure}

\eproof
\end{lem}



\begin{thm}\em
\label{T.4.2.}
{\bf (Relative Hypernormalization)} Let $\reg$ be a regular stable set of
terms in a stable DRS $R$, and let $t\not\in \reg$ be a term in $R$. Then
\ben
\item[(1)] $t$ contains at least one $\reg$-needed redex.

\item[(2)] $t$ has an $\reg$-normal form  iff it does not possess a reduction in
which infinitely many times $\reg$-needed redexes are contracted.
\een

\bproof
\ben
\item[(1)] By \Dr{D.rel.need.} if $t$ is not $\reg$-normalizing, and by
\delete{\Cr{T.4.1.}} \Lr{L.4.4.} otherwise.

\item[(2)]
\ben
\item[\suf] Let $t\dored{P}s\in \reg$. Suppose on the contrary that there is an
$\reg$-quasi-needed $Q$ starting from $t$. Then by \Lr{L.4.5.} $Q/P$ is
$\reg$-quasi-needed as well -- a contradiction, since all terms of $Q/P$
are in $\reg$, by the closure of $\reg$ under reduction, and therefore
$Q/P$ must be $\reg$-unneeded.

\item[\nec] By (1), one can repeatedly
contract $\reg$-needed redexes in $t$, unless a term in $\reg$ is reached;
the latter is inevitable since $t$ does not have an infinite $\reg$-needed
reduction.
\een
\een
\eproof
\end{thm}

%



\begin{rem}\em
\label{R.irreg.no.hyper.}
If $\stab$ is not regular, then \Lr{L.4.4.} does not  hold. Indeed, consider
the example from~\cite{[ctrs]}: take $R=\{f(x)\ar h(f(x),f(x)),\,a\ar
b\}$ and take for $\stab$ the set of terms not containing occurrences of
$a$. It is easy to check that $\stab$ is stable, but is not regular, since
the outermost redex in $t=f(a)$ is $\stab$-unneeded, while the innermost
one is $\stab$-needed. Then the reduction $P:f(a)\ar h(f(a),f(a))\ar
h(f(b),f(a))\ar
h(f(b),h(f(a),f(a)))\ar  h(f(b),h(f(b),f(a)))\ar\ldots$ is
$\stab$-quasi-needed, while the $\stab$-needed part $Q:f(a)\ar f(b)$ of
$K(P)$ is $\stab$-normalizing, and $P/Q=f(b)\ar h(f(b),f(b))\ar
h(f(b),h(f(b),f(b)))\ar\ldots$ is $\stab$-unneeded, thus not
$\stab$-quasi-needed any more. Because of that, the proof of \Lr{L.4.5.}
fails, and the $\stab$-needed strategy need not be hypernormalizing.
\end{rem}







\section{Relative Normalization and Optimality in Deterministic Family
Structures}
\label{S.rn.fs.}


In order to generalize the \rn\ theorem to all stable sets in DRSs, and to
prove a Relative Optimality theorem, we
introduce \emph{Deterministic Family structures} (DFSs)
by defining a notion of \emph{family}
in a DRS, and by imposing some axioms on the \emph{contribution}
relation on families. This enables us to repeat the proof of the \rn\
theorem in~\cite{[ctrs]} for all DFSs, and makes explicit the properties of
family relation needed to develop an abstract theory of optimal
normalization.

\bdl{D.DRS.}
{\bf (Deterministic Family Structure)} A \emph{Deterministic Family Structure}
(DFS) is a triple $\calF =(\calR,\fami,\contr)$, where $\cal R$ is a DRS;
$\fami$ is an equivalence  relation on redexes with \emph{histories}; and
$\contr$ is the
\emph{contribution} relation on co-initial families, defined as follows:

\ben
\item[(1)]  For any co-initial reductions $P$ and $Q$, a redex $Qv$ in the final
term of $Q$ (read as $v$ \emph{with history} $Q$) is called a \emph{copy} of
a redex $Pu$ if $P\lleq Q$, i.e.,  $P+Q/P\leeqv Q$, and $v$ is a
$Q/P$-residual of $u$; the \emph{zig-zag} relation $\zfami$ is the symmetric
and transitive closure of the copy relation. The \emph{family}
relation $\fami$ is an equivalence relation among redexes with histories
containing $\zfami$. A \emph{family} is an equivalence class of the family
relation; families are ranged over by $\phi,\psi,\ldots$. $Fam(\,\,)$
denotes the family of its argument.


\item[(2)] Further, $\fami$ and $\contr$ satisfy the following axioms:
\bds
\item[{\rm [initial]}] Let $u,v\subt t$ and $u\not= v$, in $\cal R$.
Then $Fam(\emptyset_t u) \not=Fam(\emptyset_t v)$, where $\emp_t$ is the
empty reduction starting from $t$.

\item[{\rm [contribution]}] $\phi\contr \phi'$ iff for any $Pu\fin \phi'$, $P$
contracts at least one redex in~$\phi$.

\item[{\rm [creation]}] Let $e\dored{P}t\red{u}s$, and let $u$ create
$v\subt s$. Then  $Fam(Pu)\contr Fam((P+u)v)$.

\item[{\rm [FFD]}] (\emph{Finite Family Developments}) Any reduction that
contracts redexes of a finite number of families is
terminating.\footnote{This axiom is called [termination]
in~\cite{[rndrs]}.}
\eds
\een
\ed


Note that the [contribution] can be viewed as a definition of $\contr$
rather than as an axiom. Hence sometimes we will consider a DFS as a pair
${\cal F} =({\cal R},\fami)$.


One can check that all the existing definitions of family relation in the
literature~\cite{[levy],[Kl.CRS],[K.S.],[Mar],[AL],[Oos]} satisfy the above
axioms, thus our definition is consistent. Indeed, validity of the first
three axioms follow immediately from the structure of labels in the
labelling definitions of these families. The axiom [FFD] had been proved
separately for all the above systems using the syntax
in~\cite{[levy],[Kl.CRS],[Oos97]}. An axiomatic approach to [FFD] is
developed in~\cite{[Mel.th]}, but it is not fully general as for example it
does not apply to all orthogonal higher-order or graph rewriting
systems~\cite{[Oos97],[Mel.th]}. Since there are many different (and
perhaps incompatible) ways to construct a DFS from a stable DRS, and since
we want to be as general as (reasonably) possible, here we do not
investigate any further finer axiomatizations of the residual relation that
would imply [FFD]. The reason for considering more notions of family than
just the zig-zag is that we want to be more flexible and able to consider a
large class of sharing mechanisms as legal. Further, there are well-behaved
sharing mechanisms, such as the one in~\cite{[AL]}, that are strictly
larger than zig-zag (when we regard the reduction system as a DRS). We will
comment on this below. Moreover, as we will see, our sharing concept has
the nice property of compositionality, facilitating study of complex
concepts of family.


Despite its generality, our family concept does not cover all
possible sharing concepts studied in the literature. For example, consider
the TRS from~\cite{[H.P.]} for computing Fibonacci numbers, having the
following three rules: $fib(0)\ar 0,\,fib(succ(0))\ar succ(0)$ and
$fib(succ(succ(n)))\ar fib(succ(n))+fib(n)$, and rules for functions
$0,succ$ and $+$; and consider the reduction:
\begin{center}
\begin{tabular}{rl}
              & $fib(succ^4(0))$      \\
 $\ar$        & $fib(succ^3(0))+fib(succ^2(0))$   \\
 $\ar$        & $fib(succ^2(0))+fib(succ^1(0))+fib(succ^2(0))$    \\
 $\ar$        & $\ldots$    \\
\end{tabular}
\end{center}
In the Jungle Graph
implementation of that TRS~\cite{[H.P.]} (which allows `accidental' sharing
of possibly completely unrelated graphically equal subterms), it is
possible to share the two occurrences of $fib(succ^2(0))$ in the last term,
but (by [contribution]) the two occurrences cannot be considered as
members of a same family since (by [creation]) they have different
contributor families.



Let us call $\con{\phi}=\{\phi_i\,\,\vert\,\,\phi_i\contr \phi\}$ the
\emph{cone} of $\phi$. It follows immediately from the family axioms that:


\bpl{P.fam.prop.}
In any DFS ${\cal F}$:
\bds
\item[{\rm [irreflexivity]}] $\phi\not\contr \phi$.

\item[{\rm [transitivity]}] If $\phi\contr \phi'$ and $\phi'\contr \phi''$,
then $\phi\contr \phi''$.


\item[{\rm [cone]}] $\phi\contr\psi\imply \con{\phi}\subset \con{\psi}$.
(i.e.,  $\con{\phi}\subseteq \con{\psi}$ and $\con{\phi}\not=
\con{\psi}$).


\item[{\rm [finiteness]}] For any $\phi$, $\con{\phi}$ is finite, and
$\con{\emptyset_t u}=\emptyset$ for any $u\subt t$.


\item[{\rm [antisymmetry]}] If $\con{\phi}= \con{\psi}$ and $\phi\not=\psi$,
then $\phi\not\contr \psi$ (and $\psi\not\contr \phi$).
\eds

\bproof
[irreflexivity], [transitivity], and [finiteness] follow immediately from
[contribution].  [cone] follows from [irreflexivity] and [transitivity].
[antisymmetry] follows from [cone].
\eproof
\ep


The following example shows that, in a stable DRS with $\fami$ and
$\contr$, [initial], [creation] and [contribution] do not imply~[FFD].


\begin{ex}\em
\label{E.sta.no.fa.st.}
 Consider the ARS $R$ given by the figure below,
where the redex $x$ creates $u$ and $v$; $u_1$ and $u'_{2a}$ create $w$;
$v/u=v'$; $u/v=\{u_1,u_2\}$; $u_1/u_2=u'_1$, $u_2/u_1=u'_2$;
$u'_2/w=\{u'_{2a},u'_{2b}\}$; $w/u'_2=\emptyset$,
$u'_{2a}/u'_{2b}=\emptyset$, $u'_{2b}/u'_{2a}=u'_2$. All the $u$s are
residuals of $u$, hence belong to the same family $\phi_u$. Similarly, $v$ and
$v'$ must be in the same family too, say $\phi_v$. Further, take
$\phi_x=\{x\}$, take for
$\phi_w$ the set of all contracted $w$s (with histories), and define the
contribution
relation on $\phi_x,\phi_u, \phi_v,\phi_w$ by $\phi_x\contr \phi_v,\phi_u$
and $\phi_u\contr \phi_w$. Since the only
infinite reduction goes through the cycle infinitely many times, and each
time the contracted $w$ is \emph{created} by $u'_{2a}$, all developments
in the figure are terminating.
It remains to note that [FD] and the other family axioms but [FFD]
 are satisfied too. Note that the DRS $R$ is stable.
%\begin{figure}
\begin{diagram}[height=1.6em,width=1.6em]
& \rTo^x & \cdot  & & \rTo^v     &              & \cdot &              & \\
&        &        & &            & \ldTo_{u_2}  &       & \rdTo_{u_1}  & \\
&        & \dTo^u & & \cdot      &              &       &              &
\cdot & \pile{\rTo^w \\ \lTo_{u_{2a}'}} &             & \cdot \\
&        &        & &            & \rdTo^{u_1'} &       & \ldTo^{u_2'} &
&         & \ldTo_{u_{2b}'} \\
&        & \cdot  & & \rTo_{v'} &              & \cdot &              &
\pile{\rTo^{\emptyset} \\ \lTo_{\emptyset}}  & \cdot \\
\end{diagram}
%\caption{Independence of the axiom [FFD]}\label{non-hyper}
%\end{figure}
\end{ex}


\bll{L.drs.stab.pdrs.}
Any DFS ${\cal F}$ is a stable DRS.

\bproof
We want to show that if $u,v\subt t$ are different redexes, $t\red{u}e$,
$t\red{v}s$, $e\dored{v/u}o$, and $u$ creates a redex $w\subt e$, then the
redexes in $w/(v/u)\subt o$ are not $u/v$-residuals of redexes of $s$.
\delete{(see Figure~\ref{elem-diag})} By axioms [creation] and
[contribution], for any redex $w'\subt s$, $\con{Fam(w')}=\emptyset$ if
$w'$ is not a created redex, and $\con{Fam(w')}=\{Fam(v)\}$ otherwise; and
$\con{Fam(w)}=\{Fam(u)\}$. Hence the redexes in $w/(v/u)$ and $s$ are in
different families by [initial], and the lemma follows (since
$\zfami\ssq\fami$).
\eproof
\el



The following example shows that a DRS with $\fami$ and $\contr$ relations
satisfying all DFS axioms but [initial]  need
not be stable.

\begin{ex}\em
\label{E.fs.no.sta.}
Consider the DRS $R$ given by the figure below, where $w$ and $w'$
are created by $u$ and $v$, respectively, $u/v=u'$, $v/u=v'$,
$w/v'=w'/u'=w^*$. Then the sets $U=\{u,u',v,v'\}$ and $W=\{w,w',w^*\}$ with
the contribution relation $U\contr W$ do satisfy the DFS axioms except for
[initial], but the underlying
DRS $R$ is not stable.
%
%\begin{figure}
\begin{diagram}[height=1.6em,width=1.6em]
 t      & \rTo^u       & e             & \rTo^w           & o^*  \\
 \dTo^v &              &  \dTo_{v'}  &                 & \dOnto^{\emptyset}\\
s       & \rTo_{u'} & o              &                  &    \\
\dTo^{w'}  &            &                &  \rdOnto_{w^*}  &   \\
o^*     & \rOnto^{\emptyset} &            &                   &  o^*  \\
\end{diagram}
%\caption{Stability and the Property [initial]}\label{F.stab.init.}
%\end{figure}
\end{ex}





\begin{lem}\em
\label{L.4.1.c.}
Let $\stab$ be stable, let $t\not\in \stab$, let $t\red{u}t'$, let $u$ be
$\stab$-unneeded,  and let $u'\subt t'$ be a redex created by $u$, in a
DFS ${\cal F}$. Then  $u'$ also is $\stab$-unneeded.

\bproof
By \Lr{L.4.1.c.stab.}  and \Lr{L.drs.stab.pdrs.}.
\eproof
\end{lem}



Now we can generalize the RN theorem, proved in~\cite{[ctrs]} for
orthogonal ERSs, to all DFSs. We now allow for arbitrary
stable sets $\stab$.

Below $FAM(P)$ denotes the set of families (whose member redexes are)
contracted in $P$.

\begin{thm}\em
\label{T.ex.M-need.}
{\bf (Relative Normalization)} Let $\stab$ be a stable set of terms in
a DFS~$\cal F$, and let $t\not\in \stab$ be $\stab$-normalizable. Then
\ben
\item[(1)] $t$ contains an $\stab$-needed redex.

\item[(2)] Any $\stab$-needed reduction starting from $t$
eventually terminates at a term in~$\stab$.
\een

\bproof
\ben
\item[(1)] Let $P:t\doar s'\ar s\red{u}e$ be an $\stab$-normalizing, and let
$s\not\in \stab$. By the stability of $\stab$, $u$ is $\stab$-needed. By
\Lr{T.3.1.c.} and Lemma~\ref{L.4.1.c.}, $u$ is either created by
or is a residual of an $\stab$-needed redex of $s'$, and (1) follows by
repeating the argument.

\item[(2)] Let $P:t\doar s$ be an $\stab$-normalizing reduction and
$Q:t\red{u_0}t_1\red{u_1}\ldots$ be an $\stab$-needed reduction. Further,
let $Q_i:t\red{u_0}t_1\red{u_1}\ldots\red{u_{i-1}}t_i$ and $P_i=P/Q_i$
$(i\geq 1)$  (see the figure below). By $\zfami\ssq\fami$,
$FAM(P_i)\ssq FAM(P)$. Since $Q$ is $\stab$-needed and $P_i$ is
$\stab$-normalizing (by the closure of $\stab$ under parallel moves), at
least one residual of $u_i$ is contracted in $P_i$. Therefore, again by
$\zfami\ssq\fami$, $Fam(u_i)\in FAM(P_i)$. Hence $FAM(Q)\ssq FAM(P)$ and
$Q$ is terminating~by [FFD].
%
%\begin{figure}
\begin{diagram}[height=1.5em,width=4em]
  t            & \rOnto^{P}   &   s     \\
 \dOnto^{Q_i}   &              &     \dOnto \\
 t_i           & \rOnto_{P_i}&  \cdot          \\
\dTo^{u_i}     &              &     \dOnto \\
t_{i+1}        & \rOnto_{P_{i+1}}&  \cdot    \\
\dOnto          &              &     \dOnto \\
 \cdot          & \rOnto       &  \cdot         \\
\end{diagram}
%\caption{Termination of Needed Reduction}\label{term-need}
%\end{figure}
\een
\eproof
\end{thm}


Note that we have not used the acyclicity axiom in the proofs. However, it is
necessary and sufficient to insure that the set of normal forms is stable. Note
also that only by using \Tr{T.ex.M-need.} can we prove the analogue of
\Lr{L.pers.need.} for all stable~$\stab$.



\begin{lem}\em
\label{L.3.3.c.}
 Let $\stab$ be a stable set of terms in a DFS ${\cal F}$, and let
$t\red{u}s$. Then any $\stab$-needed redex $v\subt t$ different from $u$
has an $\stab$-needed residual in~$s$.

\bproof
Same as the proof of \Lr{L.pers.need.}, but using \Tr{T.ex.M-need.} instead
of \delete{\Cr{T.4.1.}} \Lr{L.4.4.}.
\eproof
\end{lem}




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


We now define \emph{weakly $\stab$-needed} redexes, and show
that their contraction in an $\stab$-normalizable term $t$ leads to an
$\stab$-normal form of $t$. We also generalize L\'evy's
Optimality theorem~\cite{[le80]} to all stable sets $\stab$ in any DFS.


\bd
We call a family $\phi$ relative to $t$ \emph{$\stab$-needed} if any
reduction from $t$ to a term in $\stab$ contracts at least one member of
$\phi$. We call redexes in $\stab$-needed families \emph{weakly
$\stab$-needed}.

\ed


\delete{
\begin{defn}\em
\label{D.weak.need.}
Let $P:t\red{u_0}t_1\red{u_1}t_1\ldots\red{u_{n-1}}t_n$ in an
FS ${\cal F}$, and let $\stab$ be a set of terms of $R$. We call $u\in
t_i$ \emph{weakly $\stab$-needed w.r.t. $t\red{u_0}t_1\red{u_1}t_1\ldots\ar
t_i$} if $u$ is in the family of an $\stab$-needed redex occurring in some
$t_j$. A reduction is \emph{weakly $\stab$-needed} if each redex
contracted in it is (w.r.t. the initial reduction).
\end{defn}
}


\begin{thm}\em
\label{T.cor.weak.need.}
Let $\stab$ be a stable set of terms in a DFS ${\cal F}$, and let $t$ be an
$\stab$-normalizable term in $\cal F$. Then any weakly $\stab$-needed
reduction starting from $t$ is terminating.

\bproof
By [FFD], since there is only a finite number of $\stab$-needed
families relative to $t$ (the number does not exceed the length of any
$\stab$-normalizing reduction starting from $t$).
\eproof
\end{thm}


The above theorem allows one to propagate
$\stab$-neededness information, obtained from earlier terms, along the
reduction, and to contract safely (without a danger of missing an
$\stab$-normal form whenever it exists) any residual of an $\stab$-needed
redex, even if it is no longer $\stab$-needed.



\begin{defn}\em
A multistep reduction $P:t_0\doar t_1\doar\ldots\doar t_n$ is
called a \emph{family-reduction} if each $P_i:t_i\doar t_{i+1}$ is
a development of a set $U_i$ of redexes belonging to the same
family. $\Vert P\Vert$ will denote the number of multisteps in
$P$. The family-reduction $P$ is \emph{complete} if each $P_i$ is
the complete development of a maximal set of redexes of $t_i$
belonging to the same family. A family-reduction $P$ is called
\emph{$\stab$-needed} if each $U_i$ contains at least one $\stab$-needed
redex (i.e., if the (single-step) reduction corresponding to  $P$
is weakly $\stab$-needed).

\end{defn}



\begin{cor}\em
Let $\stab$ be a stable set of terms
in a DFS ${\cal F}$. Then any  $\stab$-needed
family-reduction starting from an $\stab$-normalizable term is
eventually $\stab$-normalizing.
\end{cor}



\begin{lem}\em
\label{L.fam.compl.}
{\bf (Unique Families)} Every family is contracted at most once in a complete
family-reduction.

\bproof
Let $P_n:t_0\dored{U_0}t_1\dored{U_1}\ldots \dored{U_{n-1}}t_n$
be a complete family-reduction. We show by induction on $n=\Vert
P\Vert$ that $(a)_n$: all families contracted in $P_n$ are
different; and $(b)_n$: there is no redex in $t_n$ whose family
has been contracted in $P_n$.  The
case $n=0$ is clear. Further, $(a)_n$ follows immediately from
$(a)_{n-1}$ and $(b)_{n-1}$. Again by $(a)_{n-1}$ and
$(b)_{n-1}$, and by the completeness of $P_n$, all redexes in $t_n$ that
are residuals of redexes of $t_{n-1}$ are in families that have not been
contracted
before. By [creation], for the family $\phi$ of a created redex in $t_n$, we
have $Fam(U_{n-1})\contr \phi$; by $(a)_{n-1}$, $(b)_{n-1}$, and
[contribution], $Fam(U_{n-1})\not\contr Fam(U_i)$, for any $i\leq n-1$.
Hence $\con{Fam(U_i)}\not=\phi)$, and $(b)_n$ follows.
\eproof
\end{lem}




\begin{thm}\em
\label{T.unif.opt.}
{\bf (Relative Optimality)}
Let $\stab$ be a stable set of terms in a DFS~${\cal F}$, and let $t$ be an
$\stab$-normalizable term in $\cal F$. Then any  $\stab$-needed
$\stab$-normalizing complete family-reduction $Q:t\doar e\in\stab$ is
$\stab$-optimal in the sense that it has a minimal number of
family-reduction steps.

\bproof
As in the
$\lambda$-calculus~\cite{[le80]}. Let $P:t\doar s$ be an
$\stab$-normalizing family-reduction. It follows from the proof
of Theorem~\ref{T.ex.M-need.} that $FAM(Q)\subseteq FAM(P)$
(see the figure for Theorem~\ref{T.ex.M-need.}).
Hence, by Lemma~\ref{L.fam.compl.}, $\Vert
Q\Vert=n(FAM(Q))\leq n(FAM(P))\leq\Vert P\Vert$, where
$n(FAM(Q))$ denotes the number of families in $FAM(Q)$.
\eproof
\end{thm}





\section{Equivalence of Zig-zag and Extraction in ASDRSs}
\label{S.zi.ext.}


In this section, we introduce an abstract extraction algorithm for ASDRSs
and show that zig-zag related redexes (with histories) have the same
canonical representatives w.r.t. extraction, up to an equivalence on
histories. These canonical representatives are obtained as normal forms of
redexes with histories $Pv$ w.r.t. the extraction procedure, which
eliminates all steps of histories $P$ that do not `contribute' to the
family of $v$.


L\'evy introduced an extraction procedure for the \lc\
in~\cite{[levy],[le80]} in order to prove decidability of the family
relation. His extraction procedure is effective, and gives canonical
representatives of families, which are unique, thus implying the
decidability of the family relation. For higher order rewrite systems whose
reduction steps are more complicated, there are two conceptually different
extensions of L\'evy's extraction algorithm. The first is due to
Asperti and Laneve~\cite{[AL]}, and the second to van
Oostrom~\cite{[Oos]}.

A `problem' arises because a redex can create a number of
redexes `intuitively' in the same family without the help of
previous steps, something which cannot happen in the \lc\
or term rewriting.  That these redexes are intuitively in the same
family, can be seen after decomposing the rewrite step into two parts --
the \emph{TRS part} that only creates new symbols, and the
\emph{substitution part}, that performs all (often nested) substitutions.
The substitution part can duplicate or erase the redexes created during the
TRS part, and all substitution copies of a redex created by the TRS-part
are viewed to belong
to the same family, as labels of such redexes are the same. Such redexes
cannot be related by the zig-zag if one works with the original
system~\cite{[AL]}, but can be related if one works in the refinement of
the original system~\cite{[Oos]}. Now, the difference between the two
approaches is that Asperti and Laneve decided to accept the inadequacy
of the zig-zag, but extended L\'evy's extraction algorithm by the
\emph{shift} operation which relates all copies of the simultaneously
created redexes of the same family to a canonical representative, thus
making extraction match the labelling; the resulting family-relation is
non-separable. On the contrary, van Oostrom
works with the refined rewrite systems and no operation like shift is necessary
to ensure coincidence of labelling, extraction and zig-zag families.
Since we want to define an extraction procedure adequate for zig-zag,
we do not need an operation modelling \emph{shift}. Our results in
Section~\ref{S.impl.drs.} will shed further light on the separability
problem.




We start by studying standard reductions in ASDRSs. Our standardization
concept differs from the usual `left-to-right and outside-in' concept of
standardization in the \lc~\cite{[C.F.]}. Our standard reductions are
simply `self-needed' reductions -- reductions in which every step
essentially contributes to the whole computation -- since we do not have
any nesting relation imposed on redexes, unlike in ARSs~\cite{[GLM]}, and
there is no concept of `left' or `right' occurrences in DRSs. However, our
concept of standardization captures the essence of the usual one in many
respects. In particular, in the extraction process which we study below,
self-needed reductions play the same role as left-to-right outside-in
standard reductions in the extraction processes
of~\cite{[le80],[AL],[Oos]}. For a theory of standardization for stable
DRSs in general, see~\cite{[dndrs],[dndrs-rep]}. And for an `outside-in
theory' of standardization in ARSs with axiomatized nesting relation,
see~\cite{[GLM],[Mel.th]}.



\bdl{D.red.need.ess.}
\begin{itemize}
\item   Let $P:t\doar o$ and $u\subt t$, in a DRS.  We call $u$
\emph{erased} in $P$ or \emph{$P$-erased} if $u/P=\emp$. We say that $P$
\emph{discards} $u$ if $P$ is external to $u$ and erases it.

\item  We call $u$ \emph{$P$-needed} if there is no
$Q\leeqv P$ that is external to $u$, and call it \emph{$P$-unneeded}
otherwise. We call $u$ \emph{$P$-essential} if there is no $Q\leeqv P$
that discards $u$, and \emph{$P$-inessential} otherwise.

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

\item Let $Q:t\doar o$, $P:t\dored{P'}s\doar e$, and $u\subt s$. We
say that $u$ is $Q$-needed, or more precisely, $P'u$ is $Q$-needed, if $u$
is $Q/P'$-needed. We call $P$ \emph{$Q$-needed} if every redex contracted
in $P$ is. We call $P$ \emph{self-needed} or \emph{standard} if it is
$P$-needed.
The other concepts above are extended in the same way.
\end{itemize}
\ed



Note 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$, since $u/P=u/Q$ when $P\leeqv Q$. The
\emph{external} and \emph{discards} concepts however do depend on the
particular reduction in the \Lc\ class.



\bll{L.era.and.ess.im.ne.}
Let $P:s\doar t\red{u}e\dored{P'} o$ in an ASDRS.
\ben
\item[(1)] $w\in t$ is $P$-needed iff it is $P$-erased and $P$-essential.

\item[(2)] If $P:t\doar s'\red{w'}o$, then $w'\in s'$ is $P$-needed.

\item[(3)] If $u$ creates $v\subt e$ and is $P$-unneeded (resp.
$P$-inessential), then so is $v$.

\item[(4)] If $u\not=v\subt t$, then $v$ is $P$-needed ($P$-essential) iff
it has a $P$-needed ($P$-essential) residual~in~$e$.
\een

\bproof
\ben
\item[(1)]
\ben
\item[\suf] Immediate (since $P$ is non-duplicating and any $Q\leeqv P$
contracts a residual of $w$).

\item[\nec] If on the contrary $w$ was $P$-unneeded, then there would be a
reduction $Q\leeqv P$ that is external to $w$, and $Q$ erases $w$ (since
$w$ is erased in $P$ and $P\hieq Q$), contradicting $P$-inessentiality of
$w$.
\een

\item[(2)] By \Lr{L.ext.lem.mult.} (Acyclicity Lemma), there is no $Q:s\doar o$
such that $Q$ is external to $w'$ and $Q\leeqv w'$. Hence $w'$ is
$w'$-needed, i.e., is $P$-needed.


\item[(3)] If $u$ is $P$-unneeded, then it is $P$-inessential by~$(1)$.
Hence there is $Q_t\leeqv u+P'$ that discards
$u$. By \Lr{L.disj.red.creat.} (Stability Lemma), $Q_e=Q_t/u$ is
external to $v$, and $Q_e\leeqv P'$. Hence $v$ is
$P$-unneeded. Furthermore, by \Lr{L.disj.red.creat.} and $u/Q_t=\emptyset$,
we have $v/Q_e=\emptyset$, i.e., $v$ is $P$-inessential.
\suppress{
In order to show that $v$ is , it is enough to
show that . 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'}& o\\
\cdot  &       & &\dTo<{Q_t} &         &\dTo>{Q_e} &\\
\cdot  &       & & \cdot         & \rOnto_{\emptyset} & \cdot     & \\
\end{diagram}
}

\item[(4)]
\ben
\item[\suf] If on the contrary $v/u=\emp$, then $u+P'$ would discard $v$,
contradicting $P$-neededness (resp. $P$-essentiality) of $v$. So let $v'$
be the only $u$-residual of $v$. 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.

\item[\nec] Let $v$ have a $P$-needed residual $v''\in e$. If on the
contrary $v$ is $P$-unneeded, there is $Q_t\leeqv u+P'$ that is external to
$v$. Hence $u/Q_t=\emptyset$ (since $u/(u+P')=\emptyset$) and
$Q_e=Q_t/u\leeqv P'$. By
\Lr{L.external.rem.ext.}, $Q_e$ is external to $v''$, contradicting its
$P$-neededness. Now let $v''$ be $P$-essential. If $v$ is $P$-inessential,
then some $Q_t\leeqv u+P'$ discards it, and $v''/(Q_t/u)=\emp$ since
$Q_t\hieq u+Q_t/u$, i.e., $Q_e$ discards $v''$, contradicting
$P$-inessentiality of $v''$.
\een
\een
\eproof
\el



The following is a standardization procedure for reductions in ASDRSs.


\bdl{D.ess.rel.red.}
Let $P:t\doar s$. The {\em canonical standard variant of $P$},
$ST(P)$, is defined as follows: If $P=\emp$, then so is $ST(P)$. Otherwise,
let $v\subt t$ be such that it is $P$-needed and its residual is contracted
in $P$ first among $P$-needed residuals of $P$-needed redexes in $t$
(existence of such $v$ follows from \Lr{L.era.and.ess.im.ne.}). Then
$ST(P)=v+ST(P/v)$.
\ed



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

\bproof
Termination of the standardization follows immediately from the fact that,
in the above definition, $\leng{P/v}\leq\leng{P}-1$, and we have
immediately from the construction that $P\leeqv v+P/v\leeqv\ldots\leeqv
ST(P)$.
\eproof
\et

We write $P\staeq Q$ if $P\leeqv Q$ and both $P$ and $Q$ are standard.
For any standard $P$, we define $\sclas{P}=\{Q\,\vert\,Q\staeq P\}$.
Further, we write $Q\in\stav{P}$ if $Q\in\stan$ and $Q\leeqv P$, where $\stan$
denotes the set of all standard reductions, and call $Q$ a \emph{standard
variant} of $P$. Note that \Lr{L.era.and.ess.im.ne.} gives an algorithm of
construction of a standard variant of any finite reduction
$P:t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{n-1}}t_n$ in an ASDRS. Indeed, the
last step $u_{n-1}$ of $P$ is $P$-needed by \Lr{L.era.and.ess.im.ne.}.(2).
If it is created by $u_{n-2}$, then the latter is $P$-needed too, by
\Lr{L.era.and.ess.im.ne.}.(3). Otherwise, the ancestor redex of $u_{n-1}$ in
$t_{n-2}$ is $P$-needed by \Lr{L.era.and.ess.im.ne.}.(4). Similarly, we can
trace the `responsible' redex of $u_{n-1}$ in $t_0$, which is $P$-needed.
Repeated contraction of $P$-needed redexes terminates, and yields a
standard variant of $P$; this can be shown exactly as the correctness of
the standardization procedure in \Tr{L.fin.self.ese.var.}. The next
proposition shows that, moreover, all standard variants of a finite
reduction $P$ in an ASDRS can be found effectively (there are clearly only
a finite number reductions in $\stav{P}$ as they all have the same length,
which coincides with the number of $P$-needed steps in $P$).


\bpl{P.dec.stan.}
For any finite reduction $P$ in an ASDRS, $P$-neededness of redexes in all
terms of $P$ is decidable. Consequently, any standard variant of $P$ can be
constructed efficiently (in particular, the standardization procedure of
$P$ is computable).

\bproof
Let $P:t_0\red{u_0}t_1\red{u_1}\ldots \ar t_n$. $P$-(un)neededness of any
redex in a term $t_i$ can be established by induction on $n=\leng{P}$, as
follows. If $n=1$, then only the contracted redex $u_0$ is $P$-needed in
$t_0$ by \Dr{D.red.need.ess.} and \Lr{L.era.and.ess.im.ne.}.(2). Let $n>1$,
and let $P_1:t_1\red{u_1}t_2\red{u_2}\ldots \ar t_n$. We can assume to have
found all the $P$-needed redexes in all $t_i$ with $i\geq 1$, since
$P$-neededness in these terms coincides with $P_1$-neededness by
\Dr{D.red.need.ess.} (and $\leng{P_1}=n-1$). Then a redex in $t_0$
different from $u_0$ is $P$-needed iff it has such a residual in $t_1$, by
\Lr{L.era.and.ess.im.ne.}.(4). If $u_0$ does not create $u_1$, then they
can be permuted. If $u_1=u'_1/u_0$ and $u'_0=u_0/u'_1=\emp$, then $u_0$ is
$P$-unneeded by \Dr{D.red.need.ess.}; otherwise, if $u'_0\not= \emp$, by
the induction assumption, we can assume to know whether or not $u'_0$ is
needed w.r.t. $P'=u'_0+u_2+\ldots+u_{n-1}$, and $u_0$ is $P$-needed iff
$u'_0$ is $P'$-needed. Finally, if $u_0$ creates $u_1$, we can standardize
$P_1$, or construct a standard variant $P'_1$ of $P_1$; then if $u_0$ still
creates the first step of $P'_1$ (which is $P$-needed by
\Dr{D.red.need.ess.}),  then $u_0$ is
$P$-needed by \Lr{L.era.and.ess.im.ne.}.(3); if not, then we arrive to a
previously considered case, and the decidability of $P$-neededness follows.
The rest follows from the correctness of the construction of a standard
variant of $P$ discussed above.
\eproof
\ep



\bdl{D.can.re.his.}
Let $P:t\doar s$ in an ASDRS, and let $v\subt s$. We call $Pv$
\emph{standard} if so is $P$. We call $Pv$ \emph{canonical} if it is
standard and, for any $Q\leeqv P$, the last step in $Q$ creates $v$.
\ed


Note that if $P\staeq P'$, then $Pv$ is canonical iff so is $P'v$. So
canonical forms we speak of are actually objects $\sclas{P}v$, for standard
finite reductions $P$. Our extraction algorithm, defined in \Dr{D.ext.}
below,  transforms any redex with history into a canonical one, and the main
result of this section is that redexes are zig-zag related iff they have
the same canonical form.



\bll{L.sta.ex.dec.}
Let $Q:t\dored{P}s\red{u}e$, where $u$ does not create $v\subt e$. Then
there is a standard $Q'\leeqv Q$ such that $Q':t\dored{P'}s'\red{u'}e$,
where $P'u'\zleq Pu$ and $u'$ does not create $v$.

\bproof
We show that $ST(Q)$ can be taken for $Q'$. By \Dr{D.ess.rel.red.}, $ST(Q)$
is obtained from $Q$ by a sequence of transformations $Q=Q_1,Q_2,\ldots,
Q_n=ST(Q)$ such that $Q_{i+1}$ is obtained from $Q_i$ by permuting the
first $Q$-needed step that has preceding $Q$-unneeded steps before those
$Q$-unneeded steps (all $Q_i$ are L\'evy-equivalent). Since $u$ is the last
$Q$-needed step in $Q$ by \Lr{L.era.and.ess.im.ne.}.(2), any $Q_i$ with
$i<n$ has the form $P_i+u$ such that $P_i\leeqv P$, and $P_{n-1}$ has the
form $P_{n-1}:t\dored{P'}o\dored{P''}s$ where $P'$ is $Q$-needed and $P''$
is $Q$-unneeded. By \Lr{L.era.and.ess.im.ne.}.(3), $P''$ cannot create $u$,
i.e., there is $u'\subt o$ such that $u'/P''=u$, and $u'$ is $Q$-needed by
\Lr{L.era.and.ess.im.ne.}.(4) (see the diagram). Since $P''/u'$ is
$Q$-unneeded by \Lr{L.era.and.ess.im.ne.}.(4), and since the last step of
$P'+u'+P''/u'$ is
$Q$-needed by \Lr{L.era.and.ess.im.ne.}.(2), $P''/u'=\emp$. Since $u'$ is
$Q$-needed and $P''$ is $Q$-unneeded, $P''$ is external to $u'$ by
\Lr{L.era.and.ess.im.ne.}.(4). Hence, by the Stability Lemma, $u'$ does not
create $v$, and the lemma follows since $ST(Q)=P'+u'$ is standard by
\Tr{L.fin.self.ese.var.}, and $P'u'\zleq Pu$ since $u=u'/P''$.
\begin{diagram}[height=1.4em,width=1.4em]
t       &\rOnto^{P'} & o     &\rOnto^{P''}  & s      &\rTo^{u} & e\ni v \\
         &         &\dTo<{u'} &          & \dTo>u &        & \dOnto_\emp \\
{}      &       & v\in e     &\rOnto_\emp & e\ni v &\rOnto_\emp     &e\ni v  \\
\end{diagram}
\eproof
\el



It follows from \Dr{D.can.re.his.}, \Pr{P.dec.stan.} and \Lr{L.sta.ex.dec.}
that it is decidable whether a redex with history $Pv$ is canonical. And if
$Pv$ is not canonical, one can effectively find a reduction
$Q:t\dored{P'}e\red{u}s$ such that $Q\in\stan{P}$ and $u$ does not create
$v$. In the search for a shortest
reduction that creates a redex in the zig-zag class of $Pv$, contraction of
$u$ in $Q$ can be omitted -- $P'v'\zfami Pv$ and $\leng{P'}<\leng{P}$, since all
standard L\'evy-equivalent reductions have the same (minimal)
length~\cite{[dndrs],[dndrs-rep]}. Obviously, reductions creating a redex
in some family in the quickest way must be standard, since they are the
shortest in
their \Le-equivalence classes. The transformation of $Pv$ into $P'v$ is
denoted by $Pv\extrr{u}P'v'$, or just $Pv\extr P'v'$.
For example, consider the ASDRS corresponding to the TRS $R=\{f(x)\ar
g(x),\, a\ar b,\,b\ar c\}$, let $P:f(a)\ar g(a)\ar g(b)$, and let $v=b$ in
$g(b)$. Then $Pv$ is not canonical, as $P\staeq Q:f(a)\ar f(b)\ar g(b)$ and
the
last step of $Q$ does not create $v$ -- the latter is the residual of
$v'=b$ in the final term of $P': f(a)\ar f(b)$. Hence we can perform an
extraction step $Pv\extr P'v'$. The latter redex is in extraction normal
form.

The formal definition of extraction is as follows:


\bdl{D.ext.}
{\bf (Extraction)}
Let $Q:t\dored{P'}e\red{u}s$ be a standard variant of $P$, in an ASDRS, and
let $v\subt s$ be a $u$-residual of $v'\subt e$.  Then we write
$Pv\extrr{u}P'v'$, and call the transformation an \emph{extraction} step.
(Note that, since $Q$ is standard, so is $P'$ by \Dr{D.red.need.ess.}.)
$\,\,\doextr$ is the transitive and reflexive closure of $\extr$.
\ed


Since in the above definition $\leng{P'}<\leng{Q}\leq\leng{P}$, the
relation $\extr$ is trivially strongly normalizing, and in order to proof
that it is confluent (modulo $\staeq$ on histories), it is enough to prove
that it is weakly (or locally) confluent, that is,
$Qw''\lextrr{v}Nw\extrr{u}Pw'$
implies $Qw''\extrr{u'}N^*w^*\lextrr{v'}Pw'$. This will be proved in
\Tr{P.on.ca.for.}. We need two lemmas first:


\bll{L.pe.fin.ste.}
Let $u+P\staeq Q+u'$, where $u'=u/Q$ and $P=v+P'$. Then $u$ does not create
$v$, and $u$ can be contracted after $v$, i.e.,  $u+v\leeqv v^* +u^*$,
where $v=v^*/u$ and $u^* =u/v^*$. Further, $v^*/Q=\emp$ and
$u'=u^*/(Q/v^*)$.

\bproof
Let $Q'=Q/u$. Since $u+P$ is standard, so is $P$ by \Dr{D.red.need.ess.},
so $v$ is $P$-needed, and since $P\leeqv Q'$, $v$ is $Q$-needed too, i.e,
$Q'$ contracts a residual $v'$ of $v$. Since $Q'$ contracts residuals of
redexes contracted in $Q$, $Q$ contracts a redex $v''$ whose residual is
$v'$. So we have the following picture:
\begin{diagram}[height=1.4em,width=1.4em]
\cdot         &\rTo^{u} & \cdot       &\rTo^{v}  & \cdot     &\rOnto^{P'}
&\cdot  \\
\dOnto     &         &\dOnto    &          & \dOnto &            &\dOnto\\
\cdot         &\rTo     & \cdot       &\rTo^{v'} & \cdot     &\rOnto
&\cdot  \\
\dTo^{v''} &         &\dTo^{v'} &          & \dOnto &            &\dOnto\\
\cdot         &\rOnto   &  \cdot      & \rOnto   & \cdot     &\rOnto
&\cdot  \\
\dOnto     &         &\dOnto    &          & \dOnto &            &\dOnto\\
Q          &\rTo_{u'}& Q'     &\rOnto_\emp & \cdot     &\rOnto      &\cdot  \\
\end{diagram}
Now, since $Q$ is external to $u$ (since $u$ has a $Q$-residual $u'$ and
the DRS is non-duplicating), we have immediately by the Stability Lemma
that both $v$ and $v''$ are residuals of some redex $v^*$ in the initial
term. Hence $u+v\leeqv v^* +u^*$, where $v=v^*/u$ and $u^* =u/v^*$. Since
$Q$ contracts a residual $v''$ of $v^*$, $v^*/Q=\emp$. Since $Q$ is
external to $u$, we have by \Lr{L.external.rem.ext.} that $Q^*=Q/v^*$ is
external to $u^*$. Since $u$ is $u+P$-needed, so is $u^*$ by
\Lr{L.era.and.ess.im.ne.}.(4). Hence $u^*$ is $Q^* +u'$-needed. Since $Q^*$
is external to $u^*$ and $Q^* +u'$ contracts a residual of $u^*$, we have
$u'=u^*/Q^*$.
\begin{diagram}[height=1.4em,width=1.4em]
\cdot       &\rTo^{v^*} & \cdot     &\rTo^{u^*}  & \cdot     &\rOnto^{P'}
&\cdot  \\
\dOnto<Q  &         &\dOnto<{Q^*} &          & \dOnto &        & \dOnto \\
\cdot      &\rOnto^\emp & \cdot       &\rTo^{u'} & \cdot     &\rOnto
&\cdot  \\
\dTo<{u'} &         &\dTo<{u'} &          & \dOnto>\emp &            & \dOnto\\
\cdot      &\rOnto_\emp   &  \cdot    & \rOnto_\emp & \cdot     &\rOnto
&\cdot  \\
\end{diagram}
\eproof
\el


\bll{L.mov.red.cre.}
Let $P +u\staeq Q +v$ and let $u\not=v$. Then there are $P'v'$ and $Q'u'$
such that $P'+v'\staeq P$, $Q'+u'\staeq Q$, $P'\staeq Q'$, $P'v'\zfami Qv$
and $Q'u'\zfami Pu$, $u=u'/v'$ and $v=v'/u'$.
\begin{diagram}[height=1.4em,width=1.4em]
\cdot     &\rOnto^{P'}  &  \cdot    &\rTo^{v'}   &\cdot  &\rTo^{u}       &
\cdot \\
\dOnto<{Q'} &        &\dOnto>\emp &        & \dOnto>\emp &  & \dOnto>\emp \\
\cdot     &\rOnto^\emp  & \cdot     & \rTo^{v'}  & \cdot  &\rTo^{u}      &
\cdot \\
\dTo<{u'}   &        &\dTo>{u'}  &         & \dTo>{u}  &    & \dOnto>\emp \\
\cdot     &\rOnto_\emp  &  \cdot    &\rTo^{v}    &\cdot  & \rOnto_\emp   &
\cdot\\
\dTo<{v}    &        &\dTo<{v}  &       & \dOnto>\emp  &      & \dOnto>\emp \\
\cdot     &\rOnto_\emp  & \cdot     &\rOnto_\emp &\cdot  & \rOnto_\emp   &
\cdot\\
\end{diagram}

\bproof
Since $P +u\staeq Q +v$, we have $v\leeqv (P+u)/Q$. By
\Lr{L.ext.lem.mult.}, $(P+u)/Q$ contracts a residual of $v$. Note
that $P\leeqv Q$ would imply $u\leeqv v$, implying by [weak acyclicity]
that $u=v$. Thus $P\not\leeqv Q$. We show that
$P/Q\not=\emp$.

\begin{diagram}[height=1.4em,width=1.4em]
\cdot          &\rOnto^{P}     & \cdot           &\rTo^{u}     & \cdot
\\
\dOnto<Q    &             &\dOnto<{Q/P}>u  &             & \dOnto_\emp  \\
\cdot          &\rOnto^{P/Q}_v & \cdot           &\rOnto_\emp    & \cdot
\\
\dTo<v      &               &\dOnto     &             &  \dOnto_\emp \\
\cdot          &\rOnto_\emp    &  \cdot          & \rOnto_\emp & \cdot
\\
\end{diagram}
Suppose on the contrary that $P/Q=\emp$. Then, $Q/P\not=\emp$ and by [weak
acyclicity], $v=u/(Q/P)$. But $P +u\leeqv Q +v$ implies
$(Q/P)/u=\emp$. Since $Q+v$ is standard, the first (and any other) step of
$Q$ whose residual, say $w$, is contracted in $Q/P$ is $u$-needed by
\Lr{L.era.and.ess.im.ne.}.(4). Hence $w/u=\emp$ implies $u=w$, and
therefore $Q/P=u$
and $u/(Q/P)=\emp$, contrary to $v=u/(Q/P)$. So $P/Q\not=\emp$. Since $P$
is $P+u$-needed (recall that $P+u$ is standard), so is $P/Q$, i.e., $P/Q$
is $v$-needed. Hence, by [weak acyclicity], the first (and the only) step of
$P/Q$ coincides with $v$, i..e., $P/Q=v$. Thus $P$ contracts a redex $v''$
whose residual is $v$. So if $P=P_1+v''+P_2$, then $(Q+v)/P_1=Q/P_1+v$, and
we have $v''+P_2+u\staeq Q/P_1+v$ and $v''+P_2\not\leeqv Q/P_1$ (see the
figure).
\begin{diagram}[height=1.4em,width=1.4em]
\cdot       &\rOnto^{P_1} & \cdot     &\rTo^{v''}  & \cdot
&\rOnto^{P_2} &\cdot
&\rTo^{u}  & \cdot \\
\dOnto<Q  &         &\dOnto  &          & \dOnto &        & \dOnto &      &
\dOnto>\emp \\
\cdot      &\rOnto^\emp & \cdot       &\rTo^{v} & \cdot     &\rOnto^\emp
&\cdot
&\rOnto^\emp      &\cdot \\
\dTo<{v} &         &\dTo<{v} &          & \dOnto_\emp &         &
\dOnto_\emp &            & \dOnto>\emp  \\
\cdot      &\rOnto_\emp   &  \cdot    & \rOnto_\emp & \cdot     &\rOnto_\emp
&\cdot  & \rOnto_\emp & \cdot\\
\end{diagram}
Now, by repeated application of \Lr{L.pe.fin.ste.}, $v''+P_2+u$ can be
transformed into a reduction $P'_2+v'+u$ such that $v''+P_2\staeq P'_2+v'$,
$v'=v''/P'_2$, and $v=v'/(Q/(P_1+P'_2))$.
\begin{diagram}[height=1.4em,width=1.4em]
\cdot       &\rTo^{P_1} & \cdot     &\rOnto^{P'_2}  & \cdot     &\rTo^{v'}
&\cdot
&\rTo^{u}  & \cdot \\
\dOnto<Q  &         &\dOnto  &          & \dOnto &        & \dOnto &      &
\dOnto>\emp \\
\cdot      &\rOnto^\emp & \cdot       &\rOnto^\emp & \cdot     & \rTo^{v}
&\cdot
&\rOnto^\emp      &\cdot \\
\dTo<{v} &         &\dTo<{v} &          & \dTo<{v}  &            & \dOnto
&          & \dOnto>\emp  \\
\cdot      &\rOnto_\emp   &  \cdot    & \rOnto_\emp & \cdot     &\rOnto_\emp
&\cdot  & \rOnto_\emp & \cdot\\
\end{diagram}
Hence, if we take $P'=P_1+P'_2$, we have that $P'+v'\staeq P$ and
$P'v'\zleq Qv$. Existence of $Q'u'$ such that $Q'+u'\staeq Q$ and
$Q'u'\zleq Pu$ can be shown similarly.  Since $P_2/(Q/(P_1+v''))=\emp$, we
have again by repeated application of \Lr{L.pe.fin.ste.} that $P'/Q\leeqv
P'/(Q'+u')\leeqv (P'/Q')/u'=\emp$. But $P'/Q'$ is external to $u'$ since
$u'$ has a $P/Q'\leeqv P'/Q'+v'/(Q'/P')$-residual (by $Q'u'\zleq Pu$).
%\begin{figure}
\begin{diagram}[height=1.4em,width=1.4em]
\cdot     &\rOnto^{P'}  &  \cdot    &\rTo^{v'}   &\cdot  &\rTo^{u}       &
\cdot \\
\dOnto<{Q'} &        &\dOnto>\emp &        & \dOnto>\emp &  & \dOnto>\emp \\
\cdot     &\rOnto^\emp  & \cdot     & \rTo^{v'}  & \cdot  &\rTo^{u}      &
\cdot \\
\dTo<{u'}   &        &\dTo>{u'}  &         & \dTo>{u}  &    & \dOnto>\emp \\
\cdot     &\rOnto_\emp  &  \cdot    &\rTo^{v}    &\cdot  & \rOnto_\emp   &
\cdot\\
\dTo<{v}    &        &\dTo<{v}  &       & \dOnto>\emp  &      & \dOnto>\emp \\
\cdot     &\rOnto_\emp  & \cdot     &\rOnto_\emp &\cdot  & \rOnto_\emp   &
\cdot\\
\end{diagram}
%\caption{Permutation of final steps}\label{F.la.ste.mo.}
%\end{figure}
Hence we have by \Lr{L.ext.lem.mult.} and \Lr{L.era.and.ess.im.ne.}.(4) that
$P'/Q'=\emp$ (as otherwise $P'/Q'$ should have a non-empty
$u'$-residual by \Lr{L.era.and.ess.im.ne.}.(4)). The converse is proved
similarly, so $P'\leeqv Q'$. It follows that $u=u'/v'$ and $v=v'/u'$.
\eproof
\el




\btl{P.on.ca.for.}
{\bf (Extraction)}
Every redex $Pv$ in an ASDRS has exactly one extraction normal form
$\sclas{P^*}v^*$ which is canonical, and $P^* v^*\zleq Pv$.

\bproof
It is enough to show that the extraction relation $\extr$ is weakly
confluent (as it is strongly normalizing). So let
$Qw''\lextrr{v}Nw\extrr{u}Pw'$ with $u\not= v$ (since if
$u=v$ then there is nothing to prove).  We will show that
$Qw''\extrr{u'}N^*w^*\lextrr{v'}Pw'$ for some $N^*w^*$, $u'$, and $v'$ such
that $u=u'/v'$ and $v=v'/u'$. By \Dr{D.ext.}, we have from
$Qw''\lextrr{v}Nw\extrr{u}Pw'$ that $Q+v\staeq N'\staeq P+u$, where $N'$ is
a standard variant of $N$, and $w''/v=w'/u=w$. By \Lr{L.mov.red.cre.}, we
have the following situation, where $P'+v'\staeq P$, $Q'+u'\staeq Q$,
$P'\staeq Q'$, $u=u'/v'$, and $v=v'/u'$ (hence $P'v'\zfami Qv$, $Q'u'\zfami
Pu$).
\begin{diagram}[height=1.4em,width=1.4em]
\cdot     &\rOnto^{P'}  &  \cdot    &\rTo^{v'}   &\cdot  &\rTo^{u}       &
\cdot \\
\dOnto<{Q'} &        &\dOnto>\emp &        & \dOnto>\emp &  & \dOnto>\emp \\
\cdot     &\rOnto^\emp  &\bullet & \rTo^{v'}  &\bullet\ni w' &\rTo^{u}
& \cdot \\
\dTo<{u'}   &        &\dTo>{u'}  &         & \dTo>{u}  &    & \dOnto>\emp \\
\cdot   &\rOnto_\emp  &\bullet\ni w'' &\rTo^{v} &\bullet\ni w  &
\rOnto_\emp & \cdot\\
\dTo<{v}    &        &\dTo<{v}  &       & \dOnto>\emp  &      & \dOnto>\emp \\
\cdot     &\rOnto_\emp  & \cdot     &\rOnto_\emp &\cdot  & \rOnto_\emp   &
\cdot\\
\end{diagram}
Now, by [stability], there is a redex $w^*$ in
the final term of $P'$ (and $Q'$) such that $w^*/v'=w'$ and $w^*/u'=w''$.
Thus, for $N^*=P'$, we have $Qw''\extrr{u'}N^*w^*\lextrr{v'}Pw'$ by
\Dr{D.ext.}.
\eproof
\et


The extraction normal form  $\sclas{P^*}v^*$ of $Pv$ is called a
\emph{canonical form of} $Pv$, and so are all $P'v'\in \sclas{P^*}v^*$. Now
we can prove the adequacy of our extraction procedure for the zig-zag.



\btl{T.un.ex.nor.f.}
In an ASDRS, $Pu\zfami Qv$ iff they have the same
unique canonical form $\sclas{N}w$.

\bproof
\ben
\item[\suf]
By definition of $\zfami$, there are $P_0 u_0=Pu,
P_1 u_1,\ldots, P_n u_n=Qv$ such that $P_0 u_0\zgeq P_1 u_1\zleq  P_2 u_2
\zgeq\ldots P_n u_n$. By the Standardization Theorem, we can take $P_i$ to
be standard.
\begin{diagram}[height=1.4em,width=1.4em]
       &        &P_0u_0 &         &         &        &   \\
   &\ruOnto(2,6)&\uOnto_{Q_1}  &  &         &        &  \\
       &        & P_1u_1  & \rOnto  & P_2u_2 &        &   \\
   &\ruOnto(2,4)&    &\ruOnto(4,4) & \uOnto  &        &  \\
       &        &        &         &P_3u_3 &        &   \\
       &        &    &\ruOnto(4,2) &         &\rdCo &   \\
\cdot     &\rOnto  &        &         &         &        & P_nu_n\\
\end{diagram}
Since $P_0u_0\zgeq P_1u_1$, there is $Q_1$ such that $P_0\leeqv P_1+Q_1$
and $u_0=u_1/Q_1$. Let $P'_1u'_1$ be a canonical form of
$P_1u_1$: $\,P_1u_1\doextr P'_1u'_1$. Then there is $P^*_1$ such that
$P_1\staeq P'_1+P^*_1$. We show that $P'_1$ is $P'_1+P^*_1+Q_1$-needed,
i.e., $P_0$-needed (since $P'_1+P^*_1+Q_1\leeqv P_0$). Suppose on the
contrary that $P'_1$ contracts a $P_0$-unneeded redex. Let $w$ be the
latest $P_0$-unneeded step in $P'_1$. By \Lr{L.era.and.ess.im.ne.}.(3), $w$
does not create the next step in $P'_1$ (if $w$ is not the last step in
$P'_1$), therefore can be permuted with its next step. That $w$-step is
again $P'_1$-unneeded by \Lr{L.era.and.ess.im.ne.}.(4), and can be
contracted after its next step, and so on. So we can assume that $w$ is the
last step in $P'_1$ ($P'_1$ is chosen up to $\staeq$). Since $u'_1$ has a
residual along $P_1^*+Q_1$, it is $P_0$-essential by \Dr{D.red.need.ess.}.
Since $w$ is $P_0$-unneeded, it is $P_0$-inessential by
\Lr{L.era.and.ess.im.ne.}.(1). Hence $w$ does not create $u'_1$ by
\Lr{L.era.and.ess.im.ne.}.(3). But this is impossible since $P'_1u'_1$ is
canonical and $w$ is the last step of $P'_1$. So we have proven that $P'_1$
is $P_0$-needed. This implies that the standardization procedure of
\Dr{D.ess.rel.red.} does not effect $P'_1$ when applied to
$P'_1+P^*_1+Q_1$, i.e., we can assume a standard $P'_0\staeq P_0$ such that
$P'_0=P'_1+P''_0$ for some $P''_0$, and $u_0=u'_1/P''_0$. Hence
$P_0u_0\doextr P'_1u'_1$ by the definition of $\extr$, and $P'_1u'_1$ is a
canonical form of both $P_0u_0$ and $P_1u_1$. Similarly, since $P_1u_1\zleq
P_2u_2$, we have that $P'_1u'_1$ is a canonical form of $P_2u_2$, and so
on. Now it is enough to apply \Tr{P.on.ca.for.}.

\item[\nec] Immediate from \Tr{P.on.ca.for.} and the definition of~$\zfami$.
\een
\eproof
\et


This theorem, together with computability of extraction
normal forms, implies decidability of the zig-zag relation in ASDRSs. Note
that, at this stage, we do not yet know whether or not zig-zag is a family
relation. This is the subject of the next section.




\section{Affine Zig-zag and Separable Families}
\label{S.li.zi.fa.}


In this section we show that, in ASDRSs, the zig-zag  relation forms a
family relation, that is, it satisfies the family axioms of DFSs. We will
also define \emph{separability} of a family relation, and show that zig-zag
is the only separable family relation in ASDRSs.


\bdl{D.sep.fam.}
\ben
\item[(1)] We call a DFS $\cal F$ a \emph{zig-zag} DFS, ZDFS, if its family
relation is the zig-zag $\zfami$.

\item[(2)] We call an affine DFS \emph{separable}, SDFS, if, for any redex
$Pv$, $v$
cannot create two different redexes in the same family, that is, if $v$
creates $w',w''$ and $w'\not= w''$, then $Fam((P+v)w')\not= Fam((P+v)w'')$.
In a separable DFS, the  family and contribution relations will be denoted
by $\sfami$ and $\scontr$. The DFS is \emph{non-separable} otherwise.
\een
\ed


It is easy to see that not all (even linear, i.e., without duplication and
erasure) DFSs are zig-zag DFSs or separable DFSs. For example, in the
linear SDRS given by the reduction graph
\begin{diagram}[height=1.5em,width=1.5em]
\label{D.perm.cl.}
       &        &       &             &\bullet &               &        \\
       &        &       & \ruTo^{v_1} &    &  \rdTo^{v'_2} &         \\
\bullet & \rTo^u &\bullet &             &    &               &\bullet \\
       &        &       & \rdTo_{v_2} &    & \ruTo_{v'_1}  &         \\
       &        &       &             &\bullet &               &        \\
\end{diagram}
where $u$ creates $v_1$ and $v_2$, $v'_1=v_1/v_2$ and $v'_2=v_2/v_1$, we
can set all $v$s to belong to the same family $\phi$, and $u$ to form its
own family $\psi$, and define $\psi\contr\phi$. Then we get a DFS which is
not a ZDFS as for example $uv_1\not\zfami uv_2$. That DFS is not separable
either, as $u$ creates two different members of the family $\phi$. We will
show below that this is not a coincidence. We could also define
$\{v_1,v'_1\}$ and $\{v_2,v'_2\}$ to form separate families $\phi_1$ and
$\phi_2$, and define $\psi\contr \phi_1,\phi_2$, and this would yield
a ZDFS.


As already mentioned in the introduction, non-separable families (without
the name) are studied in~\cite{[AL]} for Interaction Systems, where it is
demonstrated that such a family relation is in general strictly larger than
the zig-zag.  Indeed, consider the following example from~\cite{[AL]}. Let
an Interaction System be given by the $\mu$-rule: $\mu$-rule $\mu(\lambda
x.
X)\ar [\mu(\lambda x. X)/x]X$. Then the $\mu$-reduction step $t=\mu(\lambda
x.(xx))\ar (\mu(\lambda x.(xx))\,\mu(\lambda x.(xx)))=s$ simultaneously
creates the two $\mu$-redexes in $s$; these redexes are
intuitively in the same family (and this intuition is supported by an
appropriate labelling system for Interaction Systems), but cannot be
related by zig-zag (without taking into account the structure of rewrite
steps, which is  impossible to do for DRS steps as they do not carry any
internal structure).


\delete{
At first sight, one might think that there is no need or possibility of
a stronger sharing in non-duplicating SDRSs. However, this is not the case
as the example of Asperti and Laneve~\cite{[AL]} demonstrating `inadequacy'
of L\'evy's extraction algorithm for Interaction Systems is, when considered
as an Abstract Reduction System, a non-duplicating SDRS.
These effects are caused by the fact that more than one members of a family
can be created by a single
step -- the reduction step $t=\mu(\lambda x.(xx))\ar (\mu(\lambda x.(xx))
\,\mu(\lambda x.(xx)))=s$, according to the , simultaneously creates the
two $\mu$-redexes
in $s$;
}





Another important example where a non-separable sharing is
reasonable is the \emph{lazy call-by-value} \lc,
$\lambda_{LV}$~\cite{[Plo75]}. It is obtained from the \lc\ by allowing
only $\beta$-redexes whose arguments are \emph{values} (i.e, variables or
abstractions $\lambda x.t$), and that are not in the scope of
$\lambda$-occurrences (we assume that there are no $\delta$-rules in the
calculus). it is easy to see that $\lambda_{LV}$ is linear: if $u,v$ are
redexes in a term $t$ and $u=(\lambda x.e)o$,
then $v\not\in e$ because of the main $\lambda$ of $u$, and $v\not\in o$
since $o$ is either a variable or an abstraction; orthogonality of
$\lambda_{LV}$ (i.e., that the residuals of redexes remain admissible)
follows from a similar argument. Now consider the reduction
$$t=w=(\lambda x.(xy)(xy))\lambda x.u\red{w} o=\overbrace{((\lambda
x.u)y)}^{v_1} \overbrace{((\lambda x.u)y)}^{v_2}\doar uu=s,$$ where $u$ is
a $\lambda_{LV}$-redex such that $x$ does not occur free in it. It is reasonable
to share the two occurrences of $u$ in $s$, but in order to make the
reduction graph of $t$ a DFS (in particular, for the [contribution] axiom
to be satisfied), we need to share $v_1$ and $v_2$ as well, although the
two are not related.  This goes beyond L\'evy's concept of sharing, and the
resulting DFS is not separable as the contraction of $w$ creates two
different redexes, $v_1$ and $v_2$, of the same family. Note that the
occurrences of $u$ in $s$ are \emph{created} by $v_1$ and $v_2$, as the
occurrences of $u$ in $t$ and $o$ are not $\lambda_{LV}$-redexes (they are
not admissible).


Below, $FAM_z(P)$ (resp. $SFAM_z(P)$) denotes the set of zig-zag classes whose
(resp. $P$-needed) member redexes are contracted in $P$, in an ASDRS; and
$Fam_z(Qu)$ denotes the zig-zag class of~$Qu$.  Further, if $\phi',\phi$
are zig-zag classes, we write $\phi'\zcontr\phi$ iff for
any $Pu\in\phi$, $P$ contracts a redex in $\phi'$.


\bll{L.dec.fam.ex.}
Let $P$ be $Q$-needed, in an ASDRS. Then $FAM_z(P)\ssq FAM_z(Q)$.  In
particular, if $P\in\stav{Q}$, then $FAM_z(P)\ssq FAM_z(Q)$, and if
$P\staeq Q$, then $FAM_z(P)= FAM_z(Q)$.

\bproof
Let $v$ be a contracted redex in $P$, say $P=P'+v+P''$. Then $v$ is
$Q/P'$-needed. Hence $Fam_z(P'v)\in FAM_z(Q/P')\ssq FAM_z(Q)$, implying the
lemma.
\eproof
\el


\bll{L.dif.re.sa.his.}
If $Pv\zfami Qw$, then $v/(Q/P)=w/(P/Q)$. In particular, if $P\staeq Q$,
then $v=w$.

\bproof
By \Tr{T.un.ex.nor.f.}, $Q\leeqv N+Q'$, $P\leeqv N+P'$, $w=u/Q'$ and
$v=u/P'$, where $Nu$ is a canonical form of $Qw$ and $Pv$. Then $P/Q\leeqv
P'/Q'$ and $Q/P\leeqv Q'/P'$. Hence $w/(Q/P)=w/(Q'/P')=u/(P'\sqcup
Q')=u/(Q'\sqcup P')= v/(Q'/P')=v/(Q/P)$.
\eproof
\el




\bll{L.cre.con.}
Let $Q^*:t\dored{P}s\red{u}e$ and $u$ create $v\subt e$. Then, for any
canonical form $Q'v'$ of $Q^*v$, $Q'$ contracts a redex zig-zag related to
$Pu$.

\bproof
We have by \Lr{L.sta.ex.dec.} that $Q=ST(Q^*)=P'+u'$, where $P\leeqv
P'+P''$ (for some $Q$-unneeded $P''$) and $u=u'/P''$. If $Qv$ is not a
canonical form, by \Lr{L.sta.ex.dec.} there is an extraction step
$Qv\extrr{w_1}Q_1v_1$ (i.e., $Q\staeq Q_1+w_1$ and $v=v_1/w_1$). Since
$Q_1+w_1\staeq Q=P'+u'$, we have by \Lr{L.mov.red.cre.} that $Q_1\staeq
P_1+u_1$ such that $P_1u_1\zfami P'u'\zfami Pu$. So we have
$(P'+u')v\extrr{w_1}(P_1+u_1)v_1$ such that $P_1u_1\zfami P'u'$. Similarly,
if $(P_1+u_1)v_1$ is not a canonical form, there is an extraction step
$(P_1+u_1)v_1\extrr{w_2}(P_2+u_2)v_2$ such that $P_2u_2\zfami P_1u_1\zfami
P'u'\zfami Pu$, and so on. So a canonical form of $Qv$ has the form
$(P_m+u_m)v_m$ such that $Pu\zfami P_mu_m$. Since, by \Tr{P.on.ca.for.},
for any canonical form $Q'v'$ of $Qv$ (and hence of $Q^*v$), $Q'\staeq
P_m+u_m$ and $v_m=v'$, it follows by \Lr{L.dec.fam.ex.} that $Q'$ contracts
a redex in the family of $Pu$.
\eproof
\el



\bll{L.dec.fam.ex.1}
Let $Pv\extrr{w}P'v'$. Then $FAM_z(P')\ssq FAM_z(P)$.

\bproof
By \Dr{D.ext.}, $Pv\extrr{w}P'v'$ implies that $P'+w\in \stav{P}$, and by
\Lr{L.dec.fam.ex.}, $FAM_z(P')\ssq FAM_z(P'+w)\ssq FAM_z(P)$.
\eproof
\el


The next two lemmas imply that the zig-zag relation in any ASDRS
satisfies the axioms [creation] and [FFD]:

\bll{L.dr.cre.}
Let $Q:e\dored{P}t\red{u}s$ and let $u$ create $v\subt s$. Then
$Fam_z(Pu)\zcontr Fam_z(Qv)$.

\bproof
By \Lr{L.cre.con.}, if $Q'v'$ is a canonical form of $Qv$, then
$Fam_z(Pu)\in FAM_z(Q')$. Now it follows from Lemmas~\ref{L.dec.fam.ex.}
and \ref{L.dec.fam.ex.1} and \Tr{T.un.ex.nor.f.} that for any $Q^*v^*\zfami
Qv$, $Fam_z(Pu)\in FAM_z(Q^*)$, i.e.,  $Fam_z(Pu)\zcontr Fam_z(Qv)$.
\eproof
\el


\bll{L.ne.rep.fam.zi.}
Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar t_n$. Then for any $k,m$ such
that $k<m<n$, $Fam_z(P_ku_k)\not=Fam_z(P_mu_m)$.

\bproof
By induction on the number of zig-zag classes $\zcontr$-contributing to
$Fam_z(P_ku_k)$. Suppose on the contrary that
$Fam_z(P_ku_k)=Fam_z(P_mu_m)$. Let $P'_ku'_k$ be a canonical form of
$P_ku_k$, which exists by \Tr{P.on.ca.for.}, hence there is $Q'_k$ such
that $P'_k+Q'_k\leeqv P_k$ and $u_k=u'_k/Q'_k$. So we have that
$P_{k+1}=P_k+u_k \leeqv P'_k+Q'_k+u_k\leeqv P'_k+u'_k+Q'_k/u'_k$. Since
$P'_k$ contracts redexes in all contributor zig-zag classes of
$Fam_z(P'_ku'_k)=Fam_z(P_ku_k)=Fam_z(P_mu_m)$, and since by the induction
assumption no redexes in these classes can be contracted again, $u_m$ is
not created by its preceding step in
$u'_k+Q'_k/u'_k+u_{k+1}+\ldots+u_{m-1}$, by \Lr{L.dr.cre.}. Similarly, its
ancestor redex is not a created redex, and so on. That is, $u_m$ is a
residual of some redex $u'_m$ in the final term of $P'_k$, different from
$u'_k$.  Hence $Fam_z(P'_ku'_k)=Fam_z(P_mu_m)=Fam_z(P'_ku'_m)$ and
$u'_k\not=u'_m$, which is not possible by \Lr{L.dif.re.sa.his.} --
contradiction.
\begin{diagram}[height=1.4em,width=1.4em]
\cdot    &\rOnto^{P'_k} & \cdot  &\rOnto^{Q'_k}  & \cdot  &  &  & &  & &  \\
      &      &\dTo<{u'_k}  &    & \dTo>{u_k} &        &   &      &    &    & \\
      &   & \cdot &\rOnto_{Q'_k/u'_k} & \cdot     & \rTo_{u_{k+1}}      &\cdot
&\rOnto   &\cdot & \rTo_{u_{m-1}}      &\cdot \\
\end{diagram}
\eproof
\el



\btl{T.lin.dr.sta.df.}
Let $\cal R$ be a non-duplicating SDRS. Then ${\cal
F_R}=(R,\zfami,\zcontr)$ is a non-duplicating zig-zag DFS.

\bproof
We need to show that ${\cal F_R}$ satisfies all family axioms.
[contribution] is immediate by the definition of $\zcontr$. Since for any
$u,v\subt t$, $\emp_t u$ and $\emp_t v$ are canonical forms, $u\not= v$
implies by \Tr{T.un.ex.nor.f.} that $\emp_t u\not\zfami \emp_t v$, i.e.,
[initial] holds. [creation] is immediate from \Lr{L.dr.cre.}, and [FFD]
from ~\Lr{L.ne.rep.fam.zi.}.
\eproof
\et

\begin{rem}\em
Lemmas~\ref{L.dec.fam.ex.} and ~\ref{L.dif.re.sa.his.} allow us to obtain
the following characterizations of $\leeqv$ and $\lleq$ via zig-zag; the
proofs can be found in~\cite{[azdfs]}, Section~7.


\bpl{P.leqv.sam.se.es.fa.}
Let $P,Q$ be finite co-initial reductions in an ASDRS. Then
\ben
\item[(1)] $P\lleq Q$ iff $\exists Q'\leeqv Q: FAM_z(P)\ssq FAM_z(Q')$;

\item[(2)] $P\leeqv Q$ iff $SFAM_z(P)=SFAM_z(Q)$.
\een
\ep
\end{rem}



%\section{Affine Separable Families}
%\label{S.sep.}


Next we show that an affine DFS
is a zig-zag DFS iff it is separable. First we establish a characterization
of separability of a DFS $\cal F$ via uniqueness of contracted families in
reductions in $\cal F$. It shows that, in separable DFSs, and only in such
DFSs, there is no sharing (in the affine case) -- all reductions are in
fact \emph{complete family-reductions}. Below we will only consider complete
family-reductions, and will often omit `complete'.


\bll{L.aff.un.f.l.}
Let ${\cal F}={\cal R}, \fami,\contr)$ be an affine DFS. Them the following
are equivalent:
\ben
\item[(1)] $\cal F$ is separable;

\item[(2)] Elements of any family are contracted at most once in any
reduction in~$\cal F$;

\item[(3)] $Pv\fami Pv'$ implies $v=v'$;

\item[(4)] Any reduction in $\cal F$ is in fact a family-reduction, and
vice versa.
\een

\bproof
\bds
\item{$(1)\imply (2)$:} Similar to the proof of \Lr{L.ne.rep.fam.zi.}, except
replacing $Fam_z(\,\,)$ by $Fam(\,\,)$, using [creation] instead of
\Lr{L.dr.cre.}, and using separability instead of \Lr{L.dif.re.sa.his.}.

\item{$(2)\imply (3)$:} If there were $Pv\fami Pv'$ with $v\not= v'$, then
at least
one of $P+v+v'/v$, $P+v'+v/v'$ would contract two members of $Fam(Pv)$ by
[weak acyclicity], contradicting (2).

\item{$(3)\imply (4)$:} Immediate.

\item{$(4)\imply (1)$:} If $\cal F$ was not separable, then there would be $Pv$,
$w'$ and $w''$ such that $v$ creates both $w'$ and $w''$, $w'\not= w''$,
and $Fam((P+v)w')=Fam((P+v)w'')$. By the assumption (4), the reduction
$P+v$ is also a family-reduction, implying that $P+v+w'\Vert w''$, where
$w'\Vert w''$ is the multi-step contracting $w'$ and $w''$ in parallel, is
a family-reduction which is not a reduction, contradicting~(4).
\eds
\eproof
\el




\bll{L.contr.fam.}
Let $Pv$ be a canonical element of a family $\phi$, in an affine DFS ${\cal
F}=(R,\fami,\contr)$, and let $P$ contract a redex $w$. Then $Fam(w)\contr
\phi$.

\bproof
Suppose on the contrary that $\psi=Fam(w)\not\contr\phi$, and assume that
$Pv$ and $w$ are such that $w$ is (one of) the latest among steps in
canonical elements of $\phi$ that do not contribute to $\phi$. Since $Pv$
is canonical, $w$ cannot be the last step of $P$ as the last step of $P$
creates $v$ by \Dr{D.can.re.his.}, and therefore its family contributes to
$\phi$ by [creation]. Further, if $v$ is the next to $w$ step in $P$, then
$w$ cannot create $v$ as this would imply $\psi\contr Fam(v)$ by
[creation], implying $\psi\contr \phi$ (as $Fam(v)\contr \phi$ by the
choice of $w$). Hence $w$ can be permuted with $v$ in $P$, yielding again
(by \Lr{L.era.and.ess.im.ne.}) a canonical element of $\phi$ in which a
step whose family does not contribute to $\phi$ is contracted later than
$w$ in $P$ -- a contradiction.
\eproof
\el



\btl{T.sep.eq.ig.}
An affine DFS $\cal F$ is separable iff it is a zig-zag DFS.

\bproof
\ben
\item[\suf] Let ${\cal F}=({\cal R}, \sfami,\scontr)$ be separable, and let
$Pu\sfami Qv$. (We want to prove that $Pu\zfami Qv$.) By the Extraction
Theorem, there are canonical forms $P'u'\zfami Pu$ and $Q'v'\zfami Qv$, and
since $\zfami\ssq\sfami$ (by the definition of DFSs), $P'u'\sfami Q'v'$.
Now if $P'\staeq Q'$, since both $P'u'$ and $Q'v'$ are canonical, the last
step of $P'$ creates both $u'$ and $v'$, and $u'=v'$ by separability.
Hence, $P'u'\zfami Q'v'$, implying $Pu\zfami Qv$, in this case. Otherwise,
we must have $P'\not\leeqv Q'$ (as $P',Q'\in\stan$), and if say $P'\lles
Q'$, $Q'\leeqv P'+P''$ for some $P''\not=\emp$. Again, since $P'u'$ and
$Q'v'$ are canonical, the last step of $P'$ creates $u'$, and that of
$P''$, call it $w$, creates $v'$ (since the last step of $P''$ coincides
with that of $ST(P'+P'')$). By [creation], $Fam(w)\scontr Fam(v')=Fam(u')$,
hence by [contribution] $P'$ must also contract a redex in $Fam(w)$,
contradicting separability by \Lr{L.aff.un.f.l.}. Hence $P'\not\leeqv Q'$
cannot hold, and we are done.

\item[\nec] Let $\cal F$ be a ZDFS. By
\Lr{L.ne.rep.fam.zi.}, any family is
contracted at most once in a reduction in $\cal F$, implying by
\Lr{L.aff.un.f.l.} that $\cal F$ is an SDFS.
\een
\eproof
\et


We conclude this section by a useful characterization of histories of
canonical elements of zig-zag (hence extraction and separable) families, in
ASDRSs.


\btl{C.con.fam.can.}
Let $Pv$ be a canonical element of a family $\phi$, in an AZDFS ${\cal
F_R}=(R,\zfami,\zcontr)$. Then $P$ contracts exactly one redex
in every contributor family of $\phi$.

\bproof
By \Lr{L.contr.fam.}, $P$ contracts only redexes in contributor families of
$\phi$. That every such a family is contracted in $P$ follows immediately
from [contribution]. The uniqueness of contracted families follows from
\Lr{L.aff.un.f.l.} and \Tr{T.sep.eq.ig.}.
\eproof
\et



\section{Implementation DFSs}
\label{S.impl.drs.}

We now define the \emph{implementation} $\lin{\cal F}$ of a DFS $\cal F$,
whose reductions correspond to complete family-reductions in $\cal F$,
hence the name. We also show that optimal reductions in $\cal F$, relative
to any stable set $\stab$ of results, are implemented in $\lin{\cal F}$ by
the shortest $\stab$-normalizing reductions. We will assume that the
reduction graph of $\calF$ is the reduction graph of an \emph{initial}
term, denoted by $t_\emp$, and that families are considered relative to
$t_\emp$, i.e, all histories start with~$t_\emp$.



\bdl{D.lin.dfs.drs.}
Let ${\cal F}=({\cal R},\fami,\contr)$ be a DFS. The \emph{implementation}
or \emph{L\'evy-implementation} of ${\cal F}$ is the AZDFS $\lin{{\cal
F}}=({\cal R}_I,\fami_I,\contr_I)$, where
\bit
\item the branches of the reduction graph of the underlying ARS $A$ of
${\cal R}_I=(A,/)$ are family-reductions starting from $t_\emp$, each edge
(i.e., a reduction step) being a multi-step contracting a family of
redexes.

\item the residual relation $/$ is defined as follows: let $U$ and $V$
be complete sets of redexes in two families, in a term $s$, and let $U:s\ar
o$ be the multi-step contracting $U$. Then $V/U$ is the multi-step $o\ar e$
contracting all members of the set $V/U$.

\item the family and contribution relations $\fami_I,\contr_I$ in
$\lin{{\cal F}}$ are those induced by $\fami$ and $\contr:$ let $P_I$ and
$Q_I$ be reductions in $\calR_I$ corresponding to family-reductions $P$ and
$Q$ in $\calF$; then $P_IU\fami_I Q_IV$ iff for any $u\in U, v\in V$,
$Pu\fami Qv$; and $Fam(P_IU)\contr_I Fam(Q_IV)$ iff $Fam(Pu)\contr
Fam(Qv)$.
\eit
\ed


We need to verify that $\lin{{\cal F}}$ in the above definition is indeed
an AZDFS.


\bll{L.res.fam.fam.}
Let $P:t_\emp\doar s$ be a \cfr\ in a DFS ${\cal F}=(R,\fami,\contr)$,
let $U,V\subts s$ be complete sets of redexes of families $\phi$ and $\psi$
in $s$, respectively, and let $s\dored{V}o$. Then $U'=U/V$ is the complete
set of redexes of $\phi$ in $o$.

\bproof
Since $\zfami\ssq\fami$, $U'$ consists of redexes of $\phi$. Suppose on the
contrary that there is $w\subt o$ such that $(P+V)w\in\phi$ and $w\not\in
U'$. Again by $\zfami\ssq\fami$, $w$ must be created along $V$, and we have
by [creation] that $\psi\contr\phi$. But this implies by [contribution]
that $P$ contracts a member of $\psi$, and therefore the complete family
$\psi$ (since $P$ is a \cfr), and $P+V$ contracts the family $\psi$ twice,
contradicting \Lr{L.fam.compl.}.
\eproof
\el

Thus the residual relation is well defined. Obviously, $V/V=\emp$, and
every family in $o$ has at most one ancestor
family in $s$. Further, [weak acyclicity] and [stability] for $\lin{{\cal
F}}$ follow immediately from Acyclicity Lemma and Stability Lemma,
respectively (one just needs to take for the reductions $P$ and $Q$ in
these lemmas complete developments of disjoint sets of redexes, which are
clearly external). The axiom [initial] in $\lin{{\cal F}}$ follows
immediately from [initial] in $\cal F$. If $P+U+V$ is a reduction in
$\lin{{\cal F}}$ such that $U$ creates $V$, then the redexes in $V$ are
created along $U$ (when $P+U+V$ is considered as a reduction in $\cal F$),
i.e., $Fam(U)\contr Fam(V)$ in $\cal F$, hence $Fam(U)\contr_I Fam(V)$,
implying [creation] in $\lin{{\cal F}}$. Since family-reductions can be
viewed as reduction in $\cal F$ (by considering multi-steps as
corresponding complete developments), [contribution] for $\contr_I$ follows
immediately from [contribution] for $\contr$. Finally, [FFD] for
$\lin{{\cal F}}$ follows immediately from \Lr{L.fam.compl.} for $\calF$.
Hence $\lin{{\cal F}}$ is indeed a DFS as $\fami_I$ clearly
contains the zig-zag relation. Note that $\lin{{\cal F}}$ is separable as
its steps contract entire $\fami$-families, hence it is an AZDFS by
\Tr{T.sep.eq.ig.}:



\btl{T.line.zig.}
For any DFS ${\cal F}$, $\lin{{\cal F}}$ is an AZDFS.
\et

Next we show that any sharing $\fami$ in an SDRS stronger than zig-zag can
be decomposed into any weaker sharing $\fami'$ and a \emph{non-separable}
sharing $\fami^*$ in the implementation of $\fami'$.



\bdl{D.str.sh.}
Let $\calF=(\calR,\fami)$ and $\calF'=(\calR,\fami')$ be DFSs. We say that
$\calF$ has a \emph{stronger} sharing than $\calF'$, written
$\calF\geq\calF'$,  if $\fami'\ssq\fami$.
\ed


\btl{T.dec.sh.}
Let $\calF=(\calR,\fami)$ and $\calF'=(\calR,\fami')$ be DFSs. Then $\calF
>\calF'$ iff there is a non-separable family relation $\fami^*$ on the
implementation DRS $\calR'_I$ of $\calF'$ such that $\calF^*_I=\calF_I$,
where $\calF^*=(\calR'_I,\fami^*)$.

\bproof
\ben
\item[\suf] Let $\calF>\calF'$. Define $\fami^*$ on $\calR'_I$ by:  $Pv\fami^*
Qu$ iff $P'v'\fami  Q'u'$, where $P'$ and $Q'$ are (any) reductions in
$\calR$ corresponding to $P$ and $Q$, and $v'$ and $u'$ are any
$\calR$-redexes in redex-sets contracted in multi-steps $v$ and $u$. It is
immediate that the definition is correct (since reductions in $\calF$
corresponding to a reduction in $\calR'_I$ are all sequentializations of a
multi-step reduction and are L\'evy-equivalent, and since $\calF>\calF'$).
Further, the family axioms for $\fami^*$ follow from those of $\calF$
exactly as they were verified above for $\calF_I$ in the place of $\calF^*$
(the only difference is that $\calF^*$ is a `partial implementation' of $\calF$
while $\calF_I$ is the `complete'  or L\'evy-implementation). By the
definition of $\fami^*$, family-reductions in $\calF^*$ are exactly
family-reductions in
$\calF$, and $\calF^*_I=\calF_I$ follows since both are AZDFSs by
\Tr{T.line.zig.}. Since $\calF>\calF'$ and $\calF'_I$ is an AZDFS,
$\fami^*$ is strictly larger than
zig-zag, hence is non-separable by \Tr{T.sep.eq.ig.}.

\item[\nec] Immediate from \Dr{D.str.sh.}.
\een
\eproof
\et


Thus, in particular, the study of a sharing in an SDRS strictly larger than
the zig-zag can be reduced to studying zig-zag (when it is a
family-relation) and studying non-separable affine families.




The following lemma relates neededness in a DFSs with neededness in its
implementation. Together with \Tr{T.unif.opt.}, it implies that the
implementation DRSs $\calF_I$ do indeed correctly implement family-reductions
in DFSs $\calF$: $\stab$-needed reductions in $\calF_I$, which are actually
$\stab$-needed family-reductions by
\Lr{L.aff.un.f.l.}.(4) and \Tr{T.line.zig.}, and hence are optimal w.r.t.
$\stab$, implement optimal family-reductions in $\calF$, w.r.t~$\stab$.


\bll{L.nee.imp.}
Let $\stab$ be a stable set of terms in a DFS $\calF$ not containing the
initial term $t_0=t_\emp$, let $P:t_0\dored{U_0}t_1\dored{U_1}\ldots \doar
t_n$ be
an $\stab$-normalizing family-reduction in $\calF$, and let
$P_I:t_0\red{u_0}t_1\red{u_1}\ldots \ar t_n$ be its corresponding reduction
in $\calF_I$. Then $P$ is $\stab$-needed iff so is $P_I$.
\el

\bproof
\ben
\item[\suf] Assume that $P$ be $\stab$-needed, and suppose on the contrary that
$P_I$ is not $\stab$-needed, i.e.,  $u_i$ is $\stab$-unneeded for some $i$.
Then there is an $\stab$-normalizing reduction $N:t_i\doar s$ that is
external to $u_i$. It remains to show that any corresponding
family-reduction $N'$ in $\calF$ (no matter how the multi-steps are
sequentialized) is external to $U_i$: the latter implies that $U_i$ does
not contain an $\stab$-needed redex, contradicting $\stab$-neededness of
$P$. If on the contrary a multi-step $W$ of $N'$ contracts a residual of a
redex in $U_i$, then it follows from \Lr{L.res.fam.fam.} that $W$ is the
residual of $U_i$ along $N'$ (as both $U_i$ and $W$ are complete sets of
redexes of the same family in corresponding terms), implying that the
corresponding step of $N$ is a residual of $u_i$ -- a contradiction.

\item[\nec] Let $P_I$ be $\stab$-needed. Suppose on the contrary that $U_i$
is not
$\stab$-needed for some $i$. Let $Q$ be an $\stab$-needed
$\stab$-normalizing family-reduction (which exists by \Tr{T.unif.opt.}).
Note that the residual of $U_i$ in any term along $Q$ forms a complete
family by \Lr{L.res.fam.fam.}, and all residuals of redexes in $U_i$ remain
$\stab$-unneeded by \Lr{T.3.1.c.}.
Thus residuals of $U_i$ along $Q$ are redex-sets disjoint from the
contracted redex-sets, implying that the corresponding reduction of $Q$ in
$\calF_I$ is external to $u_i$, which contradicts $\stab$-neededness of
$u_i$.
\een
\eproof

\bcl{T.impl.theo.}
{\bf (Optimal Implementation)}
Let $\stab$ be a stable set of terms in a DFS $\calF$. Then $\stab$-needed
$\stab$-normalizing reductions in $\calF_I$ are $\stab$-optimal in
$\calF_I$, and they implement $\stab$-optimal family-reductions in $\calF$.
\ec


\section{Conclusions and future work}
\label{S.concl.}


We have introduced Deterministic Residual and family Structures and
have proven two abstract versions of the \rn\ theorem: one in stable
DRSs for regular stable sets $\reg$, and another in DFSs for all stable $\stab$.
We believe that our first proof is the simplest existing proof among those
using the residual notion, though it covers all the existing normalization
results,
except for the one in~\cite{[ctrs]}, which is covered by our second RN
theorem. It is remarkable that, unlike the proofs
in~\cite{[C.F.],[H.L.],[B.K.K.S.]}, our first proof does not use the notion
of standard reduction. Similar proofs for
orthogonal CRSs in~\cite{[K.S.]} and for orthogonal DAGs
in~\cite{[Mar91],[Mar]} use an even stronger termination argument, expressed by
the [FFD] axiom; they
used suitable labelling systems to define notions of family.
Our second proof can be seen as a generalization of that proof method,
which was used already by L\'evy in~\cite{[levy],[le80]}. It would be
interesting to investigate whether it is possible to prove our second theorem
already for stable DRSs, i.e., without family axioms, but possibly some much
weaker axioms.



Further, we have introduced and studied an abstract concept of optimal
implementation of DFSs, and showed that needed computations (w.r.t. stable
sets of results) in implementation DRSs mimic optimal (in the sense of
L\'evy and beyond) computations in original DFSs.
We have shown that every affine SDRS can be turned into an affine
DFS by taking zig-zag as the family relation, and that zig-zag is the only
family relation with the separability property -- no redex can create
simultaneously two different members of the same family. Finally, we have
shown that sharing is compositional. In particular, any
family relation can be decomposed into zig-zag (when it is a family
relation) and a non-separable affine family-relation,  which facilitates
the study of complicated (non-separable) concepts of sharing in duplicating
systems (such as the one in~\cite{[AL]}). As for zig-zag in duplicating
SDRSs, we believe that suitable extensions of stable DRSs can be defined,
in which one can extended our construction of zig-zag ASDRSs to the general
(duplicating) case, and our proofs can be used as a basis. In the general
case, the [FFD] axiom of DFSs  becomes a strong requirement, and extra
axioms will be necessary to ensure it. We expect that a modification of our
extraction algorithm will be applicable.



Besides their clear relevance for the study of syntactic properties of
orthogonal rewrite systems (which we hope to have amply demonstrated), DFSs
have already proven their usefulness also in the study of concurrent
semantics of orthogonal rewrite systems: Indeed, based on the results
obtained in this paper, we have defined in~\cite{[mfcs]} a fully adequate
\emph{Prime Event Structure}~\cite{[Win],[Win89]} style semantics for
orthogonal rewrite systems in a uniform fashion.  Furthermore
in~\cite{[icalp]} we studied the concepts of \emph{independence} and
\emph{interaction} of (sub)computations in the framework of SDRSs, yielding
a nice theory of \emph{Euclidian Geometry} for reduction spaces in
orthogonal rewrite systems. We believe that one can also develop an
infinitary relative normalization theory for stable DRSs, and thereby
construct  a relativized computational semantics for orthogonal reduction
systems, extending the computational semantics of rewrite systems proposed
by Boudol~\cite{[Bou]}. Among(many other) possible directions for future
work, let us mention that it is important to extend these results,
especially the semantic part, to non-deterministic systems, to enable one
to model for example languages for concurrency as well.



\begin{thebibliography}{99}

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


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


\bibitem{[AnMi]}
S. Antoy and A. Middeldorp, A Sequential Reduction Strategy, in:
\emph{Proc. ALP'94},  Lecture Notes in Computer Science, vol~850
(Springer, Berlin, 1994) 168-185.


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


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


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


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

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


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


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


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


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

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


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


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


\delete{
\bibitem[{DeJo90}]{[D.J.]}
Dershowitz  N.,  Jouannaud  J.-P.  Rewrite Systems. In: J. van
Leeuwen  ed. Handbook of  Theoretical Computer Science, Chapter~6, vol.~B,
1990, p.~243-320.
}


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


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


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


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


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


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


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


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


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


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


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


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



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


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


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


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


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


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


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


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


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


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


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


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


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



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



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

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


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


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

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


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



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


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


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


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


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


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


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

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

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

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

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


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

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

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

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

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

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


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


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

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

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

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



