\documentstyle{llncs}

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

\renewcommand{\baselinestretch}{0.98}

\begin{document}

\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt


\title{Relating Conflict-free Stable  Transition and Event Models
(Extended Abstract)}

\author{Zurab Khasidashvili\inst{1}  and John Glauert\inst{2}}

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


\date{}
\title{}






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

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




\begin{abstract}
We describe an event-style (or poset) semantics for conflict-free rewrite
systems, such as 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.
\end{abstract}


\section{Introduction}

The goal of this paper is to provide a \emph{fully adequate} concurrent
semantics for orthogonal rewrite systems. We chose Event Structures, as
the most successful and commonly accepted model of
concurrency~\cite{[Win],[NPW],[Win89],[WN]}. Conflict-free Prime Event
Structures (PESs) are sufficient for our purposes. A (conflict-free) PES
is simply a set of events partially ordered by a \emph{causal dependency}
relation where an event can only dominate a finite
number of events (the \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. Indeed, 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],[dndrs]} proofs of analogs of the Normalization and
Standardization Theorems~\cite{[Bar]}. In DFSs one can further prove
L\'evy's Optimality Theorem~\cite{[le80]} and the Unique Families
Lemma~\cite{[rndrs]}. The latter states that any family can be contracted
at most once in a family-reduction, and corresponds to the fact that any
event may occur at most once in the course of a computation.


Since we want to restrict our attention to family-reductions, we define
\emph{implementation} of DFSs~\cite{[acoi]}. 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, \excl{(Recursive Program
Schemes are an exception~\cite{[B.L.]})} but only an upper
semi-lattice~\cite{[le80]}. This problem, caused by erasure of redexes, is
well
discussed in~\cite{[Lan94]}, 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{[Lan94]} 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.

\suppress{
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}



Let us first recall some basic theory for DRSs and DFSs developed
in~\cite{[rndrs],[dndrs],[ldrs]}. We start by introducing \emph{Abstract
Reduction Systems}~\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$.  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$.


\suppress{
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. \suppress{Several refined concepts of abstract
rewriting are studied in~\cite{[Oos.th],[Mel],[Raa.th]}.}
}

DRSs axiomatize exactly the properties of residuals in orthogonal rewrite
systems which are used in~\cite{[le80],[H.L.]} to define permutation
equivalence on reductions, and the L\'evy-embedding relation on
permutation-equivalence classes, i.e., 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. The most closely related models are Stark's
{\em Determinate Concurrent Transition
Systems}~\cite{[Sta]}, where the residual relation is non-duplicating, and
{\em Abstract Reduction Systems} of Gonthier et al.~\cite{[GLM]}, where in
addition the nesting relation on redexes is axiomatized.
\suppress{Several refined concepts of abstract rewriting are studied
in~\cite{[Oos.th],[Mel],[Raa.th]}.}



\bdl{D.levy.str.}
\suppress{{\bf (Deterministic Residual Structure)}}
A \emph{Deterministic Residual
Structure} (DRS) is a pair ${\cal R}=(A, /)$, where $A$ is an ARS and
$/$ is a \emph{residual} relation on redexes relating redexes in the source
and target term of every reduction $t\red{u}s\in A$, such that
for $v\subt t$, the set $v/u$ of \emph{residuals of $v$ under $u$} is a
set of redexes of $s$; a redex in $s$ may be a residual of only one redex
in $t$ under $u$, and $u/u=\emptyset$. If $v$ has more than one
$u$-residual, then $u$ \emph{duplicates} $v$.
If $v/u=\emptyset$, then $u$ \emph{erases} $v$.
A redex of $s$
which is not a residual of any $v\subt t$ under $u$ is said to be
\emph{$u$-new} or \emph{created} by $u$.
The set $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] (\emph{Finite Developments}~\cite{[GLM]}) All developments
are terminating; all complete developments of $U\subts t$ end at the same
term; and residuals of a redex $v\subt t$ under all complete developments
of $U$ are the same.

$\bullet$  [weak acyclicity] (\cite{[Sta]}) Let $u,v\subt t$, $u\not= v$,
and  $u/v=\emp$. Then $v/u\not=\emp$.

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

Non-duplicating stable DRSs will be called \emph{affine} SDRSs, or ASDRSs.
\ed


In a DRS $\cal R$, the residual relation on redexes is extended
to all co-initial reductions exactly as in syntactic orthogonal rewrite
systems~\cite{[H.L.],[levy],[le80],[Sta]}: $(P_1+P_2)/Q=P_1/Q+P_2/(Q/P_1)$
and $P/(Q_1+Q_2)=(P/Q_1)/Q_2$, and \emph{L\'evy-equivalence} or
\emph{permutation-equivalence} is defined as the smallest relation on co-initial
reductions satisfying: $U+ V/U\leeqv V+U/V$ and $Q\leeqv Q'\,
\Rightarrow \, P+Q+N\leeqv P+Q'+N$, where $U$ and $V$ are complete
developments of redex sets in the same term. Further,
one defines $P\lleq Q$ iff $P/Q=\emptyset$, and
can show that $P\leeqv Q$ iff
$P\lleq Q$ and $Q\lleq P$; and $P\lleq Q$ iff $Q\leeqv P+N$ for some $N$.
\suppress{Intuitively, $P\lleq Q$ expresses that $Q$ does more work than $P$,
 and $Q/P$ is the part of $Q$ that remains from it after $P$.}
Finally, one shows that for any co-initial reductions $P,Q$, $P\sqcup
Q\leeqv Q\sqcup P$, where $P\sqcup Q=P+Q/P$, and is the greatest lower
bound of $P$ and $Q$ in the reduction space ordered by L\'evy's embedding
relation $\lleq$.
The above relations can equivalently be defined also using Klop's method of
commutative diagrams~\cite{[Kl.CRS],[Bar]}.



\bdl{D.red.need.ess.}
(\cite{[dndrs]})
$\bullet$  Let $P:t\doar o$ and $u\subt t$, in a DRS.  We call $u$
{\em erased\/} in $P$ if $u/P=\emp$. We call $P$ \emph{external} to $u$ if
it does not contract its residuals. We say that $P$ {\em discards\/} $u$ if
$P$ is external to $u$ and erases it.

$\bullet$ We call $u$ {\em $P$-needed\/}\excl{, $NE_P(u,t)$,} if there is no
$Q\leeqv P$ that is external to $u$, and call it {\em $P$-unneeded\/} \excl{,
$UN_P(u,t)$,} otherwise. We call $u$ {\em $P$-essential\/}
if there is no $Q\leeqv P$ that discards $u$, and {\em $P$-inessential\/}
otherwise.

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




\suppress{
\btl{L.fin.self.ese.var.}
{\bf (Standardization~\cite{[dndrs]})} For any finite reduction $P$ in an
ASDRS, there is a standard reduction $ST(P)$ L\'evy-equivalent to~$P$.
\et
}


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

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


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

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

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

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

$\bullet$ [FFD] (\emph{Finite Family Developments}) Any reduction that
contracts redexes of a finite number of families is terminating.

We call a DFS $\cal F$ a \emph{zig-zag} DFS, ZDFS, if its family relation
is the zig-zag $\zfami$ (the corresponding contribution relation $\zcontr$
is determined by [contribution]).
We call a DFS \emph{separable}, if, for any redex $Pv$, $v$
cannot create two different redexes in the same family: if $v$
creates $w',w''$ and $w'\not= w''$, then $Fam((P+v)w')\not= Fam((P+v)w'')$.
\ed



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

\vspace{0.20cm}


It is shown in~\cite{[rndrs]} that every DFS is a stable DRS. DFSs model
all known concepts of family
relation~\cite{[levy],[le80],[Kl.CRS],[K.S.],[Mar91],[AL],[Oos]},  and
allow for an abstract proof~\cite{[rndrs]} of the Optimality
theorem~\cite{[le80]}. Further, we have shown in~\cite{[ldrs]} that any
ASDRS is in fact an affine ZDFS, AZDFS (i.e., for any ASDRS $\cal R$,
${\cal F_R}=({\cal R},\zfami,\zcontr)$ is an AZDFS), and that ${\cal F_R}$
is the only separable DFS with $R$ as the underlying SDRS. The proof of the
above result is based on an abstract concept of \emph{extraction} allowing
to construct a \emph{canonical} element $Pu$ in every family $\phi$: $P$ is
standard and $\forall P'u'\in\phi\,\exists P'':\,P'\leeqv
P+P''\,\wedge\,u'=u/P''$ (for any finite $Q$ in an ASDRS, there is a
standard reduction $ST(Q)\leeqv Q$~\cite{[dndrs]}). Further, it enables 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.}
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 nice lattice properties; therefore Event Structures have been very
successful in modelling \emph{linear} process calculi (no actions can be
erased or duplicated), such as CCS~\cite{[Mil89]}. However, any attempt to
adequately interpret higher-order process languages in Event Structures
would face the same erasure problems discussed in the introduction. As in
the case of reductions, the aim of axiomatizing permutation equivalence on
event configurations is to be able to equate configurations which differ
only by irrelevant or \emph{inessential} events.


A \emph{Prime Event Structure} (PES)~\cite{[Win89]} 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\}$, and
$\coni{e}=\{e'\,\vert\, e\geq e'\}$.


\bdl{D.DPES.}
A \emph{Deterministic Permutation Event Structure} (DPES) is a triple
${\cal P}=(E, \leq, \leeqv)$, where $\suppress{{\cal E}=}(E, \leq)$ is a
conflict-free  PES and $\leeqv\ssq \fcE \times \fcE$ is an equivalence
relation, 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 \suppress{\wedge \gamma\in\fcE} \imply \alpha\leeqv\gamma$;

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

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

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




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


\bdl{D.DEES.}
A \emph{Deterministic Erasure Event Struc\-ture} (DEES) is a triple ${\cal
C}=(E,\leq, \era)$, where  $\suppress{{\cal E}=}(E,\leq)$ is a
conflict-free PES and $\rhd\ssq \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
\suppress{\in \fcE } \Rightarrow \beta\rhd e$;


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

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

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

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

\delete{
$\fcC$ is called the set of \emph{finite configurations} or just
\emph{configurations} of $\cal C$,  and is the set of finite left-closed
subsets of $E$.
}
\ed



The next definition gives a translation between DPESs and DEESs:

\bdl{D.era.vi.per.eq.}
(1) 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}$.

(2) 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$ is called the
\emph{standard variant} of $\alpha$.
\ed



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.


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



\bpl{C.char.sea.eq.}
(1) In a DEES ${\cal C}=(E,\leq,\rhd)$,   $\forall
\alpha,\beta,\gamma\in\fcC:\alpha\cap\beta\ssq\gamma \ssq\alpha\cup\beta:\\
\alpha\eleeqv\beta\Leftrightarrow \sea=\seb\Leftrightarrow \forall e\in
\alpha\cup\beta\setminus\alpha\cap\beta: \gamma\era e$.

(2) In a DPES ${\cal P}=(E,\leq,\leeqv)$, $\alpha\leeqv\beta$ iff
$ST_{\lera}(\alpha)=ST_{\lera}(\beta)$.
\ep




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

\bproof
We need to show that $\eleeqv $ satisfies the permutation axioms [P0] --
[P3]. We only prove [P2] here. Let $\alpha\eleeqv\beta$ and
$\alpha+e,\beta+e\in\fcE$. By \Dr{D.era.vi.per.eq.}.(2), $\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.}.(1). Similarly,
$ST(\beta+e)=\seb$. Hence, $ST(\alpha+e)=ST(\beta+e)$, implying by
\Dr{D.era.vi.per.eq.}.(2) that $\alpha+e\eleeqv\beta+e$. Now let
$\sea\not\era e$. Then, by [E3], $\forall
e'\in\alpha\setminus\sea:e'\not<e$. Thus
$\alpha+e\in\fcE\imply\sea+e\in\fcE$. Since $\alpha+e\era
\alpha+e\setminus(\sea+e)$, we have by \Pr{C.char.sea.eq.} that
$ST(\alpha+e)=ST(\sea+e)$, thus $\alpha+e\eleeqv\sea+e$ by
\Dr{D.era.vi.per.eq.}.(2). Similarly, $\beta+e\eleeqv\seb+e$, implying
$\alpha+e\eleeqv\beta+e$ (since $\sea=\seb$).
\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.}.(1) and [P0], and [E4] is
immediate from \Dr{D.era.vi.per.eq.}.(1). Proofs of the other axioms are
not too long, but are   tedious to include here.}
\eproof
\et
}


The following theorem, which is proved using the DEES and DPES axioms,
implies the correctness of \Dr{D.era.vi.per.eq.}.


\bt
(1) For any DEES ${\cal C}=(E,\leq,\rhd)$, ${\cal P_C}=(E,\leq,\eleeqv)$ is
a DPES.

(2) For any DPES ${\cal P}=(E, \leq, \leeqv)$, ${\cal C_P}=(E, \leq,
\lrhd)$ is a DEES.

\et


Further, the translations between DEESs and DPESs, in
\Dr{D.era.vi.per.eq.}, commute, implying the equivalence of the two event
models:

\btl{T.dc.ps.det.equ.}
(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$.
\suppress{
\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')$. Then one
can show that $\era=\lrhd$ and $\leeqv=\leeqv'$, implying the theorem.

Let us show that $\era=\lrhd$ and $\leeqv=\leeqv'$.

(1) 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.}.(1), the latter
holds iff $ST(\alpha\cup\con{e})=ST(\alpha\cup\con{e}\setminus \coni{e})$,
which, by \Dr{D.era.vi.per.eq.}.(2) means that
$\alpha\cup\con{e}\eleeqv\alpha\cup\con{e}\setminus \coni{e}$, meaning
$\alpha\lrhd e$ by \Dr{D.era.vi.per.eq.}.(1).


(2) By \Pr{C.char.sea.eq.}.(2) and \Dr{D.era.vi.per.eq.}.(2),
$\alpha\leeqv\beta$ iff $\lsea=\lseb$ iff $\alpha\eleeqv\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.





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

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

$\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$, where $FAM(P)$ denotes the set
of families whose member redexes are contracted in $P$.


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





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





The following translation of DPESs and DEESs into ASDRSs resembles to the
representation of events in a PES $(E,\leq)$ as prime intervals of the
configuration domain $\fcE$~\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}$. \suppress{A non-empty
redex $(\lclas{\alpha},e)$ will also be called an \emph{$e$-redex}.}

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

We show that $\cal R_P$ and $\cal R_C$ are ASDRSs,  ${\cal R_P}={\cal
R_{C_P}}$, and ${\cal R_C}={\cal R_{P_C}}$.


Let us call a left-closed enumeration (i.e., respecting the causality
relation) $e_1,\ldots,e_k$ of a configuration $\alpha$ in a DEES a
\emph{reduction}, written $\rs{\alpha}$, 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}. Quasi-reductions are defined similarly in any DRS,
as `reductions containing empty steps corresponding to erased redexes'.


Note that initial reductions in $\cal R_P$ and $\cal R_C$ can be
represented as event sequences $e_1,\ldots,e_n$ respecting the causal order
-- $e_i$ represents the (contraction of) \emph{non-empty} redex
$(\{e_1,\ldots,e_{i-1}\},e_i)$, i.e., they correspond to reductions in
$\cal C$. As we will see below, not all left-closed enumerations of a
configuration represent a reduction -- they represent quasi-reductions.


\bdl{D.ps.fs.tra.}
To a DPES ${\cal P}=(E, \leq,\leeqv)$, we associate an affine DFS ${\cal
F_P}=({\cal R}_{\cal P}, \pfami,\pcontr)$ as follows (where ${\cal R}_{\cal
P}$ is the DRSs defined in \Dr{D.ps.rs.tra.}):


$\bullet$ $\pfami$-families are sets $\phi_e = \{(\redc{\alpha},
e)\,\vert\, \alpha+e\in \fcP \wedge (\lclas{\alpha},e)\not=\emp\}$, for any
$e\in E$.

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



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.}: $\cal F_P$ is an AZDFS.



For any of the four models, there is an obvious concept of
\emph{isomorphism}, $\isom$. The following theorem, combined with the
results of previous sections, implies equivalence of the considered four
transition and event models.




\btl{T.equi.four.}
(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}}$.
\et





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




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




\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 $\lclas{P}$ is the L\'evy-equivalence class of $P$, and
$\efcR=(\pfcR,\lleq)$, where $\lleq$ is L\'evy's embedding relation.
\ed




\suppress{
>From the above comparison of reductions in DPESs and ASDRSs, we have that
$\lclas{P}\lleq \lclas{Q}$ in an ASDRS $\cal R$ iff $\lclas{FAM(P)}\lleq
\lclas{FAM(Q)}$ in $\cal P_R$. Therefore
}


It has been shown in~\cite{[ldrs]} that $P\lleq Q$ iff $FAM(P)\ssq FAM(Q')$
for some $Q'\leeqv Q$, implying that $\lclas{P}\lleq \lclas{Q}$ in an ASDRS
$\cal R$ iff $\lclas{FAM(P)}\lleq \lclas{FAM(Q)}$ in ${\cal P}_{\cal F_R}$.
Therefore


\btl{T.isom.drs.dps.}
Let $\cal R$ be an ASDRS and let ${\cal P}={\cal P}_{\cal F_R}$ be its
corresponding DPES. Then $f:\lclas{P}\rightarrow \lclas{FAM(P)}$ is an
isomorphism between $\efcR$ and $\efcP$. \suppress{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)}$.
\et


Note that $\efcP$ is not a lattice since $\efcR$ is not. However, depending
on the set of `results' we are interested in, one can construct a
(distributive) lattice on configurations in $\cal P$ reflecting growth of
information relative to that goal. Construction of such `relativized'
information domains will be addressed in a separate paper.




\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 is 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. Further,
we think that our axiomatization of permutation equivalence is
interesting on its own right from the poset/lattice theoretic point of view.

We expect that the theory developed here for conflict-free systems can be
extended to the general case, \suppress{(by combining our results
with~\cite{[C.K.]}), 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 bemodelled as well.



\vspace{0.20cm}


\begin{akn}\\
We thank  Richard Kennaway and Fer-Jan de Vries 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,~1993.


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

\suppress{
\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[{Bou85}]{[Bou]}
Boudol G. Computational semantics of term rewriting systems.
In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds.
Camb. Univ. Press, 1985, p.~169-236.


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

\bibitem[{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. PROCOMET'94, IFIP Transactions
A-56, 1994.



\bibitem[{GK96}]{[rndrs]}
Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic
residual structures. CAAP'96, Springer LNCS, vol.~1059,  H.~Kirchner, ed.
1996,  p.~180-195.


\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. 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, p.~394-443,~1991.

\bibitem[{KS89}]{[K.S.]}
Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in  regular
combinatory reduction systems.
Report. University of East Anglia, 1989.


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


\bibitem[{KG96}]{[dndrs]}
Khasidashvili Z.,  Glauert J. R. W. Discrete normalization and
Standardization in Deterministic Residual Structures. 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. Technical Report
IR-420, Free University, Amsterdam, February 1997.


\bibitem[{KG97a}]{[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[{Lan94}]{[Lan94]}
Laneve C.  Distributive evaluations of $\lambda$-calculus,
Fundamenta Informaticae, 20(4):333 -- 352, 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.


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


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


\suppress{
\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. \excl{In: Proc. of the Dagstuhl Seminar 9301 on Graph
Transformations in Computer Science,} Springer LNCS, vol.~776, Schneider
H.-J. Ehrig H., eds, 1994,  p.~326-340.




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

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


\bibitem[{Win86/89}]{[Win89]}
Winskel G. An introduction to Event Structures. \suppress{In proc. of
School/Workshop on `Linear time, branching time and partial order in logics
and models of concurrency'.} Springer LNCS, vol.~354, 1989, p.~364-397.
Full version: Cambr. Univ. Comp. Lab. Report n. 95, 1986.


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


\end{thebibliography}
\end{document}



