\documentstyle[twocolumn]{article}
%\input{amssym.def}
%\input{amssym}
\pagestyle{empty}
\setlength{\textheight}{8.75in}
\setlength{\columnsep}{2.0pc}
\setlength{\textwidth}{6.8in}
\setlength{\footheight}{0.0in}
\setlength{\topmargin}{0.25in}
\setlength{\headheight}{0.0in}
\setlength{\headsep}{0.0in}
\setlength{\oddsidemargin}{-.19in}
\setlength{\parindent}{1pc}
\makeatletter

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

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

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

%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\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{\pcontr}{\hookrightarrow_{\cal P}}

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

\newcommand{\fcE}{{\cal L}(E)}
\newcommand{\fcC}{{\cal L}({\cal C})}
\newcommand{\fcP}{{\cal L}({\cal P})}
\newcommand{\fcR}{{\cal L}({\cal R})}

\newcommand{\pfcP}{{\cal L}^{\leeqv}({\cal P})}
\newcommand{\efcP}{{\cal L}^{\emb}({\cal P})}
\newcommand{\pfcR}{{\cal L}^{\leeqv}({\cal R})}
\newcommand{\efcR}{{\cal L}^{\emb}({\cal R})}

\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{\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}_l $}}

\newcommand{\fin}{\in}
%\newcommand{\lleq}{\triangleleft}
%\newcommand{\lles}{\triangleleft}
\newcommand{\lleq}{\unlhd}
\newcommand{\lles}{\lhd}
\newcommand{\leeqv}{\approx}
\newcommand{\eleeqv}{\approx_\rhd}
\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{\pfami}{\simeq_{\cal P}}
\newcommand{\redc}[1]{\mbox{$[{#1}]$}}
\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{deff}\em}
\newcommand{\bdl}[1]{\begin{deff}\em\label{#1}}
\newcommand{\bl}{\begin{lem}\em}
\newcommand{\bll}[1]{\begin{lem}\em\label{#1}}
\newcommand{\bp}{\begin{prop}\em}
\newcommand{\bpl}[1]{\begin{prop}\em\label{#1}}
\newcommand{\bt}{\begin{thm}\em}
\newcommand{\btl}[1]{\begin{thm}\em\label{#1}}
\newcommand{\bel}[1]{\begin{ex}\em\label{#1}}
\newcommand{\bc}{\begin{cor}\em}
\newcommand{\bcl}[1]{\begin{cor}\em\label{#1}}
\newcommand{\bproof}{\begin{pruuf}}
\newcommand{\eproof}{\end{pruuf}}
\newcommand{\ed}{\end{deff}}
\newcommand{\el}{\end{lem}}
\newcommand{\ep}{\end{prop}}
\newcommand{\et}{\end{thm}}
\newcommand{\ee}{\end{ex}}
\newcommand{\ec}{\end{cor}}
\newcommand{\suf}{($\Rightarrow$)}
\newcommand{\nec}{($\Leftarrow$)}
\newcommand{\setm}{\setminus}
\newcommand{\crea}{\vdash}
\newcommand{\emp}{\emptyset}
\newcommand{\cfr}{complete family-reduction}
\newcommand{\cfrs}{complete family-reductions}
\newcommand{\qp}{quasi-persistently}
\newcommand{\stc}{strongly cofinal}
\newcommand{\rn}{RN}
\newcommand{\trnt}{the Relative Normalization theorem}
%\newcommand{\qp}{quasi-persistently}
%\newcommand{\stc}{strongly cofinal}
\newcommand{\pmn}{persistently $\stab$-needed}
\newcommand{\qprn}{quasi-persistently $\reg$-needed}
\newcommand{\qpmn}{quasi-persistently $\stab$-needed}
\newcommand{\das}{\downarrow_{\stab}}
\newcommand{\dar}{\downarrow_{\reg}}
\newcommand{\stab}{{\cal S}}
\newcommand{\reg}{{\cal R}}
\newcommand{\imply}{\,\Rightarrow\,}

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



\title{Relating Conflict-free Stable Transition and Event Models\\
(Extended Abstract, Submitted to LICS'97)}


\author{Zurab Khasidashvili   \\
NTT Basic Research Laboratories\\
Atsugi-shi, Kanagawa-ken, 243-01, Japan \\ 
zurab@theory.brl.ntt.jp
\and  
John Glauert \\
School of Information Systems, UEA \\
Norwich NR4 7TJ England \\ 
jrwg@sys.uea.ac.uk
\thanks{Part of this work was supported by the Engineering and Physical Sciences
Research Council of Great Britain under grant GR/H 41300.}}

 
\maketitle
\thispagestyle{empty}

 

\begin{abstract}
We describe an Event Structure semantics for conflict-free (term and graph, possibly with bound variables and substitution) rewrite systems, including the \lc, and other stable transition systems with residual relation. Our interpretation is based on interpreting redex-families as events. It treats permutation-equivalent reductions as representing the same concurrent computation, which was thought impossible as L\'evy's ordering on the reduction space is not in general a lattice (but only an upper semi-lattice). In order to achieve a fully adequate event semantics based on the permutation-equivalence (which Winskel's Event Structures cannot do), we extend the Prime Event Structure model by axiomatizing the permutation-equivalence on concurrent computations (configurations) in two different ways (for the conflict-free case), and show that thus extended models are equivalent to known stable transition models with axiomatized residual and family relations.
\end{abstract}

 

\section{Introduction}


The prime goal of this paper is to provide a fully adequate concurrent semantics for orthogonal rewrite systems. As an abstract model of concurrency, we chose Event Structures, the most successful and commonly accepted one~\cite{[NPW],[Win89]}. Conflict-free Prime Event Structures (PESs) are sufficient for our purposes. A (conflict-free) PES is simply a set of events ordered by \emph{causal dependency} relation where an event can only dominate a finite number of events. The idea is to view a process as performing events (some \emph{atomic} tasks), and an event can only occur if all events on which it depends already have. 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, no matter in which order 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{[le80]}, which formalizes the idea of the `same atomic task'. Therefore we want to base our interpretation on interpreting redex-families as events, hence to interpret  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 family-reductions in the original system.

Recent advances in abstract study of orthogonal rewrite systems~\cite{[Sta],[GLM],[rndrs],[dndrs],[ldrs]} allows us to address the problem in an 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 there in addition the concept of redex-family is axiomatized. Stable DRSs allow~\cite{[rndrs]} to prove analogs of the Normalization and Standardization Theorems~\cite{[Bar]}. In DFSs one can further prove L\'evy's Optimality Theorem and the Unique Families Lemma. The latter states that any family can be contracted at most once in a 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 event structure interpretation of DRSs based on interpreting families as events. 


Since we want to restrict our attention to family-reductions only, we define \emph{linearization} of any DFS, which is a non-duplicating, also called affine SDRS, ASDRS. We have already shown~\cite{[ldrs]} that any ASDRS forms a DFS with the \emph{zig-zag}~\cite{[le80]} as the family relation. Family-reductions in a DFS precisely correspond to reductions in its linearization, and this allows us to concentrate on construction of event semantics for affine SDRSs only.


To view a process as the domain of all its configurations, an \emph{adequacy} requirement is desirable. Namely,  \emph{runs} of a configuration (i.e., all its possible sequentializations) should be in one-to-one correspondence with all reductions in the equivalence class which the configuration is supposed to represent. Because of the huge importance of the \emph{permutation} or \emph{L\'evy} equivalence~\cite{[le80]} to the whole theory of (not only orthogonal) rewrite systems~\cite{[Bou]}, which is well understood by now, and to the concurrency theory too~\cite{[Sta]}, we want to treat permutation-equivalent reductions as representing the same concurrent computation, as indeed permutation-equivalent reductions result one from another by permuting concurrent consecutive steps.  


In order for this to be possible, permutation-equivalence classes of (finite) reductions must be partially ordered in a way to form distributive lattices, as the domains of (finite) configurations of a PES ordered by inclusion are such lattices~\cite{[Win89]}. However, it is a well known problem that L\'evy's ordering on the reduction space is not in general a lattice (Recursive Program Schemes are exception~\cite{[B.L.]}), but only an upper semi-lattice, as the greatest lower bound of two co-initial reductions need not exist~\cite{[le80]}. 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 of this problem. Laneve~\cite{[Lan.th]} introduces the \emph{distributive} equivalence on $\beta$-reductions which only allow permutation of steps that cannot erase or duplicate one another, and consequently all equivalent sequences have the same length.  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 (needed redexes cannot be erased, and all needed normalizing reductions are of the same length in affine systems). Similarly, Clark and Kennaway~\cite{[C.K.]} work with \pc\ and allow infinite reductions but restrict themselves to standard reductions only (which are unique in their \pc\ class). 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.


To deal with that (lattice) problem, we introduce a different ordering on permutation classes of finite reductions in ASDRSs which makes the latter a distributive lattice (and again generates \pc). Its ideal completion forms a prime algebraic domain, and therefore~\cite{[Win89]} a PES can be associated with the ASDRS whose domain of configurations is isomorphic to the one we have constructed on reductions. But this interpretation is still inadequate as configurations in the constructed ES cannot represent all reductions in a \pc\ class (simply because the latter may contain infinitely many elements while the former has only a finite number of runs). Our ordering coincides with L\'evy's one on needed reductions, and therefore, when restricted to needed reductions, the constructed PES corresponds to the one constructed in~\cite{[KKSdV]}.


In order to cope with the adequacy problem we extend the PES model by axiomatizing \pc\ on event configurations in them in two equivalent ways. One by directly constraining the class of all equivalence relations on configurations, and another by axiomatizing the \emph{inessentiality} or \emph{erasure} relation expressing redundancy of an event for a configuration. The latter extends by further axioms an incomplete axiomatization of the inessentiality relation in~\cite{[rndrs]}. In the resulting extended models, Deterministic \emph{Permutation} and \emph{Erasure} Event Structures, DPESs and DEESs, we can identify configurations with different number of events but still representing the same \pc\ class of reductions. Our ordering on reductions precisely matches the inclusion order on canonical representatives of equivalence classes of configurations (which are the smallest elements in every configuration). We then show that DPESs and DEESs are actually isomorphic to ASDRSs, therefore give a \emph{fully adequa


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 construct distributive lattices from \pc\ of configurations and reductions in DPESs and ASDRSs, respectively,  and an isomorphism between them, implying faithfulness and full abstraction of our interpretation of ASDRSs into DPESs. Finally, in section~\ref{linear.}, we extend this interpretation to duplicating orthogonal rewrite systems by encoding the latter into ASDRSs using the linearization method mentioned above. Conclusions appear in section~\ref{concl.}





\section{Deterministic Residual and Family Structures}



In this section we recall some basic theory for DRSs and DFSs developed in~\cite{[rndrs],[dndrs],[ldrs]}.

\suppress{
In this section we recall \emph{Deterministic Residual Structures} (DRSs) and \emph{Deterministic Family Structures} (DFSs),
introduced in \cite{[rndrs]}. DRSs and DFSs are \emph{Abstract Reduction Systems} (ARSs) with axiomatized notions of
residual. In DFSs, in addition, L\'evy's concept of redex-family is axiomatized. 
We also recall some of the basic theory developed for DRSs and DFSs in~\cite{[rndrs],[dndrs],[ldrs]}.
 }

\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 $\mapsto(u)=(t,s)$, written $t\red{u}s$. This set will be known as the redexes of term $t$, where $u\subt t$ denotes that $u$ is a member of the redexes of $t$ and $U\subts t$ denotes that $U$ is a subset of the redexes. Note
that $\ar$ is a {\em total\/} function, so one can identify $u$ with the
triple $t\red{u}s$. \suppress{\footnote{Klop's ARSs~\cite{[Kl.TRS]} 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 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],[Raa.th]}.
DRS are intended to model all orthogonal term and graph 
rewrite systems, both first and higher-order, 
\delete{such as  \cite{[le80],[H.L.],[Kl.CRS],[OCRS],[Nip.b],[Lam],[Kath],[SPE],[Oos.th],[AL2],[Raa.th]}, 
}
and other conflict-free transition systems with a reasonable level of abstraction, while say ARSs of~\cite{[GLM]}
do not cover e.g., orthogonal term graph rewriting systems~\cite{[SPE]}.


 

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

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

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

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

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

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


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$.
\suppress{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$.
\suppress{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 [acyclicity] and [stability] axioms from one step reductions to any co-initial \emph{external} reductions, that is, reductions that do not contact redexes having common residuals. 



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

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

\begin{diagram}[height=1.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}
\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 Lemma)} 
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 (Acyclicity Lemma)} 
Let $P,N$ be co-initial finite reductions in a DRS, and 
let $P$ be external to $N$. Then $N\not\leeqv P$.
\el

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

(1)  For any co-initial reductions $P$ and $Q$, a redex $Qv$ in the final
term of $Q$ (read as $v$ \emph{with history} $Q$) is called a \emph{copy} of
a redex $Pu$ 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.


(2) Further, $\fami$ and $\contr$ satisfy the following axioms:

$\bullet$ [initial] Let $u,v\subt t$ and $u\not= v$, in $\cal R$.
Then $Fam(\emptyset_t u) \not=Fam(\emptyset_t v)$, where $\emp_t$ is the empty reduction starting from $t$.

$\bullet$ [contribution] $\phi\contr \phi'$ iff for any $Pu\fin \phi'$, $P$
contracts at least one redex in $\phi$.

$\bullet$ [creation] if $e\dored{P}t\red{u}s$ and $u$ creates 
$v\subt s$, then  $Fam(Pu)\contr Fam((P+u)v)$.

$\bullet$ [termination] Any reduction that contracts redexes of a finite
number of families is terminating.

We call a DFS $\cal F$ a \emph{zig-zag} DFS, ZDFS, if its family relation is the zig-zag $\zfami$ (the corresponding contribution relation $\zcontr$ is determined by [contribution]).
\ed

  
\noindent It is shown in~\cite{[rndrs]} that every DFS is a stable DRS. 


\vspace{0.20cm}

\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{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 Structures, 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, under a \emph{reduction} we mean a \emph{finite} reduction. Reductions starting from $\emp$ will also be called \emph{initial} reductions or \emph{histories}.
 



 
 
\subsection{Standardization}
\label{stan.ssc.}
 
We recall some definitions and results from~\cite{[dndrs]} concerning standardization of reductions in non-duplicating, i.e., affine, SDRSs, ASDRSs. 




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

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

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


Note that $P$-neededness, $P$-erasure, and $P$-essentiality do not depend
on the choice of a reduction in the class $\lclas{P}$ of reductions
L\'evy-equivalent to $P$, since $u/P=u/Q$ 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. 

(1) $NE_P(w,t)$ iff $ER_P(w,t)$ and $ES_P(w,t)$. 

(2) If $P:t\doar s'\red{w}o$, then $NE_P(w,s')$.

(3) If $u$ creates $v\subt e$ and $UN_P(u,t)$ (resp. $IE_P(u,t)$, then so is $v$.

(4) If $u\not=v\subt t$, then $NE_P(v,t)$ (resp. $ES_P(v,t)$) iff
$v$ has a $P$-needed ($P$-essential) residual in $e$.
\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 (i.e,. self-needed, or equivalently, self-essential) reduction, and call $Q$ a \emph{standard variant} of $P$. In particular, $ST(P)\in\stav{P}$.

 
\delete{
Obviously, a reduction $P$ is self-needed iff $ST(P)=P$.
The notion of self-essential reduction is the
best approximation to the outside-in left-to-right notion of 
standard reduction~\cite{[Bar],[H.L.],[Kl.CRS]} for DRSs, since we do not 
have any nesting relation imposed on redexes, unlike 
ARSs of ~\cite{[GLM]}, and there is no concept of `left' or `right' 
occurrences in DRSs. Furthermore, our concept of standardization 
captures the essence of the usual one in many respects. In particular, 
in the extraction process which we studied in~\cite{[ldrs]}, self-essential reductions play the same role as outside-in left-to-right standard reductions in the extraction processes of~\cite{[le80],[AL],[Oos]}.
 



\bdl{D.stanndrs.}
We call a reduction $P$ in a DRS \emph{standard}, written $P\in\stan$, if it is self-needed, or equivalently, self-essential. 

\ed
}

 
\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
 

 
\subsection{Families in Affine SDRSs}
\label{fam.ssc.}

In this section we recall construction of DFSs from non-duplicating SDRSs from~\cite{[ldrs]}.


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 co-initial finite reductions in an affine zig-zag DFS. Then $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


\btl{P.on.ca.for.}
{\bf (Affine Extraction)} Every redex $Pv$ in an ASDRS has a zig-zag related redex $P'v'$ in \emph{canonical} form, meaning that $P'\in\stan$ and there is $P''v''\zfami Pv$, such that $\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^*$.
\et


\btl{T.lin.dr.sta.df.}
{\bf (Affine Zig-zag Families)} Let $\cal R$ be a non-duplicating SDRS. Then ${\cal F_R}=({\cal R},\zfami,\zcontr)$ is a zig-zag DFS, called the \emph{corresponding} ZDFS of $\cal R$.
\et


\delete{
\bdl{D.rs.fs.tra.}
We call ${\cal F_R}=({\cal R},\zfami,\zcontr)$ as in \Tr{T.lin.dr.sta.df.} the \emph{corresponding} ZDFS of $\cal R$.
\ed
} 





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



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

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


We only consider \emph{conflict-free} or \emph{deterministic} PESs, where no event can prevent others from occurring, and therefore the consistency predicate is the set of all finite subsets of $E$, $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 E\,\wedge\, e'< e \Rightarrow e'\in\alpha\}$. 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 $\suppress{{\cal E}=}(E, \leq)$ is a conflict-free  PES and $\leeqv\ssq \fcE \times \fcE$ is an equivalence relation, \emph{permutation-equivalence}, \delete{and $\fcP=\fcE$,} satisfying the following axioms, where $\alpha,\beta,\gamma\in\fcE$:

$\bullet$ [P0] $\forall e\in E: \ocon{e}\not\leeqv \con{e}$;  


$\bullet$ [P1] $\alpha\leeqv\beta \wedge \alpha\cap\beta \ssq\gamma\ssq \alpha\cup\beta \suppress{\wedge \gamma\in\fcE} \imply \alpha\leeqv\gamma$;

$\bullet$ [P2] $\alpha\leeqv\beta \wedge \alpha +e,\beta+e\in \fcE \imply \alpha +e\leeqv \beta +e$;  \delete{where $X\in Fin(E)$;}

$\bullet$ [P3] $\alpha\leeqv \alpha-e\wedge e<e' \wedge 
\alpha+e'  \in\fcE \imply \alpha \leeqv\alpha+e'$;

\delete{
\noindent $\fcP$ is called the set of \emph{configurations} of $\cal P$, and is the set of finite left-closed subsets of $E$.   
}
\ed




DEESs extend \emph{Deterministic Computation Structures} (DCS)~\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 ${\cal C}=(E,\leq, \era)$, where  $\suppress{{\cal E}=}(E,\leq)$ is a conflict-free PES and $\rhd\ssq \fcC \times E$ is \emph{inessentiality} or \emph{erasure} relation, \delete{ and $\fcC=\fcE$,} satisfying the following axioms, where $\alpha,\beta\in\fcE$:

$\bullet$ [E0] $\forall e\in E: \emptyset\not\era e$;

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

$\bullet$  [E2] $\alpha\rhd e'\wedge \alpha\rhd e \wedge 
\alpha-e'\in\fcE  \Rightarrow  \alpha-e'\rhd e$;

$\bullet$  [E3] $\alpha\era e \wedge e<e'\imply \alpha\era e'$;

$\bullet$  [E4] $\suppress{\alpha\in\fcE \wedge }\alpha\cup \ocon{e} \era e \imply
\alpha\era e$.  

\noindent  We read $\alpha\,\rhd\, e$ as: `$e$ is \emph{$\alpha$-inessential}'.

\delete{
$\fcC$ is called the set of \emph{finite configurations} or just \emph{configurations} of $\cal C$,  and is the set of finite left-closed subsets of $E$. 
} 
\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$. Next we 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:

$\bullet$ $\alpha\lrhd e$ iff $\alpha\cup \con{e}\leeqv (\alpha\cup \con{e}) \setminus \coni{e}$.


\noindent In particular, when $e\in\alpha$ and $\alpha-e\in\fcE$, 

$\bullet$ $\alpha\lrhd e$ iff $\alpha \leeqv \alpha-e$.


\delete{
$\bullet$ $\alpha\lrhd e$ iff there  are $\beta,\gamma\leeqv \alpha$ such that $e\not\in\beta$ and $e\in\gamma$. 
}
\ed



\bdl{D.eq.in.era.}
For a DEES ${\cal C}=(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:

$\bullet$ $\alpha\eleeqv \beta$ iff $ST_{\rhd}(\alpha)=ST_{\rhd}(\beta)$, where
$ST_{\rhd}(\alpha)=\{e\in\alpha\,\,\vert\,\,\alpha\not\rhd e\}$ is the set of
\emph{$\alpha$-essential} events of $\alpha$.

\noindent  (The subscript $\rhd$ in $ST_{\rhd}(\alpha)$ will often be omitted.)

$\sea$ is called the \emph{standard variant} of $\alpha$.
\ed


\suppress{
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. Then $\sea\in \fcC$ and $ST(\sea)=\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$.
\eproof
\el


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

\bproof
\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$, $\alpha_{i+1}=\alpha_i +e_{i+1}$, and hence $\alpha=\alpha_n$. By the definition of $\sea$, we have $\alpha_n\rhd e_i$ for all $i=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$. \nec\ By [E1].
\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$.
\delete{iff $\forall e\in\beta\setminus\alpha:ST(\beta)\era e$.}

\bproof
\delete{By \Lr{L.alp.eq.sel.al.}, it is enough to prove that $ST(\alpha)=ST(\beta)$ iff $\forall e\in\beta\setminus\alpha:\beta\era e$.} \suf\  By \Dr{D.eq.in.era.}. \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] 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$.
\eproof
\el
 



\bpl{C.char.sea.eq.}
$\forall \alpha,\beta,\gamma\in\fcC:\alpha\cap\beta\ssq\gamma \ssq\alpha\cup\beta, \sea=\seb\Leftrightarrow \gamma\era\alpha\cup\beta\setminus\alpha\cap\beta$.

\bproof
\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 \alpha\cap\beta\era\alpha\cup\beta\setminus\alpha\cap\beta$. \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$. \zurab{need to complete.}
\eproof
\ep
} 



\delete{
\bpl{C.se.alp.se.bet.}
Let $\cal C$ be a DEES. For any $\alpha,\beta\in FCon({\cal C})$, $\alpha\eleeqv \beta$ in $\cal P_C$ iff $\forall e: \,\alpha\rhd e \,\Longleftrightarrow\, \beta\rhd e$ in~$\cal C$.

\bproof
By \Lr{L.alp.eq.sel.al.}, $\alpha\rhd e$ iff $\sea\rhd e$ and $\beta\rhd e$ iff $\seb\rhd e$. But we have by definition of $\eleeqv$ (\Dr{D.eq.in.era.}) that $\alpha\eleeqv \beta$ iff $\sea=\seb$, and the proposition follows.
\eproof
\ep



\bdl{D.se.es.con.}
Let $\cal C$ be a DEES. We call an $\alpha\in \fcC$ {\em self-essential\/} if, for any $e\in\alpha$, $\alpha\not\rhd e$.
\ed

It follows immediately from definition of $\sea$ that $\alpha$ is self-essential iff $\sea=\alpha$.



\bll{se.al.se.essen.}
Let $\cal C$ be a DEES. For any $\alpha\in FCon({\cal C})$, $\sea$ is self-essential.

\bproof
We want to show that, for any $e\in \sea$, $\sea\not\rhd e$. Suppose on the contrary that there is $e_0\in \sea$ such that $\sea\rhd e_0$. Since $\sea\ssq \alpha$, we have by [E1] that $\alpha\rhd e_0$. But this implies $e_0\not\in \sea$ -- a contradiction.
\eproof
\el

 

\bll{L.eras.vers.eq.}
Let $\alpha,\alpha+e,\alpha-e\in \fcC$, in a DEES $\cal C$. Then $\alpha\rhd e$ iff $\alpha +e\rhd e$ iff $\alpha -e \rhd e$.

\bproof
$\alpha\rhd e\Rightarrow \alpha +e\rhd e$ holds by [E1], and the converse is a special case of [E2] (when $e=e'$). The rest, $\alpha +e\rhd e \Longleftrightarrow \alpha -e \rhd e$, follows immediately from $\alpha \rhd e \Longleftrightarrow \alpha +e \rhd e$, by taking $\alpha=\beta-e$ (note that $\beta-e+e=\beta+e$, but $\beta-e+e\not=\beta$ when $e\not\in\beta$).
\eproof
\el


\bll{L.rhd2}
Let $\alpha,\alpha+e,\alpha-e\in \fcC$, in a DEES $\cal C$. Then $\alpha\rhd e$ iff $\alpha +e\eleeqv\alpha
\eleeqv \alpha - e$.

\bproof
We show that $\alpha\rhd e \Longleftrightarrow \alpha +e\eleeqv\alpha$. 
The rest (i.e., $\alpha\rhd e \Longleftrightarrow \alpha -e\eleeqv\alpha+e$) follows from $\alpha\rhd e \Longleftrightarrow \alpha +e\eleeqv\alpha$ by 
taking $\alpha=\beta-e$, since $\beta-e\rhd e \Longleftrightarrow \beta\rhd e$ by \Lr{L.eras.vers.eq.}.

\suf\ We need to show that $\sea=ST(\alpha+e)$, i.e., $\{e_0\in\alpha\,\,\vert\,\,\alpha\not\rhd e_0\}=\{e_1\in\alpha+e\,\,\vert\,\,\alpha+e\not\rhd e_1\}$.
Since $\alpha\rhd e$, we have by [E1] that $\alpha+e\rhd e$,
hence $e\not\in ST(\alpha+e)$. It remains to show that for any $e_0\in\alpha$, $\alpha\rhd e_0$ iff $\alpha+e\rhd e_0$. \suf\ follows from [E1], and \nec\ from [E2].

\nec\ $\alpha+e\eleeqv\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\rhd e$. Therefore, $\alpha\rhd e$ by [E2].
\eproof
\el
}


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





\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]. 
\incl{We only prove [E3]. Other axioms are similar or easy.}

\suppress{
[E0]: By \Dr{D.era.vi.per.eq.} and [P0].
}

[E3]: 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\era e$ and  $\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 

\suppress{
[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\leq 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$, 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., $\alp


[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$.} In each of the three cases of relative ordering of $e$ and $e'$, one easily checks that $(\alpha\cup\con{e}\setminus \coni{e})\cap (\alpha-e'\cup\con{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.}.  


[E4]: Immediate from \Dr{D.era.vi.per.eq.}.
}
\eproof
\et

\incl{ 
We need the following characterization of $\eleeqv$ via $\era$ and $\leeqv$ via $\lera$,  which is not difficult to prove from the erasure and permutation axioms.



\bpl{C.char.sea.eq.}
$\forall \alpha,\beta,\gamma\in\fcC:\alpha\cap\beta\ssq\gamma \ssq\alpha\cup\beta, \alpha\eleeqv\beta\Leftrightarrow \sea=\seb\Leftrightarrow \gamma\era\alpha\cup\beta\setminus\alpha\cap\beta$.
\ep

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



\btl{T.lee.imp.eras.}
For any DEES ${\cal C}=(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]. \incl{We only prove [P2] here.}

\suppress{
[P0]: $\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\not\in ST(\con{e})$, and therefore $ST(\con{e})\not=ST(\ocon{e})$. Thus $ST(\con{e})\not\eleeqv ST(\ocon{e})$ by \Dr{D.eq.in.era.}.

[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 $\seb=\seg$ by \Lr{L.se.con.}, implying $gamma\eleeqv\alpha$ by \Dr{D.eq.in.era.}.
}

[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 [E3], $\forall e'\in\alpha\setminus\sea:e'\not<e$. Thus $\alpha+e\in\fcE\imply\sea+e\in\fcE$. Since $\alpha+e\era \alpha+e\setminus(\sea+e)$, 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$).

\suppress{
[P3]: Let $\alpha\eleeqv \alpha-e$, $e<e'$ and $\alpha+e'\in\fcE$. 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.}.
}
\eproof
\et


\suppress{
\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
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 \cap_{i=1}^n \alpha\setminus\coni{e_i}\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
By \Lr{L.al.le.se.al.}, $\alpha\leeqv\beta$ iff  $ST_{\lrhd}(\alpha)\leeqv ST_{\lrhd}(\beta)$, and \nec\ is immediate. \suf\ Suppose on the contrary that $ST_{\lera}(\alpha)\not=ST_{\lera}(\alpha)$. Then $\exists e\in ST_{\lera}(\alpha)\cup ST_{\lera}(\alpha)\setminus ST_{\lera}(\alpha)\cap ST_{\lera}(\alpha)$. Let say $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$.
\eproof
\ep
}

\btl{T.dc.ps.det.equ.}
{\bf (Equivalence of DPESs and DEESs)}

(1) For any DEES ${\cal C}=(E,\leq,\rhd)$, $\cal C_{P_C}=\cal C$.

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

\bproof
Note that the translations of DEESs into DPES and vice versa does not effect the sets of events and the causality relation. Let ${\cal C_{P_C}}=(E,\leq,\rhd')$ and ${\cal P_{C_P}}=(E,\leq,\leeqv')$, and let us show that $\era=\era'$ and $\leeqv=\leeqv'$.

(1) \suppress{We need to prove that $\alpha\rhd e$ in $\cal C$ iff $\alpha\rhd' e$ in $\cal 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(\alpha\cup\con{e})=ST(\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'e$ by \Dr{D.era.vi.per.eq.}.
 

(2) \suppress{We need to prove that $\alpha\leeqv \beta$ in $\cal P$ iff $\alpha\leeqv' \beta$ in $\cal P'$.} By \Pr{C.sees.eq.leeq.} and \Dr{D.eq.in.era.}, $\alpha\leeqv\beta$ iff $\lsea=\lseb$ iff $\alpha\leeqv'\beta$. 
\eproof
\et






\section{Relating Transition and Event models}
\label{rel.mod.}


We now define translations of ASDRSs and ADFSs into DPESs and DEESs, define the converse translations, and show that the translations commute, implying equivalence of the four computational models. 




\subsection{Translation of affine SDRSs and DFSs into DPESs and DEESs}




\bdl{D.tra.dfs.dps.}
To a DFS ${\cal F}=({\cal R},\fami,\contr)$, we associate the DPES ${\cal P}_{{\cal F}}=(E_{{\cal F}},\leq,\leeqv)$, and the DEES ${\cal C}_{{\cal F}}=(E_{{\cal F}},\leq,\rhd)$, where

$\bullet$ $E_{{\cal F}}=FAM({\cal F})$, the set of all families  of ${\cal
F}$; \delete{ relative to $t$; } 

$\bullet$ $\phi<\psi$ iff $\phi \contr \psi$;   

$\bullet$ $\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$;
 

\delete{
$\bullet$ $\alpha\leeqv\beta$ iff for any reductions $P,Q:t\doar s$ in ${\cal F}$ such that $\alpha=FAM(P)$ and $\beta=FAM(Q)$, $P\leeqv Q$.
}

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

\delete{
$\bullet$ $\alpha\rhd e$ iff there are reductions $P,Q,N:t\doar s$ such that $P\leeqv Q\leeqv N$, $\alpha=FAM(P)$, $e\in FAM(Q)$ and $e\not\in FAM(N)$. 
}
\ed


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

\bproof
Since $IE_Q(v,t)$, $v/Q=\emp$ and $UN_Q(v,t)$. Since $Q'$ is $Q$-needed, it is external to $v$ by \Lr{L.era.and.ess.im.ne.}, 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$. 
\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). Then by \Lr{L.era.and.ess.im.ne.}, $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$, $IE_Q(Pv,o)$, and let $Q'\in\stav{Q}$, 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 affine SDRS. 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 the 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. $IE_P(v,e)$.

\begin{diagram}[height=1.5em,width=1.5em]
  {}           &     &      &         &    & \rOnto^{P'} &    {}   \\
 \dOnto^{Q'}   &           &       &         &    &     &  \dOnto   \\
 {}     & \rOnto     & {}   & \rTo^w   & {} &  \rOnto^{P''}  & {}   \\
 \dTo^u &          &  \dTo^{u'} &   &     \dOnto_{\emp}   &   & \dOnto_{\emp} \\
 {}   & \rOnto   & {} & \rTo^{w'}   & {} &  \rOnto^{ P^*}   &  {}   \\
 \dTo^v &          &  \dTo^{v'} &   &     \dOnto_{\emp}   &   & \dOnto_{\emp} \\
 {}    & \rOnto   & {} & \rOnto   & {} &  \rOnto   & {} &    & {}   \\
\end{diagram}
\eproof
\el


\bll{L.dis.can.al.}
Let $P:t\doar s$, $\phi$ be a family in an AZDFS ${\cal F}$, $Qv,Q'v'\in\phi$, let $Qv$ be canonical, and let $Qv$ be $P$-inessential. Then so is $Q'v'$. 

\bproof
By the Affine Extraction Theorem, there is $Q''$ such that $Q'\leeqv Q+Q''$ and $v'=v/Q''$. Since $Qv$ is $P$-inessential, $ST(P)/Q$ discards $v$ by \Lr{C.sta.dis.}, and $ST(P)/Q'$ discards $v'$ by CR for residuals.
\eproof
\el


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

\bproof
 $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
}




\incl{
In order to prove the correctness of \Dr{D.tra.dfs.dps.}, we need, among others, the following lemma, which is obtained using results in subsections~\ref{stan.ssc.} and \ref{fam.ssc.}.


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

\delete{
\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 affine SDRS. Then $(Q'+u)v$ is $P$-inessential too.
\el

\bll{L.dis.can.al.}
Let $P:t\doar s$, $\phi$ be a family in an AZDFS ${\cal F}$, $Qv,Q'v'\in\phi$, let $Qv$ be canonical, and let $Qv$ be $P$-inessential. Then so is $Q'v'$. 
\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, \psi\in F_1:\phi\not\contr \psi$. Then $\exists Q\in\stav{P} :Q=Q_1+Q_2, FAM(Q_i)=F_i$.

\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



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

\bproof
We need to show that ${\cal C_F}=(E_{{\cal F}},\contre,\rhd)$ satisfies the erasure axioms. \excl{[E0] -- [E4].} 
\incl{We only prove [E4].}

\excl{
[E0] and [E1] follow from Definitions~\ref{D.red.need.ess.} and \ref{D.tra.dfs.dps.}. 

[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$.

[E3]: By Definitions~\ref{D.red.need.ess.} and \ref{D.tra.dfs.dps.} and \Lr{L.crea.dis,drs.}.
}

[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{P} :Q'=Q_1+Q_2, FAM(Q_i)=F_i$. By \Lr{C.sta.dis.}, $Q'$ discards $Pv$, and \excl{by \Lr{L.sam/fam.er.},} $Q'/P=Q_1/P$, since $\ocon{\phi}\ssq  FAM(P)$. Hence $Q_1$  discards $Pv$ and $FAM(Q_1)\ssq \alpha$, implying $\alpha\era \phi$.
\eproof
\el


\excl{
\btl{T.tra.fs.dc.ps.com.}
For any DFS $\cal F$, ${\cal P_F}={\cal P_{C_F}}$.

\bproof
Let ${\cal F}=({\cal R},\leeqv,\contr)$. By \Dr{D.tra.dfs.dps.} and \Dr{D.eq.in.era.}, ${\cal P_F}=(FAM({\cal F}),\contre,\leeqv)$, ${\cal C_F}=(FAM({\cal F}),\contre,\rhd)$ and ${\cal P_{C_F}}=(FAM({\cal F}),\contre,\eleeqv)$. We need to show that $\leeqv=\eleeqv$. By \Dr{D.tra.dfs.dps.}, $\alpha\leeqv\beta$ iff $\alpha\cap\beta\era\alpha\cup\beta\setminus\alpha\cap\beta$. By \Pr{C.sees.eq.leeq.} and \Tr{T.dfs.dees.tr.}, the latter holds iff $\sea=\seb$, meaning that $\alpha\eleeqv\beta$ by \Dr{D.eq.in.era.}.
\eproof
\et
}


It is an immediate consequence of Definitions~\ref{D.tra.dfs.dps.} and \ref{D.eq.in.era.}, \Pr{C.sees.eq.leeq.} and the above lemma that for any DFS $\cal F$, ${\cal P_F}={\cal P_{C_F}}$. By combining this with Theorems ~\ref{T.lee.imp.eras.} and \ref{T.dc.ps.det.equ.}, we get the following theorem.

\bt
For any AZDFS ${\cal F}$, ${\cal C_F}$ is a DEES, ${\cal P_F}$ is a DPES, ${\cal P_F}={\cal P_{C_F}}$ and ${\cal C_F}={\cal C_{P_F}}$.
\et



Since ASDRSs are ZDFSs by \Tr{T.lin.dr.sta.df.}, from the above results we immediately get interpretations of ASDRSs into DPESs and DEESs.




\subsection{Translation of DPESs and DEESs into stable DRSs and DFSs}



The following translation of DPESs and DEESs into stable DRSs resembles to the representation of events in a PES $(E,\leq)$ as prime intervals of the configuration domain $\fcE$, used for construction of PESs from stable families of configurations in~\cite{[Win89]}.


\bdl{D.ps.rs.tra.}
To a DPES ${\cal P}=(E, \leq,\leeqv)$ (resp. a DEES ${\cal C}=(E,\leq,\era)$) we associate an SDRS $\cal R_P$ (resp. $\cal R_C$)  as follows:

$\bullet$ The terms of ${\cal R}_{\cal P}$ ($\cal R_C$) are
L\'evy-equivalence classes $\lclas{\alpha},\lclas{\beta},\ldots$ of
configurations of ${\cal C}$ ($\cal P$);

$\bullet$ The reduction relation of ${\cal R}_{\cal P}$ (${\cal R}_{\cal C}$) consists of sets of pairs  $u=(\lclas{\alpha},e)$, where $\alpha,\alpha+e\in \fcE$ and $\alpha\not\leeqv\alpha+e$ (resp. $\alpha\not\era e$). Pairs $u=(\lclas{\alpha},e)$ such that $\alpha\leeqv\alpha+e$ ($\alpha\era e$) are identified with the empty redex $\emp=(\lclas{\alpha},\emp)$ in $\lclas{\alpha}$. \suppress{A non-empty redex $(\lclas{\alpha},e)$ will also be called an \emph{$e$-redex}.}

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

It is easily seen that ${\cal R_P}={\cal R_{C_P}}$ and ${\cal R_C}={\cal R_{P_C}}$. In~\cite{[rndrs]}, a similar translation of DCSs into SDRSs is given, and its correctness implies also the correctness of \Dr{D.ps.rs.tra.}, i.e., $\cal R_P$ and $\cal R_C$ are indeed SDRSs.


  
Note that initial reductions in $\cal R_P$ and $\cal R_C$ can be represented as event sequences $e_1,\ldots,e_n$ respecting the causal order -- $e_i$ represents the (contraction of) \emph{non-empty} redex $(\{e_1,\ldots,e_{i-1}\},e_i)$. That is, reductions are (some of) left-closed enumerations of configurations $\alpha\in\fcE$, and will be denoted by $\rs{\alpha}$. (As we will see below, not all left-closed enumerations of a configuration represent a reduction.)


\bdl{D.ps.fs.tra.}
To a DPES ${\cal P}=(E, \leq,\leeqv)$, we associate a DFS ${\cal F_P}=({\cal R}_{\cal P}, \pfami,\pcontr)$ as follows:

$\bullet$ ${\cal R}_{\cal P}$ is the DRSs defined in \Dr{D.ps.rs.tra.}.

$\bullet$ $\forall e\in E$, we define the $\pfami$-family $\phi_e$ corresponding to $e$ \suppress{also called the \emph{$e$-family},} by $\phi_e = \{(\redc{\alpha}, e)\,\vert\, \alpha+e\in \fcP \wedge (\lclas{\alpha},e)\not=\emp\}$. That is,  $(\redc{\alpha},e)\pfami (\redc{\beta},e')$ iff $e=e'$, $\alpha+e,\beta+e\in \fcP, (\lclas{\alpha},e)\not=\emp, (\lclas{\beta},e)\not=\emp$.

$\bullet$ Define $\pcontr$ by: $\phi_e\pcontr\phi_{e'}$ iff $e<e'$.
\ed



\incl{
One easily shows that translations ${\cal P} \rightarrow \cal F_P$ and  ${\cal P} \rightarrow \cal R_P$ commute with the zig-zag embedding ${\cal R}\rightarrow {\cal F_R}$, i.e., ${\cal F_{R_P}}=({\cal R_P},\zfami,\zcontr)=({\cal R_P},\pfami,\pcontr)=\cal F_P$, implying in particular the correctness of \Dr{D.ps.fs.tra.}. 


\btl{T.ps.dr.fs.zig.}
For any DPES $\cal P$, $\cal F_P$ is an AZDFS.
\et
}



\excl{
\btl{T.ps.dr.fs.zig.}
Let ${\cal P}=(E,\leq,\leeqv)$ be a DPES, let $\cal R_P$ and $\cal F_P=({\cal R_P},\pfami,\pcontr)$ be as in \Dr{D.ps.fs.tra.}, and let ${\cal F_{R_P}}=({\cal R_P},\zfami,\zcontr)$ be the corresponding ZDFS of ${\cal R_P}$. Then ${\cal F_{R_P}}=\cal F_P$.

\bproof
We need to show that $\zfami=\pfami$ and $\zcontr=\pcontr$.

By \Dr{D.ps.rs.tra.}, $(\redc{\alpha},e)\zfami (\redc{\beta},e')\Rightarrow e=e'$, implying $\zfami\ssq\pfami$. For the converse, consider two redexes $u=(\redc{\alpha},e)\pfami (\redc{\beta},e)=v$. Then $w=(\redc{\alpha\cap\beta},e)$ is also a redex since $\alpha\cap\beta+e=\alpha+e\cap\beta+e\in\fcE$, and $u$ and $v$ are its residuals. \suppress{(Note that $(\lclas{\alpha\cap\beta},e)\not=\emp$ since $(\lclas{\alpha\cap\beta},e)=\emp \Rightarrow (\lclas{\alpha},e)=\emp$, i.e., $\alpha\cap\beta=\alpha\cap\beta+e\Rightarrow \alpha\leeqv \alpha+e$, by [P2].)}  Hence $u\zfami v$.

Let $\phi_e = \{(\redc{\alpha}, e)\,\vert\, \alpha+e\in \fcP\}$ and 
$\phi_{e'} = \{(\redc{\alpha}, e')\,\vert\, \alpha+e'\in \fcP\}\}$ be two families (by (a), they are families both w.r.t. $\pfami$ and $\zfami$). Then $\phi_e\zcontr\phi_{e'}$ means that for any $(\redc{\alpha}, e')\in \phi_{e'}$, the sequence $\redc{\alpha}$ contains $e$; and $\phi_e\pcontr\phi_{e'}$ just means that $e< e'$. Hence in order to prove $\phi_e\zcontr\phi_{e'}\Longleftrightarrow \phi_e\pcontr\phi_{e'}$ it is enough to show that $e<e' \Longleftrightarrow e\in\redc{\beta}$ for any $(\redc{\beta}, e')\in \phi_{e'}$. \suf\ is immediate since $\beta+e'\in \fcP$ is left closed. \nec\ Let $(\redc{\gamma}, e')$ be a canonical element of $\phi_{e'}$ which exists by \Tr{P.on.ca.for.} (when $\phi_{e'}$ is considered as a zig-zag family); it has the property that $\gamma\ssq\alpha$ for any $\alpha$ such that $(\redc{\alpha},e)\in\phi_{e'}$. Then $e\in \gamma$. If on the contrary $e\not<e'$, then $\exists\gamma'\fcE:e'\in\gamma'\wedge e\not\in\gamma'$, and since $e\in\gamma$, $\gamma+e'$ is not the smallest
\eproof
\et
}



\subsection{Equivalence of the four models}


  
\excl{

We now establish a correspondence between DPESs and ADFSs, implying together with the results of previous sections equivalence of the considered four transition and event models.



\bdl{D.drs.isom.}
(1) We call DRSs ${\cal R}=(A,/)$ and ${\cal R}'=(A',/')$ \emph{isomorphic} if there is an isomorphism between reduction graphs of $A$ and $A'$ respecting the residual relation.

(2) We call DFSs ${\cal F}=({\cal R},\fami,\contr)$ and ${\cal F}'=({\cal R}',\fami',\contr')$ \emph{isomorphic} if there is an isomorphism between $\cal R$ and ${\cal R}'$ respecting $\fami$ and $\fami'$ (and hence, by [contribution], respecting $\contr$ and $\contr'$).

(3) We call DPESs ${\cal P}=(E,\leq,\leeqv)$ and ${\cal P'}=(E',\leq',\leeqv)$ \emph{isomorphic} if there is an isomorphism between $(E,\leq)$ and $(E',\leq')$ respecting $\leeqv$ and $\leeqv'$.
\ed
}


\incl{
For any of the four models, there is an obvious concept of \emph{isomorphism}, $\isom$. For example, DFSs ${\cal F}=({\cal R},\fami,\contr)$ and ${\cal F}'=({\cal R}',\fami',\contr')$ are isomorphic if there is an isomorphism between the underlying reduction graphs of $\cal R$ and ${\cal R}'$ respecting the residual, family, and contribution relations in ${\cal F}$ and ${\cal F}'$.  
}


\btl{T.equi.four.}
\mbox{}

(1) For any DPES $\cal P$, ${\cal P}\isom{\cal P}_{{\cal F}_{\cal P}}$.

(2) For any AZDFS ${\cal F}$, ${\cal F}\isom{\cal F}_{{\cal P}_{\cal F}}$.

\bproof
Routine, from \Dr{D.tra.dfs.dps.} and \Dr{D.ps.fs.tra.}.
\eproof
\et


\incl{
This theorem, combined with the results of previous sections, implies equivalence of the considered four transition and event models.
}


\section{Configuration Domains}
\label{latt.str.}


 
Let us call a left-closed enumeration (i.e, respecting the causality relation) $e_1,\ldots,e_k$ of a configuration $\alpha$ a \emph{reduction} or an \emph{$\alpha$-reduction} if no event $e_i$ in the sequence is \emph{vacuous}, i.e., $\forall i:\{e_1,\ldots,e_{i-1}\}\not\era e_i$. An $\alpha$-reduction will be denoted by $\rs{\alpha}$.  
 

Thus reductions in a DPES $\cal P$ precisely correspond to initial reductions in the corresponding ASDRS $\cal R_P$, and the use of notation $\rs{\alpha}$ both for reductions in $\cal P$ and $\cal R_P$ should not be confusing. 

Note that, unlike Prime Event Structures, not every configuration $\alpha$ 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 is a 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'_2\}\era e'_1$. 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 \fcC$, in a DEES $\cal C$. 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.perm.latt.}
Let $\cal P$ be a DPES, $\pfcP=\fcP/_{\leeqv}=\{\lclasa \,\vert\,\alpha\in\fcP\}$, where $\lclasa$ is the $\leeqv$-class of configurations containing $\alpha$, and let $\efcP=(\pfcP,\emb)$ be a partial order defined by $\lclasa\emb\lclasb$ iff $\sea\ssq\seb$. Further, define $\lclasa\sqcup\lclasb=\lclas{\alpha\cup\beta}$ and $\lclasa\sqcap\lclasb=\lclas{\alpha\cap\beta}$.
\ed



\btl{T.perm.ev.dom.}
Let $\cal P$ be a DPES. Then $\efcP=(\pfcP,\emb)$, with the join $\sqcup$ and meet $\sqcap$ defined as in \Dr{D.perm.latt.}, is a distributive lattice.

\bproof
Easy.
\eproof
\et


Note that if $P,Q$ are initial reductions in an ASDRS $\cal R$ and ${\cal P_R}$ is its corresponding DPES, then $P\lleq Q$ in $\cal R$ need not imply $\lclas{FAM(P)}\emb \lclas{FAM(Q)}$ in ${\cal P_R}$. For example, take a term $v=(\lambda x.y)u$ in the \lc, where $x\not=y$ and $u$ is a $\beta$-redex, and let $P=u$ and $Q=v$. Then $P\lles Q$ but $\lclas{FAM(P)}\not\emb \lclas{FAM(Q)}$ since $ST(FAM(P))=\{Fam(u)\}\not=\{Fam(v)\}=ST(FAM(Q))$. This is not unexpected, as it is a well known problem of L\'evy's reduction space that it is not a lattice but only an upper semi-lattice. We now define an ordering on (L\'evy-equivalence classes of) reductions in $\cal R$ that matches the embedding on configurations defined above, and makes $\cal R$ a distributive lattice.


\bdl{D.emb.per.red.}
Let $P, Q$ be co-initial finite reductions in an ASDRS $\cal R$. Define $P\emb Q$ iff  $ST(P)$ is $ST(Q)$-needed. We refer to $\emb$ as the \emph{embedding} relation (while we call $\lleq$ \emph{L\'evy-embedding} relation).
\ed


\excl{
\bpl{P.el.emb.le.emb.}
In an ASDRS, $P\emb Q\imply P\lleq Q$, but not conversely; and $P\leeqv Q$ iff $P\emb Q$ and $Q\emb P$.
\ep



\bll{L.fam.dec.gen.}
Let $P,Q\in\stan$ and be initial. Then $FAM(Q/P)=FAM(Q)\setminus FAM(P)$. If moreover $P\lleq Q$, then $FAM(P)\ssq FAM(Q)$, hence $FAM(Q)=FAM(Q/P)\cup FAM(P)$.
\el



\bll{L.fam.dec.nee.}
Let $P$ be $Q$-needed, and let $P,Q\in\stan$, in an AZDFS. Then $FAM(Q)=FAM(P)\cup FAM(Q/P)$.

\bproof
Since $P$ be $Q$-needed, $P\lleq Q$, hence $Q\leeqv P+Q/P$. Since $Q/P$ is standard by \Lr{L.sta.rem.sta.} and $P$ is $P\sqcup Q$-needed, $P\sqcup Q$ is standard. By \Pr{P.leqv.sam.se.es.fa.}, $FAM(Q)=FAM(P\sqcup Q)=FAM(P)\cup FAM(Q/P)$.
\eproof
\el


\bll{L.char.nee.vi.fam.}
Let $P,Q\in\stan$, in an AZDFS. Then $P$ is $Q$-needed iff $FAM(P)\ssq FAM(Q)$.

\bproof
\nec\ By \Lr{L.fam.dec.nee.}. \suf\ Let $FAM(P)\ssq FAM(Q)$, and suppose on the contrary that $P$ is not $Q$-needed. Let $P=P'+u+P''$, where $u$ is the first $Q$-unneeded step of $P$. Since $Q/P'$ is standard by \Lr{L.sta.rem.sta.} and erases $u$, it is external to $u$ by \Lr{L.ines.sta.dis.}. Thus $Fam(u)\not\in FAM(Q/P')$. By the Unique Families Lemma, $Fam(u)\not\in FAM(P')$,  hence $Fam(u)\not\in FAM(Q)$ by \Lr{L.fam.dec.nee.}, contradiction.
\eproof
\el



\bcl{C.char.emb.vi.fam.}
In an affine ZDFS, $P\emb Q$ iff $SFAM(P)\ssq SFAM(Q)$.

\bproof
By \Pr{P.leqv.sam.se.es.fa.}, $SFAM(P)\ssq SFAM(Q)$ iff $FAM(ST(P))\ssq SFAM(ST(Q))$. Further, $ST(P),ST(Q)\in\stan$ by the Standardization theorem, and the statement follows from \Dr{D.emb.per.red.} and \Lr{L.char.nee.vi.fam.}.
\eproof
\ec
}

\incl{
It is easy to see that $P\emb Q\imply P\lleq Q$, but not conversely. However, $P\leeqv Q$ iff $P\emb Q$ and $Q\emb P$. The intuition behind $\emb$ is that, if $P,Q\in\stan$, $P\emb Q$ iff $P\sqcup Q$ is standard, i.e., $Q/P$ does not make the steps of $P$ inessential in $P+Q/P$. Alternatively, one shows for any $P,Q$ that $P\emb Q$ iff $SFAM(P)\ssq SFAM(Q)$, from which the following proposition follows as $SFAM(P)=ST(FAM(P))$.
}


\bpl{emb.ver.sinc.}
In an affine ZDFS, $\lclas{P}\emb \lclas{Q}$ iff $\lclas{FAM(P)}\emb \lclas{FAM(Q)}$.
\ep



\bdl{D.perm.latt.red.}
Let $\cal R$ be an ASDRS, $\pfcR=\fcR/_{\leeqv}=\{\lclas{P} \,\vert\,P\in\fcR\}$, where $\fcR$ is the set of initial reductions in $\cal R$ and $\lclas{P}$ is the $\leeqv$-class containing $P$, and let $\efcR=(\pfcR,\emb)$, where $\emb$ is the embedding relation defined in \Dr{D.emb.per.red.}. Further, define $\lclas{P}\sqcup \lclas{Q}=\lclas{P\sqcup Q}$ and $\lclas{P}\sqcap \lclas{Q}=\lclas{\rs{SFAM(P)\cap SFAM(Q)}}$, i.e., $\lclas{P}\sqcap \lclas{Q}=\lclas{N}$, where $N$ is an initial reduction with $SFAM(N)=SFAM(P)\cap FAM(Q)$.
\ed


Existence of $\lclas{P}\sqcap \lclas{Q}$ follows from \Lr{L.se.red.}, but we can directly construct a \emph{canonical} element $P\sqcap Q\in \lclas{P}\sqcap \lclas{Q}$ by the following algorithm. First, standardize $P$ and $Q$. Let $P'=ST(P)$ and $Q'=ST(Q)$. Using the algorithm in \Lr{L.reor.fam.}, construct $P''\in\stav{P'}$ in which the steps  \emph{not} in $FAM(Q')$ form a tail. $P\sqcap Q$ is obtained from $P''$ by removing that tail. Clearly, $FAM(P\sqcap Q)=SFAM(P)\cap SFAM(Q)$, hence $P\sqcap Q\in \lclas{P}\sqcap \lclas{Q}$.


\delete{
If all steps of $P'$ with families \emph{not} in $FAM(Q')$ form a tail of $P'$, then we construct $P\sqcap Q$ from $P'$ just by removing that tail. Otherwise, let $u$ be the latest among steps in $P'$ such that $\phi=Fam(u)\not\in FAM(Q')$ and it has a next step $v$ such that $\psi=Fam(v)\in FAM(Q')$. Then $u$ does not create $v$, as otherwise we would have $\phi\contr\psi$ by [creation], and a redex in $\phi$ should be contracted in $Q'$ by [contribution], which is not the case by the choice of $u$. Hence $v=v'/u$ for some redex $v'$, and the steps $u$ and $v$ can be permuted -- replace $u+v$ by $v'+u/v'$. The obtained reduction can be transformed similarly, until a reduction is constructed in which all redexes with families not in $FAM(Q')$ are pushed to the end, and we again remove such steps to obtain $P\sqcap Q$. Clearly, $FAM(P\sqcap Q)=SFAM(P)\cap SFAM(Q)$, hence $P\sqcap Q\in \lclas{P}\sqcap \lclas{Q}$.
} 


\btl{T.isom.drs.dps.}
Let $\cal R$ be an ASDRS and let ${\cal P}=\cal P_R$ be its corresponding DPES. Then $f:\lclas{P}\rightarrow \lclas{FAM(P)}$ is the isomorphism between $\efcR$ and $\efcP$, with the inverse $f^{-1}: \lclas{\alpha}\rightarrow \lclas{\rs{\sea}}$.

\bproof
By \Pr{emb.ver.sinc.}.  
\eproof
\et



As a consequence, we get from \Tr{T.perm.ev.dom.} that $\efcR$ is a distributive lattice too.



\delete{
\btl{T.matc.emb.}
(1) $P\emb Q$ in an ASDRS iff $FAM(P)\emb FAM(Q)$ in the corresponding DPES. 

(2)  $\alpha\emb\beta$ in a DPES iff for any $\sea$- and $\seb$-reductions $\rs{\sea}$ and $\rs{\seb}$, $\rs{\sea}\emb\rs{\seb}$.
\et
}



\suppress{

\section{Preservation of neededness and stability by the translations}

\subsection{Neededness and stability in DEESs and DPESs}


This section develops normalization-by-neededness theory for DEESs and DPESs, and relates them with those in affine SDRSs and DFSs, establishing relationship between concepts of stability intrinsic to the above particular affine models, and between neededness and stability in each model. This comparison gives a simple explanation of why is the needed strategy normalizing wrt stable sets in SDRSs.  

 
 
\subsection{Relative Normalization}  


\delete{
In this section, we recall the basic theory of relative normalization in non-duplicating, i.e., affine, stable DRSs, ASDRSs, as developed in~\cite{[rndrs]}.  
}


We first recall the basic theory of relative normalization in ASDRSs, as developed in~\cite{[rndrs]}.  


\begin{deff}\em
\label{D.rel.need.}
Let $\stab$ be a set of terms in a DRS $\cal R$.
We call a redex $u\subt t$
\emph{$\stab$-needed}, written $NE_\stab (u,t)$, if at least one residual of
it is contracted in any reduction from $t$ to a term in $\stab$, and call
it \emph{$\stab$-unneeded}, written $UN_\stab (u,t)$, otherwise.
\end{deff}


\begin{deff}\em
We call a set $\stab$ of terms \emph{stable} if: (a)
$\stab$ is \emph{closed under parallel moves}: for any $t\not\in \stab$, any
$P:t\doar o\in \stab$, and any $Q:t\doar e$ which does not contain terms
in $\stab$, the final term of $P/Q$ is in $\stab$; and  (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. \delete{(2) We call a stable set $\stab$ \emph{regular} if $\stab$-unneeded redexes cannot duplicate $\stab$-needed ones.}
\end{deff}

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. 
The sets of normal forms, head-normal
forms, weak-head-normal forms, root-stable forms, etc. are all stable.  



 


\begin{thm}\em
\label{T.4.2.}
{\bf (Relative Normalization)} Let $\stab$ be a stable set of
terms in an affine stable DRS $\cal R$, and let $t\not\in \stab$ be a term in $\cal R$ having an $\stab$-normal form. Then $t$ contains at least one $\stab$-needed redex, and it does not possess a reduction in
which infinitely many times $\stab$-needed redexes are contracted.
\end{thm}


\bd
Let $\stab$ be a set of configurations in a DPES ${\cal P}=(E,\leq,\leeqv)$, resp. in a DEES be a DPES ${\cal C}=(E,\leq,\era)$.

(1) We call $\stab$ \emph{stable} if 

\noindent (a) $\alpha \in\stab\,\wedge\,\beta\in\fcC\,\wedge\, \forall\gamma\in S:\,\, \gamma\not\ssq \beta \Rightarrow \,\alpha\cup\beta\in\stab$; 

\noindent (b) $\alpha \in\stab\, \wedge \beta \in\stab\,\Rightarrow \,\alpha \cap\beta\in\stab$; and

\noindent (c) $\alpha\in \stab \,\wedge\,\beta\leeqv\alpha\,\Rightarrow \, \beta \in \stab$, resp. $\alpha\in \stab \,\wedge\,\beta\eleeqv\alpha\,\Rightarrow \, \beta \in \stab$.  


(2) We call $e\in E$ $\stab$-\emph{needed} if, for any $\alpha\in\stab$, $e\in \alpha$.
\ed

It is easy to see that every stable set has exactly one minimal element. Conversely, a set of configurations having the smallest element is stable if it is closed under the subset relation, but need not be so otherwise.


The following theorem shows that the \emph{stability} concept for Event Structures~\cite{[Win]} is a special case of our concept of stability of configuration sets. Recall first that a conflict-free Event Structure (ES) is a pair ${\cal E}=(E,\vdash)$, where $E$ is a set of events and $\vdash\,\,\ssq Fin(E)\times E$ is the \emph{enabling} relation, such that $X\vdash e \wedge X\ssq Y \Rightarrow Y\vdash e$. A
\emph{configuration} $\alpha$ is a subset of $E$ such that, for any
$e\in \alpha$, there are $e_1,\ldots,e_n=e$ such that
$\{e_0,\ldots,e_{i-1}\}  \vdash e_i$, for all $i\leq n$~\cite{[Win]}.
A conflict-free ES is \emph{stable} if $X\vdash e\,\,\wedge\,\, Y\vdash e\Rightarrow X\cap Y\vdash e$~\cite{[Win]}. Consequently, for every $e\in E$, there is exactly one minimal event set $X_e$ enabling $e$. It is shown in~\cite{[Win]} that Any Prime Event Structure is a stable ES.



\bt
An Event Structure ${\cal E}=(E,\vdash)$ is stable iff, for any event $e$, so is the set $\stab_e$ of all configurations containing $e$.

\bproof
\suf\ Let $\cal E$ be stable. Then, for any $e\in E$, there is the smallest set $X_e$ enabling $e$. Hence $X_e$ is the smallest element of $\stab_e$, and its stability follows by its closure under $\ssq$.

\nec\  Let $S_e$ be stable for any $e\in E$. Then every $S_e$ has the smallest element, $X_e$, and $X_e\vdash e$ is the smallest set enabling $e$, implying stability of $\cal E$.
\eproof
\et



Similarly, the stability concept for DRSs is a special case of our concept of stability for term sets in DRSs:


\bt
Let $\cal R$ be an affine DRS. Then $\cal R$ is stable iff, for any redex with history $Pv$, so is the set consisting of terms containing redexes zig-zag related to $Pv$, and all their reducts.
\et





\bll{L.ne.ev.ne.red.}
Let $\stab'$ be a set of 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 $(\lclas{\alpha},e)$ be a non-empty $e$-redex in $\cal R_C$. Then $e$ is $\stab'$-needed in $\cal C$ iff $(\lclas{\alpha},e)$ is $\stab$-needed in $\cal R_C$. (Thus, if an $e$-redex is $\stab$-needed, so are the others.)

\bproof
\suf\ Let $(\lclas{\alpha},e)\not=\emp$ (thus $e\not\in\alpha$), and let $P:\lclas{\alpha}\red{e_1}\lclas{\alpha+e_1}\red{e_2}\ldots\red{e_n}\lclas{\alpha+e_1+\ldots+e_n}$ be an $\stab$-normalizing reduction in $\cal R_C$ (not containing empty steps and not containing terms in $\stab$ except for $\lclas{\alpha+e_1+\ldots+e_n}$). If $P$ does not contract a $e$-redex, i.e., $e\not= e_i$ for all $i$, then $e\not\in \alpha+e_1+\ldots+e_n\in \stab'$, contradicting $\stab'$-neededness of $e$.
\nec\ Let $(\lclas{\alpha},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$, $\alpha\cup\beta\in\fcC$, and $e\not\in\alpha\cup\beta$ ($e\not\in\alpha$ since $(\lclas{\alpha},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 $\lclas{\alpha}\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$) by omitting empty steps. But the latter reduction does not contract $e$-redexes, contradicting $\stab$-neededness of $(\lclas{\alpha},e)$.
\eproof
\el



\bll{L.sta.imp.sta.}
Let $\stab'$ be a set of configurations in a DEES $\cal C$, and let $\stab$ be the set of corresponding terms in the corresponding SDRS $\cal R_C$. Then $\stab'$ is stable in $\cal C$ iff $\stab$ is stable in $\cal R_C$.

\bproof
\suf\ We need to show that $\stab$ is (a) closed under unneeded expansion and (b) closed under parallel moves.

(a) Let $u=(\lclas{\alpha}, e)$ be a step in $\cal R_C$ entering $\stab$. Suppose on the contrary that $u$ is not $\stab$-needed in $\lclas{\alpha}$. Then there is an $\stab$-normalizing reduction $\lclas{\alpha}\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 the condition (b) of stability for $\stab'$.

(b) Let $Q:\lclas{\alpha}\red{e'_1}\lclas{\alpha+e'_1}\red{e'_2}\ldots\red{e'_k}\lclas{\alpha+e'_1+\ldots+e'_k}$ be a reduction not containing terms in $\stab$ and 
$P:\lclas{\alpha}\red{e_1}\lclas{\alpha+e_1}\red{e_2}\ldots\red{e_n}\lclas{\alpha+e_1+\ldots+e_n}$ be $\stab$-normalizing. Then the final term of $P/Q$ is $\lclas{\alpha+e_1+\ldots+e_n+e'_1+\ldots+e'_k}$, and it is in $\stab$ since $\alpha+e_1+\ldots+e_n+e'_1+\ldots+e'_k\in\stab'$ by the condition (a) of stability for $\stab'$.

\nec\ We only need to prove conditions (a) and (b) of stability for $\stab'$, since $\stab'$ is closed under permutation equivalence by the hypothesis.

(a) Let $\alpha\in\stab'$ and let $\beta$ be a configuration not containing elements of $\stab'$. Further, let $\rs{\alpha}$ and $\rs{\beta}$ be reductions corresponding to $\alpha$ and $\beta$, respectively. Then the reduction $\rs{\alpha}/\rs{\beta}$ ends in the term $\lclas{\alpha\cup\beta}$, since $\rs{\alpha}$ ends in $\lclas{\alpha}$ and $\rs{\beta}$ ends in $\lclas{\beta}$. By stability of $\stab$, $\lclas{\alpha\cup\beta}\in\stab$, implying $\alpha\cup\beta\in\stab'$.

(b) Let $\alpha,\beta\in\stab'$. we need to show that $gamma=\alpha\cap\beta\in\stab'$. Since $\gamma$ is left-closed, there are enumerations $e_1,\ldots,e_k,e_{k+1},\ldots, e_n$ and $e_1,\ldots,e_k,e'_{k+1},\ldots, e'_m$ such that $e_1,\ldots,e_k$ is an enumeration of $\gamma$. Suppose on the contrary that $\gamma\not\in \stab'$. Then $\lclas{\gamma}\not\in\stab$. Hence a step of the reduction corresponding to the quasi-reduction $\lclas{\gamma}\red{e_{k+1}}\lclas{\gamma+e_{k+1}}\ar\ldots\red{e_n}\lclas{\gamma+e_{k+1}+\ldots+e_n}$ enters $\stab$, hence must be $\stab$-needed by stability of $\stab$. Therefore, by \Lr{L.ne.ev.ne.red.}, at least one of the events $e_{k+1},\ldots,e_n$, say $e_j$, is $\stab'$-needed. But $e_j\not\in\beta\in\stab'$, contradicting $\stab'$-neededness of $e_j$.
\eproof 
\el

Let $\cal F$ be an ADFS, and let $\stab$ be a set of terms in it. One could define a family $\phi$ to be $\stab$-needed in two ways: when at least one of its members is $\stab$-needed, or when all of its members are. Now let $\cal F=\cal F_C$ for some DEES $\cal C$,  and let $\stab'$ be a set of configurations in  $\cal C$, and let $\stab$ be the set of corresponding terms in the corresponding SDRS $\cal R_C$. As we have already shown, the $e$-family in $\cal F_C$ (corresponding to an event $e\in\cal C$) consists of all $e$-redexes. Hence, by \Lr{L.ne.ev.ne.red.}, with either definition of $\stab$-neededness of a family, $e$ is $\stab'$-needed in $\cal C$ iff the $e$-family is $\stab$-needed in $\cal F$.


The results of previous sections relating DEESs, DPESs, SDRSs and DFSs allow us to speak about \emph{corresponding} DEES $\cal C$, DPES $\cal P$, ASDRS $\cal R$ and ADFS $\cal F$, meaning that $\cal R$ is isomorphic to $\cal R_C$ and $\cal R_P$, $\cal P$ is isomorphic to $\cal P_R$, etc. Similarly, we can speak of \emph{corresponding} permutation-equivalence classes of reductions in $\cal R$ and $\cal F$ and permutation-equivalence classes of configurations in $\cal C$ and $\cal P$, \emph{corresponding} events in $\cal C$ and $\cal P$ and redex-families in $\cal R$ and $\cal F$, etc. Therefore, we can also speak of \emph{corresponding} sets $\stab'$ of configurations in $\cal C$ and $\cal P$ and sets $\stab$ of terms in $\cal R$ and $\cal F$, where the terms in $\stab$ are endpoints of reductions corresponding to configurations in $\stab'$. Hence, we have by Lemmas~\ref{L.ne.ev.ne.red.} and~\ref{L.sta.imp.sta.} that:


\bt
Let $\cal R, F, C, P$ be corresponding ASDRS, ADFS, DEES and DPES, and let $\stab'$ and $\stab$ be respectively corresponding sets of configurations in $\cal C$ and $\cal P$, closed under permutation equivalence, and of terms in $\cal R$ and $\cal F$. Then:

(a) An event $e$ in $\cal C$ or $\cal P$ is $\stab'$-needed iff an $e$-redex is $\stab$-needed in $\cal R$ iff the $e$-family is $\stab$-needed in $\cal F$.

(b) $\stab'$ is stable in $\cal C$ iff $\stab$ is stable in $\cal R_C$.
\et


\delete{
\bll{L.nee.red.ne.ev.}
Let $\stab'$ be a set of configurations in a DEES $\cal C$, and let $\stab$ be the set of corresponding terms in the corresponding SDRS $\cal R_C$. Then any $\stab$-needed $\stab$-normalizing reduction starting from $\lclas{\emp}$ (with all terms except the last outside $\stab$) contracts exactly the redexes corresponding to $\stab'$-needed events.
\el
}
 
We conclude this section by a theorem expressing the relationship between concepts of stability and neededness:


\bt
Let $\stab'$ be a stable set of configurations in a DPES $\cal P$ (or a DEES $\cal C$), and let $\stab$ be its corresponding set of terms in the corresponding SDRS $\cal R$. Then $\stab'$ has a minimal element which consists of $\stab'$-needed events, and any $\stab$-needed $\stab$-normalizing reduction starting from $\lclas{\emp}$ contracts exactly the redexes that correspond to that smallest event set of $\stab'$.

\bproof
Let $\lclas{\emp}\red{e_1}\lclas{e_1}\red{e_2}\ldots\red{e_n}\lclas{e_1,\ldots,e_n}$ be an $\stab$-needed $\stab$-normalizing reduction in $\cal R_C$. Then every event $e_i$ is $\stab'$-needed by \Lr{L.ne.ev.ne.red.}. And since $\lclas{e_1,\ldots,e_n}\in\stab$, $\{e_1,\ldots,e_n\}\in\stab'$ and every $\stab'$-needed event is among $e_1,\ldots,e_n$ by definition of $\stab'$-neededness. 
\eproof
\et

 
}


\section{Event Structure semantics for stable DRSs}
\label{linear.}


Now we come to constructing event semantics for orthogonal rewrite systems. Our interpretations is based on interpretation of redex-families as events, so we assume that if the system is duplicating, then it comes with a notion of redex-family (defined via labelling, extraction or zig-zag~\cite{[levy],[le80],[Mar91],[AL],[Oos]}) satisfying our family axioms.  


Recall that a multi-step reduction in a DFS is a \emph{(complete) family-reduction} if each multi-step is a complete development of the maximal set of redexes of some family.  
it is immediate that for any DFS  ${\cal F}=({\cal R},\fami,\contr)$, ${\cal E}_{{\cal F}}=(FAM({\cal F}),\contre)$ is a PES~\cite{[rndrs]}. Note however that some of the events in $FAM({\cal F})$ may never occur in reduction sequences of ${\cal E}_{{\cal F}}$ that correspond to family-reductions in $\cal F$.  
\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 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, but no family-reduction can create redexes in $Fam(Pv)$. 
\excl{
$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)$.
}
}
As argued in the introduction, we want events in the corresponding DPES of $\cal F$ to match precisely to families contracted in family-reductions in $\cal F$. Therefore, we first associate an ASDRS $\lin{{\cal F}}$ to a DFS $\cal F$, called the \emph{linearization} of $\cal F$, and interpret $\cal F$ in the DEES or DPES corresponding to $\lin{{\cal F}}$. The reduction steps in $\lin{{\cal F}}$ correspond to family-reduction multi-steps of $\cal F$.



\bdl{D.lin.dfs.drs.}
Let ${\cal F}=({\cal R},\fami,\contr)$ be a DFS. The \emph{linearization} of ${\cal F}$ is the ASDRS $\lin{{\cal F}}=(A,/)$, where 

$\bullet$ the branches of the reduction graph of the underlying ARS $A$ are family-reductions starting from $\emp$, each edge (i.e., a reduction step) being a multi-step contracting a family of redexes.

$\bullet$ the residual relation $/$ is defined as follows: let $U$ and $V$ be complete sets of redexes in two different families in a term $s$, and let $U:s\ar o$ be the multi-step contacting $U$. Then $V/U$ is the multi-step $o\ar e$ contracting all members of the set $V/U$ in a multi-step. 
\ed


It is easy to check that $\lin{{\cal F}}$ in the above definition is indeed an ASDRS. One first checks that if $U$ and $V$ are complete sets of redexes in two different families in a term $s$ and $s\red{U}o$, then $V/U$ forms a complete family too, in $o$. Obviously, $V/V=\emp$, and every family in $o$ has at most one ancestor family in $s$. Finally, [acyclicity] and [stability] for $\lin{{\cal F}}$ follow immediately from the Acyclicity Lemma and Stability Lemma, respectively. From the correctness of \Dr{D.lin.dfs.drs.} and \Tr{T.lin.dr.sta.df.}, we have the following theorem.



\btl{T.line.zig.}
For any DFS ${\cal F}$, $\lin{{\cal F}}$ is an AZDFS.
\et



The extraction procedure~\cite{[ldrs]} in the linearization $\lin{R}$ of an orthogonal (possibly duplicating) rewrite system $R$, first or higher order, which comes with the labelling concept of family, corresponds to `family-extraction' in family-reductions, eliminating all family-steps not contributing to a family. (So family-extraction is different from extraction in that the latter eliminates particular redexes in a history, which need not be a family-reduction.) Two families in different family-reductions can be family-extracted to the same canonical representative iff the families have the same label (since extraction preserves labels of every family). Here a canonical representative of a family is one whose history is a family-reduction  contracting only contributor families, and is unique up to the order of contraction of causally independent families. Since labelling and extraction families coincide in orthogonal rewrite systems~\cite{[levy],[Mar91],[AL],[Oos]}) and zig-zag and extraction families 

By combining the translation (linearization) of DFSs into AZDFS with the translations of the latter into DPESs and DEESs, we achieve our objective of defining an adequate event style semantics for orthogonal rewrite systems.



\section{Conclusions}
\label{concl.}

We have established an equivalence between deterministic stable operational (ASDRSs) and domain-theoretic (DPESs and DEESs) 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 the denotational semantics is well studied~\cite{[Win89]}, and we hope that our results contribute to better understanding of relationship between operational and denotational semantics of sequential and concurrent languages.

For example, the theory of normalization by neededness relative to \emph{stable sets of terms} from~\cite{[rndrs]} has a counterpart in DPESs, thus implying another concept, different from the one in~\cite{[Win89]}, of \emph{stable sets of configurations} in DPESs.\footnote{A set $\stab$ of configuration in a DPES $\cal P$is \emph{stable} if  it is closed under L\'evy-equivalence, closed under intersection, and $(\alpha \in\stab\,\wedge\,\beta\in\fcP\,\wedge\, \not\exists\gamma\in S:\,\, \gamma\ssq \beta) \Rightarrow \,\alpha\cup\beta\in\stab$.} This concept applies to Event Structures $(E,\vdash)$ as well (with an \emph{enabling} relation $\vdash$ instead of a causal order $\leq$), and it is easy to see that $(E,\vdash)$ is stable iff for any $e\in E$, so is the set of all configurations containing $e$. Study of precise relationship between syntactic and semantic concepts of stability and its relationship with sequentiality (neededness) goes beyond the scope of this paper.

We think that our axiomatization of permutation equivalence is interesting on its own right from the lattice theory 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.


\vspace{0.20cm}

%\section*{Acknowledgements}


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


\begin{thebibliography}{99}




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


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


\bibitem[{Ber79}]{[berry]}
Berry G. Mod\'eles compl\'etement ad\'equats et stables des
$\lambda$-calculs typ\'es. Th\`ese de l'Universit\'e
de Paris VII, 1979.


\bibitem[{BeL\'e79}]{[B.L.]} 
Berry G., L\'evy J.-J. Minimal and optimal computations of recursive
programs. JACM 26, 1979, p.~148-175.


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


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

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

\bibitem[{CELMR94}]{[CEL]}
Corradini A., Ehrig H., L\"owe M., Montanari U., Rossi F. An event structure semantics for safe graph grammars. In proc. PROCOMET'94, IFIP Transactions A-56, 1994.


\excl{
\bibitem[{CF58}]{[C.F.]}
Curry H.~B., Feys R. Combinatory Logic. vol.~1, North-Holland, 1958.
}

\delete{
\bibitem[{GK94}]{[ctrs]}
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[{GK96}]{[rndrs]}
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.

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

\bibitem[{GLM92}]{[GLM]}
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[{Hin64}]{[Hin]}
Hindley R.J. An abstract form of the Church-Rosser theorem I. JSL, 34(4):545-560, 1969.  


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



\bibitem[{KKSV93}]{[KKSdV]}
Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Event structures and
orthogonal term graph rewriting. In~\cite{[SPE]}.  


\bibitem[{KG96}]{[dndrs]}
Khasidashvili Z.,  Glauert J. R. W. Discrete normalization and Standardization in Deterministic Residual Structures. In: Proc. of 
\delete{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[{KG96a}]{[ldrs]}
Khasidashvili Z., Glauert J.R.W. Zig-zag and extraction families in 
non-duplicating stable Deterministic Residual Structures. Submitted.
({\sf ftp://ftp.sys.uea.ac.uk/pub/zurab/LinZig.ps.gz})


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


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


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


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


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

\delete{
Axiomatizing permutation equivalence in the \lc. In: Proc. of  \delete{the $3^{rd}$ International Conference on Algebraic and Logic Programming,} ALP'92, Springer LNCS, vol.~632, 1992, p.350-363.
}

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


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


\bibitem[{Mar91}]{[Mar91]}
Maranget L. Optimal derivations in weak $\lambda$-calculi and in orthogonal
Term Rewriting Systems. In: Proc. of POPL'91, p.~255-269.

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

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


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


 
\bibitem[{Oos94}]{[Oos.th]}
 Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D.
Thesis, Free University, Amsterdam,~1994.

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

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


\bibitem[{Sch94}]{[Sch]}
Schied G. On relating rewrite systems and graph grammars to event structures. \excl{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[{SPE93}]{[SPE]}
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[{Sta89}]{[Sta]}
Stark E.~W. Concurrent transition systems. TCS 64(3):221-270, 1989.


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


\bibitem[{Win86/89}]{[Win89]}
Winskel G. An introduction to Event Structures. \suppress{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 Cambr. Univ. Comp. Lab. Report n. 95, 1986.

\end{thebibliography}
\end{document}
