\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 adequate} semantics to them.


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-emptyset 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 in the previous
case, and [E3] follows.

\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.,
$\alpha+e'\era e$ by \Dr{D.era.vi.per.eq.}.


[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 (wrt $\ssq$)
left-closed subset containing $e'$ -- contradiction.
\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{\al
pha+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{\al
pha+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}\lcl
as{\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 coincide in ASDRSs~\cite{[ldrs]},
families contracted in family-reductions in $R$ are in one-to-one
correspondence with zig-zag families in $\lin{R}$.

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}



