\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{NTT Basic Research Laboratories \\
Atsugi, Kanagawa, 243-01, Japan \\
\emph{zurab@theory.brl.ntt.co.jp}}
\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 sets of results for
which 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}^{\leq}\rceil$}}
\newcommand{\coni}[1]{\mbox{$\lceil{#1}^{\geq}\rceil$}}
\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. \zurab{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 interpreted into 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 only.}

\delete{
Since we want events in the corresponding DPES of $\cal F$ to match
precisely the families contracted in complete family-reductions in $\cal
F$, we first associate with $\calF$ a non-duplicating, or affine, DFS
$\lin{\calF}$, called the \emph{implementation} of $\cal F$, and interpret
$\cal F$ in the DEES $\calC_{\lin{\calF}}$ and DPES $\calP_{\lin{\calF}}$
corresponding to $\lin{\calF}$. The reduction steps in $\lin{\calF}$
correspond to family-reduction multi-steps of $\cal F$, and zig-zag
families in $\calF_I$ exactly correspond to events of $\calC_{\lin{\calF}}$
and $\calP_{\lin{\calF}}$. (Note that there may be families in $\calF$
which are never contracted in a complete family-reduction in $\calF$, and
such families have no corresponding events in $\calC_{\lin{\calF}}$ and
$\calP_{\lin{\calF}}$.
\footnote{For example, consider a CRS (\cite{[Kl.CRS]}) $R$ with rules
$\{F[x]Z(x) \ar Z(Z(x)),\, H(x)\ar a,\, G(a)\ar b\}$, restricted to the
reduction graph of the term $t=F[x]H(G(x))$. Let $P:F[x]H(G(x))\ar
H(G(H(G(x))))\ar H(G(a))$ and $v=G(a)$. Then the redex $Pv$ has a
corresponding event in the corresponding PES $(FAM(R),\contre)$, but no
family-reduction can create redexes in $Fam(Pv)$.
$F[x]H(G(x))\ar H(G(H(G(x))))$, $F[x]H(G(x))\ar H(G(H(G(x))))\doar a$, and
$F[x]H(G(x))\ar F[x]a \ar a$ are all family-reductions in $R$, but neither
contracts $Fam(Pv)$.
}
)


Since we want to restrict our attention to family-reductions, we define
\emph{linearization} or \emph{implementation} of DFSs. We show that the
implementation of any DFS
is a non-duplicating, or \emph{affine}, DFS, with
\emph{zig-zag}~\cite{[le80]} as the family relation (AZDFS).
Family-reductions in a DFS precisely correspond to reductions in its
implementation, allowing us to concentrate on construction of event
semantics for AZDFSs only. We have shown in~\cite{[ldrs],[acoi-rep]} that
any affine
SDRS (or ASDRS) is in fact an AZDFS.
}

To view a process as the domain of all its configurations, an
\emph{adequacy} requirement is desirable. Namely, that \emph{runs} of a
\zurab{finite} configuration (i.e., all its possible sequentializations) should
be in one-to-one correspondence with all \zurab{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, for example, a \pc\ class of a
finite reduction may have an infinite number of elements.
\zurab{For example, consider the $\lambda$-term $Kx\Omega$, where $K=\lambda
x y.x$ and $\Omega=(\lambda x.x)\lambda x.x$. Intuitively, all reductions
consisting of a number of $\Omega$-steps followed by a $K$-steps are
`equal', as $\Omega$-steps are performed in an erased part of $t$ (or in
`garbage'). And indeed, the 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 finite reductions must be
partially ordered so as to form distributive, or equivalently, prime
algebraic lattices, since the domains
of finite configurations of a PES ordered by inclusion are such
lattices~\cite{[Win89]}. \zurab{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$ (whose symmetric
closure is 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.]}.} \zurab{As a consequence, although the lattice
properties can be restored by taking the ideal completion~\cite{[B.L.]},
the adequacy requirement above cannot be meet even when the reduction is
non-duplicating.}  This problem, caused by erasure of redexes, is well
discussed in~\cite{[Lan.th]}, where it is argued that event semantics say
for the \lc\ cannot therefore be based on \pc.



Several authors have proposed different ways to get round this problem.
Laneve~\cite{[Lan.th]} 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. \zurab{Similarly, Corradini et al~\cite{[CGM]} base
their interpretation on the equivalence relation generated by allowing
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 affine).  Clark and Kennaway~\cite{[C.K.]} also work
with \pc\ and allow for (finitely) non-normalizable terms, but restrict
themselves to standard reductions. Schied~\cite{[Sch]} and Corradini et
al~\cite{[CEL]}  work with linear rewrite systems (no duplication, no
erasure), mainly graph grammars, 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 space -- appropriately ordered \pc\ classes of
finite configurations in a DPES/DEES -- is isomorphic to
L\'evy's reduction space of the corresponding ASDRSs, and therefore
DPESs/DEESs give a \emph{fully adequate} semantics to ASDRSs.




\delete{PES semantics of a transition system is appealing partly because
the configuration domains of PESs -- \zurab{(finite and infinite)}
configurations ordered by the subset relation -- enjoy nice algebraic
properties: they form \emph{finitary prime algebraic
domains}~\cite{[Win89]}.}

\zurab{As a consequence, similarly to L\'evy's reduction space, L\'evy's
configuration domains in DEESs/DPESs.} 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, and thereby reconstruct finitary
prime algebraic domains from configuration domains of DEESs/DPESs: The
isomorphism between ASDRSs and DEESs discussed above induces  a concept of
\emph{stable sets of configurations} in DEESs,  and the theory of
normalization by neededness relative to stable sets of terms in ASDRSs
\cite{[rndrs]} has its counterpart in DEESs. This relativized concept of
neededness enables us to show that the relativized stable orderings on
configuration domains of DEESs/DPESs do form finitary prime algebraic
domains.

\delete{
We therefore introduce orderings $\sleq$ on reductions relative to
particular \emph{stable} sets $\stab$ of values one may be interested in,
such as normal forms, head-normal forms, or weak head-normal forms, in the
\lc.  We show that $\seqv$-equivalence classes of finite reductions, where
$\seqv$ is the equivalence relation generated by $\sleq$, do form finitary
prime algebraic domains, and that stability of $\stab$ is indeed a
necessary condition for that.  Therefore, similar orderings $\sples$ can be
defined on the domains of configurations of DEESs, relativized w.r.t.
stable sets of configurations $\stab'$, and this allows us to construct
algebraic lattices from the configuration domains in DEESs, as promised
in~\cite{[mfcs]}.
}


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 and zig-zag DFSs, showing the equivalence of the four
models. In Section~\ref{latt.str.}, we define L\'evy-embedding on
configurations 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.nee.}, 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.



\bd
(\cite{[Hin]}) 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 $\ar(u)=(t,s)$, written $t\red{u}s$. This set will be known as the
redexes of term $t$, where $u\subt t$ denotes that $u$ is a member of the
redexes of $t$ and $U\subts t$ denotes that $U$ is a subset of the redexes.
Note
that $\ar$ is a {\em total\/} function, so one can identify $u$ with the
triple $t\red{u}s$. \footnote{Klop's ARSs~\cite{[Klo92]} are pairs
$(Ter,\ar)$, and do not allow one to distinguish transitions with the same
source and target terms.} A {\em 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$. $P+Q$ denotes the concatenation of $P$ and $Q$.  $u$ also
denotes the reduction that contracts $u$.
\ed


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 reduction $P$ is defined by
transitivity.

A \emph{development} of $U\subts t$ is a reduction $P:t\doar $ that only
contracts residuals of redexes from $U$; it is \emph{complete} if
$U/P=\cup_{u\in U}\,u/P=\emptyset$. Development of $\emptyset$ is
identified with the empty reduction. $U$ will also denote a complete
development of $U\subts t$. The residual relation satisfies the following
two axioms:
\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 the
residual relation is non-duplicating. Note that, since the only observables
of DRSs are redexes, duplicating syntactic rewrite systems may still form
affine SDRSs. For example, the DRS corresponding to innermost reductions in
an orthogonal TRS is an affine SDRS, although innermost redexes may
duplicate their arguments.

In a DRS $\cal R$, the residual relation on redexes is extended
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]}.


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$. We call $P$ {\em
external\/} to $Q$ if for any $i,j$,  $u_i/(Q_j/P_i)\cap
v_j/(P_i/Q_j)=\emp$ (see the diagram, where $U_{i,j}=u_i/(Q_j/P_i)$ and
$V_{i,j}=v_j/(P_i/Q_j)$).

\begin{diagram}[height=1.5em,width=1.5em]
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


\delete{
\bll{L.ext.lem.}
{\bf (Externality Lemma)} Let $P,Q,N$ be co-initial finite reductions in a
DRS, and let $P$ be external to $Q$. Then $P/N$ is external to $Q/N$.
\el
}


\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 affine, SDRSs, 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 so is every redex
contracted in $P$. 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$. The latter
property will be referred to as \emph{CR for residuals}. The
\emph{discards} concept however does depend on the particular reduction in
the \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$, when so is $ST(P)$. Otherwise,
let $v\subt t$ be such that it is $P$-needed and its residual is contracted
in $P$ first among $P$-needed residuals of $P$-needed redexes in $t$
(existence of such $v$ follows from \Lr{L.era.and.ess.im.ne.}). Then
$ST(P)=v+ST(P/v)$. 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 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
$\emp$, by analogy with the initial state in an Event Structure, although
$\emp$ will also be used to denote empty reductions. Further, in DFSs,
families will always be considered relative to $\emp$, i.e., all histories
start with $\emp$.
Unless otherwise stated, by a \emph{reduction} we mean a \emph{finite}
reduction. Reductions starting from $\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~\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 (no actions can
be erased or duplicated), 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 orderon $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$, $Fin(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$;  \delete{where $X\in Fin(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



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].  Further, 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$.


\suppress{
Finally, if $e<e'$, then $\alpha+e'\in\fcE\imply e\in\alpha$, and
$\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}$.
By [E3] which we have already proved above for $\lera$, $\alpha\lera
e\imply\alpha\lera e'$, implying by \Dr{D.era.vi.per.eq.} that
$\alpha=\alpha\cup\con{e}\leeqv
\alpha\cup\con{e}\setminus\coni{e}+e'=\alpha+e'$. Hence
$\alpha+e'\cup\con{e}\setminus\coni{e}\leeqv \alpha+e'\cup\con{e}$, i.e.,
$\alpha+e'\era e$ by \Dr{D.era.vi.per.eq.}.
}

\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}$. \delete{Obviously, either
$e\leq e'$, $e'<e$, or $e\not\leq e'\wedge e'\not< e$, and in the latter
case either $e\in\alpha$ or $e\not\in\alpha$.} One easily checks 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$.


Similarly, since ASDRSs and AZDFSs are equivalent transition models by the
Affine Families Theorem, we will mostly speak of AZDFSs, since the zig-zag
relation of the latter is important for establishing an equivalence between
the considered event and transition models, which is the subject of the
next section.





\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.}
To 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:\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:\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 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:\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 CR for residuals.
Conversely, if $Q'\lleq P$, then $Q''/(P/Q)=\emp$, and
$v'/(P/Q')=v/(P/Q)=\emp$ again by CR for residuals, thus $Qv$ is
$P$-inessential.
\eproof
\el


\bll{L.sam/fam.er.}
Let $\emp\dored{Q}s\red{u}s'$, let $\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 CR for residuals, $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 again a 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 reductions.
\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 resembles to 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.}
To a DEES $\calC=(E,\leq,\era,\leeqv)$ we associate an ASDRS $\cal R_C$ as
follows:
\bit
\item  The terms of $\cal R_C$ 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.

\delete{
\bll{L.add.eras.}
Let $\calC=(E,\leq,\era)$ be a DEES, let ${\cal P}=(E, \leq,\leeqv)$ be a
DPES, let $\alpha, \alpha+e\in \fcE$, and let $e\not\in\alpha$. Then
\ben
\item[(1)] $\alpha\era e$ iff $\alpha +e\eleeqv\alpha$.

\item[(2)] $\alpha\lrhd e$ iff $\alpha +e\leeqv\alpha$.
\een

\bproof
\ben
\item[(1)]
\ben
\item[\suf] By \Dr{D.eq.in.era.}, we need to show that
$\sea=\{e_0\in\alpha\,\,\vert\,\,\alpha\not\era
e_0\}=\{e_1\in\alpha+e\,\,\vert\,\,\alpha+e\not\era e_1\}=ST(\alpha+e)$.
Since $\alpha\era e$, we have by [E1] that $\alpha+e\era e$,
hence $e\not\in ST(\alpha+e)$. It remains to show that for any
$e_0\in\alpha$, $\alpha\era e_0$ iff $\alpha+e\era e_0$. \suf\ follows from
[E1], and \nec\ from [E2] (since $\alpha+e\era e$).
\item[\nec] By \Dr{D.eq.in.era.}, $\alpha+e\leeqv\alpha$ means that
$ST(\alpha+e)=\sea$. But $\sea\ssq \alpha$,
thus $e\not\in \sea$. Hence $e\not\in ST(\alpha+e)$,
i.e., $\alpha+e\era e$. Therefore, $\alpha\era e$ by~[E2].
\een

\item[(2)] By \Dr{D.era.vi.per.eq.}, $\alpha\lrhd e$ iff
$\alpha\cup\con{e}\leeqv \alpha\cup\con{e}\setminus\coni{e}$. It remains to
note that, since $e\in\alpha$, $\alpha\cup\con{e}=\alpha+e$ and
$\alpha\cup\con{e}\setminus\coni{e}=\alpha$.
\een
\eproof
\el
}


\bt
Let $\calC=(E,\leq,\era,\leeqv)$ be a DEES. Then ${\cal R_C}$ 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.}
To 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 $\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:\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:\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:\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:\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 $\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.}, $Q\lleq P_j$, i.e., $P_j\leeqv
Q+Q'$ for some $Q'$. Let $Q_j=Q+Q'$. It follows from \Dr{D.red.need.ess.}
that $Q_j$ too discards $N_jv_j$; thus $v_j/(Q_j/N_j)=\emp$. But
$N_j/Q_j=\emp$, thusthe final term of $Q_j/N_j$ contains the redex
$u_j\in\phi_j$ (see the figure), which must be a residual of $v_j$ since
$N_jv_j\zfami Q_ju_j$ (see Lemma 5.2 in~\cite{[ldrs]} or Lemma~4.2
in~\cite{[acoi-rep]}) -- a contradiction.
\begin{diagram}[height=1.5em,width=1.5em]
\emp         &\rOnto^{Q_j}& & t_j       &\rTo^{u_j}   &   {}\\
\dOnto<{N_j}&            & &\dOnto<{\emp}&         &      \\
{}     &\rOnto_{Q_j/N_j}& & {}    & \rTo_{u_{j}} & {}   \\
\dTo<{v_j}   &         & &   &             &     \\
{}      &      & &  {}       &       & {}   \\
\end{diagram}

\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 CR for residuals. 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, and let $e_0, e_1,\ldots,e_n$ be a left-closed
enumeration of $\alpha\in\calL_{fin}(\calC_\calF)$. Further, 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=\calC_\calR$: 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.nee.}


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{[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. Since in this paper we are
interested in computing a term in a set of `results' $\stab$ starting from
the initial term $\emp$, we will assume that there is a need for a further
computation in a term $t$ only if $t$ is \emph{early} w.r.t. $\stab$, or is
\emph{$\stab$-early}: no term in $\stab$ can be reduced to $t$. That is, we
will be interested in $\stab$-normalizing reductions which start from
$\emp$ and ends as soon as a term in $\stab$ is reached; all terms in such
reductions are $\stab$-early since the reduction relation in $\calR_\calC$
is acyclic. We will call redexes in $\stab$-early terms \emph{$\stab$-early
redexes}, and call reductions contracting only $\stab$-early redexes
\emph{$\stab$-early reductions}.  It is easy to see that  $\stab$-early
terms in ASDRSs $\calR_\calC$ correspond to \emph{$\stab'$-early
configurations} -- configurations $\alpha\in\fcC$ such that for any
$\beta\subset\alpha:\,\beta\not\in\stab'$, where $\stab'$ is the
corresponding to $\stab$ set of configurations in $\calC$. The set of
$\stab'$-early configurations will be denoted by $\stab'_{early}$.
Therefore, we correspondingly alter the definition of relative neededness
given in~\cite{[rndrs]} -- we will only allow $\stab$-early redexes to be
$\stab$-needed. This is also necessary for a sound definition of relative
neededness of events in DEESs if we want to allow sets of results $\stab'$
which are not closed under the subset relation.


\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}, written $NE_\stab (u,t)$, if $t$ is $\stab$-early
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}, \delete{written $UN_\stab (u,t)$,} otherwise.

\item[(2)] We call a set $\stab$ of terms \emph{stable} if:
\ben
\item[$(a)$] $\stab$ is \emph{closed under parallel moves}: \\
for any $\stab$-early $t$, any $P:t\doar o\in \stab$, and any $\stab$-early
$Q:t\doar e$, the final term of $P/Q$ is in $\stab$; 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}


A stable set need not be closed under reduction --
$Q/P$ in the definition above may contain terms not in $\stab$,
but closure under parallel moves requires that the final term is.
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.



The 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)$.
\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 parallel moves}: \\
$\alpha \in\stab'\,\wedge\,\beta\in\stab'_{early}\,\Rightarrow
\,\alpha\cup\beta\in\stab'$;

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

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



The next theorem gives two equivalent definitions of stability in DEESs,
more in the spirit of the definition stability in PESs~\cite{[Win89]}.
However, as before, and unlike~\cite{[Win89]}, we again require closure
under parallel moves, in order to guarantee that a configuration in a
stable set can be constructed even after executing unneeded events. We will
see that the new definition works when infinite configurations are also
allowed.


\btl{T.stab.eq.}
Equivalent definitions of stability of finite sets of 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{semi-closed under intersection}: \\
$\alpha \in\stab'\, \wedge \beta \in\stab'\,\Rightarrow \,\exists
\gamma\ssq \alpha \cap\beta:\,\gamma\in\stab'$;

\item[$(b'')$] $\stab'$ is \emph{has a unique $\ssq$-minimal element
$\alpha_{\stab'}$}: \\
$\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
$\forall \gamma\ssq\alpha\cap\beta:\,\gamma\not\in\stab'$. 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_k\}\not\in\stab'$ for all
$k\leq j$, 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\not\subset\alpha$, contradicting the minimality of
$\alpha$.


\item[$(iii)$] Let $\alpha, e$ be such that $\alpha\in\stab'_{early}\wedge
\alpha+e\in\stab'$. If on the contrary $e$ is $\stab'$-unneeded, there is a
configuration $\delta\in\stab'$ such that $e\not\in\delta$. By $(b'')$,
$e\not\in\alpha_{\stab'}$ and $\alpha+e\not\in\alpha_{\stab'}$,
contradicting the minimality of $\alpha_{\stab'}$ since
$\alpha+e\in\stab'$.
\delete{
By $(b')$, $\exists\delta'\ssq \delta\cap \alpha+e:\,\delta'\in\stab'$,
contradicting the assumption since $\delta'\ssq\alpha$.
}
\een
\eproof
\et


Note that a stable $\stab'$ need not be closed under intersection unless it
is closed under the subset relation: Consider the process given on the
picture below, where endpoints of configurations in $\stab'$ are encircled
and the events are ordered as follows: $e\leq e'\leq e_1,e_2$. We can
assume that the erasure relation is empty. Then $\stab'$ is indeed stable,
$\{e,e',e_1\},\{e,e',e_2\}\in\stab'$, but
$\{e,e',e_1\}\cap\{e,e',e_2\}=\{e,e'\}\not\in\stab'$. Note that only the
event $e$ is needed for $\stab'$, thus even non-erasable events can be
unneeded in general, and hence the relative neededness concept makes sense
already for PESs. \zurab{We will see below that for stable sets $\stab'$
corresponding to \emph{fair} computations, only (and all) non-erasable
events are $\stab$-needed.}
\begin{diagram}[height=1.5em,width=1.5em]
\label{D.perm.cl.}
       &        &       &           &       &              &\odot  \\
       &        &       &           &       &  \ruTo^{e_1} &       \\
\emp   & \rTo^e &\odot  & \rTo^{e'} & \cdot &              &       \\
       &        &       &           &       & \rdTo_{e_2}  &       \\
       &        &       &           &       &              &\odot  \\
\end{diagram}




\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 $\cal R_C$ (which are the endpoints of reductions
corresponding to configurations in $\stab'$). Then $\stab'$ is stable in
$\cal C$ iff $\stab$ is stable in $\cal R_C$.

\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 $\cal R_C$, 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 parallel moves.

\item[(b)] Let $u=(\lclasa, e)$ be a step in $\cal R_C$ 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 closure of $\stab'$ under
intersection.
\een

\item[\nec] We only need to verify that $\stab'$ is closed (a) under
parallel moves 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 $\cal
R_C$.
Further, let $e\in E$, and let $(\lclasa,e)$ be a non-empty $\stab$-early
$e$-redex in $\cal R_C$. Then $e$ is $\stab'$-needed in $\cal C$ iff
$(\lclasa,e)$ is $\stab$-needed in $\cal R_C$.

\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 $\cal R_C$ (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 parallel moves, 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 by 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 $\stab'$-early
configuration, possibly interleaved by finite sequences of
$\stab'$-unneeded steps, eventually yields a configuration in $\stab'$.

\bproof
Immediate from closure of $\stab'$ under parallel moves (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 -- 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]}.


\bd
\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 any 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

\suppress{
\bd
\bit
\item A \emph{complete partial order}, cpo, $D$ is a partial order having a
least element $\bot$ and such that any directed set has a lub.

\item A cpo $D$ is \emph{distributive} if $x\cap (y\cup z)=(x\cap y)\cup
(x\cap z)$ for all $x$ and all upperbounded $y,z$.

\item A cpo $D$ is \emph{consistently complete} if any upperbounded subset
has lub, or equivalently, if any non-empty subset has a glb.

\item A \emph{stable} cpo is a consistently complete distributive cpo such
that the glb (meet) operation is continuous.

\item A subset (of a cpo $D$?) is \emph{pairwise consistent} if any two
points in the set have an upper bound. Then a partial order is
\emph{coherent} if any pairwise consistent set has an upper bound. (Any
coherent partial order is a consistently complete cpo.)
\eit
\ed
}


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

\bdl{D.inf.con.era.}
Let $\calC=(E,\lleq,\era,\leeqv)$ be a DEES, and let $\stab'\ssq\cC$.
\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$ stable if it is closed under parallel
moves, has a unique $\ssq$-minimal element $\alpha_{\stab'}$, and is closed
under permutation equivalence.
\delete{
\item[(4)] An event $e\in E$ is $\stab'$-needed if
$\forall\alpha\in\cC:\,e\in\alpha$.

\item[(5)] Let $\alpha\in\cC$. As for finite configurations, we call a
\emph{reduction} or an \emph{$\alpha$-reduction}, written $\rs{\alpha}$, an
enumeration of $\alpha$ that does not contain vacuous events (i.e., events
erased by the set of preceding events).
}
\een
\ed

It is easy to check that the above definition does 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


\bll{L.min.elm.}
Let $\stab'$ be a stable set of configurations in a DEES $\calC$. Then its
minimal element $\alpha_{\stab'}$ consists of all $\stab'$-needed events of
$\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'}$.
\eproof
\el


Let us call a reduction $\stab'$-need fair if it eventually fires every
$\stab'$-needed event. For example, firing all events at any state, or all
$\stab'$-needed events, in parallel yield $\stab'$-fair reductions, as by
closure of $\stab'$ under parallel moves, any finite $\stab'$-early
configuration can fire at least one $\stab'$-needed event.

\bt
Let $\stab'$ be a stable set of configurations in a DEES $\calC$. Then
every $\stab'$-needed fair reduction is $\stab'$-normalizing.

\bproof
By \Lr{L.min.elm.}, the corresponding configuration $\alpha$ of any
$\stab'$-needed fair reduction can be represented as
$\alpha=\alpha_{\stab'}\cup\beta$, thus $\alpha\in\stab'$ by closure of
$\stab'$ under parallel moves.
\eproof
\et


The above concept of stability of configuration sets in a DEES $\calC$ has
its counterpart for (initial, finite or infinite) reductions (which are
also reductions in the ASDRS $\calC_\calR$). It is easy to verify that the
sets of reductions computing `infinite results' such as
B\"ohm-trees~\cite{[Bar]} or L\'evy-Longo trees~\cite{[Lon]}  (i.e.,
reductions computing at least all defined nodes in the corresponding trees,
and possibly doing more computation at locations corresponding to undefined
nodes), form stable sets of reductions. The situation is however different
with 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$. The set of all fair
configurations need not be stable for every DEES $\calC$, and the reason is
that, unlike the finite case, a configuration $\alpha$ need not be
equivalent with 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
generated by $e_0,e'_1,e_1,\ldots e'_k\era e'_j$, for any $j<k$ and
$k=1,2,\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}$, $l\ar\infty$, and it is immediate that this set does not have
the minimal element. Note that for any fair configuration $\alpha$,  $\sea$
consists of all non-erasable events $e_i$, and $\alpha\not\leeqv\sea$ since
$\alpha\not\era e'_k$ for any $k$. Thus $\sea=\seb$ does not imply
$\alpha\leeqv\beta$ as $ST(\sea)=\sea$. The following lemma shows that 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 say $\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 a `\emph{progress towards $\stab'$}
is.


\bdl{D.mmet.jo.}
Let $\alpha,\beta$ be configurations in a DEES $\cal C$, and let $\stab'$
be a stable set of configurations in $\calC$. The meet and join operations
$\spsqcup,\spsqcap$ on $\alpha$ and $\beta$, as well as on their
$\speqv$-classes $\spclas{\alpha}$ and $\spclas{\beta}$, relative to a
stable ordering $\spleq$ of configurations, is defined by:
\bit
\item $\alpha\spsqcup \beta=\spne{\alpha}\cup\spne{\beta}$;

\item $\spclas{\alpha}\spsqcup\spclas{\beta}=\spclas{\alpha\spsqcup \beta}$;

\item $\alpha\spsqcap \beta=\spne{\alpha}\cap\spne{\beta}$;

\item $\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}\in\stab'_{early}$. Hence $\beta=\alpha_{\stab'}\cup
(\alpha\setminus \coni{e})\in\stab'$ by closure of $\stab'$ under parallel
moves. 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 \Lr{L.min.elm.},
$\spne{\alpha}=\alpha\cap\alpha_{\stab'}=(\alpha\cap\beta)\cap\alpha_{\stab'
} =\beta \cap\alpha_{\stab'}=\spne{\beta}$.
\eproof
\ep


\bll{L.spne.con.}
Let $\alpha\in\cC$. Then $\spne{\alpha}\in\cC$, and moreover,
$\spne{\alpha}$ is standard.

\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 \Lr{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). It is immediate
from  \Lr{L.sta.nn.nera.} that $\spne{\alpha}$ is standard.
\eproof
\el



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


\bproof
Immediate from \Dr{D.mmet.jo.}and \Lr{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 \zurab{ASDRS $\calR_\calC$, we can define $P\sleq Q$ iff
$FAM_\stab(P)\spleq FAM_\stab(Q)$ in $\calC$, 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, 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)$.


\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.} and \Lr{L.se.red.}, $\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 its
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 do depend on the syntax).


We expect that the theory developed here for conflict-free systems can be
extended to the general case (by combining our results with the
construction of Event Structures for non-orthogonal Term Graph Rewriting
Systems in~\cite{[C.K.]}, based on the work~\cite{[Bou]}), 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.

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

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


\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]}
Corradini A., Gadduchi F., Montanari U. Relating two categorical models of
term rewriting, in: J.~Hsiang, ed., \emph{Proc. Sixth International
Conference on Rewriting Techniques and Applications, RTA'95}, Lecture Notes
in Computer Science, Vol.~914 (Springer, Berlin, 1995) 225-240.


\bibitem{[ctrs]} %[{GK94}]
Glauert J.R.W., Khasidashvili Z.  Relative Normalization in
Orthogonal Expression Reduction Systems. In: Proc. of the
$4^{th}$ International workshop on Conditional (and Typed) Term
Rewriting Systems, CTRS'94, Springer LNCS, vol.~968, N.~Dershowitz,
N.~Lindenstrauss eds. Jerusalem, 1994, p.~144-165.



\bibitem{[morn]} %[{GK94}]
Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization
in Orthogonal Expression Reduction Systems. Report SYS-C94-06, UEA,
Norwich, 1994.


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



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


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


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


\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}]
Kathail V. Optimal Interpreters for lambda-calculus based functional
languages, Ph.D. thesis, MIT, 1990.


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


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


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


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


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



\bibitem{[acoi-rep]} %
Khasidashvili Z., Glauert J. R. W. An abstract concept of optimal
imple\-men\-ta\-tion. 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.


\bibitem{[Laf]} % [{Laf90}]
Lafont Y. Interaction nets. In: Proc. of POPL'90, p.~95-108.


\bibitem{[Lam]} % [{Lam90}]
Lamping J. An algorithm for optimal lambda calculus reduction.
In: Proc. of the $17^{th}$ ACM Symposium on Principles of
Programming Languages, POPL'90, pp.~16-30, 1990.


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


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


\bibitem{[L.M.]} %[{LM94}]
Laneve C., Montanari U. Axiomatizing permutation equivalence.
\emph{Mathematical Structures in Computer Science}, 6:219 - 249,
\delete{Cambridge University Press,} 1994.


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


\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: Proc. of POPL'91, p.~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}]
Milner R. Communication and concurrency. Prentice Hall, 1989.


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


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

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


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


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



\bibitem{[Sch]}  % [{Sch94}]
Schied G. On relating rewrite systems and graph grammars to event
structures. In: Proc. of the Dagstuhl Seminar 9301 on Graph Transformations
in Computer Science, Springer LNCS, vol.~776, Schneider H.-J. Ehrig H.,
eds, 1994,  p.~326-340.




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


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


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


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


\end{thebibliography}

\end{document}



