\documentstyle{elsart}



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

\begin{document}


\begin{frontmatter}

\title{Relating Conflict-free Stable\\ Transition and Event Models\thanksref{EPCRC}}
\thanks[EPCRC]{Part of this work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300.} 

\author{Zurab Khasidashvili}
\address{Department of Mathematics and Computer Science \\
Bar-Ilan University, Ramat-Gan 52900, Israel \\
\emph{khasidz@cs.biu.ac.il}}
\author{John Glauert}
\address{School of Information Systems, UEA \\
Norwich NR4 7TJ, UK\\
\emph{jrwg@sys.uea.ac.uk}}



\begin{abstract}
We describe an event-style (or poset) semantics for conflict-free rewrite
systems, including term and graph rewriting (possibly with bound
variables), the $\lambda$-calculus, and other stable transition systems 
with a residual relation. Our interpretation is based on considering 
redex-families as
events. It treats permutation-equivalent reductions as representing the
same concurrent computation. Due to erasure of redexes, Event Structures
are inadequate for such an interpretation. We therefore extend the Prime
Event Structure model in two different but equivalent ways: by axiomatizing 
permutation-equivalence on finite configurations, and by axiomatizing the 
erasure of events, for the conflict-free case, and show that these extended 
models are equivalent to stable transition models with axiomatized residual 
and family relations. We then construct finitary prime algebraic domains 
from the set of configurations in these extended models by defining 
orderings relative to stable sets of `results'. All useful sets of results 
for which the normalization (by neededness) theorem can be proved are stable.
\end{abstract}
\end{frontmatter}




\maketitle
 


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

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

\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{pruuf}{\noindent{\bf 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}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand{\inputpic}[1] {\begin{center} \input{#1} \end{center}}

\newcommand{\con}[1]{\mbox{$\lceil{#1}\rceil^{\leq}$}}
\newcommand{\coni}[1]{\mbox{$\lceil{#1}\rceil^{\geq}$}}
\newcommand{\ocon}[1]{\mbox{$\lceil{#1}\rceil^{<}$}}
\newcommand{\oconi}[1]{\mbox{$\lceil{#1}\rceil^{>}$}}


\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{\zcontr}{\hookrightarrow_z}
\newcommand{\ccontr}{\hookrightarrow_{\cal C}}

\newcommand{\emb}{\preceq}
\newcommand{\stemb}{\prec}

\newcommand{\fcE}{{\cal L}_{fin}(E)}
\newcommand{\fcC}{{\cal L}_{fin}({\cal C})}
\newcommand{\fcP}{{\cal L}_{fin}({\cal P})}
\newcommand{\fcR}{{\cal L}_{fin}({\cal R})}
\newcommand{\cC}{{\cal L}({\cal C})}
\newcommand{\cP}{{\cal L}({\cal P})}
\newcommand{\cE}{{\cal L}({\cal E})}
\newcommand{\cR}{{\cal L}({\cal R})}



\newcommand{\pfcP}{{\cal L}_{fin}^{\leeqv}({\cal P})}
\newcommand{\efcP}{{\cal L}_{fin}^{\lleq}({\cal P})}
\newcommand{\pfcR}{{\cal L}_{fin}^{\leeqv}({\cal R})}
\newcommand{\efcR}{{\cal L}_{fin}^{\lleq}({\cal R})}
\newcommand{\pfcC}{{\cal L}_{fin}^{\leeqv}({\cal C})}
\newcommand{\efcC}{{\cal L}_{fin}^{\lleq}({\cal C})}



\newcommand{\snp}[1]{\mbox{$[{#1}]_{\stab}$}}
\newcommand{\sunp}[1]{\mbox{$[{#1}]_{\stab}^-$}}

\newcommand{\snf}[1]{FAM_{\stab}(#1)}
\newcommand{\spne}[1]{[#1]_{\stab'}}

\newcommand{\ssqcup}{\sqcup_{\stab}}
\newcommand{\ssqcap}{\sqcap_{\stab}}
\newcommand{\spsqcup}{\sqcup_{\stab'}}
\newcommand{\spsqcap}{\sqcap_{\stab'}}


\newcommand{\era}{\rhd}
\newcommand{\sea}{ST(\alpha)}
\newcommand{\seb}{ST(\beta)}
\newcommand{\seg}{ST(\gamma)}
\newcommand{\lsea}{ST_{\lera}(\alpha)}
\newcommand{\lseb}{ST_{\lera}(\beta)}
\newcommand{\lseg}{ST_{\lera}(\gamma)}
\newcommand{\lclasa}{\lclas{\alpha}}
\newcommand{\lclasb}{\lclas{\beta}}
\newcommand{\lclasg}{\lclas{\gamma}}

\newcommand{\spfcP}{{\cal L}^{\speqv}({\cal P})}
\newcommand{\sefcP}{{\cal L}^{\spleq}({\cal P})}
\newcommand{\spfcR}{{\cal L}^{\seqv}({\cal R})}
\newcommand{\sefcR}{{\cal L}^{\sleq}({\cal R})}

\newcommand{\spfcC}{{\cal L}^{\speqv}({\cal C})}
\newcommand{\sefcC}{{\cal L}^{\spleq}({\cal C})}
\newcommand{\spfcF}{{\cal L}^{\seqv}({\cal F})}
\newcommand{\sefcF}{{\cal L}^{\sleq}({\cal F})}

\newcommand{\spclas}[1]{\mbox{$\langle{#1}\rangle_{\stab'}$}}
\newcommand{\spclasa}{\spclas{\alpha}}
\newcommand{\spclasb}{\spclas{\beta}}
\newcommand{\spclasg}{\spclas{\gamma}}


\newcommand{\isom}{\rightleftharpoons}


\newcommand{\lce}[1]{\mbox{$\overline{{#1}} $}}
\newcommand{\rs}[1]{\mbox{$[{#1}] $}}
\newcommand{\stan}{STA}
\newcommand{\stav}[1]{STV(#1)}
\newcommand{\lin}[1]{\mbox{${#1}_I $}}

\newcommand{\fin}{\in}
%\newcommand{\lleq}{\triangleleft}
%\newcommand{\lles}{\triangleleft}
\newcommand{\lleq}{\unlhd}
\newcommand{\lles}{\lhd}
\newcommand{\lgeq}{\unrhd}

\newcommand{\leeqv}{\approx}
\newcommand{\eleeqv}{\approx_\rhd}

\newcommand{\sleq}{\unlhd_{\stab}}
\newcommand{\sles}{\lhd_{\stab}}
\newcommand{\spleq}{\unlhd_{\stab'}}
\newcommand{\sples}{\lhd_{\stab'}}
\newcommand{\sqleq}{\sqsubseteq}
\newcommand{\sqles}{\sqsubset}
\newcommand{\seqv}{\approx_{\stab}}
\newcommand{\speqv}{\approx_{\stab'}}


\newcommand{\lrhd}{\rhd_\approx}
\newcommand{\lera}{\rhd_\approx}
\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{\cfami}{\simeq_{\cal C}}
\newcommand{\err}[2]{\mbox{$ST_{{#1}}({#2})$}}
\newcommand{\staeq}{\approx_S}
\newcommand{\Le}{L\'evy}


\newcommand{\Tr}[1]{Theorem~\ref{#1}}
\renewcommand{\Pr}[1]{Proposition~\ref{#1}}
\newcommand{\Cr}[1]{Corollary~\ref{#1}}
\newcommand{\Lr}[1]{Lemma~\ref{#1}}
\newcommand{\Dr}[1]{Definition~\ref{#1}}
\newcommand{\lc}{$\lambda$-calculus}
\newcommand{\ovl}{\overline}
\newcommand{\unl}{\underline}
\newcommand{\bd}{\begin{defn}\em}
\newcommand{\bdl}[1]{\begin{defn}\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{defn}}
\newcommand{\el}{\end{lem}}
\newcommand{\ep}{\end{prop}}
\newcommand{\et}{\end{thm}}
\newcommand{\ee}{\end{ex}}
\newcommand{\ec}{\end{cor}}

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



\newcommand{\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{\pmn}{persistently $\stab$-needed}
\newcommand{\das}{\downarrow_{\stab}}
\newcommand{\dar}{\downarrow_{\reg}}
\newcommand{\stab}{{\cal S}}
\newcommand{\reg}{{\cal R}}
\newcommand{\imply}{\,\Rightarrow\,}

 
\newcommand{\pc}{permutation-equivalence}
\newcommand{\pt}{permutation-equivalent}


\newcommand{\calF}{{\cal F}}
\newcommand{\calR}{{\cal R}}
\newcommand{\calP}{{\cal P}}
\newcommand{\calC}{{\cal C}}
\newcommand{\calL}{{\cal L}}

 


\section{Introduction}



The prime goal of this paper is to provide a fully adequate concurrent
semantics for orthogonal rewrite systems. We chose Event Structures, as
the most successful and commonly accepted model of
concurrency, developed by Winskel, Nielsen and Plotkin~\cite{[Win],[NPW],[Win89],[WN]}. Conflict-free Prime Event
Structures (PESs) are sufficient for our purposes. A (conflict-free) PES
is simply a set of events partially ordered by a \emph{causal dependency}
relation (a \emph{poset}) where an event can only dominate a finite
number of events (the so called \emph{axiom of finite causes}). The idea
is to view a process as performing events (some \emph{atomic} tasks), and
an event can only occur after all events on which it depends. Causally
independent events are \emph{concurrent} events and can be evaluated in
parallel. Stages of a computation are thus represented by
\emph{configurations} -- left-closed event sets w.r.t. the causal order,
and the same configuration represents all sequential computations
executing events in that configuration, ignoring the order in which the
concurrent events occur.

In the theory of orthogonal rewrite systems, such as the \lc, there is
the well established concept  of `redex-family', due to
L\'evy~\cite{[levy],[le80]}, which formalizes the idea of the `same atomic
task'. Therefore it is natural to base our interpretation on considering
redex-families as events, and to interpret complete family-reductions (contracting entire families as multi-steps) as configurations of the corresponding PES. This is also justified by the fact that reductions in optimal
graph-implementations of orthogonal systems precisely correspond to
complete family-reductions in the original system~\cite{[Lam],[Kath]}.

Recent advances in the abstract study of the syntax and operational semantics of rewrite and transition systems~\cite{[Sta],[GLM],[rndrs],[dndrs],[ldrs],[acoi-rep]} allow us to address the problem in an entirely abstract setting. Stable Deterministic Residual Structures (SDRSs) and Deterministic Family Structures (DFSs) model computation in orthogonal rewrite systems. DRSs are Abstract
Rewrite Systems with an axiomatized residual relation; DFSs are DRSs
where in addition the concept of redex-family is axiomatized. Stable DRSs
allow~\cite{[rndrs],[dndrs]} proofs of analogs of the Normalization and
Standardization Theorems~\cite{[Bar]}. In DFSs one can further prove
the Optimality Theorem and the Unique Families Lemma~\cite{[rndrs]}. The latter states that any family can be contracted at most once in a complete
family-reduction.  It corresponds to the fact that any event may occur at
most once in the course of a computation, and is needed for the event
structure interpretation of DRSs based on interpreting families as
events. 


Thus we can start our interpretation by assuming that an orthogonal rewrite system is given in the form of a DFS. Furthermore, it has been shown in~\cite{[acoi-rep]} that any DFS can be given an interpretation by a non-duplicating or affine DFS with zig-zag as the family relation (AZDFS), called the \emph{implementation} of the original DFS: the reduction steps in the implementation DFS correspond to complete family-reduction multi-steps of the original DFS. Therefore it is enough to concentrate on defining PES semantics for AZDFSs.

  

To view a process as the domain of all its configurations, an
\emph{adequacy} requirement is desirable. Namely, that \emph{runs} of a
finite configuration (i.e., all its possible sequentializations) should
be in one-to-one correspondence with all finite reductions in the equivalence
class which the configuration is supposed to represent. Because of the
huge importance of \emph{permutation} or \emph{L\'evy equivalence} to the whole theory of (not only orthogonal) rewrite systems~\cite{[le80],[H.L.],[Bou]}, and to concurrency theory as
well~\cite{[Sta]}, we want to be able to treat permutation-equivalent finite reductions as representing the same concurrent computation, as indeed
permutation-equivalent finite reductions result one from another by permuting
concurrent consecutive steps. However, this is clearly impossible in the
present PES framework~\cite{[Win89]}, as a finite configuration in a PES has
only a finite number of runs while, a \pc\ class of a
finite reduction may have an infinite number of elements.


For example, consider the $\lambda$-term $t=Kx\Omega$, where $K=\lambda x y.x$
and $\Omega=(\lambda x.x)\lambda x.x$. Intuitively, all reductions of the form 
$t\red{\Omega}t\red{\Omega}\ldots \red{\Omega}t\red{K}x$, or $\Omega^mK$ in short, consisting of a number of $\Omega$-steps followed by a $K$-step, are `equal', as the $\Omega$-steps are performed in an erased part of $t$ (or in `garbage'). And indeed, permutation equivalence equates all the above reductions. However, there is no means in PESs to equate the corresponding configurations. 


The same problem can also be observed from a different angle.
In order for an equivalence relation to satisfy the adequacy requirement,
the corresponding equivalence classes of reductions must be
partially ordered so as to form finitary prime algebraic (or equivalently, distributive) complete lattices (see \Dr{D.fpad.}), since the domains
of configurations of PESs ordered by inclusion are such
lattices~\cite{[Win],[Win89]}. The latter are commonly accepted poset models for distributed computation. However, it is well known that L\'evy's
reduction space -- permutation equivalence classes of co-initial finite reductions ordered by L\'evy's embedding relation $\lleq$ (which generates permutation equivalence) --  is not in general a lattice but only an upper semi-lattice, as the greatest lower bound of two co-initial finite reductions w.r.t. $\lleq$  need not exist~\cite{[le80]}.\footnote{Recursive Program Schemes are an exception~\cite{[B.L.]}.} As a consequence, although the lattice properties can be restored by taking the ideal completion~\cite{[B.L.]}, the resulting domain need not be finitary prime algebraic even when the reduction relation is non-duplicating.  
For example, L\'evy's configuration domain of the $K$-$\Omega$ term above is not finitary as the $K$-step $Kx\Omega\red{K}x$ is a finitary element but it dominates (w.r.t. $\lleq$) an infinite number of elements: reductions of the form~$\Omega^m$.  


Several authors have proposed different ways to get round this problem.
Laneve~\cite{[Lan94]} introduced \emph{distributive} equivalence on
$\beta$-reductions which only allows permutation of steps that cannot
erase or duplicate one another, and consequently all equivalent sequences
have the same length. Similarly, Corradini et al~\cite{[CGM]} base their 
interpretation on the equivalence relation generated by permutations of 
disjoint redexes only, in a general categorical model of rewriting. 
Kennaway et al~\cite{[KKSdV]} do work with permutation equivalence for 
orthogonal Term Graph Rewriting, but they
only restrict themselves to needed events of a normalizable term to cope
with problems with erasure. As needed redexes cannot be erased, all
needed normalizing reductions are of the same length, and on needed
reductions, the permutation and distributive equivalences coincide (since
the system is non-duplicating).  Clark and Kennaway~\cite{[C.K.]} also work
with \pc\ and allow for (finitely) non-normalizable terms, but restrict themselves to standard reductions, and their ordering on standard reductions is a strong restriction of L\'evy's embedding relation. Other authors (e.g.,~\cite{[B.C.],[Sch]}) work with linear rewrite/transition systems (no duplication, no erasure), and do not therefore encounter the erasure problems.


In order to cope with the adequacy problem, we extend the PES model in two different but equivalent ways: by axiomatizing \pc\ on event configurations, by directly constraining the class of all equivalence relations
on configurations; and 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 finite
configurations with different numbers of events but still representing
the same \pc\ class of finite reductions.  We show that L\'evy's configuration domain -- appropriately ordered \pc\ classes of
finite configurations in a DEES/DPES -- is isomorphic to
L\'evy's reduction space of the corresponding AZDFS, and therefore DPESs/DEESs give a \emph{fully adequate} semantics to AZDFSs.



As a consequence,  L\'evy's configuration domains in DEESs/DPESs need not be finitary prime algebraic. However, having axiomatized the erasure relation and permutation equivalence on event configurations, we can define orderings on configurations reflecting the growth of information relative to \emph{stable} sets of `results', called \emph{stable orderings}, and thereby reconstruct finitary prime algebraic domains from configuration domains of DEESs/DPESs: The isomorphism between AZDFSs and DEESs/DPESs discussed above induces  a concept of stable sets of configurations in DEESs/DPESs,  and the theory of normalization by neededness relative to stable sets of terms in AZDFSs~\cite{[rndrs]} has its counterpart in DEESs/DPESs; and this relativized concept of neededness enables us to show that the stable orderings on configuration domains of DEESs/DPESs do form finitary prime algebraic domains.  


The paper is organized as follows. In the next section, we review the
existing theory of DRSs and DFSs used in this paper. In
Section~\ref{dees.dpes.} we introduce DPESs and DEESs and establish their
equivalence. In Section~\ref{rel.mod.} we relate the latter event models
with affine SDRSs (ASDRSs) and AZDFSs, showing the equivalence of the four
models. In Section~\ref{latt.str.}, we define L\'evy's
configuration domain in a DPES/DEES and show its isomorphism with L\'evy's
reduction space of the corresponding ASDRS. We study normalization by neededness in DEESs in Section~\ref{S.pres.need.}, and use it to construct finitary prime algebraic domains from configurations in DEESs/DPESs in Section~\ref{S.rel.in.dom.}. Conclusions appear in Section~\ref{concl.}.





\section{Deterministic Residual and Family Structures}
\label{S.dfs-drs.}


In this section, we recall some basic theory of \emph{Deterministic 
Residual} and  \emph{Family Structures} (DRSs and DFSs), developed 
in~\cite{[rndrs],[dndrs],[ldrs],[acoi-rep]}. DRSs and DFSs are 
\emph{Abstract Reduction Systems} (ARSs) with an axiomatized notion of
residual. In DFSs, in addition, L\'evy's concept of redex-family is 
axiomatized.  Related abstract residual models are studied 
in~\cite{[Hin],[Sta],[GLM],[Mel.th]}.


Our definition of ARSs allows multiple transitions with the same source 
and target, unlike Klop's definition~\cite{[Klo92]}.

\bd
An ARS is a triple $A$ = ({\em Ter},{\em Red},$\ar$)
where {\em Ter} is a set of {\em terms}, ranged over by
$t,s,o,e$; {\em Red} is a set of {\em redexes} (or {\em redex occurrences}),
ranged over by $u,v,w$; and $\ar:Red\mapsto (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 $\mapsto(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$. If $P$ is finite and its final term coincides with the initial term 
of $Q$, then $P+Q$ denotes the concatenation of $P$ and $Q$.  Finally, 
$u$ also denotes the reduction that contracts $u$.  
\ed

\delete{
DRSs axiomatize exactly the properties of residuals which are used
in~\cite{[le80],[H.L.]} to define permutation equivalence on reductions, and the L\'evy-embedding relation on permutation-equivalence classes which is used to construct L\'evy's reduction space. DRSs are similar to Stark's {\em Determinate Concurrent Transition Systems} (DCTSs) \cite{[Sta]} and {\em Abstract Reduction Systems} of Gonthier et al.~\cite{[GLM]}. Unlike DCTSs, the residual relation in DRSs may be duplicating, and unlike ARSs of~\cite{[GLM]},  we do
not have a nesting relation on redexes.  Several refined concepts of abstract rewriting are studied in~\cite{[Oos.th],[Mel.th],[Raa.th]}.
DRS are intended to model all orthogonal term and graph rewrite systems,
both first and higher-order, and other conflict-free transition systems with a reasonable level of abstraction. In contrast, ARSs of~\cite{[GLM]} do not cover orthogonal Term Graph Rewriting Systems~\cite{[KKSdV]}, for example, and Interaction Nets~\cite{[Laf]}, which form DRSs (when restricted to finite nets), do not have or need any nesting order on redexes (as nets are undirected, possibly cyclic, graphs).
}
 

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

A \emph{development} of $U\subts t$ is a reduction $P:t\doar $ that only contracts residuals of redexes from $U$; it is \emph{complete} if it is finite and $U/P=\cup_{u\in U}\,u/P=\emptyset$. Development of $\emptyset$ is identified with the empty reduction. $U$ will also denote a complete development of $U\subts t$. The residual relation satisfies the following two axioms:
\bds
\item[{[\rm{FD}]}] (\emph{Finite Developments}~\cite{[GLM]}) All developments are terminating; all complete developments of $U\subts t$ end at the same term; and residuals of a redex $v\subt t$ under all complete developments of $U$ are the same.

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

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

In a DRS $\cal R$, the residual relation on redexes extends
to all co-initial reductions exactly as in syntactic orthogonal rewrite 
systems~\cite{[H.L.],[levy],[le80],[Sta]}: $(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 \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'\,
\Rightarrow \, 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$.
Intuitively, $P\lleq Q$ expresses that $Q$ does more work than $P$,
 and $Q/P$ is the part of $Q$ that remains from it after $P$.
Finally, one shows that for any co-initial reductions $P,Q$, $P\sqcup Q\leeqv Q\sqcup P$, where $P\sqcup Q=P+Q/P$, and is the greatest lower bound of $P$ and $Q$ in the reduction space ordered by L\'evy's embedding relation $\lleq$.
The above relations can equivalently be defined also using Klop's method of commutative diagrams~\cite{[Kl.CRS],[Bar]}. Finally, we will need the following \emph{Cube Lemma}: for any finite co-initial reductions $P,Q$ and $N$, $N/(P\sqcup Q)= N/(Q\sqcup P)$.
 

The following two lemmas, established in~\cite{[rndrs],[dndrs]}, are fundamental in proving properties in SDRSs. They extend [weak acyclicity] and [stability] axioms from one step reductions to any co-initial \emph{external} reductions, that is, reductions that do not contract redexes having common residuals. 



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

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

\begin{diagram}[height=1.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     \\
s_j     &\rOnto^{P_i/Q_j}& & {}    & \rOnto^{U_{i,j}} & {}   \\
\dTo<{v_j}   &         & &\dOnto^{V_{i,j}} &             &  \dOnto   \\
s_{j+1}      &\rOnto      & &  {}       & \rOnto      & {}   \\
\end{diagram}
\eit
\ed



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


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

 

Next we recall some definitions and results from~\cite{[dndrs]} concerning standardization of reductions in ASDRSs, used in this paper. 



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

\item  We call $u$ \emph{$P$-needed} if there is no
$Q\leeqv P$ that is external to $u$, and call it \emph{$P$-unneeded} 
otherwise. We call $u$ \emph{$P$-essential} if there is no $Q\leeqv P$ 
that discards $u$, and \emph{$P$-inessential} otherwise. 
 
We extend these concepts to reductions co-initial with those containing
$u$ as a redex of one of its terms.

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


Note that $P$-neededness, $P$-erasure, and $P$-essentiality do not depend
on the choice of a reduction in the class $\lclas{P}$ of reductions
L\'evy-equivalent to $P$, since $u/P=u/Q$ when $P\leeqv Q$, by the Cube Lemma.
The \emph{discards} concept however does depend on the particular reduction 
in the \pc\ class.



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

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

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

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


Self-needed reductions play the role of \emph{standard} reductions in SDRSs, and the following algorithm is a standardization procedure for reductions in ASDRSs.
Let $P:t\doar s$. The {\em canonical standard variant of $P$},
$ST(P)$, is defined as follows: If $P=\emp$, then $ST(P)=\emp$. 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)$. 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$. In particular, $ST(P)\in\stav{P}$.

 
 
\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
 

 


It is shown in~\cite{[ldrs],[acoi-rep]} that all standard variants of a finite reduction $P$ can be constructed effectively.



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

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


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

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

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

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

Note that [contribution] can be viewed as a definition of $\contr$
rather than as an axiom. It is shown in~\cite{[rndrs]} that every DFS is a stable DRS. 


\noindent {\bf Convention}
In this paper we only consider \emph{comma-DRS}s and \emph{comma-DFS}s. 
That is, the term set of any DRS will be the \emph{reduction graph} of a 
term, called the \emph{initial} term, i.e., the set of terms to which 
the initial term is reducible. The initial term will often be denoted by 
$t_\emp$, by analogy with the initial state $\emp$ in an Event Structure. Further, 
in DFSs, families will always be considered relative to $t_\emp$, i.e., 
all histories start with $t_\emp$. 
Unless otherwise stated, by a \emph{reduction} we mean a \emph{finite} 
reduction. Reductions starting from $t_\emp$ will also be called 
\emph{initial} reductions.


\bd
\bit
\item We call a DFS $\cal F$ a \emph{zig-zag} DFS, ZDFS, if its family relation is the zig-zag $\zfami$. Affine ZDFSs will be called AZDFSs.

\item We call an affine DFS \emph{separable} 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'')$.
\eit
\ed

  

The following lemma from~\cite{[ldrs],[acoi-rep]} gives a useful characterization of $\lleq$ and $\leeqv$ in ASDRSs via zig-zag classes.
Below, $FAM(P)$ (resp. $SFAM(P)$) denotes the set of \emph{zig-zag classes} whose member (resp. $P$-needed) redexes are contracted in $P$, in an ASDRS.



\bpl{P.leqv.sam.se.es.fa.}
Let $P$ and $Q$ be initial reductions in an AZDFS. Then $P\lleq Q$ iff $\exists Q'\leeqv Q: FAM(P)\ssq FAM(Q')$, and $P\leeqv Q$ iff $SFAM(P)=SFAM(Q)$. Further, $SFAM(P)=FAM(ST(P))=\cap_{N\leeqv P} FAM(N)$. Consequently, if $P,Q\in\stan$, then $P\leeqv Q$ iff $FAM(P)=FAM(Q)$ (since in that case $P=ST(P)$ and $Q=ST(Q)$).
\ep


The results of this paper are based on the following properties of ASDRSs, which show that ASDRSs and AZDFSs are essentially the same transition models, and that every zig-zag family has a unique (up to an equivalence on histories) minimal element~\cite{[ldrs],[acoi-rep]}.



\btl{T.lin.dr.sta.df.}
{\bf (Affine Families)} Let $\cal R$ be an ASDRS. Then ${\cal F_R}=(\calR,\zfami,\zcontr)$ is an affine zig-zag DFS, called the \emph{corresponding} ZDFS of $\cal R$. Further, ${\cal F_R}$ is the only separable DFS with $R$ as the underlying SDRS, and in general, an affine DFS is separable iff it is a zig-zag DFS.
\et


\btl{P.on.ca.for.}
{\bf (Affine Extraction)} Every redex $Pv$ in an ASDRS $\cal R$ has a zig-zag related redex $P'v'$ in \emph{canonical} form, meaning that $P'\in\stan$, its last step creates $v'$, and for any $P''v''\zfami Pv$, $\exists N':P''\leeqv P'+N'\wedge v''=v'/N$. For any other canonical form $P^*v^*$ of $Pv$,  $P'\leeqv P^*$ and $v'=v^*$. Further, $P'$ contracts exactly one redex in every contributor zig-zag family of $Pv$, in the corresponding AZDFS ${\cal F_R}=(\calR,\zfami,\zcontr)$ of $\cal R$.
\et
 
 
  


\section{Deterministic Permutation and Erasure Event Structures}
\label{dees.dpes.}



In this section, we introduce Deterministic Permutation and Erasure Event Structures, DPESs and DEESs, which extend conflict-free Prime Event Structures by an axiomatized permutation-equivalence and erasure relations, respectively, and establish an equivalence between them.   


The purpose of this extension is to capture \emph{directly} the phenomenon of
\emph{erasure} in event/poset models. The phenomenon is typical for
languages based on rewrite systems, but is not confined to them. In higher-order process calculi (e.g.,~\cite{[San.Th]}) processes (that can fire events) can be passed around as messages and therefore erased. Event Structures are linear in nature and consequently the configuration domains enjoy very nice lattice properties; therefore Event Structures have been very successful in modelling \emph{linear} process calculi where no actions can be erased or duplicated (see e.g.,~\cite{[B.C.],[Win89]}), such as CCS~\cite{[Mil89]}. However, any attempt to adequately interpret higher-order process languages in Event Structures would face the same erasure problems discussed in the introduction. As in the case of reductions, the aim of axiomatizing permutation equivalence on event configurations is to be able to equate configurations which represent the same concurrent computation and differ only by irrelevant or \emph{inessential} events. We believe that any equivalence relation on configurations fully capturing concurrency should contain the permutation-equivalence.


A \emph{Prime Event Structure} (PES)~\cite{[Win]} is a triple 
${\cal E}=(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 finite 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 only consider \emph{conflict-free} or \emph{deterministic} PESs, where no event can prevent others from occurring, and therefore the consistency predicate is the set of all finite subsets of $E$ and will be omitted. Finite \emph{configurations} of ${\cal E}$ are finite \emph{left-closed subsets} $\alpha,\beta,\ldots$ of $E$, i.e., subsets $\fcE=\{\alpha\ssq_{fin} E\,\vert\, e\in \alpha\,\wedge\, e'< e \Rightarrow e'\in\alpha\}$. Except for Section~\ref{S.rel.in.dom.}, we only consider finite configurations, and will omit `finite'.


Below, for better readability, we write $\alpha +e$ for $\alpha \cup\{e\}$, and write $\alpha-e$ for $\alpha \setminus\{e\}$. Further, we define $\con{e}=\{e'\,\vert\, e'\leq e\}$, $\ocon{e}=\{e'\,\vert\,e'<e\}$,  $\coni{e}=\{e'\,\vert\, e\geq e'\}$ and $\oconi{e}=\{e'\,\vert\,e'>e\}$.


\bdl{D.DPES.}
A \emph{Deterministic Permutation Event Structure} (DPES) is a triple  ${\cal P}=(E, \leq, \leeqv)$, where ${\cal E}=(E, \leq)$ is a conflict-free  PES and $\leeqv\ssq \fcE \times \fcE$ is an equivalence relation, called \emph{L\'evy-} or \emph{permutation-equivalence}, satisfying the following axioms, where $\alpha,\beta,\gamma\in\fcE$:
\bds
\item[{[\rm{P0}]}] $\forall e\in E: \ocon{e}\not\leeqv \con{e}$;  


\item[{[\rm{P1}]}] $\alpha\leeqv\beta \wedge \alpha\cap\beta \ssq\gamma\ssq \alpha\cup\beta \imply \alpha\leeqv\gamma$;

\item[{[\rm{P2}]}] $\alpha\leeqv\beta \wedge \alpha +e,\beta+e\in \fcE \imply \alpha +e\leeqv \beta +e$;  

\item[{[\rm{P3}]}] $\alpha\leeqv \alpha-e\wedge e<e' \wedge 
\alpha+e'  \in\fcE \imply \alpha \leeqv\alpha+e'$;
\eds
\ed




DEESs extend \emph{Deterministic Computation Structures}~\cite{[rndrs]} by further erasure axioms to enable a fully adequate treatment of erasure.


\bdl{D.DEES.}
A \emph{Deterministic Erasure Event Struc\-ture} (DEES) is a triple $\calC=(E,\leq, \era)$, where  ${\cal E}=(E,\leq)$ is a conflict-free PES and $\rhd\ssq \fcE \times E$ is \emph{inessentiality} or \emph{erasure} relation (read $\alpha\,\rhd\, e$ as: `$e$ is \emph{$\alpha$-inessential}'), satisfying the following axioms, where $\alpha,\beta\in\fcE$:
\ben
\item[{[\rm{E0}]}] $\forall e\in E: \emptyset\not\era e$;

\item[{[\rm{E1}]}]  $\alpha\rhd e \wedge \alpha\ssq \beta  
\in \fcE \Rightarrow \beta\rhd e$;
 

\item[{[\rm{E2}]}] $\alpha\rhd e'\wedge \alpha\rhd e \wedge 
\alpha-e'\in\fcE  \Rightarrow  \alpha-e'\rhd e$;

\item[{[\rm{E3}]}] $\alpha\era e \wedge e<e'\imply \alpha\era e'$;

\item[{[\rm{E4}]}] $\alpha\cup \ocon{e} \era e \imply
\alpha\era e$.  
\een
\ed


We may write $\alpha\era X$ if $\forall e\in X:\alpha\era e$. Sometimes we write $\fcP$ for $\fcE$ if $E$ is the domain of a DPES $\cal P$, and similarly for $\fcC$. 


Before explaining the intuition behind the axioms, we first define translations between DPESs and DEESs.


\bdl{D.era.vi.per.eq.}
For a DPES ${\cal P}=(E, \leq, \leeqv)$, we define an \emph{erasure} relation $\lrhd\ssq \fcE \times E$ and the corresponding structure ${\cal C_P}=(E,\leq, \lrhd)$ as follows:
\bit
\item  $\alpha\lrhd e$ iff $\alpha\cup \con{e}\leeqv (\alpha\cup \con{e}) \setminus \coni{e}$.
\eit
In particular, when $e\in\alpha$ and $\alpha-e\in\fcE$, 
\bit
\item  $\alpha\lrhd e$ iff $\alpha \leeqv \alpha-e$.
\eit
\ed



\bdl{D.eq.in.era.}
For a DEES $\calC=(E,\leq,\rhd)$, we define an equivalence relation $\eleeqv\ssq \fcE\times\fcE$ and the corresponding structure ${\cal P_C}=(E,\leq,\eleeqv)$ as follows:
\bit
\item  $\alpha\eleeqv \beta$ iff $ST_{\rhd}(\alpha)=ST_{\rhd}(\beta)$, where
$ST_{\rhd}(\alpha)=\{e\in\alpha\,\,\vert\,\,\alpha\not\rhd e\}$.  (The subscript $\rhd$ in $ST_{\rhd}(\alpha)$ will often be omitted.) $\sea$ will be called the \emph{standard variant} of $\alpha$. 
\eit
\ed


 
By looking at a configuration $\alpha$ as an initial reduction $P_{\alpha}$ firing redexes corresponding to events in $\alpha$, and by interpreting $\alpha\era e$ as `$Qv$ is $P$-inessential', where $Qv$ is a redex representing $v$ (so $Q$ contracts redexes corresponding to events on which $e$ causally depends), it is not difficult to understand the intuition behind the erasure axioms. For example, [E0] says that an empty reduction cannot erase any redex, and [E1] says that if $Qv$ is $P_\alpha$-inessential and $P_{\alpha}\lleq P_{\beta}$, then $Qv$ is $P_\beta$-inessential as well. This intuition will become more precise in the next section. Further, a
close inspection of the above definitions shows that the DPES axiom [P0] is a counterpart of the DEES axioms [E0] and [E4], and similarly for [P3] and [E3].  The combination of [P1] and [P2] have the same effect as that of [E1] and [E2]. [E4] does not have a `direct' counterpart among DPES axioms, but it corresponds to the fact that, according to \Dr{D.red.need.ess.}, a redex with history $Pv$ is $Q$-inessential iff $v$ is $Q/P$-inessential. Similarly, [P0] corresponds to \Lr{L.era.and.ess.im.ne.}.(2).



In order to establish equivalence of DEESs and DPESs, we need a few lemmas.


\bll{L.se.con.}
Let $\alpha\in \fcC$, in a DEES $\calC$. Then $\sea\in \fcC$. Further, $ST(\sea)=\sea$, hence $\alpha\eleeqv\sea$.

\bproof
Let $e\in \sea\wedge e'<e$. Then $e\in\alpha$ and $\alpha\not\era e$, implying by [E3] that $\alpha\not\era e'$. Since $\alpha\in \fcC$ and $e'<e$, $e'\in\alpha$, implying $e'\in \sea$. Hence $\sea\in \fcC$. If, on the contrary,  $ST(\sea)\not=\sea$, i.e., $\exists e''\in \sea:\sea\era e''$, then $\alpha\era e''$ by [E1], contradicting $e''\in \sea$. Now $\alpha\eleeqv\sea$ follows immediately from \Dr{D.eq.in.era.}.
\eproof
\el


 
\bll{L.alp.eq.sel.al.}
Let $\alpha\in \fcC$, in a DEES $\cal C$. Then $\alpha \rhd e$ iff $\sea \rhd e$.

\bproof
\ben
\item[\suf] Let $\alpha=\sea\cup \{e_1,\ldots,e_n\}$, where the enumeration $e_1,\ldots,e_n$ respects the order on $E$, let $\alpha_0=\alpha$, and let $\alpha_{i+1}=\alpha_i +e_{i+1}$ (hence $\alpha=\alpha_n$). Denote $e=e_0$. By the definition of $\sea$ and the assumption, we have $\alpha_n\rhd e_i$ for all $i=0,1,\ldots,n$. By [E2], we have from $\alpha_n\rhd e_n$ and $\alpha_n\rhd e_i$ that $\alpha_{n-1}\rhd e_i$.  Hence, again by [E2], $\alpha_{n-2}\rhd e_i$, and so on. Finally, we get $\alpha_0\rhd e_i$ for all $i$, and in particular, $\alpha_0\rhd e$. 

\item[\nec] By [E1].
\een
\eproof
\el




\bll{L.sune.seeqv.}
Let $\alpha,\beta\in\fcE$ and $\alpha\ssq\beta$, in a DEES $\cal C$. Then $ST(\alpha)=ST(\beta)$ iff $\beta\era \beta\setminus\alpha$.
 
\bproof
\ben
\item[\suf]  By \Dr{D.eq.in.era.}, since $\beta\setminus\alpha\ssq \beta\setminus ST(\alpha)$. 

\item[\nec]
Since $\beta\era \beta\setminus\alpha$, $\seb\ssq\alpha$. Let $e'\in \seb$. Then $e'\in\beta$ and $\beta\not\era e'$, implying by [E1] and $\alpha\ssq\beta$ that $\alpha\not\era e'$, i.e., $e'\in \sea$. Hence $\seb\ssq\sea$. For the converse, take $e''\in\sea$. Then $e''\in\alpha$ and $\alpha\not\era e''$. Therefore, $e''\in\beta$ and by [E1] $\seb\not\era e''$, implying by \Lr{L.alp.eq.sel.al.} that $\beta\not\era e''$, i.e., $e''\in\seb$. Hence $\sea=\seb$.
\een
\eproof
\el
 



\bpl{C.char.sea.eq.}
Let $\alpha,\beta,\gamma\in\fcC$, in a DEES $\calC$, and let $\alpha\cap\beta\ssq\gamma \ssq\alpha\cup\beta$. Then $\sea=\seb\Leftrightarrow \gamma\era\alpha\cup\beta\setminus\alpha\cap\beta$. Consequently, $\alpha\eleeqv\beta$ iff $\gamma\era\alpha\cup\beta\setminus\alpha\cap\beta$.

\bproof
\ben
\item[\suf] $\sea=\seb\imply \sea\ssq\alpha\cap\beta$, and by the definition of $\sea$, \Lr{L.alp.eq.sel.al.}, and [E1], $\sea=\seb \imply \sea\era\beta\setminus\alpha\cup\alpha\setminus\beta \imply \gamma\era\alpha\cup\beta\setminus\alpha\cap\beta$. 

\item[\nec] By [E1] and \Lr{L.sune.seeqv.}, $\alpha\cap\beta\era\alpha\cup\beta\setminus\alpha\cap\beta \imply \alpha\era \alpha\setminus\beta \wedge \beta\era \beta\setminus\alpha \imply \sea=ST(\alpha\cap\beta)=\seb$.  
\een
\eproof
\ep



\btl{T.lee.imp.eras.}
For any DEES $\calC=(E,\leq,\rhd)$, ${\cal P_C}=(E,\leq,\eleeqv)$ is a DPES.

\bproof
We need to show that $\eleeqv $ satisfies the permutation axioms [P0] -- [P3].  
\bds
\item[{[\rm{P0}]:}] Let $e\in E$. Note that $\con{e}\era e$ would imply by [E2] that $\ocon{e}\era e$, implying $\emp\era e$ by [E4], contradicting [E0]. Hence $\con{e}\not\era e$, i.e., $e\in ST(\con{e})$, and therefore $ST(\con{e})\not=ST(\ocon{e})$. Thus $\con{e}\not\eleeqv \ocon{e}$ by \Dr{D.eq.in.era.}.

\item[{[\rm{P1}]:}] Let $\alpha\eleeqv\beta$, $\alpha\cap\beta\ssq\gamma\ssq\alpha\cup\beta$, and $\gamma\in\fcE$. By \Dr{D.eq.in.era.}, $\sea=\seb$, hence $\sea\ssq\alpha\cap\beta\ssq\gamma$. Further, $\forall e\in\alpha\cup\beta\setminus\sea$, $\alpha\era e$ or $\beta\era e$, hence $\sea\era e$ by \Lr{L.alp.eq.sel.al.}. Hence $ST(\sea)=\seg$ by \Pr{C.char.sea.eq.}, and $\sea=\seg$ by \Lr{L.se.con.}, implying $\gamma\eleeqv\alpha$ by \Dr{D.eq.in.era.}.


\item[{[\rm{P2}]:}] Let $\alpha\eleeqv\beta$ and  $\alpha+e,\beta+e\in\fcE$. By \Dr{D.eq.in.era.}, $\sea=\seb$. Assume first that $\sea\era e$. Then $\alpha+e\era e$ by [E1] and $ST(\alpha+e)=\sea$ by \Pr{C.char.sea.eq.}. Similarly, $ST(\beta+e)=\seb$. Hence, $ST(\alpha+e)=ST(\beta+e)$, implying by \Dr{D.eq.in.era.} that $\alpha+e\eleeqv\beta+e$. Now let $\sea\not\era e$. Then, by \Lr{L.alp.eq.sel.al.} and [E3], $\forall e'\in\alpha\setminus\sea:e'\not<e$. Thus $\alpha+e\in\fcE\imply\sea+e\in\fcE$. By \Lr{L.alp.eq.sel.al.}, $\sea\not\era e$ implies $\alpha\not\era e$, thus $e\in\sea$ iff $e\in\alpha$, and therefore $\alpha+e\setminus(\sea+e)=\alpha\setminus\sea$.
Hence $\alpha+e\era \alpha+e\setminus(\sea+e)$ by [E1] (as $\alpha\era \alpha\setminus\sea$), and we have by \Pr{C.char.sea.eq.} that $ST(\alpha+e)=ST(\sea+e)$, thus $\alpha+e\eleeqv\sea+e$ by \Dr{D.eq.in.era.}. Similarly, $\beta+e\eleeqv\seb+e$, implying $\alpha+e\eleeqv\beta+e$ (since $\sea=\seb$).

\item[{[\rm{P3}]:}] Let $\alpha\eleeqv \alpha-e$, $e<e'$ and $\alpha+e'\in\fcE$ (hence $e\in\alpha$). By \Dr{D.eq.in.era.}, $\sea=ST(\alpha-e)$, implying $\alpha\era e$. Hence, by [E3], $\alpha\era e'$, implying by [E1] that $\alpha+e'\era e'$. Hence, by \Pr{C.char.sea.eq.}, $ST(\alpha+e')=\sea$, thus $\alpha+e'\eleeqv\alpha$ by \Dr{D.eq.in.era.}.
\eds
\eproof
\et



\btl{T.tra.dpe.dee.}
For any DPES ${\cal P}=(E, \leq, \leeqv)$, ${\cal C_P}=(E, \leq, \lrhd)$ is a DEES.

\bproof
We need to show that $\lrhd$ satisfies the erasure axioms [E0] -- [E4]. 
\bds
\item[{[\rm{E0}]:}] By \Dr{D.era.vi.per.eq.} and [P0].

\item[{[\rm{E3}]:}] Let $\alpha\lrhd e$ and $e<e'$. We want to show that $\alpha\lrhd e'$. We can assume that $\not\exists e'': e<e''<e'$.  Assume first that $e,e'\in\alpha$ (hence $\alpha\cup\con{e}=\alpha\cup\con{e'}=\alpha$). By \Dr{D.era.vi.per.eq.}, $\alpha\lera e\imply \alpha\leeqv \alpha\setminus\coni{e}$. But $\alpha\setminus\coni{e}\ssq \alpha\setminus\coni{e'}\ssq\alpha$, implying by [P1] that $\alpha\leeqv\alpha\setminus\coni{e'}$, i.e., by \Dr{D.era.vi.per.eq.}, $\alpha\lera e'$. Now let $e\in\alpha$ and $e'\not\in\alpha$. Let $\gamma=\alpha\setminus\oconi{e}$. By \Dr{D.era.vi.per.eq.}, $\alpha\lera e$ iff $\gamma\lrhd e$ iff  $\gamma\leeqv \gamma-e$. Further, $\gamma\cup\con{e'}=\gamma+e'$ and $\gamma\cup\con{e'}\setminus\coni{e'}=\gamma$. By [P3], $\gamma\leeqv\gamma+e'$, implying $\gamma\lera e'$ and equivalently $\alpha\lera e'$ by \Dr{D.era.vi.per.eq.}. Finally, let $e,e'\notin\alpha$. Take $\beta=\alpha\cup\con{e}$. Then, by \Dr{D.era.vi.per.eq.}, $\alpha\lera e$ iff $\beta\lera e$ and $\alpha\lera e'$ iff $\beta\lera e'$, and we have $e\in\beta$ and $e'\not\in \beta$ like in the previous case, and [E3] follows.

 
\item[{[\rm{E1}]:}] Let $\alpha\lrhd e\,\wedge\,\alpha\ssq \beta\, 
\in \fcE$. We can assume that $\beta=\alpha+e'$ and $e'\not\in\alpha$.  If $e\geq e'$, then $\alpha+e'\cup\con{e}=\alpha\cup\con{e}$ and $\alpha+e'\cup\con{e}\setminus\coni{e}=\alpha\cup\con{e}\setminus\coni{e}$, thus $\alpha\lera e$ iff $\alpha+e'\lera e$ by \Dr{D.era.vi.per.eq.}. If $e\not<e'$ and $e'\not< e$, then $\alpha+e'\cup\con{e}=\alpha\cup\con{e}+e'$ and $\alpha+e'\cup\con{e}\setminus\coni{e}=\alpha\cup\con{e}\setminus\coni{e}+e'$, and $\alpha+e'\lera e$ follows from $\alpha\lera e$ by [P2] and \Dr{D.era.vi.per.eq.}. Finally, if $e<e'$, then $\alpha+e'\in\fcE\imply e\in\alpha$.  By [E3] which we have already proven above for $\lera$, $\alpha\lera e\imply\alpha\lera e'$; thus  by \Dr{D.era.vi.per.eq.} we have from $\alpha\lera e$ that $\alpha=\alpha\cup\con{e}\leeqv \alpha\cup\con{e}\setminus\coni{e}$, and we have from from $\alpha\lera e'$ that $\alpha\leeqv\alpha+e'$. Hence $\alpha+e'\cup\con{e}\setminus\coni{e}\leeqv$ (since $e<e'$) $\leeqv \alpha\cup\con{e}\setminus\coni{e}\leeqv \alpha\leeqv \alpha+e'=\alpha+e'\cup \con{e}$, which means by \Dr{D.era.vi.per.eq.} that $\alpha+e'\era e$.



\item[{[\rm{E2}]:}] We can assume that $e'\in\alpha$. Let $\alpha\lrhd e'$,  $\alpha\lrhd e$ and $\alpha-e'\in\fcE$. By \Dr{D.era.vi.per.eq.}, $\alpha\lera e\Rightarrow \alpha\cup\con{e}\leeqv \alpha\cup\con{e}\setminus \coni{e}$ and $\alpha\lrhd e'\Rightarrow \alpha\leeqv \alpha-e'$, implying by repeated application of [P2] that $\alpha\cup\con{e}\leeqv \alpha-e'\cup\con{e}$. It is easy to check� that $(\alpha\cup\con{e}\setminus \coni{e})\cap (\alpha-e'\cup\con{e})= 
(\alpha\cup\con{e})\cap (\alpha-e'\cup\con{e})\setminus \coni{e}= \alpha-e'\cup\con{e}\setminus \coni{e}$ implying by [P1] that $\alpha-e'\cup\con{e}\leeqv \alpha-e'\cup\con{e}\setminus \coni{e}$. Hence, $\alpha-e'\lera e$ by \Dr{D.era.vi.per.eq.}.  


\item[{[\rm{E4}]:}] We need to show that $\alpha\cup \ocon{e} \lrhd e \imply
\alpha\lrhd e$. Indeed, by \Dr{D.era.vi.per.eq.}, $\alpha\cup \ocon{e} \era e$ iff $(\alpha\cup \ocon{e})\cup\con{e}\setminus \coni{e}\leeqv(\alpha\cup \ocon{e})\cup\con{e} \Leftrightarrow \alpha\cup\con{e}\setminus \coni{e}\leeqv \alpha\cup\con{e}$ iff $\alpha\lrhd e$.
\eds
\eproof
\et


\bll{L.al.le.se.al.}
Let ${\cal P}=(E,\leq,\leeqv)$ be a DPES, and let $\alpha\in \fcE$. Then $\alpha\leeqv ST_{\lrhd}(\alpha)$.

\bproof
By \Tr{T.tra.dpe.dee.} and \Lr{L.se.con.}, $ST_{\lrhd}(\alpha)$ is a configuration. Let $\alpha\setminus ST_{\lera}(\alpha)=\{e_1,\ldots, e_n\}$. By \Dr{D.era.vi.per.eq.}, $\alpha\lera e_i\imply \alpha\leeqv\alpha\setminus\coni{e_i}$. Clearly, $\cap_{i=1}^n \alpha\setminus\coni{e_i}\ssq\lsea\ssq\alpha$, implying by [P1] and $\alpha\leeqv\alpha\setminus\coni{e_i}$ that $\alpha\leeqv ST_{\lrhd}(\alpha)$.
\eproof
\el



The next proposition gives a characterization of $\leeqv$ via $\lera$, needed for establishing an isomorphism between DPESs and DEESs.


\bpl{C.sees.eq.leeq.}
In a DPES ${\cal P}=(E,\leq,\leeqv)$, $\alpha\leeqv\beta$ iff $ST_{\lera}(\alpha)=ST_{\lera}(\beta)$.

\bproof
\ben
\item[\nec] Immediate from \Lr{L.al.le.se.al.}. 

\item[\suf] By \Lr{L.al.le.se.al.}, $\alpha\leeqv ST_{\lrhd}(\alpha)\leeqv ST_{\lrhd}(\beta)$. Suppose on the contrary that $ST_{\lera}(\alpha)\not=ST_{\lera}(\beta)$, say $\exists e\in \lsea \setminus (\lsea\cap\lseb)$. By [P1], $\lsea\leeqv\lsea\cap\lseb$. Further, $\lsea\cap\lseb\ssq\alpha\setminus\coni{e}\ssq \alpha$ (since $\lsea\cap\lseb$ is left-closed), hence again by [P1] $\alpha\cup\con{e} \setminus\coni{e}=\alpha\setminus\coni{e}\leeqv \alpha=\alpha\cup \con{e}$, implying by \Dr{D.era.vi.per.eq.} that $\alpha\lera e$, contradicting $e\in\lsea$.
\een
\eproof
\ep
 

\btl{T.dc.ps.det.equ.}
{\bf (Equivalence of DPESs and DEESs)}
\ben
\item[(1)] For any DEES $\calC=(E,\leq,\rhd)$, $\cal C_{P_C}=\cal C$.

\item[(2)] For any DPES ${\cal P}=(E,\leq,\leeqv)$, $\cal P_{C_P}=\cal P$.
\een

\bproof
Note that the translations of DEESs into DPES and vice versa does not effect the sets of events and the causality relation. Thus ${\cal C_{P_C}}=(E,\leq,\era_{\eleeqv})$ and ${\cal P_{C_P}}=(E,\leq,\leeqv_{\lera})$. We need to show that (1) $\era=\era_{\eleeqv}$ and (2) $\leeqv=\leeqv_{\lera}$.
\ben
\item[(1)] We need to prove that $\alpha\rhd e$ in $\cal C$ iff $\alpha\era_{\eleeqv} e$ in ${\cal C_{P_C}}$. By [E4], [E1] and [E3], $\alpha\era e$ iff $\alpha\cup \con{e}\era e$ iff $\alpha\cup\con{e}\era\coni{e}$. By \Pr{C.char.sea.eq.}, the latter holds iff $ST_\era(\alpha\cup\con{e})=ST_\era(\alpha\cup\con{e}\setminus \coni{e})$, which, by \Dr{D.eq.in.era.} means that $\alpha\cup\con{e}\eleeqv\alpha\cup\con{e}\setminus \coni{e}$, meaning $\alpha\era_{\eleeqv} e$ by \Dr{D.era.vi.per.eq.}.
 

\item[(2)] We need to prove that $\alpha\leeqv \beta$ in $\cal P$ iff $\alpha\leeqv_{\lera} \beta$ in $\cal P_{C_P}$. By \Pr{C.sees.eq.leeq.} and \Dr{D.eq.in.era.}, $\alpha\leeqv\beta$ iff $\lsea=\lseb$ iff $\alpha\leeqv_{\lera}\beta$. 
\een
\eproof
\et



From now on, we will merge DEESs $\calC=(E,\leq,\era)$ and DPESs ${\cal P}=(E,\leq,\leeqv)$ into one model   $(E,\leq,\era,\leeqv)$, where $(E,\leq)$ is a Prime Event Structure, the erasure relation $\era$ satisfies axioms [E0] - [E4], and $\leeqv=\eleeqv$. The obtained results allow us to assume that the permutation-equivalence $\leeqv$ satisfies axioms [P0] - [P3], and that $\era=\lera$. We call such models again DEESs, and denote by~$\calC$.
 




\section{Relating Conflict-Free Stable Transition and Event models}
\label{rel.mod.}



We now define translations between AZDFSs and DEESs and show that they commute, implying equivalence of the two computational models. 




\subsection{Translation of ASDRSs and AZDFSs into DEESs}




\bdl{D.tra.dfs.dps.}
With an ASDRS $\cal R$ and its corresponding AZDFS $\calF=\calF_\calR=(\calR,\zfami,\zcontr)$, we associate the DEES $\calC_{\calR}=\calC_{\calF}=(E_{\calF},\leq,\rhd,\leeqv)$, where
\bit
\item  $E_{\calF}=FAM(\calF)$, the set of all families  of $\calF$;   

\item  $\phi<\psi$ iff $\phi \zcontr \psi$;   

\item  $\alpha\leeqv\beta$ iff $\forall\phi\in \alpha\cup\beta \setminus \alpha\cap\beta$, $\exists P:t_\emp\doar s:FAM(P)\ssq \alpha\cap\beta$ and $P$ discards a canonical element of $\phi$ (see \Tr{P.on.ca.for.});
 

\item  $\alpha\rhd \phi$ iff $\exists P:t_\emp\doar s:FAM(P)\ssq \alpha$ and $P$ discards a canonical element of~$\phi$.
\eit
\ed


 
We need to check that $\calC_\calF$ in the above definition is indeed a DEES. We need a number of technical lemmas to achieve this.


\bll{L.ines.sta.dis.}
Let $Q:t\doar s$,  $v\subt t$, $Q'\in\stav{Q}$,  and let $v$ be $Q$-inessential, in an ASDRS. Then $Q'$ discards $v$.

\bproof
Since $v$ is $Q$-inessential, $v/Q=\emp$ and $v$ is $Q$-unneeded. Since $Q'$ is $Q$-needed, it is external to $v$ by \Lr{L.era.and.ess.im.ne.}.(4), and $v/Q'=v/Q=\emp$, i.e., $Q'$ discards $v$.
\eproof
\el



\bll{L.sta.rem.sta.}
Let $Q:t\doar s$ be standard and let $t\red{u}o$, in an ASDRS. Then $Q/u$ is standard.

\bproof
By induction on the length of $Q$. Let $Q'=Q/u$. Suppose on the contrary that $Q'$ is not standard and let $w'$ be the last $Q'$-unneeded step in $Q'$, say $Q'=Q'_1 +w'+Q'_2$, and let $Q=Q_1+w+Q_2$, where $w'=w/u'$ and $u'=u/Q_1$ (see the figure). 
\begin{diagram}[height=1.5em,width=1.5em]
 t      & \rOnto^{Q_1} & {} & \rTo^w   & {} &  \rOnto^{Q_2}   & {}   \\
 \dTo^u &         &  \dTo^{u'} &   &     \dTo   &   & \dTo \\
 o     & \rOnto_{Q'_1} & {} & \rTo_{w'}   & {} &  \rOnto_{Q'_2} & {} \\
\end{diagram}
%
By \Lr{L.era.and.ess.im.ne.}.(2), $w'$ is not the last step of $Q'$. So let $Q_2=v+Q_3$ and $Q'_2=v'+Q'_3$. By the choice of $w'$, $v'$ is $Q'$-needed, and $w'$ does not create $v'$ by \Lr{L.era.and.ess.im.ne.}.(3). Since $w+Q_2$ is self-needed and $w'+Q'_2$ is not, $u'\not=\emp$. Hence, by [stability], $w$ does not create $v$. Thus $w'$ and $v'$, as well as $w$ and $v$, can be permuted in $w'+v'+Q'_3$ and $w+v+Q_3$, respectively, yielding $v'^*+w'^*+Q'_3$ and $v^*+w^*+Q_3$ (see the figure below). Then by \Lr{L.era.and.ess.im.ne.}.(4), $w^*+Q_3$ is self-needed and $w'^*+Q'_3$ is not self-needed (and therefore $u''=u'/v^*\not=\emp$), contradicting the induction assumption.
\begin{diagram}[height=1.5em,width=1.5em]
 t      & \rOnto^{Q_1} &  {}     & \rTo^{v^*} & {} & \rTo^{w^*}   & {} &  \rOnto^{Q_3}   & {}   \\
 \dTo^u &         &   \dTo^{u'} &         &  \dTo^{u''} &   &     \dTo   &   & \dTo \\
o     & \rOnto_{Q'_1} & {}   & \rTo_{v'^*} & {} & \rTo_{w'^*}   & {} &  \rOnto_{Q'_3}   & {} \\
\end{diagram}
\eproof
\el



\bll{C.sta.dis.}
Let $Q:t\doar s$, $P:t\doar o$, $v\subt o$, $Q'\in\stav{Q}$, and let $Pv$ be $Q$-inessential, in an ASDRS. Then $Q'$ discards $Pv$.

\bproof
By \Lr{L.sta.rem.sta.}, $Q'/P\in\stav{Q/P}$. And since $v$ is $Q/P$-inessential, $Q'/P$ discards $v$ by \Lr{L.ines.sta.dis.}.
\eproof
\el


\bll{L.crea.dis.drs.}
Let $P:t\doar s$, $Q:t\dored{Q'}o\red{u}e\red{v}s'$, let $Q'u$ be $P$-inessential, and let $u$ create $v$, in an ASDRS. Then $(Q'+u)v$ is $P$-inessential too.

\bproof
Let $P'=ST(P)$, $P''=P'/Q'$, and $P^*=P''/u$. By \Lr{C.sta.dis.}, $P''$ discards $u$. So let $w$ be the step of $P''$ that discards a residual $u'$ of $u$, and let $v'$ be the corresponding residual of $v$ along $P^*$, see the figure. If $v'\not=\emp$, then $v'/(w/u')=\emp$ by [stability] (since $u'/w=\emp)$). So, in any case, $v/P^*=\emp$. By the Stability Lemma, $P^*$ is external to $v$ (since $P''$ is external to $u$). Hence $P^*$ discards $v$, i.e. $v$ is $P$-inessential. 
\begin{diagram}[height=1.5em,width=1.5em]
  {}           &     &      & \rOnto^{P'} &    &       &    {}   \\
 \dOnto^{Q'}   &           &       &         &    &     &  \dOnto   \\
 {}     & \rOnto     & {}   & \rTo^{w\in P''}   & {} & \rOnto & {}   \\
 \dTo^u &          &  \dTo^{u'} &   &     \dOnto_{\emp}   &   & \dOnto_{\emp} \\
 {}   & \rOnto   & {} & \rTo^{w' \in P^*}   & {} & \rOnto  &  {}   \\
 \dTo^v &          &  \dTo^{v'} &   &     \dOnto_{\emp}   &   & \dOnto_{\emp} \\
 {}    & \rOnto   & {} & \rOnto   & {} &  \rOnto   & {}    \\
\end{diagram}
\eproof
\el


\bll{L.dis.can.al.}
Let $P:t_\emp\doar s$, $\phi$ be a family in an AZDFS $\calF$, let $Qv,Q'v'\in\phi$, and let $Qv$ be canonical. If $Qv$ is $P$-inessential, then so is $Q'v'$. Further, if $Q'\lleq P$, then the converse is also true. 

\bproof
By the Affine Extraction Theorem, there is $Q''$ such that $Q'\leeqv Q+Q''$ and $v'=v/Q''$. If $Qv$ is $P$-inessential, then $ST(P)/Q$ discards $v$ by \Lr{C.sta.dis.}, and $ST(P)/Q'$ discards $v'$ by the Cube Lemma. Conversely, if $Q'\lleq P$, then $Q''/(P/Q)=\emp$, and $v'/(P/Q')=v/(P/Q)=\emp$ again by the Cube Lemma, thus $Qv$ is $P$-inessential.
\eproof
\el


\bll{L.sam.fam.er.}
Let $t_\emp\dored{Q}s\red{u}s'$, let $t_\emp\dored{P}o\red{v}o'$, and let $Qu\zfami Pv$, in an AZDFS $\calF$. Then $v/((Q+u)/P)=\emp$.

\bproof
If $v'=v/(Q/P)=\emp$, then we are done. Otherwise, by the Affine Extraction Theorem, there are $Nw\zfami Qu$ and reductions $N'$ and $N''$ such that $Q\leeqv N+N'$, $P\leeqv N+N''$, $u=w/N'$ and $v=w/N''$. Further, $N'+P/Q\leeqv N''+Q/P$, and by the Cube Lemma, $v'=w/(N'+P/Q)$. But $u$ is the only $N'$-residual of $w$, thus $v'=u/(P/Q)$, implying $v/((Q+u)/P)=\emp$.
\eproof
\el




\bll{L.reor.fam.}
Let $P\in\stan$, $FAM(P)=F_1\cup F_2$, $F_1\cap F_2=\emp$ and $\forall \phi\in F_2, \forall \psi\in F_1:\phi\not\contr \psi$, in an AZDFS $\calF$. Then $\exists Q\in\stav{P} :Q=Q_1+Q_2\wedge FAM(Q_i)=F_i$, $=1,2$.

\bproof
Let $u$ be the latest step in $P$ such that $\phi=Fam(u)\in F_2$ and it has a next step $v$ with $\psi=Fam(v)\in F_1$. Then $\phi\not\contr \psi$ by the hypothesis, and $u$ does not create $v$ by [creation]. Hence $u$ and $v$ can be permuted, yielding another standard reduction by \Lr{L.era.and.ess.im.ne.}.(4). The resulting reduction can be transformed similarly until all steps in $F_2$ are pushed to the end. The transformation terminates as it does not change the length of the reduction.
\eproof
\el



\btl{T.dfs.dees.tr.}
For any AZDFS $\calF$, ${\cal C_F}$ is a DEES.

\bproof
We need to show that ${\cal C_F}=(E_{\calF},\contre,\rhd,\leeqv)$ satisfies the erasure axioms [E0] -- [E4], and that $\leeqv=\eleeqv$.
\bds
\item[{[\rm{E0}]:}] Immediate from Definitions~\ref{D.red.need.ess.} and \ref{D.tra.dfs.dps.}.

\item[{[\rm{E1}]:}]  Again from Definitions~\ref{D.red.need.ess.} and \ref{D.tra.dfs.dps.}. 

\item[{[\rm{E2}]:}] Let $\alpha\era \phi$, $\alpha\era \phi'$, and let $\alpha-\phi\in\fcE$. Then there are $P$ and $P'$ such that $FAM(P), FAM(P')\ssq\alpha$, a canonical element $Qv$ of $\phi$ is $P$-inessential, and a canonical element $Q'v'$ of $\phi'$ is $P'$-inessential. Let $P^*=P\sqcup P'$. Then $FAM(P^*)\ssq\alpha$ and both $Qv$ and $Q'v'$ are $P^*$-inessential. By \Lr{L.dis.can.al.}, all members of $\phi$ and $\phi'$ are $P^*$-inessential. Since $ST(P^*)$ is $P^*$-essential, it does not contract members of $\phi$ and $\phi'$. Hence $FAM(ST(P^*))\ssq\alpha - \phi'$, and $\alpha-\phi'\era \phi$ by \Dr{D.tra.dfs.dps.}.

\item[{[\rm{E3}]:}] Let $\alpha\era\phi$ and $\phi\contr\phi'$. It is enough to consider the case when $\not\exists \phi'': \phi\contr\phi''\contr\phi'$. By \Lr{L.reor.fam.} and the Affine Extraction Theorem, there is a canonical $P'v'\in\phi'$ such that $P'=P+v$, $v$ creates $v'$, and $Pv\in\phi$. Further, by \Dr{D.tra.dfs.dps.},  $\exists Q: FAM(Q)\ssq\alpha$ which discards a canonical element of $\phi$. Hence, by Lemmas~\ref{L.dis.can.al.}, \ref{L.crea.dis.drs.} and~\ref{C.sta.dis.}, $ST(Q)$ discards $P'v'$, i.e., 
$\alpha\era\phi'$.


\item[{[\rm{E4}]:}] Let $\alpha\cup \ocon{\phi} \era \phi$. By \Dr{D.tra.dfs.dps.}, there is a $Q$ such that $FAM(Q)\ssq \alpha\cup \ocon{\phi}$ and $Q$ discards a canonical element $Pv$ of $\phi$. By \Pr{P.leqv.sam.se.es.fa.} and \Lr{C.sta.dis.}, $Q$ can be chosen standard. Let $F_2=FAM(Q)\cap (\ocon{\phi}\setminus\alpha)$ and $F_1=FAM(Q)\setminus F_2$. Since $\alpha\in\fcE$, $\forall \phi\in F_2, \psi\in F_1:\phi\not\contr \psi$. Hence, by \Lr{L.reor.fam.}, $\exists Q'\in\stav{Q} :Q'=Q_1+Q_2\wedge FAM(Q_i)=F_i$. By \Lr{C.sta.dis.}, $Q'$ discards $Pv$, and by \Lr{L.sam.fam.er.}, $Q'/P=Q_1/P$, since $\ocon{\phi}= FAM(P)$. Hence $Q_1$  discards $Pv$ and $FAM(Q_1)\ssq \alpha$, i.e., $\alpha\era \phi$.
\eds

It remains to show that $\leeqv=\eleeqv$. Indeed, by \Dr{D.tra.dfs.dps.}, $\alpha\leeqv\beta$ iff $\alpha\cap\beta\era\alpha\cup\beta\setminus\alpha\cap\beta$, and by \Pr{C.char.sea.eq.}, the latter holds iff $\alpha\eleeqv\beta$.
\eproof
\et

 

\subsection{Translation of DEESs into ASDRSs and AZDFSs}



The following translation of DEESs into ASDRSs uses a techniques resembling the representation of events in a PES as prime intervals of its configuration domain, used for construction of PESs from stable families of configurations in~\cite{[Win89]}.


\bdl{D.ps.rs.tra.}
With a DEES $\calC=(E,\leq,\era,\leeqv)$ we associate an ASDRS $\calR_\calC$ as follows:
\bit
\item  The terms of $\calR_\calC$ are
L\'evy-equivalence classes $\lclasa,\lclasb,\ldots$ of
configurations of $\cal C$;

\item  The reduction relation of $\calR_\calC$ consists of sets of pairs  $u=(\lclasa,e)$, where $\alpha,\alpha+e\in \fcE$ and $\alpha\not\leeqv\alpha+e$. Pairs $u=(\lclasa,e)$ such that $\alpha\leeqv\alpha+e$ are identified with the empty redex $\emp=(\lclasa,\emp)$ in $\lclasa$. A non-empty redex $(\lclasa,e)$ will also be called an \emph{$e$-redex}.

\item  The residual relation is defined as follows: if
$u=(\lclasa,e)$ and $v=(\lclasa,e')$, then
$u/v=(\lclas{\alpha+e'},e)$. (Thus $u/v=\emptyset$ iff
$\alpha+e'\leeqv\alpha+e'+e$.)
\eit
\ed


Next we show that the definition above is correct.

 

\bt
Let $\calC=(E,\leq,\era,\leeqv)$ be a DEES. Then ${\calR_\calC}$ is an ASDRS. 

\bproof
For any step $v:\lclasa\red{(\lclasa,e)}\lclas{\alpha+e}$ in
$R_\calC$, and any redex $u=(\lclasa,e')$ in $\lclasa$, $u/v$ is either a (non-empty) redex in $\lclas{\alpha+e}$, or $u/v=\emp$. Also, for any other redex $w=(\lclasa,e'')$ in $\lclasa$ such that $w/v\not=\emp$, $w/v=(\lclas{\alpha+e},e'')\not=(\lclas{\alpha+e},e')=u/v$, i.e., no redex in $\lclas{\alpha+e}$ is a residual of more than one redex in $\lclasa$. Further, $v/v=(\lclas{\alpha+e},e)=\emp$. So to show that $R_\calC$ is an ASDRS, it remains to show [FD], [weak acyclicity], and [stability].  

\bds
\item[{[\rm{FD}]}] let $U$ be a set of redexes in $\lclasa$, let $e_0,\ldots,e_{l-1}$ be an enumeration of $U$, and let $\alpha_n=\alpha+e_0+\ldots+e_{n-1}$ $(0\leq n\leq l)$. Then a complete development of $U$ has a form $P:\lclas{\alpha_0}\red{(\lclas{\alpha_0},e_0)}\lclas{\alpha_1}\red{(\lclas{\alpha_1},e_1)}\ldots\ar\lclas{\alpha_k}$, where for any $m=k,\ldots,l-1$, $(\lclas{\alpha_0},e_m)/P=\emp$, that is, $\lclas{\alpha_k}=\lclas{\alpha_k+e_m}$. We show by induction on $j=l-k$ that $\alpha_k\leeqv\alpha_k+e_k+\ldots +e_{l-1}$. The case $j=1$ (i.e., $\alpha_k\leeqv\alpha_k+e_k$) is immediate.  By the induction assumption, $\alpha_k\leeqv \alpha_{l-2}\leeqv \alpha_{l-2}+e_{l-2}\leeqv \alpha_{l-2}+e_{l-1}$. By [P2], $\alpha_{l-2}+e_{l-2}+e_{l-1}\leeqv\alpha_{l-2}+e_{l-1}$. Hence, $\alpha_k\leeqv\alpha_{l-2}+e_{l-2}+e_{l-1}=\alpha_l$. Thus every complete development of $U$ ends at $\lclas{\alpha_k}=\lclas{\alpha_l}$. Further, for any $u=(\lclasa, e)$, $u/P=(\lclas{\alpha_k},e)$, i.e., $u/U$ does not depend on the particular complete development of $U$, hence [FD] holds.

\item[{[\rm{weak acyclicity}]}] Let $u=(\lclasa,e)$, $v=(\lclasa,e')$, $e\not=e'$, and suppose $u/v=v/u=\emp$. That is, $\alpha+e+e'\leeqv\alpha+e\leeqv \alpha+e'$. Then, by [P1], $\alpha+e\leeqv\alpha+e'\leeqv\alpha$, i.e, $u=v=\emp$.


\item[{[\rm{stability}]}] Suppose on the contrary that $R_\calC$ is not stable. Then there are $u\not=v$, $w$, $w'$ and $w''$ such that $w$ and $w'$ are created by $u$ and $v$ respectively,  and $w''=w/v'=w'/u'\not=\emp$, where $u'=u/v$ and $v'=v/u$. That is, there are  $u=(\lclasa,e)$, $v=(\lclasa,e')$, $w=(\lclas{\alpha+e},e'')$, $w'=(\lclas{\alpha+e'},e'')$, and $w''=(\lclas{\alpha+e+e'},e'')$ such that $\lclasa$, $\lclas{\alpha+e}$ and $\lclas{\alpha+e+e''}$ are different; so are $\lclasa$, $\lclas{\alpha+e'}$ and $\lclas{\alpha+e'+e''}$; and $\lclas{\alpha+e+e'}\not=\lclas{\alpha+e+e'+e''}$ (see the diagram). 
Further, $(\lclasa,e'')$ is not a redex since $w$ is a created redex. Hence either $\alpha+e''\not\in \fcC$, or $\alpha+e''\in \fcC$
and  $\alpha\leeqv\alpha+e''$; but the latter would imply by [P2] that $\alpha+e+e''\leeqv \alpha+e$, contradicting the fact that $w$ is a non-empty redex. Thus $\alpha+e+e''$ and $\alpha+e'+e''$ are both configurations, but their intersection $\alpha+e''$ is not  -- a contradiction, since the intersection of left-closed subsets remains left-closed.
\begin{diagram}[height=1.5em,width=1.5em]
\lclasa & \rTo^u   &\lclas{\alpha+e}  & \rTo^w  & \lclas{\alpha+e+e''} \\
 \dTo^v &              &  \dTo_{v'}  &                 & \dTo      \\
\lclas{\alpha+e'} & \rTo_{u'} & \lclas{\alpha+e+e'} &                  &    \\
\dTo^{w'}  &            &                &  \rdOnto^{w''}  &   \\
\lclas{\alpha+e'+e''} & \rTo  &            &       &\lclas{\alpha+e+e'+e''} \\
\end{diagram}
\eds
The theorem is now proved.
\eproof
\et



  
Clearly, an initial reduction in an ASDRS $\calR_\calC$ can be represented as a left-closed enumeration $e_1,\ldots,e_k$ of a configuration $\alpha$ where no event $e_i$ in the sequence is \emph{vacuous}, i.e., $\forall i:\{e_1,\ldots,e_{i-1}\}\not\era e_i$; the event $e_i$ represents the \emph{non-empty} redex $(\{e_1,\ldots,e_{i-1}\},e_i)$. We call such a sequence also an \emph{initial reduction} or an \emph{$\alpha$-reduction} in the DEES $\calC$, written $\rs{\alpha}$. Thus we have the following lemma:



\bll{L.red.dp.df.}
Let $\calC$ be a DEES, and let $\calR_\calC$ be its corresponding ASDRS. Then there is a $1-1$ correspondence between initial reductions in $\calC$ and~$\calR_\calC$.
\el


Note that, unlike PESs, not every configuration in a DEES has a reduction. For example, consider the DEES consisting of four events $\{e_1, e_2, e'_1, e'_2\}$, ordered as follows: $e_1 < e'_1$ and $e_2 < e'_2$, and let $\era$ be given by: $\alpha\era e'_1$ iff $e_2 \in \alpha$, and $\alpha\era e'_2$ iff $e_1 \in \alpha$. Then $\{e_1, e_2, e'_1, e'_2\}$ is a configuration, but any of its left-closed enumerations, such as $e_1, e_2, e'_1, e'_2$, ends either with $e'_1$ or with $e'_2$, and we have $\{e_1,e_2,e'_2\}\era e'_1$ and $\{e_1,e_2,e'_1\}\era e'_2$. This is not surprising as the vacuous events in left-closed sequences correspond to empty reductions in the corresponding ASDRS, performed in the `garbage' (erased redexes). However, we have the following lemma:



\bll{L.se.red.}
Let $\alpha\in \fcE$, in a DEES. Then any left-closed enumeration of $\sea$ is a reduction.

\bproof
Let $e_0,\ldots, e_n$ be a left-closed enumeration of $\sea$. If there was an $i$ such that $e_0,\ldots, e_{i-1}\rhd e_i$, then $\alpha\rhd e_i$ by [E1], contradicting $e_i\in \sea$.
\eproof
\el

 


\bdl{D.ps.fs.tra.}
With a DEES $\calC=(E,\leq,\era,\leeqv)$, we associate a DFS ${\calF_\calC}=(\calR_\calC, \cfami,\ccontr)$ as follows:
\bit
\item $\calR_\calC$ is the DRSs defined in \Dr{D.ps.rs.tra.}.

\item $\forall e\in E$, we define the $\cfami$-family $\phi_e$ corresponding to $e$, or the \emph{$e$-family}, as the set of all $e$-redexes $(\rs{\alpha}, e)$. That is,  $(\rs{\alpha},e)\cfami (\rs{\beta},e')$ iff $e=e'$.

\item Define $\ccontr$ by: $\phi_e\ccontr\phi_{e'}$ iff $e<e'$.
\eit
\ed




\btl{T.ps.dr.fs.zig.}
Let $\calC=(E,\leq,\era,\leeqv)$ be a DEES, let ${\calF_\calC}=({\calR_\calC},\cfami,\ccontr)$, and let ${\calF_{\calR_\calC}}=({\calR_\calC},\zfami,\zcontr)$. Then $\calF_\calC=\calF_{\calR_\calC}$, hence $\calF_\calC$ is an AZDFS.  

\bproof
We need to show that (a) $\zfami=\cfami$ and (b) $\zcontr=\ccontr$.
\ben
\item[(a)] By \Dr{D.ps.rs.tra.}, $(\rs{\alpha},e)\zfami (\rs{\beta},e')\Rightarrow e=e'$, implying $\zfami\ssq\cfami$. For the converse, consider two redexes $(\rs{\alpha},e)\cfami (\rs{\beta},e)$. Then $(\rs{\alpha\cap\beta},e)$ is also a redex since $\alpha\cap\beta+e=\alpha+e\cap\beta+e\in\fcE$, and $(\rs{\alpha},e)$ and $(\rs{\beta},e)$ are its residuals. (Note that $(\lclas{\alpha\cap\beta},e)\not=\emp$ since $(\lclas{\alpha\cap\beta},e)=\emp \Rightarrow (\lclasa,e)=\emp$ by [P2].)  Hence $(\rs{\alpha},e)\zfami (\rs{\beta},e)$.

\item[(b)] In order to show that $\phi_e\ccontr\phi_{e'} \Leftrightarrow \phi_e\zcontr\phi_{e'}$, we need to show that $e<e'$ iff $e\in\rs{\gamma}$ for any $(\rs{\gamma}, e')\in \phi_{e'}$ (by (a), $\phi_e,\phi_{e'}$ are families both w.r.t. $\cfami$ and $\zfami$). Sufficiency is immediate since $\gamma+e'$ is left closed. For the converse, we have from \Tr{P.on.ca.for.} that $(\rs{\ocon{e'}},e')$ is a canonical element of $\phi_{e'}$ (when $\phi_{e'}$ is considered as a $\zfami$-family), hence $e<e'$.
\een
\eproof
\et





\subsection{Equivalence of the transition and event models}


  
We now establish an equivalence between DEESs and AZDFSs, implying together with the results of previous sections equivalence of the considered four transition and event models -- ASDRSs, AZDFSs, DEESs and DPESs.


Let $\calR$ be a DRS. Let us define the \emph{reduction tree} of $\calR$ to be a tree whose nodes are labelled with terms in $\calR$, whose root is labelled with $t_\emptyset$, the initial term of $\calR$, and whose arcs correspond to redexes in $\calR$. Thus sons of a node are target terms of redexes whose source term is the label of that node. (Reduction trees are considered up to the order of arcs coming out of a node: the order in which the arcs are drown is irrelevant.) Note that different nodes can be labelled with the same term, so even if $\calR$ has cycles, its reduction tree is a tree. Thus the branches of the reduction tree of $\calR$ are in $1-1$ correspondence with initial reductions in $\calR$. We call two such trees \emph{isomorphic} if the trees obtained by removing all labels are identical. Hence, we can define two DRSs to be \emph{isomorphic} if there is an isomorphism between their reduction trees preserving the residual relation. An isomorphism between two DFSs must further preserve the family and contribution relations.



 
\bll{L.dpred.drred.}
Let $\calF$ be an AZDFS and let $\calC_\calF$ be its corresponding DEES.
\ben
\item[(1)] For any initial reduction $\rs{\alpha}=e_0, e_1,\ldots,e_n$ in $\calC_\calF$ there is a unique initial reduction $g(\rs{\alpha})=P:t_\emp=t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{n-1}}t_n$ in $\calF$ such that $Fam(P_iu_i)=e_i$, where $P_i:t_\emp=t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{i-1}}t_i$. (Thus $FAM(P)=\alpha$.)

\item[(2)] Let $P:t_\emp=t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{n-1}}t_n$ in $\calF$, and let $e_i=\phi_i=Fam(P_iu_i)$, where $P_i:t_\emp=t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{i-1}}t_i$. Then $f(P)=e_0, e_1,\ldots,e_n$ is a reduction in~$\calC_\calF$.

\item[(3)] the translation functions $g$ and $f$ between reductions in $\calF$ and $\calC_\calF$ commute: for any initial reduction $P$ in $\calF$, $g(f(P))=P$, and for any reduction $\rs{\alpha}$ in $\calC_\calF$, $f(g(\rs{\alpha}))=\rs{\alpha}$.
\een

\bproof
\ben
\item[(1)] By definition of a reduction in a DEES, $e_0, e_1,\ldots,e_n$ is left-closed, and $\{e_0,\ldots,e_{j-1}\}\not\era e_j$ for any $j=0,\ldots,n$. Take for $u_0$ the redex in $t_\emp$ such that $Fam(\emp u_0)=e_0$; existence of such a redex is immediate from the definition of $\calC_\calF$, and uniqueness follows from [initial]. Suppose $u_1,\ldots,u_{i-1}$ are already defined so that $Fam(P_ku_k)=e_k$ for all $1\leq k < i$. We need to show that $\exists u_i\in t_i$ such that $Fam(P_iu_i)=e_i$; uniqueness of such a redex follows from the separability of $\calF$ (see \Tr{T.lin.dr.sta.df.}) and from the fact that in separable AZDFSs, a term may contain at most one redex of a given family (see Lemma~6.1 in~\cite{[ldrs]}, or Lemma~5.2 in~\cite{[acoi-rep]}). Let $N_iv_i$ be a canonical element of $e_i$ which exists by the Affine Extraction Theorem. By the same theorem, $N_i$ contracts exactly one redex in every contributor family of $e_i$ (and does not contract any other redex). Thus, by [contribution], $FAM(N_i)\ssq FAM(P_i)$, and $N_i\lleq P_i$ by \Pr{P.leqv.sam.se.es.fa.}. Now we can take $u_i=v_i/(P_i/N_i)$. If on the contrary $u_i=\emp$, then $P_i$ would discard $N_iv_i$ (since $P_i/N_i$ is external to $v_i$ as $Fam(N_iv_i)\not\in FAM(P_i)$), and we would have by \Dr{D.tra.dfs.dps.} that $\{e_0,\ldots,e_{i-1}\}\era e_i$, contradicting the assumption. Thus a reduction $P$ as above exists, and is unique.

\item[(2)] We need to show that $f(P)=e_0, e_1,\ldots,e_n$ is left-closed and does not contain vacuous events (by \Dr{D.tra.dfs.dps.}, $\phi_i=e_i$ are events in $\calC_\calF$). By [contribution], $P_i$ contracts at least one redex in every contributor family of $\phi_i$, hence $f(P)$ is left-closed. If on the contrary say $\phi_j$ is vacuous, i.e., $\{\phi_0,\ldots,\phi_{j-1}\}\era \phi_j$, then by \Dr{D.tra.dfs.dps.} there is an initial reduction $Q$ such that $FAM(Q)\ssq \{\phi_0,\ldots,\phi_{j-1}\}$ and $Q$ discards a canonical element $N_jv_j$ of $\phi_j$. By \Pr{P.leqv.sam.se.es.fa.}, $N_j,Q\lleq P_j$, and by \Dr{D.red.need.ess.}, $P_j$ erases $N_jv_j$, i.e., $v_j/(P_j/N_j)=\emp$. Hence $u_j/((N_j+v_j)/P_j)=u_j/\emp=u_j$, contradicting \Lr{L.sam.fam.er.} (since $N_jv_j\zfami P_ju_j$).
\item[(3)] Immediate from the constructions in (1) and (2).
\een
\eproof
\el





\btl{T.equi.four.}
{\bf (Equivalence of AZDFSs and DEESs)}
\ben

\item[(1)] For any DEES $\calC$, $\calC$ and $\calC_{\calF_\calC}$ are isomorphic.

\item[(2)] For any AZDFS $\calF$, $\calF$ and $\calF_{\calC_\calF}$ are isomorphic.
\een

\bproof
\ben
\item[(1)] Let $\calC=(E,\leq,\era,\leeqv)$ and $\calC'=\calC_{\calF_\calC} =(E',\leq',\era',\leeqv')$. By Definitions~\ref{D.ps.fs.tra.} and~\ref{D.tra.dfs.dps.}, $E'=\{\phi_e\vert e\in E\}$, where $\phi_e$ is the $e$-family of $\calF_\calC$. We show that $f:e\mapsto \phi_e$ is an isomorphism between $\calC$ and $\calC'$.  Since $f$ clearly an isomorphism between $E$ and $E'$, and since $\calC'$ is a DEES by Theorems~\ref{T.dfs.dees.tr.} and \ref{T.ps.dr.fs.zig.}, we need to show that (a) $e\leq e'$ iff $\phi_e\leq'\phi_{e'}$; and (b) $\alpha\leeqv \beta$ iff $\phi_\alpha \leeqv' \phi_\beta$, where $\phi_\alpha=\{\phi_e\vert e\in\alpha\}$ and $\phi_\beta=\{\phi_e\vert e\in\beta\}$.
\ben
\item[(a)] Immediate from Definitions~\ref{D.ps.fs.tra.} and~\ref{D.tra.dfs.dps.}. 

\item[(b)] By \Dr{D.tra.dfs.dps.}, $\phi_\alpha \leeqv' \phi_\beta$ iff $\forall e\in \alpha\cup\beta\setminus\alpha\cap\beta$, there is a reduction $\rs{\gamma}$  in ${\calF_\calC}$ such that $FAM(\rs{\gamma})\ssq \phi_\alpha\cap\phi_\beta$ and $\rs{\gamma}$ discards a canonical element $\rs{\ocon{e}}e$ of $\phi_e$ (see \Tr{P.on.ca.for.}). By Definitions~\ref{D.red.need.ess.} and \ref{D.ps.rs.tra.}, the latter means that $e\not\in\gamma,\,\gamma\ssq\alpha\cap\beta$, and  $\gamma\cup\ocon{e}\leeqv \gamma\cup\con{e}$, thus by \Dr{D.era.vi.per.eq.}, and Lemmas~\ref{L.se.red.} and \ref{L.alp.eq.sel.al.} we need to prove that $\alpha\leeqv\beta$ iff 
$\exists \,\,standard\,\, \gamma:\gamma\ssq\alpha\cap\beta\wedge \gamma\era \alpha\cup\beta\setminus\alpha\cap\beta$. But this is immediate from \Pr{C.char.sea.eq.} (since $\leeqv=\eleeqv$) and \Lr{L.alp.eq.sel.al.}.
\een

\item[(2)] By \Tr{T.ps.dr.fs.zig.} and \Tr{T.dfs.dees.tr.}, $\calF_{\calC_\calF}$ is an AZDFS, hence it is enough to show that the underlying ASDRSs $\calR$ and $\calR_{\calC_\calF}$ of $\calF$ and $\calF_{\calC_\calF}$ are isomorphic. This follows immediately from Lemmas~\ref{L.dpred.drred.} and~\ref{L.red.dp.df.}.
\een
\eproof
\et


 

\section{L\'evy's Configuration Domains}
\label{latt.str.}


Next we define L\'evy's configuration domains in DEESs and show that they are isomorphic to  L\'evy's reduction spaces in corresponding ASDRSs.


\bdl{D.perm.latt.}
\ben
\item[(1)] Let $\calC$ be a DEES. Then \emph{L\'evy's configuration domain} $\efcC=(\pfcC,\lleq)$, where $\pfcC=\fcC/_{\leeqv}=\{\lclasa \vert\alpha\in\fcC\}$ and $\lleq$ is a partial order defined by: $\lclasa\lleq\lclasb$ iff  $\exists \beta'\in\lclasb:\alpha\ssq\beta'$. 

\item[(2)] Let $\cal R$ be an ASDRS, and let $\fcR$ be the set of initial reductions in $\cal R$. Then \emph{L\'evy's reduction space} $\efcR=(\pfcR,\lleq)$, where $\pfcR=\fcR/_{\leeqv}=\{\lclas{P} \vert P\in\fcR\}$, and $\lclas{P}\lleq \lclas{Q}$ iff $P\lleq Q$. 
\een
\ed


Note that if $\lclasa\lleq\lclasb$, $\alpha\leeqv\alpha'$ and $\beta\leeqv\beta'$, then $\lclas{\alpha'}\lleq\lclas{\beta'}$, implying that \Dr{D.perm.latt.}.(1) is correct: Indeed, $\lclasa\lleq\lclasb$ iff $\exists \beta''\leeqv\beta:\,\alpha\ssq\beta''$, and by \Pr{C.char.sea.eq.} and [E1], $\alpha\leeqv\alpha'\Rightarrow \alpha\era (\alpha'\setminus\alpha)\Rightarrow \beta''\era (\alpha'\setminus\alpha)\Rightarrow \beta'\leeqv\beta\leeqv\beta''\leeqv\beta'' \cup (\alpha'\setminus\alpha)=\beta''\cup\alpha'$, thus $\lclas{\alpha'}\lleq\lclas{\beta'}$.


  
\bll{L.st.eq.st.}
Let $P$ be an initial reduction in an AZDFS $\calF$. Then, in the corresponding DEES $\calC_\calF$, $FAM(ST(P))=ST(FAM(P))$.

\bproof
First note that, by [contribution] and the definition of $\leq$ (\Dr{D.tra.dfs.dps.}), for any initial reduction $Q$, $FAM(Q)$ is indeed a configuration.
\ben
\item[($\ssq$)] Let $\phi\in FAM(ST(P))$. By \Pr{P.leqv.sam.se.es.fa.}, $\phi\in SFAM(P)$, i.e., there is $P'v'\in\phi$ that is contracted in $P$ and is $P$-needed, thus is $P$-essential. Let $P^*v^*$ be a canonical element of $\phi$. Then it is $P$-essential by \Lr{L.dis.can.al.}. For any initial reduction $Q$ with $FAM(Q)\ssq FAM(P)$, $Q\lleq P$ by \Pr{P.leqv.sam.se.es.fa.}, thus $P^*v^*$ is $Q$-essential too. Hence $Q$ does not discard $P^*v^*$, implying by \Dr{D.tra.dfs.dps.} that $FAM(P)\not\era\phi$, i.e., $\phi\in ST(FAM(P))$.

\item[($\supseteq$)] Let $\phi\in ST(FAM(P))$. Then $\phi\in FAM(P)$ and $FAM(P)\not\era\phi$, which  by \Dr{D.tra.dfs.dps.} means that there is no initial $Q$ with $FAM(Q)\ssq FAM(P)$ such that $Q$ discards a canonical element $P^*v^*$ of $\phi$. In particular, $ST(P)$ does not discard $P^*v^*$, and by Lemmas~\ref{L.dis.can.al.} and~\ref{L.era.and.ess.im.ne.}.(1), the redex $P'v'\in\phi$ contracted in $P$ is $P$-needed, i.e., $\phi\in SFAM(P)$; thus $\phi\in FAM(ST(P))$ by \Pr{P.leqv.sam.se.es.fa.}.
\een
\eproof
\el


\bll{L.leeq.leeq.}
Let $Q,Q'$ be initial reductions in an AZDFS $\calF$. Then $Q\leeqv Q'$ in $\calF$ iff $FAM(Q)\leeqv FAM(Q')$ in the corresponding DEES $\calC_\calF=(E_\calF,\leq,\era,\leeqv)$.

\bproof
\ben
\item[\suf] By \Dr{D.tra.dfs.dps.}, we need to show that $\forall\phi\in FAM(Q)\cup FAM(Q')\setminus FAM(Q)\cap FAM(Q')$, an initial reduction $P$ with $FAM(P)\ssq FAM(Q)\cap FAM(Q')$ discards a canonical element $Nv$ of $\phi$. Take $P=ST(Q)$. By \Pr{P.leqv.sam.se.es.fa.}, $FAM(P)\ssq FAM(Q)\cap FAM(Q')$. Let $Q^*v^*$ be an element of $\phi$ contracted in $Q$. Since by \Pr{P.leqv.sam.se.es.fa.} $\phi\not\in FAM(P)=SFAM(Q)$, $Q^*v^*$ is $Q$-unneeded, hence $Q$-inessential by \Lr{L.era.and.ess.im.ne.}.(1). Hence, by \Lr{C.sta.dis.}, $P$ discards $Q^*v^*$. By the Affine Extraction Theorem, $\exists N':N+N'\leeqv Q^*$ and $v^*=v/N'$. Since $Q^*\leq Q\leeqv P$, $N'/(P/N)=\emptyset$, hence $v/(P/N)=v^*/(P/Q^*)=\emp$ by the Cube Lemma. Since $\phi\not\in FAM(P)$, $P/N$ is external to $v$, thus $P$ discards~$Nv$. 

\item[\nec] By \Pr{C.sees.eq.leeq.}, $FAM(Q)\leeqv FAM(Q')$ implies that $ST(FAM(Q))=ST(FAM(Q'))$; hence, by \Lr{L.st.eq.st.}, $FAM(ST(Q))=FAM(ST(Q'))$, implying by \Pr{P.leqv.sam.se.es.fa.} that $Q\leeqv Q'$.
\een
\eproof
\el



\bll{Lred.fr.conf.}
Let $\calF$ be an AZDFS, let $e_0, e_1,\ldots,e_n$ be a left-closed enumeration of $\alpha\in\calL_{fin}(\calC_\calF)$, and let $e_{i_0},\ldots,e_{i_m}$ be obtained from $e_0, e_1,\ldots,e_n$ by eliminating all vacuous events, i.e., $e_j\in \{e_{i_0},\ldots,e_{i_m}\}$ iff $\{e_0, \ldots,e_{j-1}\}\not\era e_j$. Then $e_{i_0},\ldots,e_{i_m}$ is a reduction in $\calC_\calF$ and $\{e_{i_0},\ldots,e_{i_m}\}\leeqv \{e_0,\ldots,e_n\}$.

\bproof
If there were $l,k$ such that $e_l<e_{i_k}$ (hence $l<i_k$) and $l\not= i_0,\ldots,i_{k-1}$, then $\{e_0, \ldots,e_{l-1}\}\era e_l$, $\{e_0, \ldots,e_{i_k-1}\}\not\era e_{i_k}$, and by [E1], $\{e_0, \ldots,e_{i_k-1}\}\era e_l$, contradicting [E3]. Hence $e_{i_0},\ldots,e_{i_m}$ is left-closed. Since $\{e_0, \ldots,e_{i_k-1}\}\not\era e_{i_k}$, $\{e_{i_0},\ldots,e_{i_{k-1}}\}\not\era e_{i_k}$ by [E1], thus $e_{i_0},\ldots,e_{i_m}$ is a reduction in $\calC_\calF$.  Finally, $\{e_{i_0},\ldots,e_{i_m}\}\leeqv \{e_0,\ldots,e_n\}$ follows from \Pr{C.char.sea.eq.}.
\eproof
\el

 


\bpl{emb.ver.sinc.}
Let $P,Q$ be initial reductions in an ASDRS $\cal R$. Then $\lclas{P}\lleq \lclas{Q}$  iff $\lclas{FAM(P)}\lleq \lclas{FAM(Q)}$ in $\calC_\calR$.

\bproof
\ben
\item[\suf] By \Pr{P.leqv.sam.se.es.fa.}, $\lclas{P}\lleq \lclas{Q}$ iff $\exists Q'\leeqv Q: FAM(P)\ssq FAM(Q')$, which by \Dr{D.perm.latt.} holds iff $\lclas{FAM(P)}\lleq \lclas{FAM(Q')}$ in $\calC_\calR$. But $Q\leeqv Q'$ implies $FAM(P)\leeqv FAM(Q')$ in $\calC_\calR$ by \Lr{L.leeq.leeq.}, thus $\lclas{FAM(P)}\lleq \lclas{FAM(Q)}$ in $\calC_\calR$.

\item[\nec] By \Dr{D.perm.latt.}, $\exists\alpha:\alpha\leeqv FAM(Q)\wedge FAM(P)\ssq \alpha$; thus by \Lr{Lred.fr.conf.} $\exists\rs{\beta}: FAM(P)\ssq \beta\ssq\alpha \wedge \beta\leeqv\alpha$ (assuming that say $e_0, e_1,\ldots,e_n$ is an enumeration of $\alpha$ whose initial part is an enumeration of $FAM(P)$, we can take $e_{i_0},\ldots,e_{i_m}$ as in \Lr{Lred.fr.conf.} for $\rs{\beta}$). By \Lr{L.dpred.drred.}, there is a $Q'$ such that $FAM(Q')=\beta$ and $P$ is an initial part of $Q'$. By \Lr{L.leeq.leeq.}, $Q\leeqv Q'$, hence $P\lleq Q$, therefore $\lclas{P}\lleq \lclas{Q}$.
\een
\eproof
\ep





\btl{T.isom.drs.dps.}
Let $\cal R$ be an ASDRS and let $\calC=\calC_\calR$ be its corresponding DEES. Then $f:\lclas{P}\mapsto \lclas{FAM(P)}$ is the isomorphism between $\efcR$ and $\efcC$, with the inverse $f^{-1}: \lclasa\mapsto \lclas{\rs{\sea}}$. Moreover, reductions in $\lclas{P}$ and $\lclas{FAM(P)}$ are in one-to-one correspondence.

\bproof
By Lemmas~\ref{L.leeq.leeq.} and~\ref{L.se.red.} and \Pr{C.sees.eq.leeq.}, $f$ and $f^{-1}$ are well defined. The rest is immediate from \Lr{L.dpred.drred.} and \Pr{emb.ver.sinc.}.
\eproof
\et

A similar statement is valid when $\calC$ is an arbitrary DEES and 
$\calR=\calR_\calC$: We only need to replace $FAM(P)$ in the definition of $f$ with $EVN(P)$, where $EVN(P)$ is the set of events fired in $P$.




\section{Preservation of Neededness and Stability by the Translations}
\label{S.pres.need.}



This section develops a normalization-by-neededness theory for DEESs, and relates it with that in affine SDRSs, establishing relationship between concepts of stability intrinsic to the above particular models, and between neededness and stability in each model.  



In order to extend the theory of Relative Normalization~\cite{[rel-jlc],[rndrs]} from SDRSs to DEESs, we can restrict ourselves to ASDRSs of the form $\calR_\calC$, where $\calC$ is a DEES: by \Tr{T.isom.drs.dps.}, such ASDRSs contain an isomorphic copy of any ASDRS. 




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

\item[(2)] We call $\stab$ \emph{stable}\footnote{Our definition 
follows~\cite{[rel-jlc]} rather than~\cite{[rndrs]}; in the latter, 
the definition of stability of sets does not require closure under 
reduction, but a slightly weaker condition.} if: 
\ben
\item[$(a)$] $\stab$ is \emph{closed under reduction};  and  

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



All interesting sets of `finite results', such as of normal forms, head-normal
forms, weak-head-normal forms, etc. are stable~\cite{[ctrs]}. It has been shown in~\cite{[rndrs]} (a corollary of the so called Relative Normalization theorem) that, for any stable set $\stab$ of terms in an ASDRS $\cal R$ and any $\stab$-normalizable term $t\not\in\stab$, $t$ contains at least one $\stab$-needed redex, and repeated contraction of $\stab$-needed redexes is $\stab$-normalizing, which justifies the concept of stable sets.

  

Our translation of AZDFSs into DEESs suggests the following definition of relative neededness and stability in DEESs.



\bdl{D.sta.nee.con.}
Let $\stab'$ be a set of configurations in a DEES $\calC=(E,\leq,\era,\leeqv)$.
\ben
\item[(1)] We call $e\in E$ $\stab'$-\emph{needed}, written $NE_{\stab'}(e)$ if, for any $\alpha\in\stab'$, $e\in \alpha$, and call it $\stab'$-\emph{unneeded} otherwise.

\item[(2)] We call $\stab'$ \emph{stable} if:
\ben
\item[$(a)$] $\stab'$ is \emph{closed under inclusion}.

\item[$(b)$] $\stab'$ is \emph{closed under unneeded expansion}: \\
$\alpha +e\in\stab'\, \wedge \,\alpha\not\in\stab' \,\Rightarrow \,
NE_{\stab'}(e)$; and

\item[$(c)$] $\stab'$ is \emph{closed under permutation equivalence}.
\delete{: \\
$\alpha\in \stab'\,\wedge\,\beta\leeqv\alpha\,\Rightarrow \,\beta\in\stab'$.} 
\een
\een 
\ed


 
Note that the relative neededness concept makes sense already for PESs. 


The next theorem gives two equivalent definitions of stability in DEESs, more in the spirit of the definition stability in PESs~\cite{[Win89]}, and more convenient to generalize to the case of infinite configurations. 


\btl{T.stab.eq.}
Equivalent definitions of stability of sets of finite configurations in a DEES can be obtained from \Dr{D.sta.nee.con.} by replacing the condition $(b)$ with either of the following two conditions $(b')$ or $(b'')$:


\ben
\item[$(b')$] $\stab'$ is \emph{closed under intersection}.

\item[$(b'')$] $\stab'$ is \emph{has a unique $\ssq$-minimal element $\alpha_{\stab'}$}. 
\delete{: \\
$\exists\alpha_{\stab'}\in\stab':\,\beta \in\stab' \,\Rightarrow \,\alpha_{\stab'}\ssq\beta$.}
\een


\bproof
We show that $(i)$ $(b)\Rightarrow (b')$; $(ii)$ $(b')\Rightarrow (b'')$ and $(iii)$ $(b'')\Rightarrow (b)$.
\ben
\item[$(i)$] Let $\alpha,\beta\in\stab'$, and suppose on the contrary that $\alpha\cap\beta\not\in\stab'$. Further, let $e_1,\ldots,e_m,\ldots,e_n$ be a left-closed enumeration of $\alpha$ such that $e_1,\ldots,e_m$ is a left-closed enumeration of  $\alpha\cap\beta$ (such an enumeration exists since $\alpha\cap\beta$ is left-closed). Then there is $m\leq j< n$ such that $\{e_1,\ldots,e_j\}\not\in\stab'$ and $\{e_1,\ldots,e_{j+1}\}\in\stab'$. By $(b)$, $e_{j+1}$ is $\stab'$-needed, which is not possible since $e_{j+1}\not\in\beta\in\stab'$. 

\item[$(ii)$] If $\stab'$ does not have a unique $\ssq$-minimal element, then it has at least two different $\ssq$-minimal elements $\alpha$ and $\beta$ (i.e., $\not\exists\gamma\subset\alpha:\,\gamma\in \stab'$, and similarly for $\beta$). By $(b')$, $\alpha\cap\beta\in\stab'$. But $\alpha\cap\beta\subset\alpha$, contradicting the minimality of $\alpha$.


\item[$(iii)$] Let $\alpha, e$ be such that $\alpha\not\in\stab'\wedge \alpha+e\in\stab'$. By $(b'')$, this means that $\alpha_{\stab'}\not\subseteq\alpha \wedge \alpha_{\stab'}\subseteq\alpha+e$. Hence $e\in \alpha_{\stab'}$, and therefore $\forall \delta\in\stab':\,e \in \delta$ (since $\alpha_{\stab'}\subseteq \delta$ by $(b'')$).
\een
\eproof
\et





The proof of the following proposition is routine, therefore omitted.

\bp
Let $\stab'$ be a set of configurations, in a DEES $\calC$, closed under permutation equivalence, and let $\stab$ be the set of corresponding terms in the corresponding ASDRS $\calR_\calC$ (which are L\'evy-equivalence classes of configurations in $\calC$). 
Then $\stab'$ is stable in $\cal C$ iff $\stab$ is stable in $\calR_\calC$.
Furthe, if $\stab'$ is stable, an event $e$ is $\stab'$-needed in $\cal C$ iff 
any  $e$-redex is $\stab$-needed in $\calR_\calC$.
\ep



\excl{
\bll{L.sta.imp.sta.}
Let $\stab'$ be a set of configurations in a DEES $\cal C$ closed under permutation equivalence, and let $\stab$ be the set of corresponding terms in the corresponding SDRS $\calR_\calC$ (which are the endpoints of reductions corresponding to configurations in $\stab'$). Then $\stab'$ is stable in $\cal C$ iff $\stab$ is stable in $\calR_\calC$.

\bproof
\ben
\item[\suf] We need to verify that $\stab$ is closed (a) under parallel moves and (b) under unneeded expansion.
\ben
\item[(a)] Let $Q:\lclasa\red{e'_1}\lclas{\alpha+e'_1}\red{e'_2}\ldots\red{e'_k}\lclas{\alpha+e'_1+\ldots+e'_k}$ be an $\stab$-early reduction in $\calR_\calC$, and let 
$P:\lclasa\red{e_1}\ldots\red{e_n}\lclas{\alpha+e_1+\ldots+e_n}$ be $\stab$-normalizing. Then $P/Q$ ends with $\lclas{\alpha+e_1+\ldots+e'_k}$, which is in $\stab$ since $\alpha+e_1+\ldots+e'_k\in\stab'$ by closure of $\stab'$ under inclusion.

\item[(b)] Let $u=(\lclasa, e)$ be a step in $\calR_\calC$ entering $\stab$. Suppose on the contrary that $u$ is not $\stab$-needed in $\lclasa$. Then there is an $\stab$-normalizing reduction $\lclasa\red{e_1}\lclas{\alpha+e_1}\red{e_2}\ldots\red{e_n}\lclas{\alpha+e_1+\ldots+e_n}$ such that $e_i\not= e$. Then we have $\alpha+e, \alpha+e_1+\ldots+e_n \in\stab'$, but $\alpha+e\cap\alpha+e_1+\ldots+e_n =\alpha\not\in\stab'$, contradicting semi-closure of $\stab'$ under intersection (since $\alpha$ is $\stab$-early).
\een

\item[\nec] We only need to verify that $\stab'$ is closed (a) under inclusion and (b) under unneeded expansion, since $\stab'$ is closed under permutation equivalence by the hypothesis.
\ben
\item[(a)] Let $\alpha\in\stab'$ and let $\beta$ be an $\stab'$-early configuration. Further, let $\rs{\alpha}$ and $\rs{\beta}$ be any reductions corresponding to $\alpha$ and $\beta$, respectively (which exist by \Lr{L.se.red.}). Then the reduction $\rs{\alpha}/\rs{\beta}$ ends in the term $\lclas{\alpha\cup\beta}$, since $\rs{\alpha}$ ends in $\lclasa$ and $\rs{\beta}$ ends in $\lclasb$. By closure of $\stab$ under parallel moves, $\lclas{\alpha\cup\beta}\in\stab$ (since $\rs{\alpha}$ is $\stab$-early and $\rs{\beta}$ is $\stab$-normalizing), implying $\alpha\cup\beta\in\stab'$.

\item[(b)] Let $\alpha$ be $\stab$-early and let $\alpha+e\in\stab'$. Suppose on the contrary that $e$ is $\stab'$-unneeded. Then there is a $\delta\in\stab'$ such that $e\not\in\delta$. We can assume that no proper subset of $\delta$ is in $\stab'$.  Then the corresponding reduction $\rs{\delta}$ in $\calR_\calC$ is $\stab$-normalizing and $\rs{\delta}/\rs{\alpha}$ is external to $(\lclasa,e)$, implying that $(\lclasa,e)$ is $\stab$-unneeded, contradicting closure of $\stab$ under unneeded expansion.
\een
\een
\eproof 
\el

 

\bll{L.ne.ev.ne.red.}
Let $\stab'$ be a set of stable configurations in a DEES $\cal C$, and let $\stab$ be the set of corresponding terms in the corresponding SDRS $\calR_\calC$. 
Further, let $e\in E$, and let $(\lclasa,e)$ be a non-empty $\stab$-early $e$-redex in $\calR_\calC$. Then $e$ is $\stab'$-needed in $\cal C$ iff $(\lclasa,e)$ is $\stab$-needed in $\calR_\calC$. 

\bproof
\ben
\item[\suf] Let $(\lclasa,e)\not=\emp$ (thus $e\not\in\alpha$), and suppose on the contrary that there is a reduction $P:\lclasa\red{e_1}\lclas{\alpha+e_1}\red{e_2}\ldots\red{e_n}\lclas{\alpha+e_1+\ldots+e_n}$ in $\calR_\calC$ (not containing empty steps and not containing terms in $\stab$ except for $\lclas{\alpha+e_1+\ldots+e_n}$) that is external to $(\lclasa,e)$ and is $\stab$-normalizing. Then $e\not= e_i$ for all $i$, and $e\not\in \alpha+e_1+\ldots+e_n\in \stab'$, contradicting $\stab'$-neededness of~$e$.

\item[\nec] Let $(\lclasa,e)$ be $\stab$-needed, and suppose on the contrary that $e$ is not $\stab'$-needed. That is, there is a $\beta\in\stab'$ such that $e\not\in\beta$. Since $\alpha,\beta\in\fcC$ and $\alpha$ is $\stab'$-early,  $\alpha\cup\beta\in\stab'$ by the closure of $\stab'$ under inclusion, and $e\not\in\alpha\cup\beta$ ($e\not\in\alpha$ since $(\lclasa,e)\not=\emp$). Let $e_1,\ldots,e_n$ be an enumeration of $\alpha\setminus\beta$ such that, for any left-closed enumeration $e'_1,\ldots,e'_k$ of $\alpha$, $e'_1,\ldots,e'_k,e_1,\ldots,e_i$ is left-closed for any $i=1,\ldots,n$. Then, from the sequence $\lclasa\red{e_1}\lclas{\alpha+e_1}\red{e_2}\ldots\red{e_n}\lclas{\alpha+e_1+\ldots+e_n}$ we can construct an $\stab$-normalizing reduction (since $\lclas{\alpha+e_1+\ldots+e_n}=\lclas{\alpha\cup\beta}\in\stab$ as $\alpha\cup\beta\in\stab'$) by omitting empty steps. But the latter reduction does not contract $e$-redexes, contradicting $\stab$-neededness of~$(\lclasa,e)$.
\een
\eproof
\el


Thus, $\stab$-neededness of the $e$-family $\phi_e$ in $\calF_\calC$ can be defined soundly when $\stab$ is closed under parallel moves:  we can define $\phi_e$ to be $\stab$-needed iff an (or equivalently, every) $\stab$-early $e$-redex is $\stab$-needed.
}
 
We conclude this section with a theorem expressing the relationship between concepts of stability and neededness in DEESs, analogous to the Relative Normalization Theorem for ASDRSs~\cite{[rndrs]}:


\btl{T.min.el.}
Let $\stab'$ be a stable set of configurations in a DEES $\cal C$. Then a repeated execution of $\stab'$-needed events in any  configuration  $\alpha\not\in\stab'$, possibly interleaved by finite sequences of $\stab'$-unneeded steps, eventually yields a configuration in $\stab'$.

\bproof
Immediate from closure of $\stab'$ under inclusion (since $\stab'$ consists of finite configurations, hence there are only a finite number of $\stab'$-needed events).
\eproof
\et




 
\section{Relativized Information Domains}
\label{S.rel.in.dom.}




In this section, we introduce orderings on configurations relativized w.r.t. stable sets of results, in a DEES $\calC$, and show that they form finitary prime algebraic complete lattices. Unlike the previous sections, we will now allow for infinite configurations -- (countable) infinite left-closed sets of events in $\calC$. The set of finite and infinite configurations in $\calC$ will be denoted by $\cC$.


We start by some preliminary lattice theoretic definitions; we follow~\cite{[Win89]}.


\bdl{D.fpad.}
\bit
\item A \emph{complete lattice} is a partial order ${\cal L}=(L,\sqleq)$ which has least upper bounds (joins or suprema) $\sqcup X$ and greatest lower bounds (meets or infima) $\sqcap X$ of arbitrary subsets $X\ssq L$. We write $x\sqcup y$ and $x\sqcap y$ for the join and meet respectively of two elements $x,y\in L$.

\item A \emph{directed subset} of a partial order ${\cal L}$ is a subset $Y\ssq L$ with the property that for any finite set $X\ssq Y$ there is an element $y\in Y$ such that $\forall x\in X. x\sqleq y$.

\item A \emph{finite element} of a complete lattice is an element $z$ with the property that, for all directed subsets $Y$, if $z\sqleq \sqcup Y$, then there is some $y\in Y$ for which $z\sqleq y$.

\item A complete lattice ${\cal L}$ is \emph{algebraic} if for any element $d\in L$ the set $\{x\sqleq d\,\vert\,x\,\,is\,\,finite\}$ is directed and has least upper bound~$d$.

\item A \emph{complete prime} of a complete lattice $\cal L$ is an element $p\in L$ such that $p\sqleq\cup X\Rightarrow \exists x\in X. p\sqleq x$ for any subset $X\ssq L$. ${\cal L}$ is \emph{prime algebraic} if, for all $x\in L$, $x=\sqcup\{p\sqleq x\,\vert\,p\,\,is\,\,a\,\,complete\,\,prime\}$.

\item An algebraic lattice is \emph{finitary} iff every finite element dominates only a finite number of elements, i.e., $\{x\,\vert\,x\sqleq d\}$ is finite for every finite element~$d$.

\item A complete lattice ${\cal L}$ is \emph{distributive} if $x\sqcap (y\sqcup z)=(x\sqcap y)\sqcup (x\sqcap z)$, for all elements $x,y,z\in L$.
\eit
\ed



\btl{T.pal.}
(\cite{[Win89]}) Let ${\cal L}$ be a finitary algebraic lattice. 
Then ${\cal L}$ is prime algebraic iff it is distributive.
\et

 
We now extend some of the previously introduced concepts from finite to 
infinite configurations. The concepts of an \emph{$\alpha$-reduction}  and 
a \emph{$\stab'$-needed} event generalize immediately.

\bdl{D.inf.con.era.}
Let $\calC=(E,\lleq,\era,\leeqv)$ be a DEES.
\ben
\item[(1)] Let $\alpha\in\cC$. Then $\alpha\era e$ iff $\exists \beta\ssq_{fin}\alpha:\,\beta\era e$.

\item[(2)] Let $\alpha,\beta\in\cC$. Then $\alpha\leeqv\beta$ iff $\alpha\era \beta\setminus\alpha\wedge\beta\era \alpha\setminus\beta$.

\item[(3)] We call $\stab'\ssq\cC$ \emph{stable} if it is closed under $\ssq$, has a unique $\ssq$-minimal element $\alpha_{\stab'}$, and is closed under permutation equivalence.
\een
\ed


It is easy to check that Definitions~\ref{D.inf.con.era.}.(1)-(2) do not conflict with definitions of the corresponding concepts for finite configurations. Further, it is an easy consequence of \Dr{D.inf.con.era.}.(1) and [E1] that:


\bll{L.sub.era.}
Let $\alpha\era e$ and $\alpha\ssq\beta\in\cC$. Then $\beta\era e$.
\el

\delete{
Since we want for stable sets $\stab'$ all \emph{$\stab'$-needed-fair}, or simply \emph{$\stab'$-fair}, reductions -- reductions firing at least all $\stab'$-needed events -- to generate configurations in $\stab'$, we need to restrict ourselves to stable sets which are closed under $\ssq$, as closure under parallel moves is no longer sufficient: Indeed, consider a DEES whose events are 
$e_0,e'_1,e_1,e'_2,e_2,\ldots$, whose causal dependency is generated from the dependencies $e_i<e_{i+1},e'_{i+1}$ ($i=0,1,\ldots$), and whose erasure relation is empty, and let $\stab'$ be the set of all configurations containing all $e_i$ and a finite number of $e'_j$s. Then $\stab'$ is closed under parallel moves (since any $\stab'$-early configuration may only contain a finite number of $e'_j$s), but the configuration consisting of all events is not in $\stab'$ although it is \emph{$\stab'$-fair}, i.e., contains all $\stab'$-needed events~$e_i$.
}


We call a reduction in a DEES \emph{$\stab'$-needed-fair}, or simply \emph{$\stab'$-fair}, if it fires  at least all $\stab'$-needed events. $\stab'$-fair configurations are defined similarly.


\btl{L.min.elm.}
Let $\stab'$ be a stable set of configurations in a DEES $\calC$. Then its $\ssq$-minimal element $\alpha_{\stab'}$ consists of all $\stab'$-needed events of $\calC$. Consequently, $\stab'$ consists of all $\stab'$-fair configurations, and any $\stab'$-fair reduction generates a configuration in $\calC$.

\bproof
Since $\alpha_{\stab'}\in\stab'$, all $\stab'$-needed events of $\calC$ are in $\alpha_{\stab'}$. If on the contrary $\alpha_{\stab'}$ contains an $\stab'$-unneeded events $e$, then $\exists\beta\in\stab': e\not\in\beta$, hence $\beta\not\ssq\alpha_{\stab'}$, contradicting the minimality of $\alpha_{\stab'}$. The rest is immediate.
\eproof
\et


For example, firing all events at any state, or all $\stab'$-needed events, in parallel yields $\stab'$-fair reductions since any finite configuration not yet in $\stab'$ can fire at least one $\stab'$-needed event. 


Note that the set of all \emph{fair configurations} -- configurations $\alpha\in\calC$ such that $\forall e\in\calC:\ e\not\in\alpha\,\Rightarrow\,\alpha\era e$ -- need not be stable for every DEES $\calC$. The reason is that, unlike the finite case, a configuration $\alpha$ need not be equivalent to its standard variant $ST_{\rhd}(\alpha)=\{e\in\alpha\,\,\vert\,\,\alpha\not\rhd e\}$.  Indeed, consider the DEES corresponding to the ASDRS from~\cite{[dndrs]} demonstrating the failure of infinitary standardization theorem: there are infinitely many events $e_0,e'_1,e_1,e'_2,e_2,\ldots$, the causal dependency is the transitive reflexive closure of dependencies $e_i<e_{i+1},e'_{i+1}$ ($i=0,1,\ldots$), and the erasure relation is defined by $\alpha\era e'_j$ iff $e'_k\in\alpha$ for some  $k>j$, $k=2,3,\ldots$. Then any fair configuration consists of all non-erasable events $e_i$, and at least one infinite sequence of erasable events $e'_{i_l}$, and it is immediate that the set of all fair configurations does not have the $\ssq$-minimal element. Note that for any fair configuration $\alpha$ in that DEES,  $\sea$ consists of all non-erasable events $e_i$, and $\alpha\not\leeqv\sea$ since $\sea\not\era e'_k$ for any $k$. Thus $\sea=\seb$ does not imply $\alpha\leeqv\beta$ as $ST(\sea)=\sea$. However, the converse is always true:

 

\bl
Let $\alpha,\beta\in\cC$. Then $\alpha\leeqv\beta$ implies $\sea=\seb$.

\bproof
By \Dr{D.inf.con.era.},(2), $\alpha\era\beta\setminus\alpha\cap\beta$ and $\beta\era\alpha\setminus \alpha\cap\beta$. Hence $\sea,\seb\in\alpha\cap\beta$. Suppose on the contrary that $\exists e\in \sea\setminus\seb$. Then $\alpha\not\era e$ and $\beta\era e$, i.e., $\exists\beta_0\ssq_{fin} \beta: \beta_0\era e$, implying by \Lr{L.sub.era.} that $\alpha\cap\beta\not\era e$  and $\beta'=\beta_0\cap(\alpha\cap\beta)\not\era e$. Therefore, by \Pr{C.char.sea.eq.}, $\exists e'\in\beta_0\setminus\beta':\beta'\not\era e'$. Thus $\alpha\not\era e'$ by \Lr{L.sub.era.} (since $\beta'\ssq \alpha\cap\beta\ssq\alpha$) and $e'\in \beta\setminus \alpha\cap\beta$, contradicting $\alpha\era\beta\setminus\alpha\cap\beta$.
\eproof
\el



\bdl{D.sta.or.}
Let $\alpha,\beta\in\cC$, and let $\stab'$ be a stable set of configurations in $\cal C$. We define $\alpha\spleq\beta$ if $\spne{\alpha}\ssq\spne{\beta}$, where $\spne{\alpha}$ denotes the set of $\stab'$-needed events of $\alpha$. We write $\alpha\speqv\beta$ iff $\alpha\spleq\beta$ and $\beta\spleq\alpha$, i.e., $\spne{\alpha}=\spne{\beta}$. We call $\spleq$ a \emph{stable embedding} or $\stab'$-\emph{embedding}, and call $\speqv$ a \emph{stable equivalence} or $\stab'$-\emph{equivalence}. $\spclas{\alpha}$ will denote the $\speqv$-equivalence class of $\alpha$. We write $\spclas{\alpha}\spleq\spclas{\beta}$ if $\alpha\spleq \beta$. Finally, we define $\spfcC=\cC/_{\speqv}=\{\spclasa \,\vert\,\alpha\in\cC\}$  and  $\sefcC=(\spfcC,\spleq)$.
\ed


Note that $\speqv$ does not satisfy [P0], although it does satisfy the other permutation axioms [P1] - [P3]. This means that for permutation equivalence `\emph{progress in any direction}' is equally important, while for a stable equivalence $\speqv$ only  `\emph{progress towards $\stab'$}' matters. Actually, $\leeqv$ is a special case of $\speqv$: the two coincide when $\cal C$ is a PES and $\stab$ is the set of all events.


\bdl{D.mmet.jo.}
Let $\stab'$ be a stable set of configurations in a DEES $\calC$. The meet and join operations $\spsqcup,\spsqcap$ on $\sefcC$ are defined by:
\bit
\item $\alpha\spsqcup \beta=\spne{\alpha}\cup\spne{\beta}$ and $\spclas{\alpha}\spsqcup\spclas{\beta}=\spclas{\alpha\spsqcup \beta}$;

\item $\alpha\spsqcap \beta=\spne{\alpha}\cap\spne{\beta}$ and $\spclas{\alpha}\spsqcap\spclas{\beta}=\spclas{\alpha\spsqcap \beta}$;
\eit
\ed


It is immediate from the definition of $\speqv$ that the above definition is correct.


\bll{L.era.dif.leeqv.}
Let $\beta\era e$, in a DEES $\calC$. Then $\beta\leeqv \beta\setminus\coni{e}$.

\bproof
If $\beta$ is finite, then the lemma follows from \Pr{C.char.sea.eq.}. Otherwise, we have from \Dr{D.inf.con.era.}.(1)-(2) and [E3] that $\beta\era e \Rightarrow \exists\beta_0\ssq_{fin}\beta: \beta_0\era e \Rightarrow \beta_0\era\coni{e}\Rightarrow \beta\era\coni{e}\Rightarrow \beta\leeqv \beta\setminus\coni{e}$.
\eproof
\el



\bll{L.sta.nn.nera.}
Let $\stab'$ be a stable set of configurations in a DEES $\calC$, and let $e$ be $\stab'$-needed. Then $e$ is non-erasable: $\forall\alpha\in\cC: \,\alpha\not\era e$.

\bproof
Suppose on the contrary that $\exists\alpha\in\cC: \,\alpha\era e$. We can assume that $\alpha\in\fcC$. By [E3] and [E2], $\alpha\setminus \coni{e}\era e$. But since $e$ is $\stab'$-needed, $\alpha\setminus \coni{e}\not\in\stab'$. Hence $\beta=\alpha_{\stab'}\cup (\alpha\setminus \coni{e})\in\stab'$ by closure of $\stab'$ under inclusion. But $\beta\era e$ by \Lr{L.sub.era.}, and $\beta\leeqv \beta\setminus \coni{e}$ by \Lr{L.era.dif.leeqv.}. Thus, by closure of $\stab'$ under permutation equivalence, $\beta\setminus \coni{e}\in\stab'$, and $e\not\in \beta\setminus \coni{e}$, contradicting $\stab'$-neededness of $e$.
\eproof
\el


The following proposition shows that $\leeqv\ssq\speqv$, which agrees with our intuition that a concurrent semantics must not discriminate between permutation equivalent configurations/reductions.

\bpl{P.leeq.imp.seqv}
Let $\alpha,\beta$ be configurations in a DEES $\calC$, and let $\stab'$ be a stable set of configurations in $\calC$. Then $\alpha\leeqv\beta$ implies $\alpha\speqv\beta$.

\bproof
By \Dr{D.inf.con.era.}.(1), $\alpha\era\beta\setminus\alpha$ and $\beta\era\alpha\setminus\beta$. Hence, by \Lr{L.sta.nn.nera.}, $\spne{\alpha},\spne{\beta}\ssq \alpha\cap\beta$, and by \Tr{L.min.elm.}, $\spne{\alpha}=\alpha\cap\alpha_{\stab'}=(\alpha\cap\beta)\cap\alpha_{\stab'} =\beta \cap\alpha_{\stab'}=\spne{\beta}$.
\eproof
\ep




\btl{T.main.}
Let $\stab'$ be a stable set of configurations in a DEES $\cal C$. Then 
$\sefcC=(\spfcC,\spleq)$ is a finitary prime algebraic complete lattice.


\bproof
Immediate from \Dr{D.mmet.jo.} and \Tr{L.min.elm.}, since the set of subsets of any non-empty set (in our case, $\alpha_{\stab'}$) ordered by the subset relation is a finitary prime algebraic complete lattice with intersection and union as meet and join operations~\cite{[Win89]}.
\eproof
\et



For any initial reductions $P,Q$, and any stable set of reductions $\stab$, in an ASDRS $\calR$, we can define $P\sleq Q$ iff $FAM_\stab(P)\spleq FAM_\stab(Q)$ in $\calC_\calR$, where $FAM_\stab(P)$ denotes the set of $\stab$-needed families contracted in $P$ (hence coincides with the set of $\stab'$-needed events in the configuration corresponding to $P$). Further, we define $P\seqv Q$ iff $P\sleq Q$ and $Q\sleq P$. We call $\sleq$ and $\seqv$ a \emph{stable embedding} or $\stab$-\emph{embedding} and a \emph{stable equivalence} or $\stab$-\emph{equivalence}, respectively. $\sclas{P}$ denotes the $\seqv$-equivalence class of $P$. We write $\sclas{P}\sleq\sclas{Q}$ if $P\sleq Q$. Now, if $\cR$ is the set of (finite or infinite) initial reductions in $\calR$, we can define $\spfcR=\cR/_{\seqv}=\{\sclas{P} \,\vert\,P\in\cR\}$ and $\sefcR=(\spfcR,\sleq)$. 


\bll{L.spne.con.}
Let $\alpha\in\cC$. Then $\spne{\alpha}\in\cC$. Moreover, $\spne{\alpha}$ is standard, and any of its left-closed enumerations is a reduction.

\bproof
Let $e,e'\in \alpha$, let $e<e'$ and let $e'$ be $\stab'$-needed. We need to show that $e$ is $\stab'$-needed too. By \Tr{L.min.elm.}, $e'\in \alpha_{\stab'}\in\cC$, implying that $e\in\alpha_{\stab'}$. Thus $\spne{\alpha}\in\cC$ ($\spne{\alpha}$ is left-closed). The rest is immediate from  \Lr{L.sta.nn.nera.}.
\eproof
\el


\btl{T.isom.drs.dps.sta.}
Let $\cal R$ be an ASDRS and let $\calC=\cal C_R$ be its corresponding DEES. Further, let $\stab'$ be a set of configurations in $\cal C$, and let $\stab$ be the set of corresponding terms in $\cal R$. Then $f:\sclas{P}\rightarrow \spclas{FAM(P)}$ is an isomorphism between $\sefcR$ and $\sefcC$, with the inverse $f^{-1}: \spclas{\alpha}\rightarrow \sclas{\rs{\spne{\alpha}}}$.  

\bproof
By \Lr{L.spne.con.}, $\rs{\spne{\alpha}}$ and hence $f^{-1}$ are well defined. The rest is immediate from the definitions above.
\eproof
\et


Hence we can define on $\sefcR$ that $\sclas{P}\ssqcup\sclas{Q}=f^{-1}(f(\sclas{P})\spsqcup f(\sclas{Q}))$ and $\sclas{P}\ssqcap\sclas{Q}=f^{-1}(f(\sclas{P})\spsqcap f(\sclas{Q}))$, and we get from \Tr{T.main.} that $\sefcR$ with $\spsqcup$ and $\spsqcap$ as join and meet is a finitary prime algebraic domain. It is not difficult to define $\sleq,\ssqcup$ and $\ssqcap$ on (corresponding equivalence classes of) reductions in $\calR$ directly.  




\section{Conclusions}
\label{concl.}

We have established an equivalence between deterministic stable
operational (ASDRS) and domain-theoretic (DEES) models of
computation, and based on this, constructed a fully adequate event style
concurrent semantics for orthogonal rewrite systems. The correspondence between Event Structures and other models of concurrency, as well as with denotational semantics, are well studied~\cite{[Win89],[WN]}, and we hope that our results contribute to better understanding of the relationship between operational and denotational semantics of sequential and concurrent languages.


We think that our axiomatization of permutation equivalence is
interesting on its own right from the poset/lattice theoretic point of view.
Definitions of permutation equivalence without using a residual calculus
have been studied before~\cite{[L.M.]}, but they still use the syntax of
the rewrite system essentially (axioms depend on the syntax).

\delete{
Based on the work~\cite{[Bou]}, we expect that the theory developed here for conflict-free systems can be extended to the general case, so that higher order process calculi in which processes can be passed and erased can be modelled as well. 
}


\vspace{0.20cm}

%\section*{Acknowledgements}



\begin{akn}
We thank  R.~Kennaway for useful comments.
\end{akn}



\begin{thebibliography}{99}




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


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

\delete{
\bibitem{[berry]} %[{Ber79}]
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{[B.L.]} %[{BeL\'e79}]
G. Berry and J.-J. L\'evy,  Minimal and optimal computations of recursive
programs, \emph{J. of the Association for Computing Machinery} {\bf 26} (1979) 148-175.


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


\bibitem{[B.C.]} %[{BC88}]
G. Boudol and I. Castellani, A non-interleaving semantics for CCS based on proved transitions, \emph{Fundamenta Informaticae} {\bf 11(4)} (1988) 433-452.


\bibitem{[C.K.]} %[{CK96}]
D. Clark and J.R. Kennaway, Event structures and non-orthogonal term graph rewriting, \emph{Mathematical Structures in Computer Science} {\bf 6} (1996) 545-578. 

\delete{
\bibitem{[CEL]} %[{CELMR94}]
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{[CGM]}  
A. Corradini, F. Gadduchi and U. Montanari, Relating two categorical models of term rewriting, in: \emph{Proc.  RTA'95}, Lecture Notes in Computer Science, Vol.~914 (Springer, Berlin, 1995) 225-240.

\bibitem{[rel-jlc]}
J.R.W. Glauert, J.R. Kennaway and Z. Khasidashvili, Stable
results and relative normalization, \emph{Journal of Logic and Computation}, 
{\bf 10(3)} (2000). Special Issue on Type Theory and Term Rewriting, 
F.~Kamareddine and J.W.~Klop, eds. Oxford University Press.


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

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


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

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

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


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


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

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


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


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


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

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

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



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



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


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

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

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

\delete{
\bibitem{[Lan.th]} % [{Lan93}]
C. Laneve, Optimality and concurrency in interaction systems. Ph.D.
Thesis, University of Pisa,~1993.
}

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


\bibitem{[L.M.]} %[{LM94}]
C. Laneve and U. Montanari, Axiomatizing permutation equivalence,  
\emph{Mathematical Structures in Computer Science} {\bf 6} (1994) 219 - 249.  

 
\delete{
\bibitem{[Lon]}
G. Longo, Set theoretic models of lambda calculus: theories, expansions 
and isomorphisms, \emph{Annals of pure and applied logic} {\bf 24} (1983) 153-188.
}    

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


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


\delete{
\bibitem{[Mar91]} %[{Mar91}]
Maranget L. Optimal derivations in weak $\lambda$-calculi and in orthogonal
Term Rewriting Systems. in: \emph{Proc. 8th ACM Symp. on Principles of Programming Languages} (1991) 255-269.

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

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


\bibitem{[Mil89]} %[{Mil89}]
R. Milner, \emph{Communication and Concurrency} (Prentice Hall, 1989).


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

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


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

\bibitem{[San.Th]} %[{San93}]
D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms, Ph.D. Thesis, Edinburgh University,~1993.



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



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


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


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


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


\end{thebibliography}

\end{document}
