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

\topmargin   0pt

\textwidth   6.5in
\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}{complete family-reduction}
\newcommand{\cfrs}{complete family-reductions}
\newcommand{\qp}{quasi-persistently}
\newcommand{\stc}{strongly cofinal}
\newcommand{\rn}{RN}
\newcommand{\trnt}{the Relative Normalization theorem}
%\newcommand{\qp}{quasi-persistently}
%\newcommand{\stc}{strongly cofinal}
\newcommand{\pmn}{persistently $\stab$-needed}
\newcommand{\qprn}{quasi-persistently $\reg$-needed}
\newcommand{\qpmn}{quasi-persistently $\stab$-needed}
\newcommand{\das}{\downarrow_{\stab}}
\newcommand{\dar}{\downarrow_{\reg}}
\newcommand{\stab}{{\cal S}}
\newcommand{\reg}{{\cal 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}



\title{Zig-zag, Extraction and Separable Families \\
in Non-duplicating Stable Deterministic Residual Structures}
\author{Zurab Khasidashvili\\
Department of Mathematics and Computer Science
\\ Free University\\
De Boelelaan 1081a, 1081 HV Amsterdam, Netherlands\\
zurab@cs.vu.nl
 \and
John Glauert\\
School of Information Systems \\University of East Anglia \\
Norwich NR4 7TJ England \\
jrwg@sys.uea.ac.uk
\thanks{This work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300. It was
(essentially) completed during a fruitful visit of the first author to
Vrije Universiteit in October 1996, where he was supported by a Dutch NWO
grant.}
}


\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 are SDRSs
with 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 start to investigate ways of constructing DFSs from SDRSs.
This is interesting for at least the following two purposes:

\begin{enumerate}
\item[(1)]
 to develop
an \emph{algebraic} theory of sharing for conflict-free rewrite and
transition systems in order to understand what properties a sharing concept must
possess to imply a reasonable theory of optimal evaluation, and

\item[(2)]
to give an \emph{Event Structure} style semantics to conflict-free rewrite
and transition systems with \emph{erasure} of redexes.
\end{enumerate}

\noindent As a first step, we only consider non-duplicating systems, and
show that every non-duplicating SDRS is already a DFS if the \emph{zig-zag}
is taken for the family relation. (Zig-zag is simply the symmetric and
transitive closure of theresidual relation on redexes with histories.) We
also show that the family relation in a non-duplicating DFS coincides with
the zig-zag if and only if it is \emph{separable} in some sense. To achieve
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. As a side result, we get a Prime Event Structure semantics for
non-duplicating SDRSs. Various forms of conflict-free Graph Rewriting
Systems (or Graph Grammars) fall in the category of SDRSs.
\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', hoping that it would be possible to mimic
reductions contracting whole families in multi-steps by reduction of some
graph representation in which every multi-step would be represented by
contraction of a single redex~\cite{[levy],[le80]}.  There was no other way
-- 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 of it to Interaction
Systems, which cover most of the languages  with a constructor-destructor
discipline~\cite{[AL],[AL2]}. Recently, van Oostrom has generalized the
optimality theory to the whole class of orthogonal Higher-order Rewrite
Systems (HORSs)~\cite{[Oos]}.

\Le\ introduced the family concept in three different ways: via a suitable
notion of \emph{labelling}, via \emph{extraction}, and as \emph{zig-zag}.
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
(therefore unique in its permutation-equivalence class), 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 \Le\ 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 family concept~\cite{[AL]}. Independently
and much earlier, Kennaway and Sleep~\cite{[K.S.]} defined their concept of
labelling for orthogonal Combinatory Reduction Systems (CRSs), improving
Klop's original labelling system for CRSs~\cite{[Kl.CRS]}, which cover
orthogonal TRSs and Interaction Systems, and 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.]}, DAG (Directed Acyclic Graph)
Rewriting~\cite{[Mar91]}, and many others (in particular, covering cyclic
graph reduction as well), 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. First such structures were indeed introduced by the
authors of this paper in~\cite{[rndrs]} as \emph{Deterministic Family
Structures} (DFSs). This became possible also due to recent developments of
abstract reduction systems with axiomatized residual relation, such as
\emph{Concurrent Transition Systems} (CTSs) of Stark~\cite{[Sta]} and
\emph{Abstract Reduction Systems} of Gonthier et al~\cite{[GLM]}.

Our DFSs are defined as \emph{Deterministic Residual Structures} (DRSs)
with axiomatized family relation. DRSs, in turn, are Abstract Reduction
Systems with axiomatized residual relation, similar to CTSs~\cite{[Sta]}
and ARSs~\cite{[GLM]}, 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. (Therefore,
DRSs cover more rewrite and transition systems than conflict-free CTSs or
ARSs.) CTSs have successfully been used to give semantics to machine
networks, while ARSs have been used to study more syntactic properties of
orthogonal rewrite systems, such as standardization. Despite its highly
abstract nature, a counterpart of Berry's \emph{stability}
property~\cite{[berry]} enables 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 `(partial) 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, 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, and DFSs
can be interpreted as (\emph{deterministic} or \emph{conflict-free}) Prime
Event Structures (PESs)~\cite{[NPW],[Win],[Win89]}.


In this paper, we study the possibility of defining  a family relation in
stable DRSs.  As the first step, we will only consider non-duplicating
SDRSs. At first sight, one might think that there is no need or possibility
of sharing in such SDRSs, and that the optimality theory for
non-duplicating SDRSs is simple. However, this is not the case -- the very
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 (i.e.,
with the \emph{shift} operation) extraction families. These 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$ (in a slightly simplified notation),
simultaneously creates the two $\mu$-redexes in $s$; this redexes are
intuitively in the same family, but cannot be related by the zig-zag, nor
by an extraction procedure similar to L\'evy's one. The situation is
different with van Oostrom's approach to extraction~\cite{[Oos]}, and we
will comment on it later (see a discussionin section~\ref{S.zi.ext.}).


We will show that the zig-zag relation is a family relation in the sense
that it satisfies the family-axioms of DFSs. So every non-duplicating
stable DRSs is in fact a DFS with the zig-zag as the family relation. The
family relation in a non-duplicating DFS need not coincide with the
zig-zag. However, if the family relation is \emph{separable}, i.e., no
redex can create two different redexes in the same family, then it must
coincide with the zig-zag. The converse is also true -- zig-zag is
separable in non-duplicating DFSs. This results are obtained by defining an
abstract extraction procedure and showing that zig-zag coincides with our
extraction-family relation. The technical contribution 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. \footnote{Actually, the extraction process was
claimed to be syntactic in~\cite{[le80]}. To quote \Le~\cite{[le80]}: `We
turn now to the hard part of this paper, which is to show that the family
relation is decidable. The trouble comes from the \emph{necessity} of
looking now inside $\lambda$-expressions and from not being able to go on
with algebraic manipulations'.}




Construction of DFSs from non-duplicating SDRSs has particularly important
semantic applications. Since families in DFSs, ordered by the contribution
relation, form (conflict-free) PESs, our construction yields a translation
of determinate \emph{stable} CTSs into conflict-free PESs  (which are
\emph{stable} Event Structures~\cite{[Win89]}), linking two widely accepted
(operational and domain-theoretic) models of computation. Moreover, in a
forthcoming paper~\cite{[dpes]}, we define extensions of PESs with
axiomatized permutation equivalence and erasure relations, we show that
thus extended event models are equivalent to non-duplicating SDRSs (as they
yield isomorphic reduction/configuration domains), and the construction in
this paper of a DFS from non-duplicating SDRSs is one of the essential
blocks in establishing the above isomorphism.





The paper is organized as follows. In next two sections, we recall
definitions of DRSs and DFSs, and some relevant standardization results
for them. 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, which is
the main result of this paper. In section~\ref{S.sep.} and show that a
family relation in a non-duplicating SDRS is separable iff it is the
zig-zag. In section~\ref{S.leeq.zig.}, we give useful characterizations of
L\'evy's embedding and equivalence relations via zig-zag. In
section~\ref{S.app.}, we discuss an application of our results. Conclusions
appear in Section~\ref{S.con.}.




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


In this section we recall definition of \emph{Deterministic Residual
Structures} (DRSs), which are \emph{Abstract Reduction Systems} (ARSs)
satisfying certain properties concerning residuals, and \emph{Deterministic
Family Structures} (DFSs) which are DRSs with axiomatized \emph{family}
relation on redexes with histories. We will also introduce \emph{zig-zag}
and \emph{separable} DFSs, and discuss an example.


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


\bd
An ARS is a triple $A$ = (\emph{Ter},\emph{Red},$\ar$)
where \emph{Ter} is a set of \emph{terms}, ranged over by
$t,s,o,e$; \emph{Red} is a set of \emph{redexes} (or \emph{redex occurrences}),
ranged over by $u,v,w$; and
$\ar:Red\ar (Ter\times Ter)$ is a function such that for any $t\in Ter$
there is only a finite set of $u\in Red$ such that $\ar(u)=(t,s)$,
written $t\red{u}s$. This set will be known as the redexes of term $t$, where
$u\subt t$ denotes that
$u$ is a member of the redexes of $t$ and $U\subts
t$ denotes that $U$ is a subset of the redexes.
Note
that $\ar$ is a \emph{total} function, so one can identify $u$ with the
triple $t\red{u}s$. A \emph{reduction} is a sequence
$t\red{u_1}t_2\red{u_2}\ldots$. Reductions are denoted by $P,Q,N$. We write
$P:t\doar s$ or $t\dored{P}s$ if $P$ denotes a reduction (sequence) from
$t$ to $s$. \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.
\ed

\delete{
DRSs are similar to Determinate CTSs of Stark~\cite{[Sta]},
to ARSs of Gonthier et al.~\cite{[GLM]}, and to
Descendant Rewriting Systems of van Oostrom~\cite{[Oos.th]}.
The main difference from DCTSs is that Stark requires a
non-duplicating residual relation, and distinguishes a start state.
So Differently from ARSs, we do not impose a nesting relation on redexes. The
difference from van Oostrom's DRSs is that in the latter the notion of {\em
descendant} of any subterm/position of a term is formalized, not only the
notion of residual of redexes. Several refined concepts of abstract
rewriting are studied in~\cite{[Lan.th]}.
}

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~\cite{[levy],[H.L.],[Kl.CRS],[Kath],[Lam],[OCRS],[KKSdV],[Nip.b],[O
os.th],[Raa.th],[Gue]}. Besides CTSs of Stark~\cite{[Sta]}, and ARS of
Gonthier et al.~\cite{[GLM]}, closely related, but more syntactically
oriented, models are studied in~\cite{[Oos.th],[Mel],[Raa.th]}.



\bdl{D.levy.str.}
{\bf (Deterministic Residual Structure)}  A \emph{Deterministic Residual
Structure} (DRS for short) 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 of residuals of a
redex under any reduction is defined by transitivity.

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

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

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

We call a DRS $\cal R$ \emph{non-duplicating} or \emph{affine}, ADRS, if
the residual relation in $\cal R$ is non-duplicating.
\ed

Non-duplicating DRSs which we study here are essentially determinate CTSs,
 with no
distinguished start states. Having in mind possible generalization
of our results to the non-affine case, we will still speak of affine
DRSs, rather than DCTSs.


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$. The above relations can
equivalently be defined also using Klop's method of commutative
diagrams~\cite{[Kl.CRS],[Bar]}.

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

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

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


\begin{figure}
\begin{diagram}[height=2em,width=2em]
 t      & \rTo^u       & e             & \rTo^w           & {}  \\
 \dTo^v &              &  \dOnto_{v/u}  &                 &      \\
s       & \rOnto_{u/v} & o              & \rOnto_{w/(v/u)}   & {}  \\
\end{diagram}
%\caption{Berry's Stability}\label{berry-stab}
\end{figure}

\ed


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


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. 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.8em,width=1.8em]
t_0          &\rOnto^{P_i}& & t_i       &\rTo^{u_i}   & t_{i+1} {}\\
\dOnto<{Q_j}&            & &\dTo<{Q_j/P_i}&         & \dOnto     \\
{}       &\rOnto^{P_i/Q_j}& & {}    & \rOnto^{U_{i,j}} & {}   \\
\dTo<{v_j}   &         & &\dOnto^{V_{i,j}} &             &  \dOnto   \\
{}           &\rOnto      & &  {}       & \rOnto      & {}   \\
\end{diagram}
\ed

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




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






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 is captured, and all the known family notions
(mentioned in the introduction) satisfy these axioms~\cite{[rndrs]}.
It is shown in~\cite{[rndrs]} that any DFS is a stable DRS.



\bdl{D.DRS.}
{\bf (Deterministic Family Structure)}  A \emph{Deterministic Family Structure}
(DFS for short) 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],[dndrs]}.}
\ed


The following two 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$; the corresponding contribution relation
$\zcontr$ is determined by [contribution]. (In general, one might view
[contribution] as the
definition of $\contr$ via $\fami$, rather than as an axiom.)

(2) We call a 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$.
\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.8em,width=1.8em]
\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 again $\psi\contr \phi_1,\phi_2$, and this would yield
a ZDFS.


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. They only study
`reasonable' separable families, where reasonability is only visible from
the fine structure of rewrite steps (which may involve creation of a redex
and its  duplication or erasure in an atomic move). We will comment on it
below. On the contrary, `accidental' sharing is employed in graph rewriting
systems of~\cite{[H.P.]}, where sharing of redexes with the same pattern
are allowed even if they have completely different origin. Such an approach
goes beyond L\'evy's approach of optimality, but is completely legal for
our concept of DFSs. As we have shown in~\cite{[rndrs]}, such a sharing
also allows a reasonable theory of optimality, as long as our family axioms
are satisfied.



\section{Standardization}

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}, or more precisely, $P'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{discards} concept however does 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.
Consequently, $P$ is self-needed iff it is self-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]}.


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$, when 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 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 reduction, and call $Q$ a \emph{standard
variant} of $P$. Note that \Lr{L.fin.self.ese.var.} 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.fin.self.ese.var.}.(2).
If it is created by $u_{n-2}$, then the latter is $P$-needed too, by
\Lr{L.fin.self.ese.var.}.(3). Otherwise, the ancestor redex of $u_{n-1}$ in
$t_{n-2}$ is $P$-needed by \Lr{L.fin.self.ese.var.}.(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 the next section, 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 -- the number of $P$-needed steps in $P$).



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


In this section, we introduce an abstract extraction algorithm
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. The 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 one is due to
Asperti and Laneve~\cite{[AL]}, and the second one to van
Oostrom~\cite{[Oos]}.

The `problem' arises because a redex (in general) can create a number of
redexes `intuitively' in the same family, which cannot happen in the \lc\
or in 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 arguments of the
contracted redex and 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 live with 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 to match the labelling. On the contrary, van Oostrom
works with the refined rewrite systems (where reduction steps are either
TRS steps or substitution steps) and no operation like shift is necessary
to insure coincidence of labelling, extraction and zig-zag families.



To summarise, note that~\cite{[AL]} work with non-separable families, from
which many difficulties arise, while~\cite{[Oos]} works with separable
ones, and coincidence of the three family concepts can be established
smoother in the latter case. We find the latter solution more appealing and
correct, as labelling anyway (implicitly) requires work with refined
systems. Therefore, the abstract extraction algorithm which we introduce
below follows van Oostrom's approach. Our results will shed further light
on the separability problem, and as we will also show in our abstract
setting, it is not surprising that the family relation of~\cite{[AL]} does
not coincide with the zig-zag in Interaction Systems in general.



\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,  transfers 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, and the standardization procedure of $P$ is
computable.

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


\bll{L.sta.ex.dec.}
Let $Q:t\dored{P}s\red{u}e$ and let $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$ (that is, $P\leeqv P'+P''$ and $u=u'/P''$) and $u'$
does not create $v$.

\bproof
We show that $ST(Q)$ can be taken for $Q'$. By \Dr{D.ess.rel.red.}, $ST(Q)$
is obtained from $Q$ by a sequence of transformations $Q=Q_1,Q_2,\ldots,
Q_n=ST(Q)$ such that $Q_{i+1}$ is obtained from $Q_i$ by permuting the
first $Q$-needed step that has preceding $Q$-unneeded steps before those
$Q$-unneeded steps (all $Q_i$ are L\'evy-equivalent). Since $u$ is the last
$Q$-needed step in $Q$ by \Lr{L.era.and.ess.im.ne.}.(2), any $Q_i$ with
$i<n$ has the form $P_i+u$ such that $P_i\leeqv P$, and $P_{n-1}$ has the
form $P_{n-1}:t\dored{P'}o\dored{P''}s$ where $P'$ is $Q$-needed and $P''$
is $Q$-unneeded. By \Lr{L.era.and.ess.im.ne.}.(3), $P''$ cannot create $u$,
i.e., there is $u'\subt o$ such that $u'/P''=u$, and $u'$ is $Q$-needed by
\Lr{L.era.and.ess.im.ne.}.(4). 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.8em,width=1.8em]
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\}$, 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 can be found in the appendix.





\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.8em,width=1.8em]
{}     &\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.8em,width=1.8em]
{}     &\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, it follows immediately from [stability] that 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 a non-duplicating stable DRS, $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.
 \begin{diagram}[height=1.8em,width=1.8em]
       &        &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 decidability of construction 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 establish the main result of this paper -- we show that,
in ASDRSs, the zig-zag  relation forms a family relation, that is, it
satisfies the family axioms of DFSs. We also give a useful characterization
of \Le-equivalence via self-needed families.


Below, $FAM_z(P)$ (resp. $SFAM_z(P)$) denotes the set of zig-zag classes whose
member (resp. $P$-needed) redexes are contracted in $P$, in an ASDRS; and
$Fam_z(Qu)$ denotes the zig-zag class of~$Qu$.


\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.6em,width=1.8em]
{}     &\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\stan{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 $Q\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
$Pv\extrr{w}P'v'$ implies that $P\leeqv P'+w$, and by \Lr{L.dec.fam.ex.},
$FAM_z(P')\ssq FAM_z(P'+w)\ssq FAM_z(P)$.
\eproof
\el

\bdl{D.zi.contr.}
Let $\phi',\phi$ be zig-zag classes. We write $\phi'\zcontr\phi$ iff for
any $Pu\in\phi$, $P$ contracts a redex (with history) in $\phi'$. (Note
that this definition does not conflict with the definition of $\zcontr$ in
\Dr{D.levy.str.}.)
\ed


\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} 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_mv_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_mv_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.} -- a
contradiction.
\begin{diagram}[height=1.8em,width=1.8em]
{}    &\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





\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 (complete) family-reductions. Recall that a \emph{family-reduction} is
a multi-step reduction contracting, in each multi-step, all members of a
single family in parallel.



\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)$ Exactly as 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 affineness instead of \Lr{L.dif.re.sa.his.}.

$(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
[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 the assumption
(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$ -- 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 affine zig-zag
DFS ${\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{Characterizing L\'evy-equivalence via Zig-zag}
\label{S.leeq.zig.}




\bll{L.sta.eq.sa.fam.}
Let $P$ and $Q$ be standard co-initial finite reductions. Then $P\leeqv Q$
iff $FAM_z(P)=FAM_z(Q)$.

\bproof
\suf\ Immediate from \Lr{L.dec.fam.ex.}. \nec\ Suppose on the contrary that
$P\not\leeqv Q$, and say $P/Q\not=\emp$. Then $P$ contracts a redex $u$,
say $P=P'+u+P''$, such that $u/(Q/P')\not=\emp$. Let $v$ be a step in $Q$,
i.e., $Q=Q'+v+Q''$ (see the \delete{Figure~\ref{F.zig-fam.}} figure
for \Lr{L.dec.fam.ex.}). Then if $u'=u/(Q'/P')$ and $v'=v/(P'/Q')$, we have
$u'\not=v'$, thus $(P'\sqcup Q')u'\not=(P'\sqcup Q')v'$. Hence, by
\Lr{L.dif.re.sa.his.}, $Fam_z(P'u)=Fam_z((P'\sqcup
Q')u')\not=Fam_z((P'\sqcup Q')v')=Fam_z(Q'v)$, i.e., $FAM_z(P)\ni
Fam_z(u)\not\in FAM_z(Q)$ -- a contradiction.
\eproof
\el


\bll{L.sfa.is,fam.of.se.}
Let $P$ be a finite reduction in an ASDRS. Then $SFAM_z(P)=FAM_z(ST(P))$.

\bproof
Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\dored{P_{i+1}}t_n$, and let
$u_{i_1}, u_{i_2},\ldots, u_{i_k}$ be all $P$-needed steps in $P$
($i_1<i_2<\ldots$). Then, by \Dr{D.ess.rel.red.} and
\Lr{L.era.and.ess.im.ne.},
$ST(P):t_0=s_0\red{v_0}s_1\red{v_1}s_2\red{u_2}\ldots\red{v_k}s_{k+1}$,
where $u_{i_j}$ is the first $P'_j$-needed step in
$P'_j=P/(v_0+v_1+\ldots+v_{j-1})$, and $u_{i_j}$  is a residual of $v_j$
along $P'_j$. Thus $Fam_z(v_j)=Fam_z(u_{i_j})$. And since
$SFAM_z(P)=\{Fam_z(u_{i_j})\,\vert\,j=0,1,\ldots,k\}$ and
$FAM_z(ST(P))=\{Fam_z(v_j)\,\vert\,j=0,1,\ldots,k\}$, the lemma follows.
\begin{diagram}[height=1.8em,width=1.8em]
t_0=s_0    &\rOnto^{P_{i_j}}  & t_{i_j}   & \rTo^{u_{i_j}}& t_{i_j+1}  &
\rOnto^{P^*_{i_j+1}}   &  t_n   &   - &  \,\,\,\,\, P'_0=P \\
\dOnto    &               &\dOnto>{\emp} &\\
s_j    &\rOnto         & t_{i_j}   & \rTo^{u_{i_j}}& t_{i_j+1}  &
\rOnto^{P^*_{i_j+1}}   &    t_n   &   - & P'_j  \\
\dTo<{v_j} &            &\dTo>{u_{i_j}}   &       &   \dOnto>{\emp}  \\
s_{j+1}  &\rOnto        & t_{i_j}   & \rOnto^{\emp}& t_{i_j+1}  &
\rOnto^{P^*_{i_j+1}}    &   t_n   &   - & P'_{j+1}  \\
\end{diagram}
\delete{
\begin{diagram}[height=1.8em,width=1.8em]
t_0=s_0    &\rOnto^{P_{i_j}}  & t_{i_j}   & \rTo^{u_{i_j}}& t_{i_j+1}  &
\rOnto^{P^*_{i_j+1}}   &  P'_0=P \\
\dOnto    &               &\dOnto>{\emp} &\\
s_j    &\rOnto         & t_{i_j}   & \rTo^{u_{i_j}}& t_{i_j+1}  &
\rOnto^{P^*_{i_j+1}}   &  P'_j  \\
\dTo<{v_j} &            &\dTo>{u_{i_j}}   &       &   \dOnto>{\emp}  \\
s_{j+1}  &\rOnto        & t_{i_j}   & \rOnto^{\emp}& t_{i_j+1}  &
\rOnto^{P^*_{i_j+1}}    & P'_{j+1}  \\
\end{diagram}
}
\eproof
\el


\bpl{P.leqv.sam.se.es.fa.}
Let $P$ and $Q$ be co-initial finite reductions. Then $P\leeqv Q$ iff
$SFAM_z(P)=SFAM_z(Q)$.

\bproof
Indeed, $P\leeqv Q$ iff (since $P\leeqv ST(P)$ and $Q\leeqv ST(Q)$  by the
Standardization Theorem) $ST(P)\leeqv ST(Q)$ iff (by the Standardization
Theorem and \Lr{L.sta.eq.sa.fam.}) $FAM_z(ST(P))=FAM_z(ST(Q))$ iff (by
\Lr{L.sfa.is,fam.of.se.}) $SFAM_z(P)=SFAM_z(Q)$.
\eproof
\ep


\bll{L.subs.lles.}
Let $P$ and $Q$ be co-initial reductions, in an ASDRS, such that
$FAM_z(P)\ssq FAM_z(Q)$. Then $P\lleq Q$.

\bproof
We need to show that, for any redex $v$ contracted in $P$, say
$P=P'+v+P''$, $v/(Q/P')=\emp$. But since $Q$ contracts a zig-zag related
redex $Q'w$, we have by \Lr{L.dif.re.sa.his.} that $v/((Q'+w)/P')=\emp$,
implying $v/(Q/P')=\emp$.
\eproof
\el


\bpl{P.char.lles.}
Let $P,Q$ be finite co-initial reductions in an ASDRS. Then $P\lleq Q$ iff
$\exists Q': FAM_z(P)\ssq FAM_z(Q')$.

\bproof
\suf\ $P\lleq Q$ implies $Q\leeqv P+Q''$ for some $Q''$, hence $FAM_z(P)\ssq FAM_z(Q')$ for $Q'=P+Q''$.  \nec\ By \Lr{L.subs.lles.}.
\eproof
\ep

\section{An Application}
\label{S.app.}


We have shown that every affine stable DRS is in fact a DFS with the
zig-zag as the family relation. The latter, when it is a comma-DFS, i.e.,
its term set is the reduction graph of a single term,  can be interpreted
as a
conflict-free Prime Event Structure (PES) by considering families as events
and the contribution relation on families as the causal dependency
relation. (A conflict-free PES is simply an event set partially ordered by
a causal dependency relation, in which any element can dominate only a
finite number of others~\cite{[Win89]}.) Important examples of affine
stable DRSs are several forms of graph rewriting systems, and many authors
have studied the correspondence between graph rewriting systems and PESs
before~\cite{[KKSdV],[Sch],[CEL],[C.K.]}. Our translation is different, and
seems conceptually more clear as it is for Abstract Reduction Systems. It
is close in spirit to that in~\cite{[KKSdV]}, but the latter construction
uses syntax of orthogonal Term Graph Rewriting Systems heavily, and our
proofs are  different.


Moreover, we construct an affine DFS model, which is more powerful
and informative than the PES model as in the latter one can not speak of
equivalence of configurations corresponding to L\'evy-equivalent
reductions. Note that~\cite{[Sch],[CEL]} construct a PES model by
constructing a corresponding trace language first, and applying known
results relating Mazurkiewicz traces with Event Structures~\cite{[Bed]},
but this is only possible because the systems considered
in~\cite{[Sch],[CEL]} (graph grammars) are linear -- no duplication and no
erasure of redexes are possible. It is well known that PESs are inadequate
to give account to erasure of redexes, and a L\'evy-equivalence class of
reductions cannot be interpreted by a single configuration. This problem is
well discussed in~\cite{[Lan.th]}, Chapter~8.


To cope with that problem (caused by erasure), in~\cite{[dpes]} we extend
the conflict-free PES model with axiomatized \Le-equivalence relation in
two different but equivalent ways: One by directly constraining the class
of all equivalence relations on configurations, and another by axiomatizing
the \emph{inessentiality} or \emph{erasure} relation expressing redundancy
of an event for a configuration. The latter extends by further axioms an
incomplete axiomatization of the inessentiality relation in~\cite{[rndrs]}.
In the resulting extended models, Deterministic \emph{Permutation} and
\emph{Erasure} Event Structures, DPESs and DEESs, we can identify
configurations with different number of events but still representing the
same \pc\ class of reductions.  We show that \pc\ classes of configurations
in a DPES/DEES, appropriately ordered, are isomorphic to L\'evy's reduction
space of the corresponding ASDRSs, therefore the former give a \emph{fully
adequate} semantics to affine SDRSs. And the construction in this paper of
DFSs from affine SDRSs is one of the essential blocks in establishing the
above isomorphism. All known duplicating orthogonal systems can be
interpreted into affine SDRSs by considering (complete) family-reductions
only, which corresponds to their optimal graph implementation.



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


We have shown that every affine SDRS can be turned into an affine DFS by
taking the zig-zag as the family relation, and that the zig-zag is the only
family relation with the separability property -- no redex can create
simultaneously two different members of the same family. This results have
been used in constructing a fully adequate Event Structure style semantics
for ASDRSs, and thereby, for all orthogonal reduction systems. The latter
was our original motivation for construction of DFSs from ASDRSs, and it
was not immediate that this would require us to develop an extensive
optimality theory for ASDRSs.

>From the point of view of the optimality theory itself, our results are
more of methodological significance rather than of practical value.
However, we believe that suitable extensions of stable DRSs can be defined,
based on the residual relation alone, in which one can extended our results
to the general (duplicating) case, and our proofs can be used as a basis.
For example, the concept `$P$ is internal to an argument of a redex $u$ in
$t$', used in all syntactic extraction algorithms, can be replaced by the
concept `$P$ is internal to a set of redexes $V$ in $t$', where $P$ is
internal to $V$ iff it is external to the compliment of $V$. In the general
case, the [FFD] axiom of DFSs becomes a strong requirement, and extra
axioms will be necessary to ensure it. We expect that a modification of our
extraction algorithm will be applicable, but proofs will become more
complicated.


To conclude, let us mention that non-deterministic Residual Structures must
be considered as well. For example, semantics of non-orthogonal rewrite
systems is studied in Boudol~\cite{[Bou]}, and constructions of Event
Structures from non-orthogonal graph rewriting systems are studied, among
others, in~\cite{[CEL],[C.K.]}. Further, the theory of Standardization and
Discrete Normalization developed in~\cite{[dndrs]} for (semi-linear) stable
DRSs, which we used here, are equally applicable to the non-deterministic
case, as non-deterministic Residual Structures, when restricted to the
L\'evy-equivalence class of a reduction, become deterministic.


 \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 Teylor's Diagram package.

\delete{
\begin{akn}
We thank  bla for useful comments.
\end{akn}
}


\begin{thebibliography}{99}


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

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



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


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


\bibitem[{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.

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


\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[{ClKe95}]{[C.K.]}
Clark D., Kennaway R. Some properties of non-orthogonal term graph rewriting.
Electronic Notes in Theoretical Computer Science, vol.~2, A.~Corradini,
U.~Montanari,  eds. Elsevier, 1995, p.~141-150. To appear in MSCS.

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



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

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

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


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


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

\bibitem[{HoPl91}]{[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, PhD thesis, MIT, 1990.


\bibitem[{KeSl89}]{[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.



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


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



\bibitem[{KhGl96a}]{[dpes]}
Khasidashvili Z., Glauert J. R. W.  Relating conflict-free transition and
event models. draft.


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


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

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

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


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


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

\bibitem[{LaMo92}]{[L.M.]}
Laneve C., Montanari U. Axiomatizing permutation equivalence in the \lc. In
proc. of the $3^{rd}$ International Conference on Algebraic and Logic
Programming, ALP'92, Springer LNCS, vol.~632, 1996, p.350-363.
}

\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. In: Proc. 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.

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

\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. In proc. of
RTA'96, Springer LNCS, vol.~1103, Ganzinger, H., ed., 1996, p.~392--407.


\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~\cite{[S.E.]}, p.~326-340.


\bibitem[{ScEh94}]{[S.E.]}
Schneider H.-J. Ehrig H., editors. Proceedings of the Dagstuhl Seminar 9301
on Graph Transformations in Computer Science, Springer LNCS, vol.~776,
1994.


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


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

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

\end{thebibliography}



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


We use the following two lemmas 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

\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.8em,width=1.8em]
{}         &\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.8em,width=1.8em]
{}       &\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 [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.no.le.eqv.}, $(P+u)/Q$ contracts a residual of $v$. We show that
$P/Q\not=\emp$.

\begin{diagram}[height=1.8em,width=1.8em]
{}          &\rOnto^{P}     & {}           &\rTo^{u}     & {}         \\
\dOnto<Q    &             &\dOnto<{Q/P}>u  &             & \dOnto_\emp  \\
{}          &\rOnto^{P/Q}_v & {}           &\rOnto       & {}         \\
\dTo<v      &               &\dOnto     &             &  \dOnto_\emp \\
{}          &\rOnto_\emp    &  {}          & \rOnto_\emp & {}         \\
\end{diagram}
Suppose on the contrary that $P/Q=\emp$. Then, by [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 [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.8em,width=1.8em]
{}       &\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.8em,width=1.8em]
{}       &\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.8em,width=1.8em]
{}     &\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.no.le.eqv.} 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}
%% End LaTeX Document



