\documentclass[12pt,twoside]{article}
\usepackage{ueareport}

\input{diagrams} % Paul Taylor's Macro Package
\usepackage{latexsym}
\ueareportno{SYS-C97-??}
\ueatitle{Relating Conflict-free Stable Transition and Event Models}
\ueaauthor{Z. Khasidashvili and J. Glauert}

\title{Relating Conflict-free Stable Transition and Event Models}

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

\begin{document}

\maketitle




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


\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}% [section]
\newtheorem{cor}[thm]{Corollary}% [section]
\newtheorem{ex}[thm]{Example}% [section]
\newtheorem{rem}[thm]{Remark}% [section]
\newtheorem{nota}[thm]{Notation}% [section]
\newtheorem{prop}[thm]{Proposition}% [section]
\newtheorem{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}^{\lleq}({\cal P})}
\newcommand{\pfcR}{{\cal L}^{\leeqv}({\cal R})}
\newcommand{\efcR}{{\cal L}^{\lleq}({\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}


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


%\thispagestyle{empty}



\begin{abstract}
We describe an event-style (or poset) semantics for conflict-free rewrite
systems, including term and graph rewriting (possibly with bound
variables), the \lc\, and other stable transition systems with a residual
relation. Our interpretation is based on considering redex-families as
events. It treats permutation-equivalent reductions as representing the
same concurrent computation. Due to erasure of redexes, Event Structures
are inadequate for such an interpretation. We therefore extend the Prime
Event Structure model by axiomatizing permutation-equivalence on finite
configurations in two different ways, for the conflict-free case, and
show that these extended models are equivalent to known stable transition
models with axiomatized residual and family relations.
\par
\vspace{0.5cm}
\noindent An extended abstract of this paper appears in Proc. of
MFCS'97~\cite{[mfcs]}.
\par
\vspace{0.5cm}
\noindent {\footnotesize \copyright~Z. Khasidashvili \& J. Glauert, UEA
Norwich, 1997}
\end{abstract}


\section{Introduction}

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

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

Recent advances in the abstract study of orthogonal rewrite
systems~\cite{[Sta],[GLM],[rndrs],[dndrs],[ldrs]} allow us to address
the problem in an \emph{entirely} abstract setting. Stable Deterministic
Residual Structures (SDRSs) and Deterministic Family Structures (DFSs)
model computation in orthogonal rewrite systems. DRSs are Abstract
Rewrite Systems with an axiomatized residual relation; DFSs are DRSs
where in addition the concept of redex-family is axiomatized. Stable DRSs
allow~\cite{[rndrs]} proofs of 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 the event
structure interpretation of DRSs based on interpreting families as
events.

\zurab{
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
reduction graph of the term $t=F[x]H(G(x))$. Let $P:F[x]H(G(x))\ar
H(G(H(G(x))))\ar H(G(a))$ and $v=G(a)$. Then the redex $Pv$ has a
corresponding event in the corresponding PES $(FAM(R),\contre)$, but no
family-reduction can create redexes in $Fam(Pv)$.
$F[x]H(G(x))\ar H(G(H(G(x))))$, $F[x]H(G(x))\ar H(G(H(G(x))))\doar a$, and
$F[x]H(G(x))\ar F[x]a \ar a$ are all family-reductions in $R$, but neither
contracts $Fam(Pv)$.
}
Since we want events in the corresponding DPES of $\cal F$ to match
precisely the families contracted in family-reductions in $\cal F$, we
first associate an AZDFS $\lin{{\cal F}}$ to a DFS $\cal F$, called the
\emph{implementation} of $\cal F$, and interpret $\cal F$ in the DEESor
DPES corresponding to $\lin{{\cal F}}$. The reduction steps in $\lin{{\cal
F}}$ correspond to family-reduction multi-steps of $\cal F$.
}


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


To view a process as the domain of all its configurations, an
\emph{adequacy} requirement is desirable. Namely, that \emph{runs} of a
(finite) 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 \emph{permutation} or \emph{L\'evy}
equivalence~\cite{[le80]} to the whole theory of (not only orthogonal)
rewrite systems~\cite{[H.L.],[Bou]}, and to concurrency theory as
well~\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. However, this is clearly impossible in the
present PES framework~\cite{[Win89]}, as a configuration in a PES has
only a finite number of runs while, for example, a \pc\ class of a
(finite) reduction may have an infinite number of elements.


In order for an equivalence relation to satisfy the adequacy requirement,
the corresponding equivalence classes of (finite) reductions must be
partially ordered so as to form distributive lattices, since the domains
of (finite) configurations of a PES ordered by inclusion are such
lattices~\cite{[Win89]}. However, it is well known that L\'evy's
reduction space is not in general a lattice, \footnote{(Recursive Program
Schemes are an 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 this problem.
Laneve~\cite{[Lan.th]} introduces \emph{distributive} equivalence on
$\beta$-reductions which only allows permutation of steps that cannot
erase or duplicate one another, and consequently all equivalent sequences
have the same length.  Kennaway et al~\cite{[KKSdV]} work with
permutation equivalence for orthogonal Term Graph Rewriting, but they
only restrict themselves to needed events of a normalizable term to cope
with problems with erasure. As needed redexes cannot be erased, all
needed normalizing reductions are of the same length, and on needed
reductions, the permutation and distributive equivalences coincide (since
the system is affine). Similarly, Clark and Kennaway~\cite{[C.K.]} work
with \pc\ and allow infinite reductions but restrict themselves to
standard reductions only. Schied~\cite{[Sch]} and Corradini et
al~\cite{[CEL]}  work with linear rewrite systems (no duplication, no
erasure), mainly graph grammars, and do not therefore encounter the erasure
problems.


In order to cope with the adequacy problem, we extend the PES model by
axiomatizing \pc\ on event configurations. We do it in two different
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 numbers of events but still representing
the same \pc\ class of reductions.  We show that \pc\ classes of
configurations in a DPES/DEES, appropriately ordered, are isomorphic to
L\'evy's reduction space of the corresponding ASDRSs, and therefore the
former give a \emph{fully adequate} semantics to ASDRSs.


The paper is organized as follows. In the next section, we review the
existing theory of DRSs and DFSs used in this paper. In
section~\ref{dees.dpes.} we introduce DPESs and DEESs and establish their
equivalence. In section~\ref{rel.mod.} we relate the latter event models
with affine SDRSs and zig-zag DFSs, showing the equivalence of the four
models. In section~\ref{latt.str.}, we define L\'evy-embedding on
configurations in a DPES/DEES and show its isomorphism with L\'evy's
reduction space of the corresponding ASDRS. Conclusions appear in
section~\ref{concl.}.





\section{Deterministic Residual and Family Structures}



In this section we recall some basic theory for \emph{Deterministic
Residual Structures} (DRSs) and \emph{Deterministic Family Structures}
(DFSs), developed in~\cite{[rndrs],[dndrs],[ldrs]}. 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.



\bd
(\cite{[Hin]}) An ARS is a triple $A$ = ({\em Ter},{\em Red},$\ar$)
where {\em Ter} is a set of {\em terms}, ranged over by
$t,s,o,e$; {\em Red} is a set of {\em redexes} (or {\em redex occurrences}),
ranged over by $u,v,w$; and $\ar:Red\mapsto (Ter\times Ter)$ is a function
such that for any $t\in Ter$ there is only a finite set of $u\in Red$ such
that $\ar(u)=(t,s)$, written $t\red{u}s$. This set will be known as the
redexes of term $t$, where $u\subt t$ denotes that $u$ is a member of the
redexes of $t$ and $U\subts t$ denotes that $U$ is a subset of the redexes.
Note
that $\ar$ is a {\em total\/} function, so one can identify $u$ with the
triple $t\red{u}s$. \footnote{Klop's ARSs~\cite{[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, and other conflict-free transition systems
with a reasonable level of abstraction. In contrast, ARSs of~\cite{[GLM]}
do not cover orthogonal Term Graph Rewriting Systems~\cite{[SPE]}, for
example, and Interaction Nets~\cite{[Laf]}, which form DRSs (when
restricted to finite nets), do not have or need any nesting order on
redexes (as nets are undirected, possibly cyclic, graphs).

DRSs axiomatize exactly the properties of residuals which are used
in~\cite{[le80],[H.L.]} to define permutation equivalence on reductions,
and the L\'evy-embedding relation on permutation-equivalence classes which
is used to construct L\'evy's reduction space. Hence DRSs are the minimal
axiomatization of the residual concept enabling one to relate the
operational and denotational semantics of orthogonal rewrite systems.


\bdl{D.levy.str.}
{\bf (Deterministic Residual Structure~\cite{[rndrs]})} 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 $u/P$ of residuals of $u$ under any reduction $P$ is defined by
transitivity.

A \emph{development} of $U\subts t$ is a reduction $P:t\doar $ that only
contracts residuals of redexes from $U$; it is \emph{complete} if
$U/P=\cup_{u\in U}\,u/P=\emptyset$. Development of $\emptyset$ is
identified with the empty reduction. $U$ will also denote a complete
development of $U\subts t$. The residual relation satisfies the following
two axioms:

$\bullet$ [FD] (Finite Developments,~\cite{[GLM]}) All developments are
terminating; all complete developments of $U\subts t$ end at the same term;
and residuals of a redex $v\subt t$ under all complete developments of $U$
are the same.

$\bullet$  [weak acyclicity] (\cite{[Sta]}) Let $u,v\subt t$, let $u\not=
v$, and let $u/v=\emp$. Then $v/u\not=\emp$.\footnote{This axiom is called
[acyclicity] in~\cite{[rndrs]}, and is axiom~(4) in~\cite{[Sta]}.}

We call a DRS $\cal R$ \emph{stable} (SDRS) if:
\delete{the following axiom is satisfied: (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 along $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$.
Intuitively, $P\lleq Q$ expresses that $Q$ does more work than $P$,
 and $Q/P$ is the part of $Q$ that remains from it after $P$.
Finally, one shows that for any co-initial reductions $P,Q$, $P\sqcup
Q\leeqv Q\sqcup P$, where $P\sqcup Q=P+Q/P$, and is the greatest lower
bound of $P$ and $Q$ in the reduction space ordered by L\'evy's embedding
relation $\lleq$.
The above relations can equivalently be defined also using Klop's method of
commutative diagrams~\cite{[Kl.CRS],[Bar]}.


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



\bdl{D.ext.reductions.}
$\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)}
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)}
Let $P,Q$ be co-initial finite reductions in a DRS, and
let $P$ be external to $Q$. Then $Q\not\leeqv P$.
\el


\bdl{D.DRS.}
{\bf (Deterministic Family Structure~\cite{[rndrs]})} 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$ [FFD] Any reduction that contracts redexes of a finite
number of families is terminating.\footnote{This axiom is called
[termination] in~\cite{[rndrs]}. Here FFD stands for \emph{Finite Family
Developments}.}


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

We call a DFS \emph{separable}, SDFS, if, for any redex $Pv$, $v$
cannot create two different redexes in the same family. That is, if $v$
creates $w',w''$ and $w'\not= w''$, then $Fam((P+v)w')\not= Fam((P+v)w'')$.
\ed


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


Recall that a  multistep reduction $P:t_0\doar t_1\doar\ldots\doar t_n$ is
called a \emph{family-reduction} if each $P_i:t_i\doar t_{i+1}$ is
a development of a set $U_i$ of redexes belonging to the same
family. The family-reduction $P$ is \emph{complete} if each $P_i$ is
the complete development of a maximal set of redexes of $t_i$
belonging to the same family. As we have already mentioned, we have the
following lemma enabling event structure interpretation of DFSs associating
events to families:


\begin{lem}\em
\label{L.fam.compl.}
({\bf Unique Families}) Every family is contracted at most once in a complete
family-reduction.
\el

We will only consider complete family-reductions, and will omit `complete'.


\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{reduction graph} of a
term, called the \emph{initial} term, i.e., the set of terms to which the
initial term is reducible. The initial term will often be denoted by
$\emp$, by analogy with the initial state in an Event Structure, although
$\emp$ will also be used to denote empty reductions. Further, in DFSs,
families will always be considered relative to $\emp$, i.e., all histories
start with $\emp$.
Unless otherwise stated, by a \emph{reduction} we mean a \emph{finite}
reduction. Reductions starting from $\emp$ will also be called
\emph{initial} reductions.






\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)$.
\incl{that $u$ is \emph{$Q$-needed}, or more precisely, $P'u$ is
\emph{$Q$-needed}, if $u$ is $Q/P'$-needed.}
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



\incl{
\bll{L.era.and.ess.im.ne.}
Let $P:s\doar t\red{u}e\doar o$ in an ASDRS.

(1) $w\in t$ is $P$-needed iff it is $P$-erased and $P$-essential.

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

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

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



Self-needed reductions play the role of \emph{standard} reductions in
SDRSs, and the following algorithm is a standardization procedure for
reductions in ASDRSs.
Let $P:t\doar s$. The {\em canonical standard variant of $P$},
$ST(P)$, is defined as follows: If $P=\emp$, when so is $ST(P)$. Otherwise,
let $v\subt t$ be such that it is $P$-needed and its residual is contracted
in $P$ first among $P$-needed residuals of $P$-needed redexes in $t$
(existence of such $v$ follows from \Lr{L.era.and.ess.im.ne.}). Then
$ST(P)=v+ST(P/v)$. We write $Q\in\stav{P}$ if $Q\in\stan$ and $Q\leeqv P$,
where $\stan$ denotes the set of all standard reduction, and call $Q$ a
\emph{standard variant} of $P$. In particular, $ST(P)\in\stav{P}$.


\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





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



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

In this section we recall the 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\lleq Q$ iff $\exists Q'\leeqv Q: FAM(P)\ssq FAM(Q')$, and $P\leeqv
Q$ iff $SFAM(P)=SFAM(Q)$. Further, $SFAM(P)=FAM(ST(P))=\cap_{N\leeqv P}
FAM(N)$. Consequently, if $P,Q\in\stan$, then $P\leeqv Q$ iff
$FAM(P)=FAM(Q)$ (since in that case $P=ST(P)$ and $Q=ST(Q)$).
\ep



\btl{T.lin.dr.sta.df.}
{\bf (Affine 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$. Further, ${\cal F_R}$ is the only
separable DFS with $R$ as the underlying SDRS, and in general, an affine
DFS is separable iff it is a zig-zag DFS.
\et


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



The above two theorems enable us to associate an AZDFS $\lin{{\cal F}}$ to
a DFS $\cal F$, called the \emph{implementation} of $\cal F$. The reduction
steps in $\lin{{\cal F}}$ correspond to (complete) family-reduction
multi-steps of $\cal F$ (i.e., multi-steps contracting maximal sets of
redexes of some family).


\bdl{D.lin.dfs.drs.}
(\cite{[acoi]})  Let ${\cal F}=({\cal R},\fami,\contr)$ be a DFS. The
\emph{L\'evy implementation} or simply \emph{implementation} of ${\cal F}$
is the AZDFS $\lin{{\cal F}}=({\cal R}_I,\fami_I,\contr_I)$, where

$\bullet$ the branches of the reduction graph of the underlying ARS $A$ of
${\cal R}_I=(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 families, in a term $s$, and let $U:s\ar
o$ be the multi-step contracting $U$. Then $V/U$ is the multi-step $o\ar e$
contracting all members of the set $V/U$.

$\bullet$ the family and contribution relations $\fami_I,\contr_I$ are
those induced by $\fami$ and $\contr$.
\ed



\btl{T.line.zig.}
(\cite{[acoi]}) For any DFS ${\cal F}$, $\lin{{\cal F}}$ is an AZDFS.
\et




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



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


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


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


We only consider \emph{conflict-free} or \emph{deterministic} PESs, where
no event can prevent others from occurring, and therefore the consistency
predicate is the set of all finite subsets of $E$, $Fin(E)$, and will be
omitted. Finite \emph{configurations} of ${\cal E}$ are finite
\emph{left-closed subsets} $\alpha,\beta,\ldots$ of $E$, i.e., subsets
$\fcE=\{\alpha\ssq Fin(E)\,\vert\, e\in \alpha\,\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 ${\cal E}=(E, \leq)$ is a conflict-free
PES and $\leeqv\ssq \fcE \times \fcE$ is an equivalence relation, called
\emph{L\'evy} or \emph{permutation-equivalence}, \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 \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  ${\cal E}=(E,\leq)$ is a conflict-free PES and
$\rhd\ssq \fcE \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
\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] $\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$.  (The subscript $\rhd$ in
$ST_{\rhd}(\alpha)$ will often be omitted.) $\sea$ will be called the
\emph{standard variant} of $\alpha$.
\ed



A close inspection of the above definitions shows that the DPES axiom [P0]
is a counterpart of the DEES axioms [E0] and [E4], and similarly for [P3]
and [E3].  Further, the combination of [P1] and [P2] have the same effect
as that of [E1] and [E2]. [E4] does not have a `direct' counterpart among
DPES axioms, but it corresponds to the fact that, according to
\Dr{D.red.need.ess.}, a redex with history $Pv$ is $Q$-inessential iff $v$
is $Q/P$-inessential. Similarly, [P0] corresponds to
\Lr{L.era.and.ess.im.ne.}.(2).



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


\bll{L.se.con.}
Let $\alpha\in \fcC$, in a DEES. 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.}
Let $\alpha\in \fcC$, in a DEES $\cal C$. Then $\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$. Denote
$e=e_0$. By the definition of $\sea$ and the assumption, we have
$\alpha_n\rhd e_i$ for all $i=0,1,\ldots,n$. By [E2], we have from
$\alpha_n\rhd e_n$ and $\alpha_n\rhd e_i$ that $\alpha_{n-1}\rhd e_i$.
Hence, again by [E2], $\alpha_{n-2}\rhd e_i$, and so on. Finally, we get
$\alpha_0\rhd e_i$ for all $i$, and in particular, $\alpha_0\rhd e$. \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$.

\bproof
\suf\  By \Dr{D.eq.in.era.}, since $\beta\setminus\alpha\ssq \beta\setminus
ST(\alpha)$. \nec\
Since $\beta\era \beta\setminus\alpha$, $\seb\ssq\alpha$. Let $e'\in \seb$.
Then $e'\in\beta$ and $\beta\not\era e'$, implying by [E1] and
$\alpha\ssq\beta$ that $\alpha\not\era e'$, i.e., $e'\in \sea$. Hence
$\seb\ssq\sea$. For the converse, take $e''\in\sea$. Then $e''\in\alpha$
and $\alpha\not\era e''$. Therefore, $e''\in\beta$ and by [E1]
$\seb\not\era e''$, implying by \Lr{L.alp.eq.sel.al.} that $\beta\not\era
e''$, i.e., $e''\in\seb$. Hence $\sea=\seb$.
\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
\gamma\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$.
\eproof
\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].

[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\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 $\sea=\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$. \zurab{By \Lr{L.alp.eq.sel.al.},
$\sea\not\era e$ implies $\alpha\not\era e$, thus $e\in\sea$ iff
$e\in\alpha$, and therefore
$\alpha+e\setminus(\sea+e)=\alpha\setminus\sea$.}
Hence $\alpha+e\era \alpha+e\setminus(\sea+e)$ by [E1] (as $\alpha\era
\alpha\setminus\sea$), and we have by \Pr{C.char.sea.eq.} that
$ST(\alpha+e)=ST(\sea+e)$, thus $\alpha+e\eleeqv\sea+e$ by
\Dr{D.eq.in.era.}. Similarly, $\beta+e\eleeqv\seb+e$, implying
$\alpha+e\eleeqv\beta+e$ (since $\sea=\seb$).

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



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

\bproof
We need to show that $\lrhd$ satisfies the erasure axioms [E0] -- [E4].
\incl{[E0] follows from  \Dr{D.era.vi.per.eq.} and [P0], and [E4] is
immediate from \Dr{D.era.vi.per.eq.}. Proofs of the other axioms are not
too long, but are   tedious to include here.}


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

[E3]: Let $\alpha\lrhd e$ and $e<e'$. We want to show that $\alpha\lrhd
e'$. We can assume that $\not\exists e'': e<e''<e'$.  Assume first that
$e,e'\in\alpha$ (hence $\alpha\cup\con{e}=\alpha\cup\con{e'}=\alpha$). By
\Dr{D.era.vi.per.eq.}, $\alpha\lera e\imply \alpha\leeqv
\alpha\setminus\coni{e}$. But $\alpha\setminus\coni{e}\ssq
\alpha\setminus\coni{e'}\ssq\alpha$, implying by [P1] that
$\alpha\leeqv\alpha\setminus\coni{e'}$, i.e., by \Dr{D.era.vi.per.eq.},
$\alpha\lera e'$. Now let $e\in\alpha$ and $e'\not\in\alpha$. Let
$\gamma=\alpha\setminus\oconi{e}$. By \Dr{D.era.vi.per.eq.}, $\alpha\lera
e$ iff $\gamma\lrhd e$ 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.


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


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

[E2]: We can assume that $e'\in\alpha$. Let $\alpha\lrhd e'$,  $\alpha\lrhd
e$ and $\alpha-e'\in\fcE$. By \Dr{D.era.vi.per.eq.}, $\alpha\lera
e\Rightarrow \alpha\cup\con{e}\leeqv \alpha\cup\con{e}\setminus \coni{e}$
and $\alpha\lrhd e'\Rightarrow \alpha\leeqv \alpha-e'$, implying by
repeated application of [P2] that $\alpha\cup\con{e}\leeqv
\alpha-e'\cup\con{e}$. \delete{Obviously, either $e\leq e'$, $e'<e$, or
$e\not\leq e'\wedge e'\not< e$, and in the latter case either $e\in\alpha$
or $e\not\in\alpha$.} One easily checks that $(\alpha\cup\con{e}\setminus
\coni{e})\cap (\alpha-e'\cup\con{e})=
(\alpha\cup\con{e})\cap (\alpha-e'\cup\con{e})\setminus \coni{e}=
\alpha-e'\cup\con{e}\setminus \coni{e}$ implying by [P1] that
$\alpha-e'\cup\con{e}\leeqv \alpha-e'\cup\con{e}\setminus \coni{e}$. Hence,
$\alpha-e'\lera e$ by \Dr{D.era.vi.per.eq.}.


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


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

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



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


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

\bproof
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$, and by \Lr{L.al.le.se.al.} $\alpha\leeqv
ST_{\lrhd}(\alpha)$. 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) 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) 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 Conflict-Free Transition and Event models}
\label{rel.mod.}


We now define translations of ASDRSs and AZDFSs 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 ZDFSs into DPESs and DEESs}




\bdl{D.tra.dfs.dps.}
To \zurab{an ASDRS $\cal R$ and its corresponding} AZDFS ${\cal
F}=\calF_\calR=({\cal R},\zfami,\zcontr)$, we associate the DPES ${\cal
P}_{{\cal R}}={\cal P}_{{\cal F}}=\calP_{\calF_\calR}=(E_{{\cal
F}},\leq,\leeqv)$, and the DEES ${\cal C}_{{\cal R}}={\cal C}_{{\cal
F}}=\calC_{\calF_\calR}=(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 \zcontr \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$ (see \Tr{P.on.ca.for.});


\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




\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}$, let
$Qv,Q'v'\in\phi$, and let $Qv$ be canonical. If $Qv$ is $P$-inessential,
then so is $Q'v'$. Further, if $Q'\lleq P$, then the converse is also
true.\footnote{We will only need the converse statement in
Section~\ref{latt.str.}.}

\bproof
By the Affine Extraction Theorem, there is $Q''$ such that $Q'\leeqv Q+Q''$
and $v'=v/Q''$. If $Qv$ is $P$-inessential, then $ST(P)/Q$ discards $v$ by
\Lr{C.sta.dis.}, and $ST(P)/Q'$ discards $v'$ by CR for residuals.
Conversely, if $Q'\lleq P$, then $Q''/(P/Q)=\emp$, and
$v'/(P/Q')=v/(P/Q)=\emp$, which means that $Q'v'$ is $P$-inessential.
\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
}



\bll{L.reor.fam.}
Let $P\in\stan$, $FAM(P)=F_1\cup F_2$, $F_1\cap F_2=\emp$ and $\forall
\phi\in F_2, \forall \psi\in F_1:\phi\not\contr \psi$. 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 [E0] -- [E4].


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



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

\btl{T.tran.ev.}
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 AZDFSs 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 P}$ ($\cal C$);

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


Next we show that the translations of DEESs and DPESs into ASDRSs commute
with the translations between DEESs and DPESs, and that the definition
above is correct. We need a lemma first.


\bll{L.add.eras.}
Let ${\cal C}=(E,\leq,\era)$ be a DEES, let ${\cal P}=(E, \leq,\leeqv)$ be
a DPES, let $\alpha, \alpha+e\in FConf(\cal E)$, and let $e\not\in\alpha$.
Then

(1) $\alpha\era e$ iff $\alpha +e\eleeqv\alpha$.

(2) $\alpha\lrhd e$ iff $\alpha +e\leeqv\alpha$.

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

(2) By \Dr{D.era.vi.per.eq.}, $\alpha\lrhd e$ iff $\alpha\cup\con{e}\leeqv
\alpha\cup\con{e}\setminus\coni{e}$. But $e\in\alpha$, hence
$\alpha\cup\con{e}=\alpha+e$ and
$\alpha\cup\con{e}\setminus\coni{e}=\alpha$, implying the lemma.
\eproof
\el



\bt
Let ${\cal C}=(E,\leq,\era)$ be a DEES and ${\cal P}=(E, \leq,\leeqv)$ be a
DPES. Then

(1) ${\cal R_C}={\cal R_{P_C}}$;

(2) ${\cal R_P}={\cal R_{C_P}}$;

(3) ${\cal R_C}$ and ${\cal R_P}$ are indeed ASDRSs.


\bproof
(1) Immediate from \Dr{D.ps.rs.tra.} and \Lr{L.add.eras.}.(1).

(2) Immediate from \Dr{D.ps.rs.tra.} and \Lr{L.add.eras.}.(2).

(3) By (1) and (2), it is enough to show that ${\cal R_P}$ is an ASDRS,
i.e., we need to check that ${\cal R_P}$ does indeed satisfy the residual
axioms of stable DRSs.

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

(a) Let $\alpha\leeqv \alpha+e_i$, $i=1,\ldots, k$. Then $\alpha\leeqv
\alpha+e_1+\ldots+e_k$.

{\it Proof of (a)}: By induction on $k$. The case $k=1$ is trivial. Let
$\beta=\alpha+e_1+\ldots+e_{k-2}$.  By the induction assumption,
$\alpha\leeqv\beta\leeqv\beta+e_{k-1}\leeqv\beta+e_k$. By [P2],
$\beta+e_{k-1}+e_k\leeqv\beta+e_k$. Hence, $\alpha\leeqv\beta+e_{k-1}+e_k$.

[FD] let $U=\{(\lclas{\alpha},e_i)\,\vert\, i=1,\ldots, l\}$ be a set of
redexes in $\lclas{\alpha}$. Then a complete development of $U$ has a form
$P:\lclas{\alpha_0}\red{(\lclas{\alpha_0},e_{i_0})}\lclas{\alpha_1}\red{(\lc
las{\alpha_1},e_{i_1})}\ldots\ar\lclas{\alpha_k}$, where
$\alpha_k=\alpha_0+e_{i_0}+\ldots+e_{i_{k-1}}$, and for any
$m\not=i_0,\ldots,i_{k-1}$, $(\lclas{\alpha_0},e_m)/P=\emp$, that is,
$\lclas{\alpha_k}=\lclas{\alpha_k+e_m}$. Hence, by (a),
$\lclas{\alpha_k}=\lclas{\alpha+e_1+\ldots+e_l}$, i.e., every complete
development of $U$ ends at $\lclas{\alpha_k}$. For any $u=(\lclas{\alpha},
e)$, $u/P=(\lclas{\alpha_k},e)$, i.e., $u/U$ does not depend on the
particular complete development of $U$, hence [FD] holds.

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


[stability] Suppose on the contrary that $R_{\cal C}$ is not stable. Then
there are $u\not=v$, $w$, $w'$ and $w''$ such that $w$ and $w'$ are created
by $u$ and $v$ respectively,  and $w''=w/v'=w'/u'\not=\emp$, where $u'=u/v$
and $v'=v/u$. That is, there are  $u=(\lclas{\alpha},e)$,
$v=(\lclas{\alpha},e')$, $w=(\lclas{\alpha+e},e'')$,
$w'=(\lclas{\alpha+e'},e'')$, and $w''=(\lclas{\alpha+e+e'},e'')$ such that
$\lclas{\alpha}$, $\lclas{\alpha+e}$ and $\lclas{\alpha+e+e''}$ are
different; so are $\lclas{\alpha}$, $\lclas{\alpha+e'}$ and
$\lclas{\alpha+e'+e''}$; and
$\lclas{\alpha+e+e'}\not=\lclas{\alpha+e+e'+e''}$ (see the diagram).
Further, $(\lclas{\alpha},e'')$ is not a redex since $w$ is a created
redex. Hence either $\alpha+e''\not\in FConf(\cal C)$, or $\alpha+e''\in
FConf(\cal C)$
and  $\alpha\leeqv\alpha+e''$; but the latter would imply by
\Lr{L.add.eras.} and [erasure~1] that $\alpha+e+e''\leeqv \alpha+e$,
contradicting the fact that $w$ is a non-empty redex. Thus $\alpha+e+e''$
and $\alpha+e'+e''$ are both configurations, but their intersection
$\alpha+e''$ is not  -- a contradiction, since the intersection of
left-closed subsets remains left-closed.

\begin{diagram}[height=1.6em,width=1.6em]
\lclas{\alpha} & \rTo^u   &\lclas{\alpha+e}  & \rTo^w  & \lclas{\alpha+e+e''} \\
 \dTo^v &              &  \dTo_{v'}  &                 & \dTo      \\
\lclas{\alpha+e'} & \rTo_{u'} & \lclas{\alpha+e+e'} &                  &    \\
\dTo^{w'}  &            &                &  \rdOnto^{w''}  &   \\
\lclas{\alpha+e'+e''} & \rTo  &            &       &\lclas{\alpha+e+e'+e''} \\
\end{diagram}

The theorem is now proved.
\eproof
\et




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, where $e_i$ represents the \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. Such enumerations
will be called \emph{quasi-reductions}. Quasi-reductions are defined
similarly in any DRS, as `reductions containing empty steps corresponding
to erased redexes'.


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




\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. (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\leeqv\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'}$ simply means that $e< e'$. Hence in order to prove
$\phi_e\zcontr\phi_{e'}\Leftrightarrow \phi_e\pcontr\phi_{e'}$ it is enough
to show that $e<e' \Leftrightarrow 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$, and $\gamma+e'$ is the
smallest configuration containing $e'$. If on the contrary $e\not<e'$, then
$\gamma'=\{e^*\,\vert\, e^*\leq e'\}$ is clearly a configuration containing
$e'$, and  $\gamma+e'\not\ssq \gamma'$, contradicting the minimality of
$\gamma+e'$.
\eproof
\et




\subsection{Equivalence of the four models}





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

Let $\calR$ be a DRS. Let us define the \emph{reduction tree} of $\calR$ to
be a tree whose nodes are labelled with terms in $\calR$, whose root is
labelled with $\emptyset$, the initial term of $\calR$, and whose arcs
correspond to redexes in $\calR$. Thus sons of a node are target terms of
redexes whose source term is the label of that node. (Reduction trees are
considered up to the order of arcs coming out of a node: the order in which
the arcs are drown is irrelevant.) Note that different nodes can be
labelled with the same term, so even if $\calR$ has cycles, its reduction
tree is a tree. Thus the branches of the reduction tree of $\calR$ are in
$1-1$ correspondence with initial reductions in $\calR$. We call two such
trees \emph{isomorphic} if the trees obtained by removing all labels are
the same, i.e., there is a $1-1$ correspondence between nodes and arcs of
the two trees such that the sources and target nodes of corresponding arcs
are corresponding nodes.



\bdl{D.drs.isom.}
(1) We call DRSs ${\cal R}=(A,/)$ and ${\cal R}'=(A',/')$ \emph{isomorphic}
if there is an isomorphism between reduction trees 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}'$ \zurab{(hence, an isomorphism between redexes with
histories in $\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




\bll{L.dpred.drred.}
Let $\calF$ be an AZDFS and let $\calP_\calF$ be its corresponding DPES.

(1) For any reduction $\rs{\alpha}=e_0, e_1,\ldots,e_n$ in $\calP_\calF$ the
re is an initial reduction
$g(\rs{\alpha})=P:\emp=t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{n-1}}t_n$ in
$\calF$ such that $Fam(P_iu_i)=e_i$, where
$P_i:\emp=t_0\red{u_0}t_1\red{u_1}\ldots\red{u_{i-1}}t_i$. (Thus
$FAM(P)=\alpha$.)

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

(3) the translation functions $g$ and $f$ between reductions in $\calF$ and
$\calP_\calF$ commute: for any finite initial reduction $P$ in $\calF$,
$f(g(P))=P$.


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

(2) We need to show that $f(P)=e_0, e_1,\ldots,e_n$ is left-closed and does
not contain vacuous events (by \Dr{D.tra.dfs.dps.}, $\phi_i=e_i$ are events
in $\calP_\calF$). By [contribution], $P_i$ contracts at least one redex in
every contributor family of $\phi$, hence $f(P)$ is left-closed. If on the
contrary say $\phi_j$ was vacuous, i.e., $\{\phi_0,\ldots,\phi_{j-1}\}\era
\phi_j$, then by \Dr{D.tra.dfs.dps.} there is an initial reduction $Q$ such
that $FAM(Q)\ssq \{\phi_0,\ldots,\phi_{j-1}\}$ and $Q$ discards a canonical
element $Nv$ of $\phi_j$. By \Pr{P.leqv.sam.se.es.fa.}, $Q\lleq P_j$, i.e.,
$P_j\leeqv Q+Q'$ for some $Q'$. Let $Q_j=Q_Q'$. It follows easily from
\Dr{D.red.need.ess.} that $Q_j$ would discard $Nv$ as well; thus
$v/(Q_j/N)=\emp$. But $N/Q_j=\emp$, thus the final term of $(Q_j/N$
contains the redex $u_j\in\phi_j$ (see the figure), which must be a
residual of $v$ by Lemma 5.2 of~\cite{[ldrs]} -- a contradiction.
\begin{diagram}[height=1.5em,width=1.5em]
\emp         &\rOnto^{P_j}& & t_j       &\rTo^{u_j}   &   {}\\
\dOnto<{N}&            & &\dOnto<{\emp}&         &      \\
{}     &\rOnto^{P_i/Q_j}& & {}    & \rTo^{u_{j}} & {}   \\
\dTo<{v}   &         & &   &             &     \\
{}      &      & &  {}       &       & {}   \\
\end{diagram}

(3) Immediate from the constructions in (1) and (2).
\eproof
\el



\bll{L. red.dp.df.}
Let $\calP$ be a DPES, and let $\calF_\calP$ be its corresponding AZDFS.
Then there is a $1-1$ correspondence between initial reductions in $\calP$
and $\calF_\calP$.
\el



\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
(1) Let $\calP=(E,\leq,\leeqv)$ and $\calP=\calP_{\calF_\calP}
=(E',\leq',\leeqv')$. By \Dr{D.ps.fs.tra.} and \Dr{D.tra.dfs.dps.},
$E'=\{\phi_e\vert e\in E\}$, where $\phi_e$ is the $e$-family of ${\cal
F}_{\cal P}$, as defined in \Dr{D.ps.fs.tra.}. We show that $f:e\ar \phi_e$
is an isomorphism between $\cal P$ and $\calP'$.  Since $f$ clearly an
isomorphismbetween the event sets $E$ and $E'$ of $\calP$ and $\calP'$, we
need to show that (a) $e\leq e'$ iff $\phi_e\leq'\phi_{e'}$; and (b)
$\alpha\leeqv \beta$ iff $\phi_\alpha \leeqv' \phi_\beta$, where
$\phi_\alpha=\{\phi_e\vert e\in\alpha\}$ and $\phi_\beta=\{\phi_e\vert
e\in\beta\}$. (a) is immediate from \Dr{D.ps.fs.tra.} and
\Dr{D.tra.dfs.dps.}. For (b), first note that by \Tr{T.tran.ev.} and
\Tr{T.ps.dr.fs.zig.}, $\calF_\calP$ is an AZDFS and $\calP_{\calF_\calP}$
is a DPES. Hence we have from \Dr{D.tra.dfs.dps.} that $\phi_\alpha \leeqv'
\phi_\beta$ iff $\forall e\in \alpha\cup\beta\setminus\alpha\cap\beta$,
there is a reduction $P$  in ${\calF_\calP}$ such that $FAM(P)\ssq
\phi_\alpha\cap\phi_\beta$ and $P$ discards a canonical element $P'e$ of
$\phi_e$. By \Dr{D.red.need.ess.} and \Dr{D.ps.rs.tra.}, the latter means
that $P$ is a left-closed sequence of (non-vacuous) events
$\rs{\gamma}=e_1,\ldots,e_k$ not containing $e$, and if $P'$ is a sequence
$e'_1,\ldots,e'_m$, then $\{e_1,\ldots,e_k\}\cup\{e'_1,\ldots,e'_m\}\leeqv
\{e_1,\ldots,e_k\}\cup\{e'_1,\ldots,e'_m\}+e$. Since $P'e$ is canonical, we
have by \Tr{P.on.ca.for.} that $\{e'_1,\ldots,e'_m\}=\ocon{e}$. Since
$e\not\in\gamma$, $\gamma\cup \ocon{e}=\gamma\cup\con{e}\setminus\coni{e}$,
thus it is enough to prove that $\alpha\leeqv\beta$ iff $\forall e\in
\alpha\cup\beta\setminus\alpha\cap\beta\,\,\exists
\rs{\gamma}.\gamma\ssq\alpha\cap\beta\wedge \gamma\cup\con{e}\leeqv
\gamma\cup\con{e}\setminus\coni{e}$. \nec\ By [P2], $\forall e\in
\alpha\cup\beta\setminus\alpha\cap\beta:\, \gamma\cup\con{e}\leeqv
\gamma\cup\con{e}\setminus\coni{e}$ implies $\gamma\leeqv\alpha$ and
$\gamma\leeqv\beta$, hence $\alpha\leeqv\beta$. \suf\ By
\Pr{C.sees.eq.leeq.}, $\alpha\leeqv\beta$ implies
$ST_{\lrhd}(\alpha)=ST_{\lrhd}(\beta)$, implying by \Lr{L.sune.seeqv.} that
$\alpha\lrhd\alpha\setminus\beta$ and $\beta\lrhd\beta\setminus\alpha$.
Hence, by \Lr{L.alp.eq.sel.al.}, $ST_{\lrhd}(\alpha)\lrhd
\alpha\cup\beta\setminus\alpha\cap\beta$, implying by \Dr{D.era.vi.per.eq.}
that $\forall e\in
\alpha\cup\beta\setminus\alpha\cap\beta:\,ST_{\lrhd}(\alpha)\cup
\con{e}\leeqv ST_{\lrhd}(\alpha)\cup\con{e}\setminus\coni{e}$, and it is
enough to take $\gamma=ST_{\lrhd}(\alpha)$.


(2) By \Tr{T.ps.dr.fs.zig.} and \Tr{T.tran.ev.}, $\calF_{\calP_\calF}$ is
an AZDFS, hence it is enough to show that the underlying ASDRSs $\calR$ and
$\calR'=\calR_{\calP_\calF}$ of $\calF$ and $\calF_{\calP_\calF}$ are
isomorphic. \zurab{This follows immediately from \Lr{L.dpred.drred.} and
\Lr{L. red.dp.df.}.}

\eproof
\et


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


\section{L\'evy's 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$ in a DPES/DEES 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$. Any other left-closed enumeration of $\alpha$ will be called a
\emph{quasi-reduction}. 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.

\zurab{Below, when we speak of an erasure relation $\era$ in a DPES
$\calP=(E,\leq,\leeqv)$, we mean that $\era=\lrhd$; similarly, by a
permutation-equivalence relation $\leeqv$ in a DEES $\calC=(E,\leq,\era)$
we mean $\eleeqv$.}

Note that, unlike Prime Event Structures, not every configuration $\alpha$
in a DPES/DEES has a reduction. For example, consider the DPES/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
left-closed enumerations, such as $e_1, e_2, e'_1, e'_2$, ends either with
$e'_1$ or with $e'_2$, and we have $\{e_1,e_2,e'_2\}\era e'_1$ and
$\{e_1,e_2,e'_1\}\era e'_2$. This is not surprising as the vacuous events
in left-closed sequences correspond to empty reductions in the
corresponding ASDRS, performed in the `garbage' (erased redexes).
\zurab{Thus quasi-reductions in a DPES/DEES correspond to quasi-reductions
in the corresponding ASDRS.} However, we have the following lemma.



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

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




\bdl{D.perm.latt.}
(1) Let $\cal P$ be a DPES. Then $\pfcP=\fcP/_{\leeqv}=\{\lclasa
\,\vert\,\alpha\in\fcP\}$  and  $\efcP=(\pfcP,\lleq)$, where $\lleq$ is a
partial order defined by: $\lclasa\lleq\lclasb$ iff  $\exists
\alpha'\in\lclas{\alpha},\exists \beta'\in\lclas{\beta}:\alpha'\ssq\beta'$.


(2) Let $\cal R$ be an ASDRS. Then $\pfcR=\fcR/_{\leeqv}=\{\lclas{P}
\,\vert\,P\in\fcR\}$, where $\fcR$ is the set of initial reductions in
$\cal R$, and $\efcR=(\pfcR,\lleq)$, where $\lleq$ is L\'evy's embedding
relation.
\ed


Note that if $\lclasa\lleq\lclasb$, $\alpha\leeqv\alpha'$ and
$\beta\leeqv\beta'$, then $\lclas{\alpha'}\lleq\lclas{\beta'}$, implying
that \Dr{D.perm.latt.}.(1) is correct. Indeed, by \Dr{D.perm.latt.}.(1),
$\lclasa\lleq\lclasb$ iff $\exists\alpha''\leeqv\alpha,\exists
\beta''\leeqv\beta:\,\lclas{\alpha''}\lleq\lclas{\beta''}$ iff
$\exists\alpha''\leeqv\alpha',\exists
\beta''\leeqv\beta':\,\lclas{\alpha''}\lleq\lclas{\beta''}$ iff
$\lclas{\alpha'}\lleq\lclas{\beta'}$.


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

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

($\supseteq$) Let $\phi\in ST(FAM(P))$. Then $\phi\in FAM(P)$ and
$FAM(P)\not\era\phi$, which  by \Dr{D.tra.dfs.dps.} means that there is no
initial $Q$ with $FAM(Q)\ssq FAM(P)$ such that $Q$ discards a canonical
element $P^*v^*$ of $\phi$. In particular, $ST(P)$ does not discard
$P^*v^*$. Since $FAM(ST(P))=SFAM(P)$ by \Pr{P.leqv.sam.se.es.fa.}, and
since $\phi\in FAM(P)$, we need to show that the redex of $\phi$ contracted
in $P$, say $P'v'$, is $P$-essential (hence $P$-needed by
\Lr{L.era.and.ess.im.ne.}.(1)). If on the contrary $P'v'$ was
$P$-inessential, $P^*v^*$ would be $P$-inessential too by
\Lr{L.dis.can.al.}, and $ST(P)$ would discard $P^*v^*$ by \Lr{C.sta.dis.}
-- a contradiction.
\eproof
\el


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

\bproof
\suf\ First note that, by [contribution] and the definition of $\leq$
(\Dr{D.tra.dfs.dps.}), $FAM(Q)$ and $FAM(Q')$ are left-closed sets of
events in $\calP_\calF$, hence are configurations. By \Dr{D.tra.dfs.dps.},
in order to prove $FAM(Q)\leeqv FAM(Q')$, we need to show that for any
$\phi\in FAM(Q)\cup FAM(Q')\setminus FAM(Q)\cap FAM(Q')$, some initial
reduction $P$ with $FAM(P)\ssq FAM(Q)\cap FAM(Q')$ discards a canonical
element $Nv$ of $\phi$. Take $P=ST(Q)$. By \Pr{P.leqv.sam.se.es.fa.},
$FAM(P)\ssq FAM(Q)\cap FAM(Q')$. Let $Q^*v^*$ be an element of $\phi$
contracted in $Q$ (hence $Q^*$ is an initial part of $Q$). Since by
\Pr{P.leqv.sam.se.es.fa.} $\phi\not\in FAM(P)=SFAM(Q)$, $Q^*v^*$ is
$Q$-unneeded, hence $Q$-inessential by \Lr{L.era.and.ess.im.ne.}.(1) (since
$v^*$ is erased in $Q$). Hence, by \Lr{C.sta.dis.}, $P$ discards $Q^*v^*$.
By the Affine Extraction Theorem (\Tr{P.on.ca.for.}), $\exists
N':N+N'\leeqv Q^*$ and $v^*=v/N'$. Since $Q^*\leq Q\leeqv P$,
$N'/(P/N)=\emptyset$, hence $v/(P/N)=v^*/(P/Q^*)=\emp$. Since $\phi\not\in
FAM(P)$, $P/N$ is external to $v$, which means that $P$ discards $Nv$.

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



\bll{Lred.fr.conf.}
Let $\calF$ be an AZDFS and let $e_0, e_1,\ldots,e_n$ be an enumeration of
a configuration $\alpha$ in the corresponding DPES $\calP_\calF$. Further,
let $e_{i_0},\ldots,e_{i_m}$ be obtained from $e_0, e_1,\ldots,e_n$ by
eliminating all vacuous events, i.e., $e_j\in \{e_{i_0},\ldots,e_{i_m}\}$
iff $\{e_0, \ldots,e_{j-1}\}\not\era e_j$. Then $e_{i_0},\ldots,e_{i_m}$ is
a reduction in $\calP_\calF$ \zurab{and $e_{i_0},\ldots,e_{i_m}\leeqv
e_0,\ldots,e_n$.}

\bproof
Since $\{e_0, \ldots,e_{i_k-1}\}\not\era e_{i_k}$,
$\{e_{i_0},\ldots,e_{i_{k-1}}\}\not\era e_{i_k}$ by [E1] (which holds for
$\era=\lera$ by \Tr{T.tra.dpe.dee.}). Further, if there were $l,k$ such
that $e_l<e_{i_k}$  and $l\not= e_{i_0},\ldots,e_{i_{k-1}}$, then we would
have by [E1] that $e_0,\ldots,e_{j-1}\era e_j$ and
$e_0,\ldots,e_{j-1}\not\era e_{i_k}$, contradicting [E3]. Thus
$e_{i_0},\ldots,e_{i_m}$ is left-closed and does not contain vacuous
events, i.e., is a reduction. \zurab{Need to complete.}
\eproof
\el




\bpl{emb.ver.sinc.}
 $\lclas{P}\lleq \lclas{Q}$ in an ASDRS $\cal R$ iff $\lclas{FAM(P)}\lleq
\lclas{FAM(Q)}$ in $\cal P_R$.

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

\nec\ By \Dr{D.perm.latt.} and $\lclas{FAM(P)}\lleq \lclas{FAM(Q)}$, there
is a configuration $\alpha\leeqv FAM(Q)$ \zurab{such that $FAM(P)\ssq
\alpha$}; thus by \Lr{Lred.fr.conf.} $\exists\rs{\beta}: FAM(P)\ssq
\beta\ssq\alpha \wedge \beta\leeqv\alpha$. By \Lr{L.dpred.drred.}, There is
a $Q'$ such that $FAM(Q')=\beta$ and $P$ is an initial part of $Q'$. By
\Lr{L.leeq.leeq.}, $Q\leeqv Q'$, hence $P\lleq Q$.
\eproof
\ep





\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}}$. Moreover, (quasi-)reductions
in $\lclas{P}$ are in one-to-one correspondence with these in
$\lclas{FAM(P)}$.

\bproof
By \Pr{emb.ver.sinc.} and \Lr{L.se.red.}, and from the above comparison of
(quasi)-reductions in DPESs and ASDRSs (in particular, \Lr{L.dpred.drred.}
and \Lr{L. red.dp.df.}).
\eproof
\et


Note that $\efcP$ is not a lattice since $\efcR$ is not. However, depending
on the set of `results' we are interested in, we can construct a
(distributive) lattice on configurations in $\cal P$ reflecting growth of
information relative to that goal. For example, if we are interested in
fair computations, we can order configurations by defining
$\alpha\emb\beta$ iff $NE(\alpha)\ssq NE(\beta)$, where $NE(\alpha)$ is the
set of \emph{fairly-needed} events of $\alpha$. Here an event is
fairly-needed in $\cal P$ if it belongs to every, possibly infinite,
configuration in the maximal element of the ideal completion of $\efcP$.
Fairly-needed redexes in $\cal R$ coincide with \emph{Maranget-needed} or
\emph{essential} redexes, and are contracted in all fair reductions in
$\cal R$, which are maximal w.r.t. $\lleq$~\cite{[morn]}. Note that $\emb$
induces an equivalence relation which is different from the \pc.
Construction of such `relativized' information domains from configurations
in DPESs will be considered elsewhere.



\delete{
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


\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

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


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



\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{Event semantics for DFSs}
\label{linear.}


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


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
reduction graph of the term $t=F[x]H(G(x))$. Let $P:F[x]H(G(x))\ar
H(G(H(G(x))))\ar H(G(a))$ and $v=G(a)$. Then the redex $Pv$ has a
corresponding event in the corresponding PES $(FAM(R),\contre)$, but no
family-reduction can create redexes in $Fam(Pv)$.
$F[x]H(G(x))\ar H(G(H(G(x))))$, $F[x]H(G(x))\ar H(G(H(G(x))))\doar a$, and
$F[x]H(G(x))\ar F[x]a \ar a$ are all family-reductions in $R$, but neither
contracts $Fam(Pv)$.
}
As argued in the introduction, we want events in the corresponding DPES of
$\cal F$ to match precisely the families contracted in family-reductions in
$\cal F$. Therefore, we first associate an AZDFS $\lin{{\cal F}}$ to a DFS
$\cal F$, called the \emph{implementation} 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{implementation}
of ${\cal F}$ is the AZDFS $\lin{{\cal F}}=({\cal R}_l,\fami_l,\contr_l)$,
where

$\bullet$ the branches of the reduction graph of the underlying ARS $A$ of
${\cal R}_l=(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 families, in a term $s$, and let $U:s\ar
o$ be the multi-step contracting $U$. Then $V/U$ is the multi-step $o\ar e$
contracting all members of the set $V/U$.

$\bullet$ the family and contribution relations $\fami_l,\contr_l$ in
$\lin{{\cal F}}$ are those induced by $\fami$ and $\contr$.
\ed


In the remainder of this section, we will check that $\lin{{\cal F}}$ in
the above definition is indeed an AZDFS. We first check 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$.


\bll{L.res.fam.fam.}
Let $P:t\doar s$ be a \cfr\ in a comma DFS ${\cal F}_t=(R_t,\fami,\contr)$,
let $U,V\subts s$ be complete sets of redexes of families $\phi$ and $\psi$
in $s$, respectively, and let $s\dored{V}o$. Then $U'=U/V$ is the complete
set of redexes of $\phi$ in $o$.

\bproof
Since $\zfami\ssq\fami$, $U'$ consists of redexes of $\phi$. Suppose on the
contrary that there is $w\subt o$ such that $(P+V)w\in\phi$ and $w\not\in
U'$.

(1) if $w$ is a $V$-residual of $w'\subt s$, then $Pw'\in\phi$ since
$\zfami\ssq\fami$ and $Pw'\zfami (P+V)w$. Hence $w'\in U$, implying $w\in
U'$ -- a contradiction.

(2) if $w$ is created along $V$, then we have by [creation] that
$\psi\contr\phi$. But this would imply by [contribution] that $P$ contracts
a member of $\psi$, and therefore the complete family $\psi$ (since $P$ is
a \cfr), and $P+V$ contracts the family $\psi$ twice. But this is
impossible by \Lr{L.fam.compl.} -- a contradiction.
\eproof
\el



\bll{L.fam.inc.le.in.}
Let $P:t\doar s$ and $Q:t\doar o$ be \cfrs\ in a comma-DFS ${\cal
F}_t=(R_t,\fami,\contr)$, and let $FAM(P)\ssq FAM(Q)$. Then there is a
multi-step reduction $N:s\doar o$ such that $Q\leeqv P+N$ is a \cfr\ (hence
$P\lleq Q$).

\bproof
Let $U$ be a family $\phi$ contracted in $P$, say $P=P'+U+P''$. Since
$FAM(P)\ssq FAM(Q)$, $Q$ contracts $\phi$ as well, say $Q=Q'+V+Q''$, where
redexes $Q'v$ with $v\in V$ from family $\phi$ is the final term of $Q'$.
let $U'=U/(P'/Q')$ and $V'=V/(Q'/P')$. By \Lr{L.res.fam.fam.}, both $U'$
and $V'$ form complete sets of redexes of family $\phi$ in the final term
of $P'\sqcup Q'$, we have $U=V'$. Hence $U/(Q/P')=\emp$, for any multi-step
$U$ of $P$, implying $P/Q=\emp$. Again by \Lr{L.res.fam.fam.}, $Q/P$ is
again \cfr, and $P+Q/P\leeqv Q$. So we can take $Q/P$ for $N$.
\eproof
\el


Obviously, $V/V=\emp$, and every family in $o$ has at most one ancestor
family in $s$. Further, [weak acyclicity] and [stability] for $\lin{{\cal
F}}$ follow immediately from Acyclicity Lemma and Stability Lemma,
respectively (one just needs to take for the reductions $P$ and $Q$ in
these lemmas complete developments of disjoint sets of redexes, which are
clearly external). The axiom [initial] in $\lin{{\cal F}}$ follows
immediately from [initial] in $\cal F$. If $P+U+V$ is a reduction in
$\lin{{\cal F}}$ such that $U$ creates $V$, then the redexes in $V$ are
created along $U$ (when $P+U+V$ is considered as a reduction in $\cal F$),
i.e., $Fam(U)\contr Fam(V)$ in $\cal F$, hence $Fam(U)\contr_l Fam(V)$,
implying [creation] in $\lin{{\cal F}}$. Since family-reductions can be
viewed as reduction in $\cal F$ (by considering multi-steps as
corresponding complete developments), [contribution] for $\contr_l$ follows
immediately from [contribution] for $\contr$. Finally, [FFD] for
$\lin{{\cal F}}$ follows immediately from the Unique Families
Lemma~\cite{[rndrs]} for $\cal F$ (which states that any family can be
contracted at most once in any complete family-reduction, in any DFS $\cal
F$) . Hence $\lin{{\cal F}}$ is indeed a DFS. Note that $\lin{{\cal F}}$ is
separable as its steps contract entire $\fami$-families, hence it is an
AZDFS by \Tr{T.lin.dr.sta.df.}:



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


\delete{
The extraction procedure~\cite{[ldrs]} in the implementation $\lin{R}$ of
an orthogonal (possibly duplicating) rewrite system $R$, first or higher
order, which comes with the labelling concept of
family~\cite{[levy],[Mar91],[AL],[Oos]}, corresponds to `family-extraction'
in family-reductions in $R$, 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 the label of a family is built exactly from the
labels of contributor families, and extraction preserves the labels). Here
a canonical representative of a family is one whose history is a
family-reduction  contracting only contributor families; its existence and
uniqueness up to the order of contraction of causally independent families
follows from the Affine Extraction theorem. Since labelling and
family-extraction families coincide in orthogonal rewrite systems 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 (implementation) 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 (ASDRS) and domain-theoretic (DPES/DEES) models of
computation, and based on this, constructed a fully adequate event style
concurrent semantics for orthogonal rewrite systems. The correspondence
between Event Structures and other models of concurrency, as well as its
denotational semantics, are well studied~\cite{[Win89],[WN]}, and we hope
that our results contribute to better understanding of the relationship
between operational and denotational semantics of sequential and concurrent
languages.


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


We expect that the theory developed here for conflict-free systems can be
extended to the general case (by combining our results with the
construction of Event Structures for non-orthogonal Term Graph Rewriting
Systems in~\cite{[C.K.]}, based on the work~\cite{[Bou]}), so that higher
order process calculi in which processes can be passed and erased can be
modelled as well.



\vspace{0.20cm}

%\section*{Acknowledgements}



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



\begin{thebibliography}{99}




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



\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[{CK96}]{[C.K.]}
Clark D., Kennaway R. Event structures and non-orthogonal term graph rewriting.
MSCS 6:545-578,~1996.


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


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


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



\bibitem[{GK96a}]{[rndrs-rep]}
Glauert J.R.W., Khasidashvili Z. Relative normalization in stable deterministic
residual structures. Technical Report SYS-C96-05, 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[{Hin69}]{[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[{KG97}]{[ldrs]}
Khasidashvili Z., Glauert J.R.W. Zig-zag, extraction and separable families in
non-duplicating stable deterministic residual structures. Report IR-420, Free University, February~1997.


\bibitem[{KG97a}]{[icalp]}
Khasidashvili Z,  Glauert J. R. W. The Geometry of Orthogonal Reduction
Spaces. In Proc. of $24^{th}$ International Colloquium on Automata,
Languages, and Programming, ICALP'97, Springer LNCS, To appear.


\bibitem[{KG97b}]{[mfcs]}
Khasidashvili Z., Glauert J. R. W. Relating conflict-free transition and
event models. In Proc. of the $22^{nd}$ International Symposium on
Mathematical Foundations of Computer Science, NFCS'97, Springer LNCS, To
appear.


\bibitem[{KG97c}]{[acoi]}
Khasidashvili Z., Glauert J.R.W. An abstract concept of optimal
implementation. Report SYS-C97-??, UEA, Norwich, 1997.



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


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



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

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


\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[{Mil89}]{[Mil89]}
Milner R. Communication and concurrency. Prentice Hall, 1989.


\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[{San93}]{[San.Th]}
Sangiorgi D. Expressing mobility in process algebras: first-order and
higher-order paradigms. Ph.D. Thesis, Edinburgh University, 1993.



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



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


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


\end{thebibliography}

\end{document}



