%% Start LaTeX Document
\documentstyle{llncs}
%\documentstyle[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
\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}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
%%%%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\newcommand{\notation}{{\bf Notation }}
%\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand{\inputpic}[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\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{\contre}{\underline{\hookrightarrow}}
\newcommand{\zcontre}{\underline{\hookrightarrow}_z}
\newcommand{\fin}{\in}
%\newcommand{\lleq}{\triangleleft}
%\newcommand{\lles}{\triangleleft}
\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{\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{$SE_{{#1}}({#2})$}}
\newcommand{\zcontr}{\hookrightarrow_z}
\newcommand{\Le}{L\'evy}

 
\title{Zig-zag and Extraction Families \\  
in Non-duplicating Stable Deterministic Residual Structures}
\author{Zurab Khasidashvili and John Glauert}
\institute{School of Information Systems, UEA \\
Norwich NR4 7TJ England \\
zurab@sys.uea.ac.uk, jrwg@sys.uea.ac.uk
\thanks{This work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300}\\
Tel: +44 1603 592671,  Fax: +44 1603 593344
}

 
\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: (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 (2)
to give an \emph{Event Structure} style semantics to conflict-free rewrite
and transition systems with \emph{erasure}. As a first step, which is
already quite complicated, 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.) 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 SDRSs.


\delete{
We consider \emph{non-duplicating Deterministic Residual Structures} (DRSs) which are abstract reduction systems with an axiomatized residual relation, and model orthogonal term and graph rewriting systems with non-duplicating residual relation.  We study \emph{sharing} concepts in DRSs, formalized by the notion of \emph{redex-family}. We introduce an abstract \emph{extraction} procedure and show that the family relation defined via extraction coincides with the zig-zag relation (the latter is the reflexive and transitive closure of the residual relation on redexes with \emph{histories}), and show that they form a family relation as formalized in  As a consequence, we obtain a precise translation between important operational (Concurrent Transition Systems) and set theoretic (Prime Event Structures) models of computation.

we show that in any non-duplicating stable Deterministic Residual Structure (DRS), the zig-zag relation on redexes with histories forms a family relation. Thus, every non-duplicating DRS is a Deterministic Family Structure, and therefore can also be interpreted as a Deterministic Prime Event Structure, there events are redex-families and the contribution relation on families is a partial order on events. An importance of this result is that it gives a sound notion of family for a large class of rewrite systems, all non-duplicating orthogonal ones in particular. A technical novelty is that we give an abstract definition of \emph{extraction} process (which was claimed to need syntactic structure of terms), and show that redexes with histories are zig-zag related if and only if they have the same canonical form w.r.t. extraction, modulo an equivalence relation on histories. 
} 
\end{abstract}

 

\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, the optimality theory has been generalized 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]}. 


\delete{
In their attempt to generalize the three family concepts to Interaction Systems, Asperti and Laneve encountered a problem -- while their generalization of labelling and extraction family concepts were still equivalent, the two were not equivalent to the zig-zag family concept. However, as explained by van Oostrom~\cite{[Oos]}, the reason of this mismatch was that labelling and extraction families were in fact defined in a refined version of the original system, in which one original step is decomposed as one rewrite step and a number of substitution step, while in the definition of zig-zag no refinement of the original steps were taken into account. Oostrom proved that the free notions of family are equivalent for all orthogonal HORSs if they all are defined in the refined version of the original HRS. Besides, independently and much earlier, Kennaway and Sleep~\cite{[K.S.]} defined their concept of labelling for orthogonal Combinatory Reduction Systems (CRSs), which cover Interaction Systems, and their labelling seems to yield the same labeling family as zig-zag. The latter labelling improved on Klop's original labelling for orthogonal CRSs, the first generalization of \Le's labelling to Higher-order rewriting systems, which suffered slight drawbacks. An early labelling concept for orthogonal TRSs, which was used in defining labelling for Interaction Systems, was introduced by Maranget~\cite{[Mar91]}, and has been used for optimal implementation of orthogonal TRSs. 
}

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 deep enough to enable proof of normalization and optimality results. 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]}. 
\delete{
Oostrom defined similar abstract rewrite systems which axiomatize some aspects of the \emph{descendent} relation on subterms in Higher-order Rewriting Systems (HORSs); the descendent relation is much more refined and powerful than that of residual. Several refined concepts of abstract rewriting are studied in~\cite{[Mel],[Raa.th]}.
}

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 one 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 (DPESs)~\cite{[NPW],[Win]}.


In this paper, we study the possibility of defining  a family relation in stable DRSs.  We will only consider non-duplicating DRSs, because of its particularly important semantic applications, and 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. This is achieved by defining an abstract extraction procedure and showing that zig-zag coincides with the extraction-family relation. For the extraction-family concept, checking the DFS family axioms are easy. Since families in DFSs, ordered by the contribution relation, form DPESs, our construction yields a translation of stable determinate CTSs into deterministic stable Event structures, linking two widely accepted (operational and set-theoretic) models of computation. 
\delete{Further, we extend this translation to translation of stable DCTSs to Deterministic Computation Structures (DCSs)~\cite{[rndrs]}, which are DPESs with an axiomatized \emph{inessentiality} or \emph{redundancy} 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. Actually, the extraction process was claimed to be syntactic in~\cite{[le80]} and \cite{[AL]}. \footnote{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'.} 

 

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. This is the main result of this paper, and it is applied in Section~\ref{S.app.} to define a translation of stable DCTSs into DPES. 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.
The 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$, 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{}.
}

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) is a pair $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 $R$ \emph{non-duplicating} or \emph{affine}, ADRS, if the residual relation in $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 $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 $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).


\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$. We call $P$ {\em external\/}
to $U$ (resp. $u$) if $P$ does not contract residuals of redexes in $U$
(resp. residuals of $u$).

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

\begin{diagram}[height=1.8em,width=1.8em]
t_0          &\rOnto^{P_i}& & t_i       &\rTo^{u_i}   & t_{i+1} {}\\
\dOnto<{Q'_j}&            & &\dTo<{Q_j/P_i}&         & \dOnto     \\
{}       &\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) ${\cal F}$ is a
triple ${\cal F} =(R,\fami,\contr)$, where $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 $R$.
Then $Fam(\emptyset_t u) \not=Fam(\emptyset_t v)$.

$\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$ [termination] Any reduction that contracts redexes of a finite
number of families is terminating.

\suppress{\noindent (One might prefer to consider [contribution] as the
definition of
$\contr$ rather than as axiom.)}
\ed


 
 

\section{Standardization}

In this section, we recall some definitions and results from~\cite{[dndrs]} concerning standardization of reductions in non-duplicating (i.e., affine) stable DRSs, ASDRSs. We define {\em $P$-needed}, {\em $P$-essential}, and {\em $P$-erased\/} redexes, for any reduction $P$, and list their (relative) properties used in this paper.


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

$\bullet$ We call $u$ {\em $P$-needed\/}, written $NE_P(u,t)$, if there is no
$Q\leeqv P$ that is external to $u$, and call it {\em $P$-unneeded\/},
$UN_P(u,t)$, otherwise. We call $u$ {\em $P$-essential\/}, $ES_P(u,t)$, 
if there
is no $Q\leeqv P$ that discards $u$, and call it {\em $P$-inessential\/},
$IE_P(u,t)$, otherwise. 
 
We extend these concepts to reductions co-initial with those containing
$u$ as a redex of one of its terms.

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


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$ if $P\leeqv Q$.


\bll{L.era.and.ess.im.ne.}
Let $u\subt t\dored{P}$, in a DRS. 

(1) If $u$ is $P$-erased and $P$-essential, then it is $P$-needed. 

(2) If $u$ is $P$-needed, then it is $P$-essential.

(3) If $P$ contracts a redex $v$, then $v$ is $P$-needed iff it is 
$P$-essential.

(4) If $P:t\doar s\red{v}o$, then $v$ is $P$-needed.
\el

 
 

\bpl{P.prop.nee.cre.res.}
Let $P:s\doar t\red{u}e\dored{P^*}$, in a stable DRS.

(1) Let $u$ create $v\subt e$, and let $u$ be $P$-unneeded (resp. $P$-inessential). Then so is $v$.

(2) Let $v\subt e$ be a $u$-residual of $w\subt t$, and let $w$ be 
$P$-unneeded (resp. $P$-inessential). Then so is $v$.

(3) Let $v\subt t$ be $P$-needed (resp. $P$-essential), and let $v\not= u$. 
Then $v$ has at least one $u$-residual $v'$, and it is the only
$u$-residual of $v$, then $v'$ is $P$-needed (resp. $P$-essential).
\ep


\delete{
% Lemma 3.10.
\bll{L.las.st.sel.nee.}
Let $P:t\doar s\red{u}o$, in a DRS. Then $u$ is $P$-needed.
\el
}


\bdl{D.ess.rel.red.}
Let $P:t\doar $ and $Q\lleq P$. The {\em $P$-needed variant of $Q$},
written $\err{P}{Q}$, is defined as follows: let $v\subt t$ be such that it
is $P$-needed and its residual is contracted in $Q$ first among $P$-needed
residuals of $P$-needed redexes in $t$. Then $\err{P}{Q}=v+\err{P/v}{Q/v}$.
If there is no such a redex in $t$, then $\err{P}{Q}=\emp$. We call 
$\err{P}{P}$ the {\em self-needed variant of $P$\/} and denote
it by $SE(P)$.
\ed

 
Obviously, a reduction $P$ is self-needed iff $SE(P)=P$.
The notion of self-essential reduction is the
best approximation to the outside-in left-to-right notion of 
standard reduction~\cite{[Bar],[H.L.],[Kl.CRS]} for DRSs, 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-essential reductions 
play the same role as outside-in left-to-right standard reductions in the
extraction processes of~\cite{[le80],[AL],[Oos]}.
 

\bdl{D.stanndrs.}
We call a reduction in a DRS {\em standard\/} if it is self-essential. 
We write $P\staeq Q$ if $P\leeqv Q$ and both $P$ and $Q$ are standard. 
For any standard $P$, we define $\sclas{P}=\{Q\,\vert\,Q\staeq P\}$.
\ed


We will use the following Standardization Theorem from~\cite{[dndrs]}.

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


\delete{
\btl{T.can.self-need.var.}
(\cite{[dndrs]} {\bf (Standardization)}
For any reduction $P:t\doar$, finite or infinite, in a non-duplicating stable DRS, $t$ has a $P$-needed (hence $P$-essential) redex. Moreover, $P$ has a self-needed variant $SE(P)$, which is standard, and if $P$ is finite, then $P\leeqv SE(P)$; if $P$ is infinite, then $SE(P)\lleq P$, but $P\leeqv SE(P)$ need not hold.
\et
}


\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, up to an equivalence on histories. These canonical representatives are obtained using our extraction algorithm, which leaves out 
all steps of histories that do not `contribute' to the family. 

 
\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 there is no $Q\leeqv P$ such that the last step in $Q$ does not create $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$.



\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 $SE(Q)$ can be taken for $Q'$. By \Dr{D.ess.rel.red.}, $SE(Q)$ is obtained from $Q$ by a sequence of transformations $Q=Q_1,Q_2,\ldots, Q_n=SE(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.}.(4), 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 \Pr{P.prop.nee.cre.res.}.(1), $P''$ cannot create $u$, i.e., there is $u'\subt o$ such that $u'/P''=u$, and $u'$ is $Q$-needed by \Pr{P.prop.nee.cre.res.}.(2). Since $P''/u'$ is $Q$-unneeded by \Pr{P.prop.nee.cre.res.}.(2), and since the last step of $P'+u'+P''/u'$ is $Q$-needed by \Lr{L.era.and.ess.im.ne.}.(4), $P''/u'=\emp$. Since $u'$ is $Q$-needed and $P''$ is $Q$-unneeded, $P''$ is external to $u'$ by \Pr{P.prop.nee.cre.res.}.(3). Hence, by the Stability Lemma, $u'$ does not create $v$, and the lemma follows since $SE(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) family 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'$; $\doextr$ is the transitive and reflexive closure of $\extr$.
The formal definition is as follows:


\bdl{D.ext.}
Let $Q:t\dored{P'}e\red{u}s$ be a \emph{standard variant} of $P$, i.e., a standard reduction permutation-equivalent to $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.}.)
\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: $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

 
 


\bpl{P.on.ca.for.}
Every redex $Pv$ in an ASDRS has exactly one canonical form $\sclas{Q'}v'$.

\bproof
It is enough to show that the extraction relation $\extr$ is weakly confluent. So let $Qw''\lextrr{v}Nw\extrr{u}Pw'$ with $u\not= v$ (since if $u=v$ then there is nothing to prove).  We will show that $Qw''\extrr{u'}N^*w^*\lextrr{v'}Pw'$ for some $N^*w^*$, $u'$, and $v'$ such that $u=u'/v'$ and $v=v'/u'$. By \Dr{D.ext.}, we have from $Qw''\lextrr{v}Nw\extrr{u}Pw'$ that $Q+v\staeq N'\staeq P+u$, where $N'$ is a standard variant of $N$, and $w''/v=w'/u=w$. By \Lr{L.mov.red.cre.}, we have the following situation, where $P'+v'\staeq P$, $Q'+u'\staeq Q$, $P'\staeq Q'$, $u=u'/v'$, and $v=v'/u'$ (hence $P'v'\zfami Qv$, $Q'u'\zfami Pu$).
\begin{diagram}[height=1.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
\ep

   

\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 \Pr{P.prop.nee.cre.res.}.(1), $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 \Pr{P.prop.nee.cre.res.}.(2), 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.}.(3). Hence $w$ does not create $u'_1$ by \Pr{P.prop.nee.cre.res.}.(1). 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 \Pr{P.on.ca.for.}.
\eproof
\et




\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 characterization of \Le-equivalence via self-needed families.


Below, $FAM(P)$ (resp. $SFAM(P)$) denotes the set of zig-zag classes whose 
member (resp. $P$-needed, or equivalently, $P$-essential) redexes are 
contracted in $P$, in an ASDRS; and $Fam(Qu)$ denotes the zig-zag class 
of $Qu$. This is not in conflict with the notation in \Dr{D.DRS.}, since 
we will show that zig-zag is a family relation. 



\bll{L.dec.fam.ex.}
Let $P$ be a standard variant of $Q$. Then $FAM(P)\ssq FAM(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(Pu)\not=Fam(Pv)$.

\bproof
Suppose on the contrary that $Fam(Pu)=Fam(Pv)$. Then they have the same canonical form by \Tr{T.un.ex.nor.f.}, say $Qw$, and we have from the extraction procedure 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(P)=FAM(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(P'u)=Fam((P'\sqcup Q')u')\not=Fam((P'\sqcup Q')v')=Fam(Q'v)$, i.e., $FAM(P)\ni Fam(u)\not\in FAM(Q)$ -- a contradiction.
\eproof
\el
 

\bll{L.sfa.is,fam.of.se.}
Let $P:t_0\doar$. Then $SFAM(P)=FAM(SE(P))$.

\bproof
Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\dored{P_{i+1}}$, and let $u_{i_1}, u_{i_2},\ldots$ be all $P$-needed steps in $P$ ($i_1<i_2<\ldots$). Then, by \Dr{D.ess.rel.red.}, $SE(P):t_0=s_0\red{v_0}s_1\red{v_1}s_2\doar$, where $u_{i_j}$ is the first $P'_j$-needed step in $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(v_j)=Fam(u_{i_j})$. And since $SFAM(P)=\{Fam(u_{i_j})\,\vert\,j=0,1,\ldots\}$ and $FAM(SE(P))=\{Fam(v_j)\,\vert\,j=0,1,\ldots\}$, 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}}   &  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(P)=SFAM(Q)$.

\bproof
$P\leeqv Q$ iff (since $P\leeqv SE(P)$ and $Q\leeqv SE(Q)$  by the Standardization Theorem) $SE(P)\leeqv SE(Q)$ iff (by the Standardization 
Theorem and \Lr{L.sta.eq.sa.fam.}) $FAM(SE(P))=FAM(SE(Q))$ iff (by \Lr{L.sfa.is,fam.of.se.}) $SFAM(P)=SFAM(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=SE(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 \Pr{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(P')\ssq FAM(P)$.

\bproof
$Pv\extrr{w}P'v'$ implies that $P\leeqv P'+w$, and by \Lr{L.dec.fam.ex.}, $FAM(P')\ssq FAM(P'+w)\ssq FAM(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'$.   
\delete{
$Cone(\phi)=\cap_{Pu\in\phi}(FAM(P))$, the set of zig-zag classes whose members are contracted in the history of any member of the zig-zag class $\phi$. Then we define $\phi'\zcontr\phi$ iff  $\phi\in Cone(\phi)$.
}
\ed 


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

\bproof
By \Lr{L.cre.con.}, if $Q'v'$ is a canonical form of $Qv$, then $Fam(Pu)\in FAM(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(Pu)\in FAM(Q^*)$, i.e.,  $Fam(Pu)\zcontr Fam(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(P_ku_k)\not=Fam(P_mv_m)$. 

\bproof 
By induction on the number of zig-zag classes $\zcontr$-contributing to $Fam(P_ku_k)$. Suppose on the contrary that $Fam(P_ku_k)=Fam(P_mv_m)$. Let $P'_ku'_k$ be a canonical form of $P_ku_k$, i.e., 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(P'_ku'_k)=Fam(P_ku_k)=Fam(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(P'_ku'_k)=Fam(P_mu_m)=Fam(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 $R$ be a non-duplicating stable DRS. Then ${\cal F_R}=(R,\zfami,\zcontr)$ is a 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
[termination] from ~\Lr{L.ne.rep.fam.zi.}.
\eproof
\et




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

Recall that a \emph{Prime} Event Structure (PES)~\cite{[Win]} is a triple 
${\cal E}^{\leq}=(E, Con, \leq)$, where $E$ is a set of 
\emph{events}, ranged over by
$e, e_1,\ldots$; the \emph{consistency predicate} $Con$ is a non-empty set
of subsets of $E$, denoted by $X, Y, \ldots$; and the \emph{causal 
dependency relation} $\leq$ is a partial order on $E$, such that 
$\{e\}\in Con$, $Y\ssq X\in Con \Rightarrow Y\in Con$, 
$X\in Con\wedge\exists e'\in X.e\leq e'\,\Rightarrow X\cup \{e\} \in Con$, 
 and  $\{e'\,\vert\, e'\leq e\}$ is finite for any $e\in E$.


We are only interested in \emph{deterministic} structures, DPESs,
where no event can
prevent others from occurring, and therefore the consistency predicate is the
powerset of $E$, and will be omitted.\footnote{Determinism in ESs is defined differently in~\cite{[Ren]}.}
\emph{Configurations} (or \emph{states}) of ${\cal E}^{\leq}$ are 
\emph{left-closed subsets}
$\alpha,\beta,\ldots$ of $E$, i.e., subsets $\{\alpha\ssq E\,\vert\, e\in E
\,\wedge\, e'< e\Rightarrow e'\in\alpha\}$. It is immediate from the definition of $\contr$ that:   

 
\bt
(\cite{[rndrs]})
For any DFS ${\cal F}_t=(R_t,\fami,\contr)$, where $R_t$ is a (sub)DRS whose
term domain is the graph of a term $t$ (i.e., the set of terms to which $t$
is reducible), ${\cal E}^{\contre}_{{\cal F}_t}=(FAM(t),\contre)$
is a DPES,
where $\phi \contre \psi$ means that $\phi \contr \psi$ or $\phi = \psi$, and
$FAM(t)$ is the set of families relative to~$t$.
\et


Note that ${\cal F}_t=(R_t,\fami,\contr)$ holds much more information than  ${\cal E}^{\contre}_{{\cal F}_t}=(FAM(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(P)$ and $FAM(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 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. Thus affine DFSs provide more faithful models for orthogonal rewrite systems than DPESs, and at the same time can easily be interpreted as DPESs.


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


We have shown that every non-duplicating 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 graph of a single term,  can be interpreted as a 
Deterministic Prime Event Structure (DPES)
by considering families as events and the contribution
relation on families as the causal dependency relation. Important examples of non-duplicating stable DRSs are several forms of graph rewriting systems, and many authors have studied the correspondence between graph rewriting systems and Prime Event Structures before~\cite{[KKSdV],[Sch],[CEL],[C.K.]}. 
Our translation is different, and
seems conceptually more clear as it is for Abstract Rewrite Systems.
And we construct an affine DFS model (which is more powerful
and informative than the DPES model) \emph{directly}, unlike the above
approaches~\cite{[Sch],[CEL]} which construct a DPES model by constructing a corresponding trace language first, and applying known results relating Mazurkiewicz traces with Event Structures~\cite{[Bed]}. Our translation 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 completely different.  

 
There are three immediate directions to continue this work. First, the
possibility of constructing DFSs from duplicating stable DRSs must be 
investigated. In the general case, the [termination] axiom of DFSs
becomes a strong requirement, and extra axioms on stable DRSs 
may be needed to ensure it. We expect that a similar extraction algorithm
will be applicable, but proofs will become more complicated. Event Structure semantics for orthogonal rewrite systems with duplicating residual relation are studied, among others, in~\cite{[L.M.],[Lan.th]}, but the results there are limited because of the problems with erasure illustrated by the example in Section~\ref{S.app.}.


Second, it is natural to extend DPESs with an axiomatized \emph{erasure}
relation or an axiomatized \emph{permutation-equivalence} relation to enable DPESs to give an adequate semantics to orthogonal rewrite systems, and to cope with the example in the previous section. This is indeed possible, and in an forthcoming paper we show that such refined event models are isomorphic to affine DFSs, therefore can serve as faithful event models for orthogonal rewrite systems. (This approach, in particular, solves the problems with erasure discussed in~\cite{[Lan.th]}, Chapter~8, and in~\cite{[KKSdV]}).


 Finally, we mention that non-deterministic Residual Structures must be considered as well. For example, normalization by neededness theory for non-orthogonal systems is studied in Boudol~\cite{[Bou],[Mel]}, and constructions of Event Structures from non-orthogonal graph rewriting systems are studied, among others, in ~\cite{[CEL],[C.K.]}.
 

\delete{
\vspace{0.20cm}

%\section*{Acknowledgements}

\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[{CK95}]{[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[{HP91}]{[H.P.]}
Hoffmann B., Plump D. Implementing term rewriting by Jungle evaluation. 
Theoretical Informatics and Applications 25:445-472, 1991.


\bibitem[{Kat90}]{[Kath]}
Kathail V. Optimal Interpreters for Lambda-calculus based functional 
languages, 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[{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 $17^{th}$ POPL, 1990,~p.16-30.


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


\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, Bazem 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 of 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, CWI Amsterdam,~1996.

\bibitem[{Ren96}]{[Ren]}
Rensink A. Denotational, Causal, and Operational Determinism in Event 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.~272-286.

\bibitem[{Sch94}]{[Sch]}
Schied G. On relating rewrite systems and graph grammars to event structures. In~\cite{[S.E.]}, p.~326-340.


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

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

\bibitem[{Win88}]{[Win]}
Winskel G. Event Structures. Univ. of Cambridge, Computer Laboratory,
Report no. $95$, 1988.

\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.stanndrs.} and \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 \Pr{P.prop.nee.cre.res.}.(3). 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 \Pr{P.prop.nee.cre.res.}.(3).
\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
