%% 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, UEA \\
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 at 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 understand what properties a sharing concept must
possess in order 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}. 
\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 reflexive and transitive closure of the residual 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 reflexive 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, which also shows that zig-zag does not coincide with the labelling and their (i.e., with the \emph{shift} operation) extraction families, is a non-duplicating SDRS! This is 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 discussion in 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, and 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.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],[Oos.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 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'_1} &         \\
\bullet & \rTo^u &\bullet &             &    &               &\bullet \\    
       &        &       & \rdTo^{v_2} &    & \ldTo^{v'_2}  &         \\
       &        &       &             &\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}$).
 


\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 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 may duplicate or erase arguments, 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 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, 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.



For any $P:t_0\red{u_0}t_1\red{u_1}\ldots \ar t_n$ in an ASDRS, $P$-(un)neededness of any redex in a term $t_i$ can be establish 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 efficiently standardize $P_1$, or construct any 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.  



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


\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.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.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.sta.eq.sa.fam.} 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.sta.eq.sa.fam.} 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 affinness 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).


\delete{
\nec\ Let $\cal F$ not be separable. By definition of separability, there are $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 [acyclicity], at least one of the redexes $w'/w''$, $w''/w'$ is non-empty, implying that at least one of the reductions $P+v+w'+w''/w'$, $P+v+w''+w'/w''$ contracts the family $Fam(w')$ twice.
}
\eproof
\el

\delete{
\bll{L.sam.his.red.}
In an affine SDRS, $Pv\fami Pv'\imply v=v'$.

\bproof
\zurab{bla.}
\eproof
\el 


As a corollary, from the general Unique Families Lemma~\cite{[rndrs]} we have the following lemma.


\begin{lem}\em
\label{L.fam.compl.}
{\bf (Unique Families)}
In an affine separable DFS, any family is contracted at most once in a reduction.
\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.

\delete{
\suf\ Let ${\cal F}=({\cal R}, \sfami,\scontr)$ be separable. By \Tr{P.on.ca.for.}, \Lr{L.contr.fam.} and \Pr{P.leqv.sam.se.es.fa.}, $Pv$ and $Qw$ have canonical forms $P'v'$ and $Q'w'$ such that $FAM_z(P')=FAM_z(Q')$ and $P'\staeq Q'$. Thus we can assume that $P'=Q'$, and its last step creates both $v'$ and $w'$ by \Dr{D.can.re.his.}, implying by separability that $v'=w'$. Hence $Pv\zfami Qw$ by \Tr{T.un.ex.nor.f.}.


\nec\ Suppose on the contrary that $\cal F$ is a zig-zag DFS ${\cal F}=({\cal R}, \sfami,\scontr)$, but it is not separable, i.e., there are $Pv$, $w'$ and $w''$ such that $v$ creates $w',w''$, $w'\not= w''$, and $Fam_z((P+v)w')= Fam_z((P+v)w'')$. By \Tr{T.un.ex.nor.f.}, $(P+v)w'$ and $(P+v)w''$ have the same canonical form $P'w$, and by the extraction algorithm, $\exists P'': P'+P''\leeqv P+v$, $w'=w/P''$ and $w''-w/P''$, implying $w'=w''$ by the affinness -- contradiction.
}
\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




 

\delete{ 


Note that ${\cal F}_t=(R_t,\fami,\contr)$ holds much more information than  ${\cal E}^{\contre}_{{\cal F}_t}=(FAM_z(t),\contre)$, as in ${\cal E}^{\contre}_{{\cal F}_t}$ one can no longer speak of \emph{inessentiality} of an event for a configuration of events, or speak of \emph{equivalence} of configurations $FAM_z(P)$ and $FAM_z(Q)$ for permutation-equivalent reductions $P$ and $Q$. For example, consider the DPES ${\cal E}^{\contre}_{{\cal F}_t}$ corresponding to the rewrite system $R_t$ with rules $\{I(x)\ar c,\, a\ar b\}$ and with the reduction graph of $t=I(a)$ as the set of terms. Its events are $I(a)\red{a}I(b)$ and $I(a)\red{I(a)} c$ (the steps $I(b)\red{I(b)}c$ and $I(a)\red{I(a)} c$ represent the same event); and its configurations are $\alpha=\{I(a)\}$, $\beta=\{a\}$, and $\gamma=\{a, I(a)\}$. Then $\alpha$, $\beta$ and $\gamma$ are different configurations, while it is natural to identify $\alpha$ with $\gamma$, since the corresponding reductions are \Le-equivalent. This problem is well known, and a good discussion can be found e.g., in~\cite{}. 

To cope with that problem, 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 non-duplicating SDRSs. All known duplicating orthogonal systems can be interpreted into non-duplicating SDRSs by considering (complete) family-reductions only, which corresponds to their optimal graph implementation.
}


\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 at all 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 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 use 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 complete development $N$ of $F\subts t$, in a
DRS, and let $Q:t\doar o$, then $P/Q$ is external to $N/Q$.  
\el

\bll{L.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
