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

\topmargin   0pt

\textwidth   6.0in
\textheight  8.5in

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



\begin{document}
\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{deff}[thm]{Definition}% [section]
\newtheorem{conv}[thm]{Convention}% [section]

\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf Proof }}{}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}

\newcommand{\notation}{{\bf Notation }}
%\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}


\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\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{\lleq}{\unlhd}
\newcommand{\lles}{\lhd}
\newcommand{\zleq}{\unlhd_z}
\newcommand{\zles}{\lhd_z}
\newcommand{\zgeq}{\unrhd_z}
\newcommand{\zgre}{\rhd_z}
\newcommand{\leeqv}{\approx_L}
\newcommand{\snpp}{\approx_{sn}}
\newcommand{\inter}{\ddagger}
\newcommand{\ind}{\perp}
\newcommand{\hole}{\circ}
\newcommand{\restr}{\vert}
\newcommand{\exten}{\updownarrow}


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

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

\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{deff}\em}
\newcommand{\bdl}[1]{\begin{deff}\em\label{#1}}
\newcommand{\bl}{\begin{lem}\em}
\newcommand{\bll}[1]{\begin{lem}\em\label{#1}}
\newcommand{\bp}{\begin{prop}\em}
\newcommand{\bpl}[1]{\begin{prop}\em\label{#1}}
\newcommand{\bt}{\begin{thm}\em}
\newcommand{\btl}[1]{\begin{thm}\em\label{#1}}
\newcommand{\bel}[1]{\begin{ex}\em\label{#1}}
\newcommand{\bc}{\begin{cor}\em}
\newcommand{\bcl}[1]{\begin{cor}\em\label{#1}}
\newcommand{\bproof}{\begin{pruuf}}
\newcommand{\eproof}{\end{pruuf}}
\newcommand{\ed}{\end{deff}}
\newcommand{\el}{\end{lem}}
\newcommand{\ep}{\end{prop}}
\newcommand{\et}{\end{thm}}
\newcommand{\ee}{\end{ex}}
\newcommand{\ec}{\end{cor}}
\newcommand{\suf}{($\Rightarrow$)}
\newcommand{\nec}{($\Leftarrow$)}
\newcommand{\setm}{\setminus}
\newcommand{\crea}{\vdash}
\newcommand{\emp}{\emptyset}
\newcommand{\cfr}{family-reduction}
\newcommand{\cfrs}{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 R}}

\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{\Le}{L\'evy}


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


\title{An Abstract Concept of Optimal Implementation}
\author{Zurab Khasidashvili   \\
NTT Basic Research Laboratories \\
Atsugi, Kanagawa, 243-01, Japan \\
zurab@theory.brl.ntt.jp
\thanks{Contact author: Tel: 81 462 403674; Fax: 81 462 404709;
 http://www.sys.uea.ac.uk/\~{}zurab. Submission category: \emph{regular
research paper.}}
\and
John Glauert \\
School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
jrwg@sys.uea.ac.uk
\thanks{Part of this work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300. The first author
was also supported by a Dutch NWO grant during his visit to Vrije
Universiteit, Amsterdam, in October 1996.}
}


\date{}

\maketitle



\begin{abstract}
In a previous paper, we introduced \emph{Stable Deterministic Residual
Structures} (SDRSs), Abstract Reduction Systems with an
axiomatized residual relation which model orthogonal term and graph rewriting
systems, and \emph{Deterministic Family Structures} (DFSs), which add
an axiomatized notion of \emph{redex-family} to capture known
\emph{sharing} concepts in the \lc\ and other orthogonal rewrite systems.
In this paper, we introduce and study a concept of \emph{implementation} of
DFSs. We show that for any DFS $\cal F$, its
implementation ${\cal F}_I$ is a non-duplicating DFSs with zig-zag as the
family relation, where zig-zag is simply the symmetric and transitive closure of
the residual relation on redexes with histories. In $\calF_I$, one can
implement optimal family-reductions in $\calF$. Further, we show that
sharing is compositional: the sharing in a DFS $\calF$ can be decomposed
into a weaker sharing $\calF'$ (such as zig-zag) and a sharing in the
implementation $\calF'_I$ of $\calF'$ stronger than zig-zag. 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, which was thought to
require the tree structure of terms, and to show that the family concepts
defined via zig-zag and via extraction yield the same relation.
\end{abstract}


%\pagebreak


\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{[BBKV]} 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 (OTRSs), 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 a suitable
notion of \emph{labelling}, via \emph{extraction}, and by \emph{zig-zag}.
\suppress{In each definition, a family is a class of objects of the form
$Pv$, where
$P$ is a finite reduction starting from a term $t$ and ending in $s$, and
$v$ is a redex in $s$. Here $P$ is called the \emph{history} of $Pv$; all
histories of redexes in the same family are co-initial, i.e., start at the
same term $t$. In the labelling definition of families, the initial term
$t$ gets an \emph{initial} labelling, and labels grow along the reduction.
Two redexes with co-initial histories are declared to be in the same family
if they have the same label. The extraction process starting from a redex
$Pv$ consists of elimination from $P$ of all redexes `not contributing' to
$v$, and results in a reduction $P'v'$ such that $P'$ is standard, and $Pv$ is a
residual of $P'v'$, i.e., $v$ is a residual of $v'$ under some reduction
from the final term of $P'$ to that of $P$. Two redexes (with histories)
are defined to be in the same extraction-family if the extraction process
yields the same result for both redexes.  Finally, the zig-zag relation is
defined simply as the transitive and symmetric closure of the residual
relation on redexes with histories.  Clearly, all the above family concepts
are equivalence relations, and} 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 OTRSs~\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 original
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. Such structures were introduced by the
authors in~\cite{[rndrs]} as \emph{Deterministic Family
Structures} (DFSs) building on recent developments of
abstract reduction systems with an axiomatized residual relation,
such as the
\emph{Concurrent Transition Systems} (CTSs) of Stark~\cite{[Sta]} and the
\emph{Abstract Reduction Systems} (ARSs) of Gonthier et al~\cite{[GLM]}.

Our DFSs are defined as \emph{Deterministic Residual Structures} (DRSs)
with an axiomatized family relation. DRSs, in turn, are Abstract Reduction
Systems with an axiomatized residual relation, similar to CTSs
and ARSs, but with the difference that, unlike CTSs, the
residual relation can be duplicating in DRSs and, unlike ARSs, there is no
nesting relation on redexes defined or axiomatized in DRSs. Despite its highly
abstract nature, a counterpart of Berry's \emph{stability}
property~\cite{[berry]} enabled us to prove the normalization theorem for
all DRSs, and  not only w.r.t. normal forms, but in general for
\emph{regular stable sets} of `intermediate results';
all interesting sets
of final terms, such as head-normal forms, weak head normal forms, etc,
fall in the category of stable term-sets~\cite{[rndrs]}. Moreover, a
\emph{discrete} theory of normalization can also be developed in
Berry-stable DRSs (SDRSs), enabling one to construct reductions
permutation-equivalent to a particular finite or infinite reduction, and to
prove a version of the Standardization Theorem~\cite{[dndrs]}. Further, as
already mentioned, in DFSs one can prove the optimality theorem.


In this paper, we continue the abstract study of optimality
theory started in~\cite{[rndrs]}. We introduce an abstract concept of
\emph{L\'evy-implementation}: With a DFS $\cal F$ we associate a
\emph{non-duplicating} DRS $\calR_I$, called the implementation of $\cal
F$, whose steps exactly correspond to complete family-reduction steps in
$\cal F$, thus, for example, they model sharing-graph implementation
of L\'evy's complete family-reductions in the \lc. It is not difficult to
show that needed reductions in
$\calR_I$ (w.r.t. any stable set of results) correspond exactly to needed
complete family-reductions in $\calF$, implying that the former indeed
implement optimal computations in $\calF$ in the sense of
L\'evy~\cite{[levy],[le80]}.




Further, we show that the family relation on $\calR_I$ induced by that of
$\calF$ coincides with zig-zag, which is the weakest family sharing. 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.  This example also
shows that zig-zag does not coincide with the labelling and
their extraction families based on the \emph{shift} operation.
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 $\mu$-rule $\mu(\lambda x.
X)\ar [\mu(\lambda x. X)/x]X$, simultaneously creates the two $\mu$-redexes
in $s$; these redexes are
intuitively in the same family, but cannot be related by zig-zag, nor
by an extraction procedure similar to L\'evy's. We call such families
\emph{non-separable.} \excl{The situation is
different with van Oostrom's approach to extraction~\cite{[Oos]}
as discussed in section~\ref{S.zi.ext.}.}


Actually, we show that the sharing concept formalized in DFSs is
\emph{compositional}: any sharing can be decomposed into a weaker sharing
(such as zig-zag, when the latter forms a family-relation) 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 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 recall the
definitions of DRSs and DFSs and some relevant standardization results
for them, and discuss examples. Section~\ref{S.zi.ext.} gives a
characterization of zig-zag relation via extraction, used in
Section~\ref{S.li.zi.fa.} to prove that zig-zag is a family relation in
every non-duplicating stable DRS. In section~\ref{S.sep.} we show that a
family relation in a non-duplicating SDRS is separable iff it is
zig-zag. In Section~\ref{S.impl.drs.} we define and study implementation
DRSs, and show the compositionality of sharing. Conclusions appear in
Section~\ref{S.con.}.



\section{Deterministic Residual and Family Structures}
\label{S.drfs.}


In this section we recall \emph{Deterministic Residual
Structures} (DRSs) and \emph{Deterministic
Family Structures} (DFSs), and give a number of examples. We will also
recall some basic theory of standardization in DRSs from~\cite{[dndrs]}.



\subsection{Deterministic Residual Structures}


A DRS is an \emph{Abstract reduction System} (ARS) with an axiomatized
residual relation. An ARS~\cite{[Hin]} 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$. \excl{, and write $P:t\doar $ if $P$ denotes a (finite or infinite)
reduction starting from $t$.} $\,\,\vert P\vert$ denotes the length of $P$.
$P+Q$ denotes the concatenation of $P$ and $Q$.
\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.



The DRS concept is based on~\cite{[le80],[H.L.]}. DRSs model orthogonal
term as well as graph rewrite systems, both first and
higher order, and including the \lc\ and its sharing evaluation models,
with the standard Church notion of residual. Besides the CTSs of
Stark~\cite{[Sta]}, and the ARSs of Gonthier et al.~\cite{[GLM]}, closely
related, but more syntactically oriented, models are studied
in~\cite{[Oos.th],[Mel],[Raa.th]}. DRSs are a minimal axiomatization of the
residual concept enabling one to develop a theory of
normalization~\cite{[rndrs]} and standardization~\cite{[dndrs]} for
conflict-free reduction systems in an abstract manner, and to study their
semantics~\cite{[dpes],[icalp]}.


\bdl{D.levy.str.}
\suppress{{\bf (Deterministic Residual Structure)}
A \emph{Deterministic Residual
Structure}} A DRS is a pair ${\cal R}=(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:

$\bullet$ [FD] (\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.

$\bullet$  [weak acyclicity] (\cite{[Sta]}) Let $u,v\subt t$, let $u\not=
v$, and let $u/v=\emp$. Then $v/u\not=\emp$.

We call a DRS $\cal R$ \emph{stable} (SDRS) if:
\delete{the following axiom is satisfied: (see Figure~\ref{berry-stab})}

$\bullet$ [stability] If $u,v\subt t$ are different redexes, $t\red{u}e$,
$t\red{v}s$, and $u$ creates a redex $w\subt e$, then the redexes in
$w/(v/u)$ are not $u/v$-residuals of redexes of $s$, i.e.,  they are
created along $u/v$ .
\ed

We call an SDRS \emph{non-duplicating} or \emph{affine}, ASDRS, if the
residual relation is non-duplicating. Note that, since the only observables
of DRSs are redexes, duplicating syntactic rewrite systems may still form
affine SDRSs. For example, the DRS corresponding to innermost reductions in
an orthogonal TRS is an affine SDRS, although innermost redexes may
duplicate their arguments.

\delete{CHECK: Similarly, sharing graph reductions implementing optimal
family reductions are affine SDRSs, although some `housekeeping' steps can
duplicate parts of the sharing graphs (such parts cannot contain redexes,
as otherwise the optimality will be lost).}



Similarly to~\cite{[H.L.],[levy],[le80],[Sta]}, in a DRS $\cal R$
the residual relation on redexes is extended
to all co-initial reductions as follows: $(P_1+P_2)/Q=P_1/Q+P_2/(Q/P_1)$
and $P/(Q_1+Q_2)=(P/Q_1)/Q_2$, and that \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'\,
\Longrightarrow \, P+Q+N\leeqv P+Q'+N$, where $U$ and $V$ are complete
developments of redex sets in the same term. Further,
one defines $P\lleq Q$ iff $P/Q=\emptyset$, and
can show that $P\leeqv Q$ iff
$P\lleq Q$ and $Q\lleq P$; and $P\lleq Q$ iff $Q\leeqv P+N$ for some $N$.
Below, $P\sqcup Q$ will denote $P+Q/P$.
Intuitively, $P\leeqv Q$ means that $P$ can be obtained from $Q$ by
a number of permutations of adjacent steps, therefore `$Q$ and $P$ do
the same work'; and $P\lleq Q$ means that $P$ does less work than $Q$,
the difference being $Q/P$, so  $P+Q/P\leeqv Q$. The following \emph{Strong
Church-Rosser} property can be proved: for any co-initial finite reductions
$P,Q$, $P\sqcup Q\leeqv Q\sqcup P$. \excl{The above relations can
equivalently be defined also using Klop's method of commutative
diagrams~\cite{[Kl.CRS],[Bar]}.}



The stability axiom, and more generally \Lr{L.disj.red.creat.} below,
states that a redex cannot arise from two `unrelated' sources.
The notion of `unrelated' is formalized by the notion of {\em externality},
which expresses the absence of shared (residuals of) redexes. \excl{For
syntactic systems externality is a natural concept relating to overlap between
components of terms involved in reduction steps.}



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

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

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





\bll{L.disj.red.creat.}
{\bf (Stability)} (\cite{[rndrs]})
Let $P:t\doar s$ be external to
$Q:t\doar e$, in a stable DRS, and let $P$
create redexes $W\subts s$. Then the residuals $W/(Q/P)$ of redexes in $W$
are created by $P/Q$, and $Q/P$ is external to~$W$.
\el

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



\subsection{Standardization}
\label{S.stand.}


In this section, we recall a fragment of results from~\cite{[dndrs]},
concerning standardization of reductions, relevant to this paper; so we
restrict ourselves to affine stable DRSs, ASDRSs, only.



\bdl{D.red.need.ess.}
$\bullet$  Let $P:t\doar o$ and $u\subt t$, in a DRS.  We call $u$
{\em erased\/} in $P$ or {\em
$P$-erased\/}\excl{, written $ER_P(u,t)$,} if $u/P=\emp$. We say that $P$
{\em discards\/} $u$ if $P$ is
external to $u$ and erases it.

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


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

$\bullet$ Let $Q:t\doar o$, $P:t\dored{P'}s\doar e$, and $u\subt s$. We
say \excl{$NE_Q(u,s)$, or more precisely $NE_Q(P'u,s)$, if $NE_{Q/P'}(u,s)$. }
\incl{that $u$ is \emph{$Q$-needed} if $u$ is $Q/P'$-needed.}
We call $P$ {\em $Q$-needed\/} if so is every redex contracted in $P$.
We call $P$ {\em self-needed\/} if it is $P$-needed.
The other concepts above are extended
in the same way.
\ed


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$. \excl{The
latter property will be referred to as \emph{CR for residuals}.} 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\doar o$ in an ASDRS.

(1) $w\in t$ is $P$-needed iff it is $P$-erased and $P$-essential.

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

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

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




Self-needed reductions play the role of \emph{standard} reductions in
SDRSs, since we do not have any nesting relation imposed on redexes, unlike
ARSs of ~\cite{[GLM]}, and there is no concept of `left' or `right'
occurrences in DRSs. Furthermore, 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 outside-in left-to-right standard reductions in the
extraction processes of~\cite{[le80],[AL],[Oos]}.


\bdl{D.stanndrs.}
We call a reduction in a DRS \emph{standard} if it is self-needed.
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\}$.
\ed


The following algorithm 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


Termination of the standardization follows immediately from the fact that
$\leng{P/v}\leq\leng{P}-1$. The following fragment (for ASDRSs) of the
standardization theorem from~\cite{[rndrs]} implies the correctness of our
standardization procedure.


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


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 algorithm (and is also a corollary of the
\emph{Discrete Normalization Theorem} of~\cite{[dndrs]}).

In Section~\ref{S.zi.ext.}, we will show 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$).



\subsection{Deterministic Family Structures}



We now recall \emph{Deterministic Family structures} (DFSs) which are
DRSs where in addition a notion of \emph{redex-family} is axiomatized so
that the essence of sharing in the sense of L\'evy~\cite{[levy],[le80]} is
captured, and all the known family notions
(mentioned in the introduction) satisfy these axioms~\cite{[rndrs]}.



\bdl{D.DRS.}
\excl{{\bf (Deterministic Family Structure)}  A \emph{Deterministic Family
Structure} (DFS for short)} A DFS is a triple ${\cal F} =({\cal
R},\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:

(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$, written $Pu\zleq Qv$, 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~\cite{[le80]}. 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.


(2) The relations $\fami$ and $\contr$ satisfy the following axioms:

$\bullet$ [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$.

$\bullet$ [contribution] $\phi\contr \phi'$ iff for any $Pu\fin \phi'$, $P$
contracts at least one redex in $\phi$.

$\bullet$ [creation] If $e\dored{P}t\red{u}s$ and $u$ creates
$v\subt s$, then  $Fam(Pu)\contr Fam((P+u)v)$.

$\bullet$ [FFD] (\emph{Finite Family Developments}) Any reduction that
contracts redexes of a finite number of families is
terminating.\footnote{This axiom was called [termination]
in~\cite{[rndrs]}.}
\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)$.

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



The following special kinds of DFSs will play an important role in this
paper.


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

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




\section{Equivalence of Zig-zag and Extraction}
\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
representations 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]}.

The `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.



\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. In order for the extraction procedure to be
decidable and imply that of the zig-zag relation, we need to  establish the
decidability of $P$-neededness for finite reductions $P$ is ASDRSs.


\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
\incl{See Appendix~A.}
\excl{
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 fist 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 in the previous section.
}
\eproof
\ep


\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
\incl{See Appendix~A.}
\excl{
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). 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



Let $\sclas{P}v$ not be canonical. By \Dr{D.can.re.his.}, there is
$Q:t\dored{P'}e\red{u}s$ such that $Q\leeqv P$ and $v$ is a $u$-residual of
some $v'\subt e$. By \Lr{L.sta.ex.dec.}, $Q$ can be chosen standard. In
$Q$, $u$ does not `contribute' to $v$, and in the search for a shortest
reduction that creates a redex in the zig-zag class of $Qv$, contraction of
$u$ 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]}. Obviously, reductions creating a redex in some
family in a 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 confluent, that is, $Qw''\lextrr{v}Nw\extrr{u}Pw'$
implies $Qw''\extrr{u'}N^*w^*\lextrr{v'}Pw'$. We need a lemma first whose
proof is delayed to Appendix~B, to enable the reader to follow the main
intuition.





\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]
{}     &\rOnto^{P'}  &  {}    &\rTo^{v'}   &{}  &\rTo^{u}       & {} \\
\dOnto<{Q'} &        &\dOnto>\emp &        & \dOnto>\emp &  & \dOnto>\emp \\
{}     &\rOnto^\emp  & {}     & \rTo^{v'}  & {}  &\rTo^{u}      & {} \\
\dTo<{u'}   &        &\dTo>{u'}  &         & \dTo>{u}  &    & \dOnto>\emp \\
{}     &\rOnto_\emp  &  {}    &\rTo^{v}    &{}  & \rOnto_\emp   & {}\\
\dTo<{v}    &        &\dTo<{v}  &       & \dOnto>\emp  &      & \dOnto>\emp \\
{}     &\rOnto_\emp  & {}     &\rOnto_\emp &{}  & \rOnto_\emp   & {}\\
\end{diagram}
\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. 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]
{}     &\rOnto^{P'}  &  {}    &\rTo^{v'}   &{}  &\rTo^{u}       & {} \\
\dOnto<{Q'} &        &\dOnto>\emp &        & \dOnto>\emp &  & \dOnto>\emp \\
{}     &\rOnto^\emp  &\bullet & \rTo^{v'}  &\bullet\ni w' &\rTo^{u}      & {} \\
\dTo<{u'}   &        &\dTo>{u'}  &         & \dTo>{u}  &    & \dOnto>\emp \\
{}   &\rOnto_\emp  &\bullet\ni w'' &\rTo^{v} &\bullet\ni w  & \rOnto_\emp & {}\\
\dTo<{v}    &        &\dTo<{v}  &       & \dOnto>\emp  &      & \dOnto>\emp \\
{}     &\rOnto_\emp  & {}     &\rOnto_\emp &{}  & \rOnto_\emp   & {}\\
\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
By definition of $\zfami$, $Pu\zfami Qv$ implies existence of $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.
\delete{
 \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 &   \\
{}     &\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. The theorem now follows from \Tr{P.on.ca.for.}.
\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 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.


Below, $FAM_z(P)$ (resp. $SFAM_z(P)$) denotes the set of zig-zag classes whose
member ($P$-needed) 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'$.



\suppress{
\bll{L.dec.fam.ex.}
Let $P$ be a standard variant of $Q$. Then $FAM_z(P)\ssq FAM_z(Q)$.

\bproof
Let $u$ be a redex contracted in $P$, say $P=P'+u+P''$. Since $P\leeqv Q$,
$u/(Q/P')=\emp$. But since $u$ is $P$-needed, it has at least one residual
along $Q/P'$ until contracted. Since $Q/P'$ only contracts residuals of
redexes contracted in $Q$, there is a redex $v$ contracted in $Q$, say
$Q=Q'+v+Q''$, such that $u/(Q'/P')=v/(P'/Q')$, i.e., $P'u\zfami Q'v$, and
the lemma follows.
%\begin{figure}
\begin{diagram}[height=1.4em,width=1.4em]
{}     &\rOnto^{P'}  &  {}    &\rTo^{u}   &{}  &\rOnto^{P''}      & {} \\
\dOnto<{Q'} &        &\dOnto   &        & \dOnto    &  & \dOnto>\emp \\
{}     &\rOnto      & {}     & \rTo^{w}  & {}  &\rOnto      & {} \\
\dTo<{v}   &        &\dTo>{w}  &         & \dOnto>\emp  &    & \dOnto>\emp \\
{}     &\rOnto      &  {}    &\rOnto_\emp  &{}  & \rOnto     & {}\\
\dTo<{Q''}    &        &\dOnto  &       & \dOnto  &      & \dOnto>\emp \\
{}     &\rOnto_\emp  & {}     &\rOnto_\emp &{}  & \rOnto_\emp   & {}\\
\end{diagram}
%\caption{} \label{F.zig-fam.}
%\end{figure}
\eproof
\el


\bll{L.dif.re.sa.his.}
If $Pu\not=Pv$, then $Fam_z(Pu)\not=Fam_z(Pv)$.

\bproof
Suppose on the contrary that $Fam_z(Pu)=Fam_z(Pv)$. Then they have the same
canonical form by \Tr{T.un.ex.nor.f.}, say $Qw$, and we have from
\Tr{P.on.ca.for.} that there is $Q'$ such that $Q+Q'\leeqv P$ and
$u=w/Q'=v$ (since $w$ has only one residual along $Q'$) --  contradiction.
\eproof
\el


}

\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




\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 $k<m$ implies
$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]
{}    &\rOnto^{P'_k} & {}     &\rOnto^{Q'_k}  & {}  &    &  {}  &   & {} &
&{} \\
      &      &\dTo<{u'_k}  &    & \dTo>{u_k} &        &   &      &    &    & \\
{}      &   & {} &\rOnto_{Q'_k/u'_k} & {}     & \rTo_{u_{k+1}}      &{}
&\rOnto   &{} & \rTo_{u_{m-1}}      &{} \\
\end{diagram}
\eproof
\el


\btl{T.lin.dr.sta.df.}
Let $\cal R$ be a non-duplicating stable DRS. Then ${\cal
F_R}=(R,\zfami,\zcontr)$ is a 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


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


\bpl{P.leqv.sam.se.es.fa.}
Let $P,Q$ be finite co-initial reductions in an ASDRS. Then

(1) $P\lleq Q$ iff $\exists Q'\leeqv Q: FAM_z(P)\ssq FAM_z(Q')$;

(2) $P\leeqv Q$ iff $SFAM_z(P)=SFAM_z(Q)$.
\ep
}



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


Based on the results of previous sections, we now 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}. Recall that a complete
family-reduction is a multi-step reduction contracting, in each multi-step,
all members of a single family in parallel (we will often omit `complete').

We will need the following lemma from~\cite{[rndrs]}.

\suppress{
Recall that 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. 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. Below we will only consider complete
family-reductions, and will omit `complete'.
}


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







\bll{L.aff.un.f.l.}
Let ${\cal F}={\cal R}, \fami,\contr)$ be an affine DFS. Them the following
are equivalent:

(1) $\cal F$ is separable;

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

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

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


\bproof
$(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.}
(see~\cite{[azdfs]}).


$(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).

$(3)\imply (4)$ Immediate.

$(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).
\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
\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. \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.
\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 $\emp$, and that families are considered relative to
$\emp$, i.e, all histories start with $\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

$\bullet$ the branches of the reduction graph of the underlying ARS $A$ of
${\cal R}_I=(A,/)$ are family-reductions starting from $\emp$, each edge
(i.e., a reduction step) being a multi-step contracting a family of
redexes.

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

$\bullet$ 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)$.
\ed


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


\bll{L.res.fam.fam.}
Let $P:\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


\excl{
\bll{L.fam.inc.le.in.}
Let $P:t\doar s$ and $Q:t\doar o$ be \cfrs\ in a comma-DFS ${\cal
F}_t=(R_t,\fami,\contr)$, and let $FAM(P)\ssq FAM(Q)$. Then there is a
multi-step reduction $N:s\doar o$ such that $Q\leeqv P+N$ is a \cfr\ (hence
$P\lleq Q$).

\bproof
Let $U$ be a family $\phi$ contracted in $P$, say $P=P'+U+P''$. Since
$FAM(P)\ssq FAM(Q)$, $Q$ contracts $\phi$ as well, say $Q=Q'+V+Q''$, where
redexes $Q'v$ with $v\in V$ from family $\phi$ is the final term of $Q'$.
let $U'=U/(P'/Q')$ and $V'=V/(Q'/P')$. By \Lr{L.res.fam.fam.}, both $U'$
and $V'$ form complete sets of redexes of family $\phi$ in the final term
of $P'\sqcup Q'$, we have $U=V'$. Hence $U/(Q/P')=\emp$, for any multi-step
$U$ of $P$, implying $P/Q=\emp$. Again by \Lr{L.res.fam.fam.}, $Q/P$ is
again \cfr, and $P+Q/P\leeqv Q$. So we can take $Q/P$ for $N$.
\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
\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.}. \nec\ Immediate from
\Dr{D.str.sh.}.
\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.



In order to prove that implementation DRS can implement optimal
family-reductions in DFSs, let us recall the relative optimality theorem
from~\cite{[rndrs]}:


\begin{deff}\em
\label{D.rel.need.}
(\cite{[rndrs]}) (1) Let $\stab$ be a set of terms in a DRS. We call a
redex $u\subt t$ {\em $\stab$-needed} \excl{ written $NE_\stab (u,t)$,} if
at least one residual of it is contracted in any reduction from $t$ to a
term in $\stab$, and call it {\em $\stab$-unneeded} \excl{written $UN_\stab
(u,t)$,} otherwise. We call a multi-step $U\subts t$ $\stab$-needed if it
contracts at least one $\stab$-needed redex.

(2) We call a set $\stab$ of terms {\em stable\/} if: (a)
$\stab$ is {\em closed under parallel moves}: for any $t\not\in \stab$, any
$P:t\doar o\in \stab$, and any $Q:t\doar e$ which does not contain redexes
in $\stab$, the final term of $P/Q$ is in $\stab$; and  (b) $\stab$ is {\em
closed under unneeded expansion}: for any $e\red{u}o$ such that $e\not\in
\stab$ and $o\in \stab$, $u$ is $\stab$-needed.
\end{deff}



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


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


\bll{L.nee.imp.}
Let $\stab$ be a stable set of terms in a DFS $\calF$ not containing the
initial term $t_0=\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



\bcl{T.impl.theo.}
{\bf (Optimal Implementation)}
Let $\stab$ be a stable set of terms in a DFS $\calF$. Then optimal (i.e.,
$\stab$-needed) reductions in $\calF_I$, w.r.t. $\stab$, implement optimal
family-reductions in $\calF$, w.r.t.~$\stab$.
\ec




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



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.  Together
with~\cite{[rndrs]}, this work completes the first chapter of an axiomatic
study of the optimality theory.



Further, 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. These results have
been used essentially in constructing a fully adequate Event Structure
style semantics for ASDRSs, and thereby, for all orthogonal reduction
systems~\cite{[dpes]}. The latter construction covers for example the
construction of Event Semantics for orthogonal graph rewriting systems
in~\cite{[KKSdV],[Sch]}. These results have also been used in the
definition of \emph{independence} of computations, and construction of
Euclidian Geometry from the reduction spaces in orthogonal rewrite
systems~\cite{[icalp]}.


Finally, we have shown that sharing is compositional. In particular, any
family relation can be decomposed into the 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]}). This makes clear the
importance of the comprehensive investigation of affine families undertaken
in this paper. As for zig-zag, we have demonstrated in~\cite{[rndrs]}
(see Example~4.1) that zig-zag need not be a family-relation in any
(duplicating) SDRS. However, 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 (which fails to hold in
Example~4.1 mentioned above)  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.


\suppress{

\vspace{0.20cm}


\section*{Acknowledgements}


The first author wishes to thank Jan Willem Klop, Jean-Jacques L\'evy, Luc
Maranget, Vincent van Oostrom and Roel de Vrijer for the opportunity to
work at INRIA Rocquencourt and VU Amsterdam and in October 1996, where this
work was essentially completed, and for fruitful discussions.


Diagrams were drawn using Paul Taylor's Diagram package.
}


\begin{thebibliography}{99}



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



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

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

\bibitem[{BBKV76}]{[BBKV]}
Barendregt H. P., Bergstra J., Klop J. W., Volken H. Degrees, reductions
and representability in the $\lambda$-calculus. Report 22, University
of Utrecht,  1976.


\suppress{
\bibitem[{Bed87}]{[Bed]}
Bednarczyk M. A. Categories of asynchronous systems. PhD Thesis, University
of Sussex, Brighton, 1987.
}

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

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


\bibitem[{CK95}]{[C.K.]}
Clark D., Kennaway R. Event structures and non-orthogonal term graph rewriting.
MSCS 6:545-578,~1996.


\bibitem[{CELMR94}]{[CEL]}
Corradini A., Ehrig H., L\"owe M., Montanari U., Rossi F. An event
structure semantics for safe graph grammars. In proc PROCOMET'94, IFIP
Transactions A-56, 1994.
}

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



\bibitem[{GAL92}]{[GAL]}
Gonthier G., Abadi M., L\'evy J.-J. The geometry of optimal lambda
reduction.     POPL'92,~p.15-26.


\bibitem[{GLM92}]{[GLM]}
Gonthier G., L\'evy J.-J., Melli\`es P.-A. An abstract Standardisation
theorem.   LICS'92, \delete{Santa Cruz, California, 1992,} p.~72-81.

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


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


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

\bibitem[{HP91}]{[H.P.]}
Hoffmann B., Plump D. Implementing term rewriting by Jungle evaluation.
Theoretical Informatics and Applications 25:445-472, 1991.


\bibitem[{Kat90}]{[Kath]}
Kathail V. Optimal Interpreters for Lambda-calculus based functional
languages, Ph.D. thesis, MIT, 1990.


\bibitem[{KS89}]{[K.S.]}
Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in  regular
combinatory reduction systems.
Report. University of East Anglia, 1989.

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


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

\bibitem[{KG96}]{[dndrs]}
Khasidashvili Z.,  Glauert J. R. W. Discrete normalization in Deterministic
Residual Structures.  \excl{In: Proc. of the $5^{th}$ International
Conference on Algebraic and Logic Programming,} ALP'96, Springer LNCS,~1139,
M.~Hanus, M. Rodr\'{\i}guez-Artalejo, eds. 1996, p.135-149.


\bibitem[{KG97}]{[azdfs]}
Khasidashvili Z., Glauert J. R. W.  Zig-zag, extraction and separable
families in stable non-duplicating Deterministic Residual Structures.
Technical Report IR-420, Free University, Amsterdam, February 1997. 24~pp.


\bibitem[{KG97a}]{[icalp]}
Khasidashvili Z., Glauert J. R. W. The Geometry of Orthogonal Reduction
Spaces. \excl{In Proc. of $24^{th}$ International Colloquium on Automata,
Languages, and Programming,} ICALP'97, Springer LNCS, vol.~1256,
P.~Degano,  R.~Gorrieri, and A.~Marchetti-Spaccamela, eds. 1997,
p.~649-659.


\bibitem[{KG97b}]{[dpes]}
Khasidashvili Z., Glauert J. R. W.  Relating conflict-free transition and
event models.   \excl{In Proc. of the $22^{nd}$ International Symposium on
Mathematical Foundations of Computer Science,} MFCS'97, Springer LNCS,
vol.~1295, I.~Pr\'{\i}vara, P.~Ru\v{z}i\v{c}ka, eds. 1997, p.~269-278.


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


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

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

\bibitem[{Lam90}]{[Lam]}
Lamping J. An algorithm for optimal lambda calculus reduction.
POPL'90,~p.16-30.

\suppress{
\bibitem[{Lan93}]{[Lan.th]}
Laneve C. Optimality and Concurrency in Interaction Systems. Ph.D.
Thesis, University of Pisa,~1993.


\bibitem[{Lan94}]{[Lan94]}
Laneve C.  Distributive evaluations of $\lambda$-calculus,
Fundamenta Informaticae, 20(4):333-352, 1994.

\bibitem[{LM94}]{[L.M.]}
Laneve C., Montanari U. Axiomatizing permutation equivalence.
MSCS, 6:219 - 249, \delete{Cambridge University Press,} 1994.
}

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


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


\bibitem[{Mar91}]{[Mar91]}
Maranget L. Optimal derivations in weak $\lambda$-calculi and in orthogonal
Term Rewriting Systems.   POPL'91, p.~255-269.

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


\bibitem[{NPW81}]{[NPW]}
Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and
Domains. Part 1. TCS 13:85-108, 1981.


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


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


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


\bibitem[{Oos96}]{[Oos]}
Van Oostrom V. Higher order families.
RTA'96, Springer LNCS, vol.~1103, Ganzinger, H., ed., 1996, p.~392--407.


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


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


\bibitem[{Sch94}]{[Sch]}
Schied G. On relating rewrite systems and graph grammars to event
structures. In: Schneider H.-J. Ehrig H., eds. GTCS'94, Springer LNCS,
vol.~776, 1994, p.~326-340.


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


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

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

\bibitem[{Win86/89}]{[Win89]}
Winskel G. An introduction to Event Structures. In proc. of School/Workshop
on `Linear time, branching time and partial order in logics and models of
concurrency'. Springer LNCS, vol.~354, 1989, p.~364-397. Extended version
appears as Cambridge University Computer Laboratory Report n.~95, 1986.
}


\bibitem[WN95]{[WN]}
Winskel G., Nielsen M.  Models for concurrency.   In:  S.~Abramsky, D.~Gabbay,
and T.~Maibaum eds.  Handbook  of Logic in Computer Science, vol.~4,
\excl{Oxford University Press} OUP, 1995, p.~1-148.

\end{thebibliography}

\pagebreak


\section*{Appendix~A}


{\bf Proof of Proposition~\ref{P.dec.stan.}}\\
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 in Subsection~\ref{S.stand.}.\\



\noindent {\bf Proof of Lemma~\ref{L.sta.ex.dec.}}
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). 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}\\



\noindent {\bf Proof of \Lr{L.nee.imp.}}
\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.

\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 Corollary~3.1 of~\cite{[rndrs]} (which states exactly
that the residuals of $\stab$-unneeded redexes remain $\stab$-unneeded).
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$.



\section*{Appendix~B: Proof of \Lr{L.mov.red.cre.}}
\label{S.append.}


We use the following lemma from~\cite{[rndrs]}, and three simple
new lemmas in this proof.

\bll{L.external.rem.ext.}
 (\cite{[rndrs]})
Let $P:t\doar s$ be external to a set $U\subts t$ of redexes, in a
DRS, and let $Q:t\doar o$. Then $P/Q$ is external to the set $U/Q$.
\el

\suppress{
\bll{L.ext.no.le.eqv.}
(\cite{[dndrs]}) Let $u\subt t_0\dored{P}t_k$, and let $P$ be external to
$u$, in a DRS. Then $u\not\leeqv P$.
\el
}


\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]
{}         &\rTo^{u} & {}       &\rTo^{v}  & {}     &\rOnto^{P'} &{}  \\
\dOnto     &         &\dOnto    &          & \dOnto &            &\dOnto\\
{}         &\rTo     & {}       &\rTo^{v'} & {}     &\rOnto      &{}  \\
\dTo^{v''} &         &\dTo^{v'} &          & \dOnto &            &\dOnto\\
{}         &\rOnto   &  {}      & \rOnto   & {}     &\rOnto      &{}  \\
\dOnto     &         &\dOnto    &          & \dOnto &            &\dOnto\\
Q          &\rTo_{u'}& Q'     &\rOnto_\emp & {}     &\rOnto      &{}  \\
\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]
{}       &\rTo^{v^*} & {}     &\rTo^{u^*}  & {}     &\rOnto^{P'} &{}  \\
\dOnto<Q  &         &\dOnto<{Q^*} &          & \dOnto &        & \dOnto \\
{}      &\rOnto^\emp & {}       &\rTo^{u'} & {}     &\rOnto      &{}  \\
\dTo<{u'} &         &\dTo<{u'} &          & \dOnto>\emp &            & \dOnto\\
{}      &\rOnto_\emp   &  {}    & \rOnto_\emp & {}     &\rOnto      &{}  \\
\end{diagram}
\eproof
\el


\bll{L.dif.no.l.eq.}
Let $P +u\staeq Q +v$ and let $u\not=v$. Then $P\not\leeqv Q$.

\bproof
Suppose on the contrary that $P\leeqv Q$. Then $P +u\staeq Q +v$ iff
$u\leeqv v$. But, by [weak acyclicity], this is only possible when $u=v$ -- a
contradiction.
\eproof
\el



\bll{L.sta.al.ne.}
Let $P\staeq Q$. Then any non-empty step in Klop's diagram of $P$ and $Q$
in $P$-needed.

\bproof
Since every step in the diagram is a residual of a redex contracted in $P$
or $Q$, the lemma follows immediately from \Lr{L.era.and.ess.im.ne.}.(4).
\eproof
\el



\noindent{\bf Proof of \Lr{L.mov.red.cre.}}
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$. We show that
$P/Q\not=\emp$.

\begin{diagram}[height=1.4em,width=1.4em]
{}          &\rOnto^{P}     & {}           &\rTo^{u}     & {}         \\
\dOnto<Q    &             &\dOnto<{Q/P}>u  &             & \dOnto_\emp  \\
{}          &\rOnto^{P/Q}_v & {}           &\rOnto_\emp    & {}         \\
\dTo<v      &               &\dOnto     &             &  \dOnto_\emp \\
{}          &\rOnto_\emp    &  {}          & \rOnto_\emp & {}         \\
\end{diagram}
Suppose on the contrary that $P/Q=\emp$. Then, by [weak acyclicity],
$v=u/(Q/P)$. Further, by \Lr{L.dif.no.l.eq.}, $P\not\leeqv Q$, hence
$P/Q=\emp$ implies $Q/P\not=\emp$. 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.sta.al.ne.}. 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]
{}       &\rOnto^{P_1} & {}     &\rTo^{v''}  & {}     &\rOnto^{P_2} &{}
&\rTo^{u}  & {} \\
\dOnto<Q  &         &\dOnto  &          & \dOnto &        & \dOnto &      &
\dOnto>\emp \\
{}      &\rOnto^\emp & {}       &\rTo^{v} & {}     &\rOnto^\emp      &{}
&\rOnto^\emp      &{} \\
\dTo<{v} &         &\dTo<{v} &          & \dOnto_\emp &         &
\dOnto_\emp &            & \dOnto>\emp  \\
{}      &\rOnto_\emp   &  {}    & \rOnto_\emp & {}     &\rOnto_\emp
&{}  & \rOnto_\emp & {}\\
\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]
{}       &\rTo^{P_1} & {}     &\rOnto^{P'_2}  & {}     &\rTo^{v'} &{}
&\rTo^{u}  & {} \\
\dOnto<Q  &         &\dOnto  &          & \dOnto &        & \dOnto &      &
\dOnto>\emp \\
{}      &\rOnto^\emp & {}       &\rOnto^\emp & {}     & \rTo^{v}      &{}
&\rOnto^\emp      &{} \\
\dTo<{v} &         &\dTo<{v} &          & \dTo<{v}  &            & \dOnto
&          & \dOnto>\emp  \\
{}      &\rOnto_\emp   &  {}    & \rOnto_\emp & {}     &\rOnto_\emp
&{}  & \rOnto_\emp & {}\\
\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]
{}     &\rOnto^{P'}  &  {}    &\rTo^{v'}   &{}  &\rTo^{u}       & {} \\
\dOnto<{Q'} &        &\dOnto>\emp &        & \dOnto>\emp &  & \dOnto>\emp \\
{}     &\rOnto^\emp  & {}     & \rTo^{v'}  & {}  &\rTo^{u}      & {} \\
\dTo<{u'}   &        &\dTo>{u'}  &         & \dTo>{u}  &    & \dOnto>\emp \\
{}     &\rOnto_\emp  &  {}    &\rTo^{v}    &{}  & \rOnto_\emp   & {}\\
\dTo<{v}    &        &\dTo<{v}  &       & \dOnto>\emp  &      & \dOnto>\emp \\
{}     &\rOnto_\emp  & {}     &\rOnto_\emp &{}  & \rOnto_\emp   & {}\\
\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.sta.al.ne.} that
$P'/Q'=\emp$. The converse is proved similarly, so $P'\leeqv Q'$. It
follows that $u=u'/v'$ and $v=v'/u'$.


\end{document}






