Relating Conflict-free Stable Transition and Event Models via Redex Families ⋆

Zurab Khasidashvili

Department of Mathematics and Computer Science Bar-Ilan University, Ramat-Gan 52900, Israel khasidz@cs.biu.ac.il

John Glauert

School of Information Systems University of East Anglia, Norwich NR4 7TJ, UK jrwg@sys.uea.ac.uk

Abstract

We describe an event-style (or poset) semantics for conflict-free rewrite systems, including term and graph rewriting (possibly with bound variables), the λ-calculus, and other stable transition systems with a residual relation. Our interpretation is based on considering redex-families as events. It treats permutation-equivalent reductions as representing the same concurrent computation. Due to erasure of redexes, Event Structures are inadequate for such an interpretation. We therefore extend the Prime Event Structure model in two different but equivalent ways: by axiomatizing permutation-equivalence on finite configurations, and by axiomatizing the erasure of events, for the conflict-free case, and show that these extended models are equivalent to stable transition models with axiomatized residual and family relations. We then construct finitary prime algebraic domains from the set of configurations in these extended models by defining orderings relative to stable sets of ‘results’. All useful sets of results for which the normalization (by neededness) theorem can be proved are stable.

Keywords: Abstract reduction systems, redex families, event structures, distributive domains.

⋆ Part of this work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300.

Preprint submitted to Elsevier Preprint 7 July 2000

1 Introduction

The primary goal of this paper is to provide a fully adequate event-style concurrent semantics for orthogonal rewrite systems. Event Structures, developed by Winskel, Nielsen and Plotkin [36,32,37,38], are a commonly accepted model of concurrency. 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 causal dependency relation (a poset) where an event can only dominate a finite number of events (the so called axiom of finite causes). The idea is to view a process as performing events (some atomic tasks), and an event can occur, only once, after all events on which it depends. Causally independent events are concurrent events and can be evaluated in parallel. Stages of a computation are thus represented by 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 λ-calculus, there is the well established concept of ‘redex-family’, due to Lévy [26,27], 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 correspond (up to book-keeping steps) to complete family-reductions in the original system [28,23,15,1].^{1}

Recent advances in the abstract study of the syntax and operational semantics of rewrite and transition systems [35,12,29,11,17,18,20] allow us to address the problem in an entirely abstract setting. Stable Deterministic Residual Structures (SDRSs) and Deterministic Family Structures (DFSs) model computation in orthogonal rewrite systems. DRSs are Abstract Rewrite Systems with an axiomatized residual relation; DFSs are DRSs where in addition the concept of redex-family is axiomatized. Stable DRSs allow [11,17] proofs of analogs of the Normalization and Standardization Theorems [3]. In DFSs one can further prove the Optimality Theorem and the Unique Families Lemma [11]. The latter states that any family can be contracted at most once in a complete family-reduction. It corresponds to the fact that any event may occur at most once in the course of a computation, and is needed for the event structure interpretation of SDRSs based on interpreting families as events.

Thus we can start our interpretation by assuming that an orthogonal rewrite

1 The book-keeping steps can be expensive in the case of λ-calculus [2].

system is given in the form of a DFS. Furthermore, it has been shown in [20] that any DFS can be given an interpretation by a non-duplicating or affine DFS with zig-zag as the family relation (AZDFS), called the implementation of the original DFS: the reduction steps in the implementation DFS correspond to complete family-reduction multi-steps of the original DFS. Therefore it is enough to concentrate on defining PES semantics for AZDFSs.

To view a process as the domain of all its configurations, an adequacy requirement is desirable. Namely, that runs of a finite configuration (i.e., all its possible sequentializations) should be in one-to-one correspondence with all finite reductions in the equivalence class which the configuration is supposed to represent. Because of the huge importance of permutation or Lévy equivalence to the whole theory of (not only orthogonal) rewrite systems [27,14,5], and to concurrency theory as well [35], we want to be able to treat permutationequivalent finite reductions as representing the same concurrent computation, as indeed permutation-equivalent finite reductions result one from another by permuting concurrent consecutive steps. However, this is clearly impossible in the present PES framework [37], as a finite configuration in a PES has only a finite number of runs while, a permutation-equivalence class of a finite reduction may have an infinite number of elements.

For example, consider the λ-term t = KxΩ, where K = λxy.x and Ω = (λx.x)λx.x. Intuitively, all reductions of the form t→^{Ω}t→^{Ω} … →^{Ω}t→^{K}x, or Ω^{m}K in short, consisting of a number of Ω-steps followed by a K-step, are ‘equal’, as the Ω-steps are performed in an erased part of t (or in ‘garbage’). And indeed, permutation equivalence equates all the above reductions. However, there is no means in PESs to equate the corresponding configurations.

The same problem can also be observed from a different angle. In order for an equivalence relation to satisfy the adequacy requirement, the corresponding equivalence classes of reductions must be partially ordered so as to form finitary prime algebraic (or equivalently, distributive) complete lattices (see Definition 55), since the domains of configurations of PESs ordered by inclusion are such lattices [36,37]. However, it is well known that Lévy’s reduction space – permutation equivalence classes of co-initial finite reductions ordered by Lévy’s embedding relation ⊴ (which generates permutation equivalence) – is not in general a lattice but only an upper semi-lattice, as the greatest lower bound of two co-initial finite reductions w.r.t. ⊴ need not exist [27].^{2} As a consequence, although the lattice properties can be restored by taking the ideal completion [4], the resulting domain need not be finitary prime algebraic even when the reduction relation is non-duplicating. For example, Lévy’s configuration domain of the K-Ω term above is not finitary as the K-step KxΩ→^{K}x is a finitary element but it dominates (w.r.t. ⊴) an infinite number of elements:

2 Recursive Program Schemes are an exception [4].

reductions of the form Ω^{m}.

Several authors have proposed different ways to get round this problem. Laneve [24] introduced distributive equivalence on β-reductions which only allows permutation of steps that cannot erase or duplicate one another, and consequently all equivalent sequences have the same length. Similarly, Corradini et al [8] base their interpretation on the equivalence relation generated by permutations of disjoint redexes only, in a general categorical model of rewriting. Kennaway et al [16] do work with permutation equivalence for orthogonal Term Graph Rewriting, but they only restrict themselves to needed events of a normalizable term to cope with problems with erasure. As needed redexes cannot be erased, all needed normalizing reductions are of the same length, and on needed reductions, the permutation and distributive equivalences coincide (since the system is non-duplicating). Clark and Kennaway [7] also work with permutation-equivalence and allow for (finitely) non-normalizable terms, but restrict themselves to standard reductions, and their ordering on standard reductions is a strong restriction of Lévy’s embedding relation. And finally, extending work of Boudol [5], Melliès [30] gives a construction of distributive domains from external reductions [14], in an axiomatic framework of rewriting. Other authors (e.g., [6,34]) work with linear rewrite/transition systems (no duplication, no erasure), and do not therefore encounter the erasure problem.

In order to cope with the adequacy problem, we extend the PES model in two different but equivalent ways: by axiomatizing permutation-equivalence on event configurations, by directly constraining the class of all equivalence relations on configurations; and by axiomatizing the inessentiality or erasure relation expressing redundancy of an event for a configuration. The latter extends by further axioms an incomplete axiomatization of the inessentiality relation in [11]. In the resulting extended models, Deterministic Permutation and Erasure Event Structures, DPESs and DEESs, we can identify finite configurations with different numbers of events but still representing the same permutation-equivalence class of finite reductions. We show that Lévy’s configuration domain – appropriately ordered permutation-equivalence classes of finite configurations in a DEES/DPES – is isomorphic to Lévy’s reduction space of the corresponding AZDFS, and therefore DPESs/DEESs give a fully adequate semantics to AZDFSs.

As a consequence, Lévy’s configuration domains in DEESs/DPESs need not be finitary prime algebraic. However, having axiomatized the erasure relation and permutation equivalence on event configurations, we can define orderings on configurations reflecting the growth of information relative to stable sets of ‘results’, called stable orderings, and thereby reconstruct finitary prime algebraic domains from configuration domains of DEESs/DPESs: The isomorphism between AZDFSs and DEESs/DPESs discussed above induces a concept of stable sets of configurations in DEESs/DPESs, and the theory of normalization by neededness relative to stable sets of terms in AZDFSs [11] has its counterpart in DEESs/DPESs; and this relativized concept of neededness enables us to show that the stable orderings on configuration domains of DEESs/DPESs do form finitary prime algebraic domains.

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 3 we introduce DPESs and DEESs and establish their equivalence. In Section 4 we relate the latter event models with affine SDRSs (ASDRSs) and AZDFSs, showing the equivalence of the four models. In Section 5, we define Lévy’s configuration domain in a DPES/DEES and show its isomorphism with Lévy’s reduction space of the corresponding ASDRS. We study normalization by neededness in DEESs in Section 6, and use it to construct finitary prime algebraic domains from configurations in DEESs/DPESs in Section 7. Conclusions appear in Section 8.

2 Deterministic Residual and Family Structures

In this section, we recall some basic theory of Deterministic Residual and Family Structures (DRSs and DFSs), developed in [11,17,18,20]. DRSs and DFSs are Abstract Reduction Systems (ARSs) with an axiomatized notion of residual. In DFSs, in addition, Lévy’s concept of redex-family is axiomatized. Related abstract residual models are studied in [13,35,12,29].

Our definition of ARSs allows multiple transitions with the same source and target, unlike Klop’s definition [22].

Definition 1 An ARS is a triple A = (Ter,Red,→) where Ter is a set of terms, ranged over by t, s, o, e; Red is a set of redexes (or redex occurrences), ranged over by u, v, w; and →: Red ↦ (T er × T er) is a function such that for any t ∈ T er there is only a finite set of u ∈ Red such that ↦ (u) = (t, s), written t→^{u}s. This set will be known as the redexes of term t, where u ⊆ t denotes that u is a member of the redexes of t and U ⊆ t denotes that U is a subset of the redexes. Note that → is a total function, so one can identify u with the triple t→^{u}s. A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . .. Reductions are denoted by P, Q, N. We write P : t → → s or t → →^{P} s if P denotes a reduction (sequence) from t to s. If P is finite and its final term coincides with the initial term of Q, then P + Q denotes the concatenation of P and Q. Finally, u also denotes the reduction that contracts u.

Definition 2 (Deterministic Residual Structure [11]) A Deterministic Residual Structure (DRS) is a pair R = (A, /), where A is an ARS and / is a residual relation on redexes relating redexes in the source and target term of every reduction t→^{u}s ∈ A, such that for v ⊆ t, the set v/u of 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 = ∅. If v has more than one u-residual, then u duplicates v. If v/u = ∅, then u erases v. A redex of s which is not a residual of any v ⊆ t under u is said to be u-new or created by u. The set u/P of residuals of u under any finite reduction P is defined by transitivity.

A development of U ⊆ t is a reduction P : t → → that only contracts residuals of redexes from U; it is complete if it is finite and U/P = ∪_{u∈U} u/P = ∅. Development of ∅ is identified with the empty reduction. U will also denote a complete development of U ⊆ t. The residual relation satisfies the following two axioms:

[FD] (Finite Developments [12]) All developments are terminating; all complete developments of U ⊆ t end at the same term; and residuals of a redex v ⊆ t under all complete developments of U are the same.

[weak acyclicity] ([35]) Let u, v ⊆ t, u ≠ v, and u/v = ∅. Then v/u ≠ ∅.^{3}

We call a DRS R stable (SDRS) if the following axiom is satisfied:

[stability] If u, v ⊆ t are different redexes, t→^{u}e, t→^{v}s, and u creates a redex w ⊆ 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.

[figure: t; u; e; w; s; v; u/v; o; v/u; w/(v/u)]

We call an SDRS non-duplicating or affine, ASDRS, if its residual relation is non-duplicating. Note that, since the only observables of DRSs are redexes, duplicating syntactic rewrite systems may still form ASDRSs. For example, the DRS corresponding to innermost reductions in an orthogonal TRS is an ASDRS, although innermost redexes may duplicate their arguments.

In a DRS R, the residual relation on redexes extends to all co-initial reductions exactly as in syntactic orthogonal rewrite systems [14,26,27,35]: (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 Lévy-equivalence or permutation-equivalence is defined as the smallest relation on co-initial reductions satisfying: U +V/U ≈ V +U/V and Q ≈ Q′ ⇒ P +Q+N ≈ P +Q′+N, where U and V are complete developments of redex sets in the same term. Further, one defines P ⊴Q iff P/Q = ∅, and can show that P ≈ Q iff P ⊴Q and Q⊴P; and P ⊴Q iff Q ≈ P +N for some N. Intuitively, P ⊴Q expresses that

3 This axiom is called [acyclicity] in [11], and is axiom (4) in [35].

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 ⊔ Q ≈ Q ⊔ P, where P ⊔ Q = P + Q/P, and is the greatest lower bound of P and Q in the reduction space ordered by Lévy’s embedding relation ⊴. The above relations can equivalently be defined also using Klop’s method of commutative diagrams [21,3]. Finally, we will need the following Cube Lemma: for any finite co-initial reductions P, Q and N, N/(P ⊔ Q) = N/(Q ⊔ P).

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

Definition 3 • Let u ∈ U ⊆ t and P : t → → o. We call P external to U (resp. u) if P does not contract residuals of redexes in U (resp. residuals of u).

• Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → t_{n} and Q : t_{0} = s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → → s_{m}. Let

U_{i,j} = u_{i}/(Q_{j}/P_{i}) and V_{i,j} = v_{j}/(P_{i}/Q_{j}) (see diagram). We call P external to Q if for any i, j, U_{i,j} ∩ V_{i,j} = ∅.

[figure: t_{0}; P_{i}; t_{i}; u_{i}; t_{i+1}]

[figure: s_{j}; Q_{j}; P_{i}/Q_{j}; Q_{j}/P_{i}; U_{i,j}]

[figure: s_{j+1}; v_{j}; V_{i,j}]

Lemma 4 (Stability) Let P : t → → s be external to Q : t → → e, in a stable DRS, and let P create redexes W ⊆ s. Then the residuals W/(Q/P) of redexes in W are created by P/Q, and Q/P is external to W.

Lemma 5 (Weak Acyclicity) Let P, Q be co-initial finite reductions in a DRS, and let P be external to Q. Then Q ≉ P.

Next we recall some definitions and results from [17] concerning standardization of reductions in ASDRSs, used in this paper.

Definition 6 • Let P : t → → o and u ⊆ t, in a DRS. We call u erased in P or P -erased if u/P = ∅. We say that P discards u if P is external to u and erases it.

• We call u P -needed if there is no Q ≈ P that is external to u, and call it P -unneeded otherwise. We call u P -essential if there is no Q ≈ P that discards u, and P -inessential otherwise.

We extend these concepts to reductions co-initial with those containing

u as a redex of one of its terms.

• Let Q : t → → o, P : t → →^{P′} s → → e, and u ⊆ s. We say that u is Q-needed, or more precisely, P′u is Q-needed, if u is Q/P′-needed. We call P Q-needed if every redex contracted in P is. We call P self-needed if it is P -needed. The other concepts above are extended in the same way.

Note that P -neededness, P -erasure, and P -essentiality do not depend on the choice of a reduction in the class ⟨P ⟩_{L} of reductions Lévy-equivalent to P, since u/P = u/Q when P ≈ Q, by the Cube Lemma. The discards concept however does depend on the particular reduction in the permutation-equivalence class.

Lemma 7 Let P : s → → t→^{u}e → → o in an ASDRS.

(1) w ∈ t is P -needed iff it is P -erased and P -essential.

(2) If P : t → → s′→^{w}o, then w ∈ s′ is P -needed.

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

(4) If u ≠ v ⊆ t, then v is P -needed (P -essential) iff v has a P -needed (P -essential) residual in e.

Self-needed reductions play the role of standard reductions in SDRSs, and the following algorithm is a standardization procedure for reductions in ASDRSs. Let P : t → → s. The canonical standard variant of P, ST (P), is defined as follows: If P = ∅, then ST (P) = ∅. Otherwise, let v ⊆ 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 Lemma 7). Then ST (P) = v + ST (P/v). We write Q ∈ ST V (P) if Q ∈ ST A and Q ≈ P, where ST A denotes the set of all standard reduction, and call Q a standard variant of P. In particular, ST (P) ∈ ST V (P).

Theorem 8 (Standardization) For any finite reduction P in a stable nonduplicating DRS, ST (P) is a standard reduction Lévy-equivalent to P.

It is shown in [18,20] that all standard variants of a finite reduction P can be constructed effectively.

Definition 9 (Deterministic Family Structure [11]) A Deterministic Family Structure (DFS) is a triple F = (R, ≃, ↪), where R is a DRS; ≃ is an equivalence relation on redexes with histories; and ↪ is the contribution relation on co-initial families, defined as follows:

(1) For any co-initial finite reductions P and Q, a redex Qv in the final term of Q (read as v with history Q) is called a copy of a redex P u if P ⊴Q, i.e., P +Q/P ≈ Q, and v is a Q/P -residual of u; the zig-zag relation ≃_{z} is the symmetric and transitive closure of the copy relation. The family relation ≃ is an equivalence relation among redexes with histories containing ≃_{z}. A family is an equivalence class of the family relation; families are ranged

over by ϕ, ψ, . . .. F am( ) denotes the family of its argument.

(2) Further, ≃ and ↪ satisfy the following axioms:

[initial] Let u, v ⊆ t and u ≠ v, in R. Then F am(∅_{t}u) ≠ F am(∅_{t}v), where ∅_{t} is the empty reduction starting from t.

[contribution] ϕ ↪ ϕ′ iff for any P u ∈ ϕ′, P contracts at least one redex

in ϕ.

[creation] Let e → →^{P} t→^{u}s, and let u create v ⊆ s. Then F am(P u) ↪ F am((P + u)v).

[FFD] (Finite Family Developments) Any reduction that contracts redexes of a finite number of families is terminating.^{4}

Note that [contribution] can be viewed as a definition of ↪ rather than as an axiom. It is shown in [11] that every DFS is a stable DRS.

Convention In this paper we only consider comma-DRSs and comma-DFSs. That is, the term set of any DRS will be the reduction graph of a term, called the initial term, i.e., the set of terms to which the initial term is reducible. The initial term will often be denoted by t_{∅}, by analogy with the initial state ∅ in an Event Structure. Further, in DFSs, families will always be considered relative to t_{∅}, i.e., all histories start with t_{∅}. Unless otherwise stated, by a reduction we mean a finite reduction. Reductions starting from t_{∅} will also be called initial reductions.

Definition 10 • We call a DFS F a zig-zag DFS, ZDFS, if its family relation

is the zig-zag ≃_{z}. Affine ZDFSs will be called AZDFSs.

• We call an affine DFS separable if, for any redex P v, v cannot create two different redexes in the same family. That is, if v creates w′, w′′ and w′ ≠ w′′, then F am((P + v)w′) ≠ F am((P + v)w′′).

The following lemma from [18,20] gives a useful characterization of ⊴ and ≈ in ASDRSs via zig-zag classes. Below, F AM(P) (resp. SF AM(P)) denotes the set of zig-zag classes whose member (resp. P -needed) redexes are contracted in P, in an ASDRS.

Proposition 11 Let P and Q be initial reductions in an AZDFS. Then P ⊴Q iff ∃Q′ ≈ Q : F AM(P) ⊆ F AM(Q′), and P ≈ Q iff SF AM(P) = SF AM(Q). Further, SF AM(P) = F AM(ST (P)) = ∩_{N≈P} F AM(N). Consequently, if P, Q ∈ ST A, then P ≈ Q iff F AM(P) = F AM(Q) (since in that case P = ST (P) and Q = ST (Q)).

The results of this paper are based on the following properties of ASDRSs, which show that ASDRSs and AZDFSs are essentially the same transition models, and that every zig-zag family has a unique (up to an equivalence on histories) minimal element [18,20].

4 This axiom is called [termination] in [11].

Theorem 12 (Affine Families) Let R be an ASDRS. Then F_{R} = (R, ≃_{z} , ↪_{z}) is an affine zig-zag DFS, called the corresponding ZDFS of R. Further, 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.

Theorem 13 (Affine Extraction) Every redex P v in an ASDRS R has a zig-zag related redex P′v′ in canonical form, meaning that P′ ∈ ST A, its last step creates v′, and for any P′′v′′ ≃_{z} P v, ∃N′ : P′′ ≈ P′ + N′ ∧ v′′ = v′/N. For any other canonical form P^{∗}v^{∗} of P v, P′ ≈ P^{∗} and v′ = v^{∗}. Further, P′ contracts exactly one redex in every contributor zig-zag family of P v, in the corresponding AZDFS F_{R} = (R, ≃_{z}, ↪_{z}) of R.

3 Deterministic Permutation and Erasure Event Structures

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 directly the phenomenon of 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., [33]) processes (that can fire events) can be passed around as messages and therefore erased. Event Structures are linear in nature and consequently the configuration domains enjoy very nice lattice properties; therefore Event Structures have been very successful in modelling linear process calculi where no actions can be erased or duplicated (see e.g., [6,37]), such as CCS [31]. However, any attempt to adequately interpret higher-order process languages in Event Structures would face the same erasure problems discussed in the introduction. As in the case of reductions, the aim of axiomatizing permutation equivalence on event configurations is to be able to equate configurations which represent the same concurrent computation and differ only by irrelevant or inessential events. We believe that any equivalence relation on configurations fully capturing concurrency should contain the permutation-equivalence.

A Prime Event Structure (PES) [36] is a triple E = (E, Con, ≤), where E is a set of events, ranged over by e, e_{1}, …; the consistency predicate Con is a non-empty set of finite subsets of E, denoted by X, Y, …; and the causal dependency relation ≤ is a partial order on E, such that {e} ∈ Con, Y ⊆ X ∈ Con ⇒ Y ∈ Con, X ∈ Con ∧ ∃e′ ∈ X.e ≤ e′ ⇒ X ∪ {e} ∈ Con, and {e′ | e′ ≤ e} is finite for any e ∈ E.

We only consider conflict-free or deterministic PESs, where no event can prevent others from occurring, and therefore the consistency predicate is the set of all finite subsets of E and will be omitted. Finite configurations of E are finite left-closed subsets α, β, … of E, i.e., subsets L_{fin}(E) = {α ⊆_{fin} E | e ∈ α ∧ e′ < e ⇒ e′ ∈ α}. Except for Section 7, we only consider finite configurations, and will omit ‘finite’.

Below, for better readability, we write α + e for α ∪ {e}, and write α − e for α \ {e}. Further, we define ⌈e⌉^{≤} = {e′ | e′ ≤ e}, ⌈e⌉^{<} = {e′ | e′ < e}, ⌈e⌉^{≥} = {e′ | e ≥ e′} and ⌈e⌉^{>} = {e′ | e′ > e}.

Definition 14 A Deterministic Permutation Event Structure (DPES) is a triple P = (E, ≤, ≈), where E = (E, ≤) is a conflict-free PES and ≈⊆ L_{fin}(E) × L_{fin}(E) is an equivalence relation, called Lévy- or permutationequivalence, satisfying the following axioms, where α, β, γ ∈ L_{fin}(E):

[P0] ∀e ∈ E : ⌈e⌉^{<} ≉ ⌈e⌉^{≤};

[P1] α ≈ β ∧ α ∩ β ⊆ γ ⊆ α ∪ β ⇒ α ≈ γ;

[P2] α ≈ β ∧ α + e, β + e ∈ L_{fin}(E) ⇒ α + e ≈ β + e;

[P3] α ≈ α − e ∧ e < e′ ∧ α + e′ ∈ L_{fin}(E) ⇒ α ≈ α + e′;

DEESs extend Deterministic Computation Structures [11] by further erasure axioms to enable a fully adequate treatment of erasure.

Definition 15 A Deterministic Erasure Event Structure (DEES) is a triple C = (E, ≤, ⊳), where E = (E, ≤) is a conflict-free PES and ⊳ ⊆ L_{fin}(E)×E is inessentiality or erasure relation (read α ⊳ e as: ‘e is α-inessential’), satisfying the following axioms, where α, β ∈ L_{fin}(E):

[E0] ∀e ∈ E : ∅ ⋫e;

[E1] α ⊳ e ∧ α ⊆ β ∈ L_{fin}(E) ⇒ β ⊳ e;

[E2] α ⊳ e′ ∧ α ⊳ e ∧ α − e′ ∈ L_{fin}(E) ⇒ α − e′ ⊳ e;

[E3] α ⊳ e ∧ e < e′ ⇒ α ⊳ e′;

[E4] α ∪ ⌈e⌉^{<} ⊳ e ⇒ α ⊳ e.

We may write α ⊳ X if ∀e ∈ X : α ⊳ e. Sometimes we write L_{fin}(P) for L_{fin}(E) if E is the domain of a DPES P, and similarly for L_{fin}(C).

Before explaining the intuition behind the axioms, we first define translations between DPESs and DEESs.

Definition 16 For a DPES P = (E, ≤, ≈), we define an erasure relation ⊳_{≈} ⊆ L_{fin}(E)×E and the corresponding structure C_{P} = (E, ≤, ⊳_{≈}) as follows:

• α ⊳_{≈} e iff α ∪ ⌈e⌉^{≤} ≈ (α ∪ ⌈e⌉^{≤}) \ ⌈e⌉^{≥}.

In particular, when e ∈ α and α − e ∈ L_{fin}(E), • α ⊳_{≈} e iff α ≈ α − e.

Definition 17 For a DEES C = (E, ≤, ⊳), we define an equivalence relation ≈_{⊳}⊆ L_{fin}(E) × L_{fin}(E) and the corresponding structure P_{C} = (E, ≤, ≈_{⊳}) as follows:

• α ≈_{⊳} β iff ST_{⊳}(α) = ST_{⊳}(β), where ST_{⊳}(α) = {e ∈ α | α ⋫e}. (The subscript ⊳ in ST_{⊳}(α) will often be omitted.) ST (α) will be called the standard variant of α.

By looking at a configuration α as an initial reduction P_{α} firing redexes corresponding to events in α, and by interpreting α ⊳ e as ‘Qv is P -inessential’, where Qv is a redex representing v (so Q contracts redexes corresponding to events on which e causally depends), it is not difficult to understand the intuition behind the erasure axioms. For example, [E0] says that an empty reduction cannot erase any redex, and [E1] says that if Qv is P_{α}-inessential and P_{α}⊴P_{β}, then Qv is P_{β}-inessential as well. This intuition will become more precise in the next section. Further, 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]. 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 Definition 6, a redex with history P v is Q-inessential iff v is Q/P -inessential. Similarly, [P0] corresponds to Lemma 7.(2).

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

Lemma 18 Let α ∈ L_{fin}(C), in a DEES C. Then ST (α) ∈ L_{fin}(C). Further, ST (ST (α)) = ST (α), hence α ≈_{⊳} ST (α).

Proof Let e ∈ ST (α) ∧ e′ < e. Then e ∈ α and α ⋫e, implying by [E3] that α ⋫e′. Since α ∈ L_{fin}(C) and e′ < e, e′ ∈ α, implying e′ ∈ ST (α). Hence ST (α) ∈ L_{fin}(C). If, on the contrary, ST (ST (α)) ≠ ST (α), i.e., ∃e′′ ∈ ST (α) : ST (α) ⊳ e′′, then α ⊳ e′′ by [E1], contradicting e′′ ∈ ST (α). Now α ≈_{⊳} ST (α) follows immediately from Definition 17.

Lemma 19 Let α ∈ L_{fin}(C), in a DEES C. Then α ⊳ e iff ST (α) ⊳ e.

Proof

(⇒) Let α = ST (α) ∪ {e_{1}, …, e_{n}}, where the enumeration e_{1}, …, e_{n} respects the order on E, let α_{0} = α, and let α_{i+1} = α_{i} + e_{i+1} (hence α = α_{n}). Denote e = e_{0}. By the definition of ST (α) and the assumption, we have α_{n} ⊳ e_{i} for all i = 0, 1, …, n. By [E2], we have from α_{n} ⊳ e_{n} and α_{n} ⊳ e_{i} that α_{n−1} ⊳ e_{i}. Hence, again by [E2], α_{n−2} ⊳ e_{i}, and so on. Finally, we get α_{0} ⊳ e_{i} for all i, and in particular, α_{0} ⊳ e.

(⇐) By [E1].

Lemma 20 Let α, β ∈ L_{fin}(E) and α ⊆ β, in a DEES C. Then ST (α) = ST (β) iff β ⊳ β \ α.

Proof

(⇒) By Definition 17, since β \ α ⊆ β \ ST (α). (⇐) Since β ⊳ β \ α, ST (β) ⊆ α. Let e′ ∈ ST (β). Then e′ ∈ β and β ⋫e′,

implying by [E1] and α ⊆ β that α ⋫e′, i.e., e′ ∈ ST (α). Hence ST (β) ⊆ ST (α). For the converse, take e′′ ∈ ST (α). Then e′′ ∈ α and α ⋫e′′. Therefore, e′′ ∈ β and by [E1] ST (β) ⋫e′′, implying by Lemma 19 that β ⋫e′′, i.e., e′′ ∈ ST (β). Hence ST (α) = ST (β).

Proposition 21 Let α, β, γ ∈ L_{fin}(C), in a DEES C, and let α ∩ β ⊆ γ ⊆ α ∪ β. Then ST (α) = ST (β) ⇔ γ ⊳ α ∪ β \ α ∩ β. Consequently, α ≈_{⊳} β iff γ ⊳ α ∪ β \ α ∩ β.

Proof

(⇒) ST (α) = ST (β) ⇒ ST (α) ⊆ α ∩ β, and by the definition of ST (α), Lemma 19, and [E1], ST (α) = ST (β) ⇒ ST (α) ⊳ β \ α ∪ α \ β ⇒ γ ⊳ α ∪ β \ α ∩ β.

(⇐) By [E1] and Lemma 20, α ∩ β ⊳ α ∪ β \ α ∩ β ⇒ α ⊳ α \ β ∧ β ⊳ β \ α ⇒ ST (α) = ST (α ∩ β) = ST (β).

Theorem 22 For any DEES C = (E, ≤, ⊳), P_{C} = (E, ≤, ≈_{⊳}) is a DPES.

Proof We need to show that ≈_{⊳} satisfies the permutation axioms [P0] – [P3].

[P0]: Let e ∈ E. Note that ⌈e⌉^{≤}⊳e would imply by [E2] that ⌈e⌉^{<}⊳e, implying ∅ ⊳ e by [E4], contradicting [E0]. Hence ⌈e⌉^{≤} ⋫e, i.e., e ∈ ST (⌈e⌉^{≤}), and therefore ST (⌈e⌉^{≤}) ≠ ST (⌈e⌉^{<}). Thus ⌈e⌉^{≤} ≉_{⊳} ⌈e⌉^{<} by Definition 17.

[P1]: Let α ≈_{⊳} β, α ∩ β ⊆ γ ⊆ α ∪ β, and γ ∈ L_{fin}(E). By Definition 17, ST (α) = ST (β), hence ST (α) ⊆ α ∩ β ⊆ γ. Further, ∀e ∈ α ∪ β \ ST (α), α ⊳ e or β ⊳ e, hence ST (α) ⊳ e by Lemma 19. Hence ST (ST (α)) = ST (γ) by Proposition 21, and ST (α) = ST (γ) by Lemma 18, implying γ ≈_{⊳} α by Definition 17.

[P2]: Let α ≈_{⊳} β and α+e, β+e ∈ L_{fin}(E). By Definition 17, ST (α) = ST (β). Assume first that ST (α)⊳e. Then α+e⊳e by [E1] and ST (α+e) = ST (α) by Proposition 21. Similarly, ST (β+e) = ST (β). Hence, ST (α+e) = ST (β+e), implying by Definition 17 that α + e ≈_{⊳} β + e. Now let ST (α) ⋫e. Then, by Lemma 19 and [E3], ∀e′ ∈ α \ ST (α) : e′ ≮ e. Thus α + e ∈ L_{fin}(E) ⇒ ST (α) + e ∈ L_{fin}(E). By Lemma 19, ST (α) ⋫e implies α ⋫e, thus e ∈ ST (α) iff e ∈ α, and therefore α + e \ (ST (α) + e) = α \ ST (α). Hence α + e ⊳ α + e \ (ST (α) + e) by [E1] (as α ⊳ α \ ST (α)), and we have by Proposition 21 that ST (α + e) = ST (ST (α) + e), thus α + e ≈_{⊳} ST (α) + e by Definition 17. Similarly, β + e ≈_{⊳} ST (β) + e, implying α + e ≈_{⊳} β + e (since ST (α) = ST (β)).

[P3]: Let α ≈_{⊳} α − e, e < e′ and α + e′ ∈ L_{fin}(E) (hence e ∈ α). By Definition 17, ST (α) = ST (α − e), implying α ⊳ e. Hence, by [E3], α ⊳ e′, implying by [E1] that α + e′ ⊳ e′. Hence, by Proposition 21, ST (α + e′) = ST (α), thus α + e′ ≈_{⊳} α by Definition 17.

Theorem 23 For any DPES P = (E, ≤, ≈), C_{P} = (E, ≤, ⊳_{≈}) is a DEES.

Proof We need to show that ⊳_{≈} satisfies the erasure axioms [E0] – [E4].

[E0]: By Definition 16 and [P0]. [E3]: Let α⊳_{≈}e and e < e′. We want to show that α⊳_{≈}e′. We can assume that

∄e′′ : e < e′′ < e′. Assume first that e, e′ ∈ α (hence α ∪ ⌈e⌉^{≤} = α ∪ ⌈e′⌉^{≤} = α). By Definition 16, α ⊳_{≈} e ⇒ α ≈ α \ ⌈e⌉^{≥}. But α \ ⌈e⌉^{≥} ⊆ α \ ⌈e′⌉^{≥} ⊆ α, implying by [P1] that α ≈ α \ ⌈e′⌉^{≥}, i.e., by Definition 16, α ⊳_{≈} e′. Now let e ∈ α and e′ ∉ α. Let γ = α \ ⌈e⌉^{>}. By Definition 16, α ⊳_{≈} e iff γ ⊳_{≈} e iff γ ≈ γ − e. Further, γ ∪ ⌈e′⌉^{≤} = γ + e′ and γ ∪ ⌈e′⌉^{≤} \ ⌈e′⌉^{≥} = γ. By [P3], γ ≈ γ + e′, implying γ ⊳_{≈} e′ and equivalently α ⊳_{≈} e′ by Definition 16. Finally, let e, e′ ∉ α. Take β = α ∪ ⌈e⌉^{≤}. Then, by Definition 16, α ⊳_{≈} e iff β ⊳_{≈} e and α ⊳_{≈} e′ iff β ⊳_{≈} e′, and we have e ∈ β and e′ ∉ β like in the previous case, and [E3] follows.

[E1]: Let α⊳_{≈}e ∧ α ⊆ β ∈ L_{fin}(E). We can assume that β = α+e′ and e′ ∉ α. If e ≥ e′, then α+e′∪⌈e⌉^{≤} = α∪⌈e⌉^{≤} and α+e′∪⌈e⌉^{≤}\⌈e⌉^{≥} = α∪⌈e⌉^{≤}\⌈e⌉^{≥}, thus α ⊳_{≈} e iff α + e′ ⊳_{≈} e by Definition 16. If e ≮ e′ and e′ ≮ e, then α + e′ ∪ ⌈e⌉^{≤} = α ∪ ⌈e⌉^{≤} + e′ and α + e′ ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥} = α ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥} + e′, and α + e′ ⊳_{≈} e follows from α ⊳_{≈} e by [P2] and Definition 16. Finally, if e < e′, then α + e′ ∈ L_{fin}(E) ⇒ e ∈ α. By [E3] which we have already proven above for ⊳_{≈}, α ⊳_{≈} e ⇒ α ⊳_{≈} e′; thus by Definition 16 we have from α ⊳_{≈} e that α = α ∪ ⌈e⌉^{≤} ≈ α ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥}, and we have from from α ⊳_{≈} e′ that α ≈ α + e′. Hence α + e′ ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥} ≈ (since e < e′) ≈ α∪⌈e⌉^{≤} \⌈e⌉^{≥} ≈ α ≈ α+e′ = α+e′ ∪⌈e⌉^{≤}, which means by Definition 16 that α + e′ ⊳ e.

[E2]: We can assume that e′ ∈ α. Let α⊳_{≈} e′, α⊳_{≈} e and α−e′ ∈ L_{fin}(E). By Definition 16, α⊳_{≈} e ⇒ α∪⌈e⌉^{≤} ≈ α∪⌈e⌉^{≤} \⌈e⌉^{≥} and α⊳_{≈} e′ ⇒ α ≈ α−e′, implying by repeated application of [P2] that α ∪ ⌈e⌉^{≤} ≈ α − e′ ∪ ⌈e⌉^{≤}. It is easy to check that (α ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥}) ∩ (α − e′ ∪ ⌈e⌉^{≤}) = (α ∪ ⌈e⌉^{≤}) ∩ (α − e′ ∪ ⌈e⌉^{≤}) \ ⌈e⌉^{≥} = α − e′ ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥} implying by [P1] that α − e′ ∪ ⌈e⌉^{≤} ≈ α − e′ ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥}. Hence, α − e′ ⊳_{≈} e by Definition 16.

[E4]: We need to show that α∪⌈e⌉^{<} ⊳_{≈} e ⇒ α⊳_{≈} e. Indeed, by Definition 16, α∪⌈e⌉^{<}⊳e iff (α∪⌈e⌉^{<})∪⌈e⌉^{≤}\⌈e⌉^{≥} ≈ (α∪⌈e⌉^{<})∪⌈e⌉^{≤} ⇔ α∪⌈e⌉^{≤}\⌈e⌉^{≥} ≈ α ∪ ⌈e⌉^{≤} iff α ⊳_{≈} e.

Lemma 24 Let P = (E, ≤, ≈) be a DPES, and let α ∈ L_{fin}(E). Then α ≈ ST_{⊳_{≈}}(α).

Proof By Theorem 23 and Lemma 18, ST_{⊳_{≈}}(α) is a configuration. Let α \ ST_{⊳_{≈}}(α) = {e_{1}, …, e_{n}}. By Definition 16, α ⊳_{≈} e_{i} ⇒ α ≈ α \ ⌈e_{i}⌉^{≥}. Clearly, ∩_{i=1}^{n}α \ ⌈e_{i}⌉^{≥} ⊆ ST_{⊳_{≈}}(α) ⊆ α, implying by [P1] and α ≈ α \ ⌈e_{i}⌉^{≥} that α ≈ ST_{⊳_{≈}}(α).

The next proposition gives a characterization of ≈ via ⊳_{≈}, needed for establishing an isomorphism between DPESs and DEESs.

Proposition 25 In a DPES P = (E, ≤, ≈), α ≈ β iff ST_{⊳_{≈}}(α) = ST_{⊳_{≈}}(β).

Proof

(⇐) Immediate from Lemma 24. (⇒) By Lemma 24, α ≈ ST_{⊳_{≈}}(α) ≈ ST_{⊳_{≈}}(β). Suppose on the contrary that

ST_{⊳_{≈}}(α) ≠ ST_{⊳_{≈}}(β), say ∃e ∈ ST_{⊳_{≈}}(α) \ (ST_{⊳_{≈}}(α) ∩ ST_{⊳_{≈}}(β)). By [P1], ST_{⊳_{≈}}(α) ≈ ST_{⊳_{≈}}(α) ∩ ST_{⊳_{≈}}(β). Further, ST_{⊳_{≈}}(α) ∩ ST_{⊳_{≈}}(β) ⊆ α \ ⌈e⌉^{≥} ⊆ α (since ST_{⊳_{≈}}(α) ∩ ST_{⊳_{≈}}(β) is left-closed), hence again by [P1] α ∪⌈e⌉^{≤} \⌈e⌉^{≥} = α \⌈e⌉^{≥} ≈ α = α ∪⌈e⌉^{≤}, implying by Definition 16

that α ⊳_{≈} e, contradicting e ∈ ST_{⊳_{≈}}(α).

Theorem 26 (Equivalence of DPESs and DEESs)

(1) For any DEES C = (E, ≤, ⊳), C_{P_{C}} = C.

(2) For any DPES P = (E, ≤, ≈), P_{C_{P}} = P.

Proof Note that the translations of DEESs into DPES and vice versa does not effect the sets of events and the causality relation. Thus C_{P_{C}} = (E, ≤, ⊳_{≈_{⊳}} ) and P_{C_{P}} = (E, ≤, ≈_{⊳_{≈}}). We need to show that (1) ⊳ = ⊳_{≈_{⊳}} and (2) ≈=≈_{⊳_{≈}}.

(1) We need to prove that α⊳e in C iff α⊳_{≈_{⊳}} e in C_{P_{C}}. By [E4], [E1] and [E3], α⊳e iff α∪⌈e⌉^{≤}⊳e iff α∪⌈e⌉^{≤}⊳⌈e⌉^{≥}. By Proposition 21, the latter holds iff ST_{⊳}(α ∪ ⌈e⌉^{≤}) = ST_{⊳}(α ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥}), which, by Definition 17 means that α ∪ ⌈e⌉^{≤} ≈_{⊳} α ∪ ⌈e⌉^{≤} \ ⌈e⌉^{≥}, meaning α ⊳_{≈_{⊳}} e by Definition 16.

(2) We need to prove that α ≈ β in P iff α ≈_{⊳_{≈}} β in P_{C_{P}}. By Proposition 25 and Definition 17, α ≈ β iff ST_{⊳_{≈}}(α) = ST_{⊳_{≈}}(β) iff α ≈_{⊳_{≈}} β.

From now on, we will merge DEESs C = (E, ≤, ⊳) and DPESs P = (E, ≤, ≈) into one model (E, ≤, ⊳, ≈), where (E, ≤) is a Prime Event Structure, the erasure relation ⊳ satisfies axioms [E0] - [E4], and ≈=≈_{⊳}. The obtained results allow us to assume that the permutation-equivalence ≈ satisfies axioms [P0] - [P3], and that ⊳ = ⊳_{≈}. We call such models again DEESs, and denote by C.

4 Relating Conflict-Free Stable Transition and Event models

We now define translations between AZDFSs and DEESs and show that they commute, implying equivalence of the two computational models.

4.1 Translation of ASDRSs and AZDFSs into DEESs

Definition 27 With an ASDRS R and its corresponding AZDFS F = F_{R} = (R, ≃_{z}, ↪_{z}), we associate the DEES C_{R} = C_{F} = (E_{F}, ≤, ⊳, ≈), where

• E_{F} = F AM(F), the set of all families of F;

• ϕ < ψ iff ϕ ↪_{z} ψ;

• α ≈ β iff ∀ϕ ∈ α ∪ β \ α ∩ β, ∃P : t_{∅} → → s : F AM(P) ⊆ α ∩ β and P discards a canonical element of ϕ (see Theorem 13);

• α ⊳ ϕ iff ∃P : t_{∅} → → s : F AM(P) ⊆ α and P discards a canonical element of ϕ.

We need to check that C_{F} in the above definition is indeed a DEES. We need a number of technical lemmas to achieve this.

Lemma 28 Let Q : t → → s, v ⊆ t, Q′ ∈ ST V (Q), and let v be Q-inessential, in an ASDRS. Then Q′ discards v.

Proof Since v is Q-inessential, v/Q = ∅ and v is Q-unneeded. Since Q′ is Q-needed, it is external to v by Lemma 7.(4), and v/Q′ = v/Q = ∅, i.e., Q′ discards v.

Lemma 29 Let Q : t → → s be standard and let t→^{u}o, in an ASDRS. Then Q/u is standard.

Proof By induction on the length of Q. Let Q′ = Q/u. Suppose on the contrary that Q′ is not standard and let w′ be the last Q′-unneeded step in Q′, say Q′ = Q′_{1} + w′ + Q′_{2}, and let Q = Q_{1} + w + Q_{2}, where w′ = w/u′ and u′ = u/Q_{1} (see the figure).

[figure: t; Q_{1}; w; Q_{2}; o; u; Q′_{1}; u′; w′; Q′_{2}]

By Lemma 7.(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 Lemma 7.(3). Since w +Q_{2} is self-needed and w′ +Q′_{2} is not, u′ ≠ ∅. Hence, by [stability], w does not create v. Thus w′ and v′, as well as w and v, can be permuted in w′ + v′ + Q′_{3} and w + v + Q_{3}, respectively, yielding v^{′∗} + w^{′∗} + Q′_{3} and v^{∗} + w^{∗} + Q_{3} (see the figure below). Then by Lemma 7.(4), w^{∗} + Q_{3} is self-needed and w^{′∗} + Q′_{3} is not self-needed (and therefore u′′ = u′/v^{∗} ≠ ∅), contradicting the induction assumption.

[figure: t; Q_{1}; v^{∗}; w^{∗}; Q_{3}; o; u; Q′_{1}; u′; v^{′∗}; u′′; w^{′∗}; Q′_{3}]

Lemma 30 Let Q : t → → s, P : t → → o, v ⊆ o, Q′ ∈ ST V (Q), and let P v be Q-inessential, in an ASDRS. Then Q′ discards P v.

Proof By Lemma 29, Q′/P ∈ ST V (Q/P). And since v is Q/P -inessential, Q′/P discards v by Lemma 28.

Lemma 31 Let P : t → → s, Q : t → →^{Q′} o→^{u}e→^{v}s′, let Q′u be P -inessential, and let u create v, in an ASDRS. Then (Q′ + u)v is P -inessential too.

Proof Let P′ = ST (P), P′′ = P′/Q′, and P^{∗} = P′′/u. By Lemma 30, P′′ discards u. So let w be the step of P′′ that discards a residual u′ of u, and let v′ be the corresponding residual of v along P^{∗}, see the figure. If v′ ≠ ∅, then v′/(w/u′) = ∅ by [stability] (since u′/w = ∅)). So, in any case, v/P^{∗} = ∅. By the Stability Lemma, P^{∗} is external to v (since P′′ is external to u). Hence P^{∗} discards v, i.e. v is P -inessential.

[figure: P′]
[figure: Q′; w ∈ P′′]
[figure: u; u′; w′ ∈ P^{∗}; ∅; ∅]
[figure: v; v′; ∅; ∅]

Lemma 32 Let P : t_{∅} → → s, ϕ be a family in an AZDFS F, let Qv, Q′v′ ∈ ϕ, and let Qv be canonical. If Qv is P -inessential, then so is Q′v′. Further, if Q′ ⊴ P, then the converse is also true.

Proof By the Affine Extraction Theorem, there is Q′′ such that Q′ ≈ Q + Q′′ and v′ = v/Q′′. If Qv is P -inessential, then ST (P)/Q discards v by Lemma 30, and ST (P)/Q′ discards v′ by the Cube Lemma. Conversely, if Q′ ⊴ P, then Q′′/(P/Q) = ∅, and v′/(P/Q′) = v/(P/Q) = ∅ again by the Cube Lemma, thus Qv is P -inessential.

Lemma 33 Let t_{∅} → →^{Q} s→^{u}s′, let t_{∅} → →^{P} o→^{v}o′, and let Qu ≃_{z} P v, in an AZDFS F. Then v/((Q + u)/P) = ∅.

Proof If v′ = v/(Q/P) = ∅, then we are done. Otherwise, by the Affine Extraction Theorem, there are Nw ≃_{z} Qu and reductions N′ and N′′ such that Q ≈ N +N′, P ≈ N +N′′, u = w/N′ and v = w/N′′. Further, N′+P/Q ≈ N′′ + Q/P, and by the Cube Lemma, v′ = w/(N′ + P/Q). But u is the only N′-residual of w, thus v′ = u/(P/Q), implying v/((Q + u)/P) = ∅.

Lemma 34 Let P ∈ ST A, F AM(P) = F_{1} ∪ F_{2}, F_{1} ∩ F_{2} = ∅ and ∀ϕ ∈ F_{2}, ∀ψ ∈ F_{1} : ϕ ↛ ψ, in an AZDFS F. Then ∃Q ∈ ST V (P) : Q = Q_{1} + Q_{2} ∧ F AM(Q_{i}) = F_{i}, i = 1, 2.

Proof Let u be the latest step in P such that ϕ = F am(u) ∈ F_{2} and it has a next step v with ψ = F am(v) ∈ F_{1}. Then ϕ ↛ ψ by the hypothesis, and u does not create v by [creation]. Hence u and v can be permuted, yielding another standard reduction by Lemma 7.(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 the reduction.

Theorem 35 For any AZDFS F, C_{F} is a DEES.

Proof We need to show that C_{F} = (E_{F}, \underline{↪}, ⊳, ≈) satisfies the erasure axioms [E0] – [E4], and that ≈=≈_{⊳}.

[E0]: Immediate from Definitions 6 and 27. [E1]: Again from Definitions 6 and 27. [E2]: Let α⊳ϕ, α⊳ϕ′, and let α−ϕ ∈ L_{fin}(E). Then there are P and P′ such

that F AM(P), F AM(P′) ⊆ α, a canonical element Qv of ϕ is P -inessential, and a canonical element Q′v′ of ϕ′ is P′-inessential. Let P^{∗} = P ⊔ P′. Then F AM(P^{∗}) ⊆ α and both Qv and Q′v′ are P^{∗}-inessential. By Lemma 32, all members of ϕ and ϕ′ are P^{∗}-inessential. Since ST (P^{∗}) is P^{∗}-essential, it does not contract members of ϕ and ϕ′. Hence F AM(ST (P^{∗})) ⊆ α − ϕ′, and α − ϕ′ ⊳ ϕ by Definition 27.

[E3]: Let α ⊳ ϕ and ϕ ↪ ϕ′. It is enough to consider the case when ∄ϕ′′ : ϕ ↪ ϕ′′ ↪ ϕ′. By Lemma 34 and the Affine Extraction Theorem, there is a canonical P′v′ ∈ ϕ′ such that P′ = P + v, v creates v′, and P v ∈ ϕ. Further, by Definition 27, ∃Q : F AM(Q) ⊆ α which discards a canonical element of ϕ. Hence, by Lemmas 32, 31 and 30, ST (Q) discards P′v′, i.e., α ⊳ ϕ′.

[E4]: Let α ∪ ⌈ϕ⌉^{<} ⊳ ϕ. By Definition 27, there is a Q such that F AM(Q) ⊆ α ∪ ⌈ϕ⌉^{<} and Q discards a canonical element P v of ϕ. By Proposition 11 and Lemma 30, Q can be chosen standard. Let F_{2} = F AM(Q) ∩ (⌈ϕ⌉^{<} \ α) and F_{1} = F AM(Q) \ F_{2}. Since α ∈ L_{fin}(E), ∀ϕ ∈ F_{2}, ψ ∈ F_{1} : ϕ ↛ ψ. Hence, by Lemma 34, ∃Q′ ∈ ST V (Q) : Q′ = Q_{1} + Q_{2} ∧ F AM(Q_{i}) = F_{i}. By Lemma 30, Q′ discards P v, and by Lemma 33, Q′/P = Q_{1}/P, since

⌈ϕ⌉^{<} = F AM(P). Hence Q_{1} discards P v and F AM(Q_{1}) ⊆ α, i.e., α ⊳ ϕ.

It remains to show that ≈=≈_{⊳}. Indeed, by Definition 27, α ≈ β iff α ∩ β ⊳ α ∪ β \ α ∩ β, and by Proposition 21, the latter holds iff α ≈_{⊳} β.

4.2 Translation of DEESs into ASDRSs and AZDFSs

The following translation of DEESs into ASDRSs uses a techniques resembling the representation of events in a PES as prime intervals of its configuration domain, used for construction of PESs from stable families of configurations in [37].

Definition 36 With a DEES C = (E, ≤, ⊳, ≈) we associate an ASDRS R_{C} as follows:

• The terms of R_{C} are Lévy-equivalence classes ⟨α⟩_{L}, ⟨β⟩_{L}, … of configurations of C;

• The reduction relation of R_{C} consists of sets of pairs u = (⟨α⟩_{L}, e), where α, α+e ∈ L_{fin}(E) and α ≉ α+e. Pairs u = (⟨α⟩_{L}, e) such that α ≈ α+e are identified with the empty redex ∅ = (⟨α⟩_{L}, ∅) in ⟨α⟩_{L}. A non-empty redex (⟨α⟩_{L}, e) will also be called an e-redex.

• The residual relation is defined as follows: if u = (⟨α⟩_{L}, e) and v = (⟨α⟩_{L}, e′), then u/v = (⟨α + e′⟩_{L}, e). (Thus u/v = ∅ iff α + e′ ≈ α + e′ + e.)

Next we show that the definition above is correct.

Theorem 37 Let C = (E, ≤, ⊳, ≈) be a DEES. Then R_{C} is an ASDRS.

Proof For any step v : ⟨α⟩_{L} →^{(⟨α⟩_{L},e)}⟨α + e⟩_{L} in R_{C}, and any redex u = (⟨α⟩_{L}, e′) in ⟨α⟩_{L}, u/v is either a (non-empty) redex in ⟨α + e⟩_{L}, or u/v = ∅. Also, for any other redex w = (⟨α⟩_{L}, e′′) in ⟨α⟩_{L} such that w/v ≠ ∅, w/v = (⟨α + e⟩_{L}, e′′) ≠ (⟨α + e⟩_{L}, e′) = u/v, i.e., no redex in ⟨α + e⟩_{L} is a residual of more than one redex in ⟨α⟩_{L}. Further, v/v = (⟨α + e⟩_{L}, e) = ∅. So to show that R_{C} is an ASDRS, it remains to show [FD], [weak acyclicity], and [stability].

[FD] let U be a set of redexes in ⟨α⟩_{L}, let e_{0}, …, e_{l−1} be an enumeration of U, and let α_{n} = α + e_{0} + … + e_{n−1} (0 ≤ n ≤ l). Then a complete development

of U has a form P : ⟨α_{0}⟩_{L} →^{(⟨α_{0}⟩_{L},e_{0})}⟨α_{1}⟩_{L} →^{(⟨α_{1}⟩_{L},e_{1})} … → ⟨α_{k}⟩_{L}, where for

any m = k, …, l − 1, (⟨α_{0}⟩_{L}, e_{m})/P = ∅, that is, ⟨α_{k}⟩_{L} = ⟨α_{k} + e_{m}⟩_{L}. We show by induction on j = l − k that α_{k} ≈ α_{k} + e_{k} + … + e_{l−1}. The case j = 1 (i.e., α_{k} ≈ α_{k} + e_{k}) is immediate. By the induction assumption, α_{k} ≈ α_{l−2} ≈ α_{l−2}+e_{l−2} ≈ α_{l−2}+e_{l−1}. By [P2], α_{l−2}+e_{l−2}+e_{l−1} ≈ α_{l−2}+e_{l−1}. Hence, α_{k} ≈ α_{l−2} + e_{l−2} + e_{l−1} = α_{l}. Thus every complete development of U ends at ⟨α_{k}⟩_{L} = ⟨α_{l}⟩_{L}. Further, for any u = (⟨α⟩_{L}, e), u/P = (⟨α_{k}⟩_{L}, e), i.e., u/U does not depend on the particular complete development of U, hence [FD] holds.

[weak acyclicity] Let u = (⟨α⟩_{L}, e), v = (⟨α⟩_{L}, e′), e ≠ e′, and suppose u/v = v/u = ∅. That is, α+e+e′ ≈ α+e ≈ α+e′. Then, by [P1], α+e ≈ α+e′ ≈ α, i.e, u = v = ∅.

[stability] Suppose on the contrary that R_{C} is not stable. Then there are u ≠ v, w, w′ and w′′ such that w and w′ are created by u and v respectively, and w′′ = w/v′ = w′/u′ ≠ ∅, where u′ = u/v and v′ = v/u. That is, there are u = (⟨α⟩_{L}, e), v = (⟨α⟩_{L}, e′), w = (⟨α + e⟩_{L}, e′′), w′ = (⟨α + e′⟩_{L}, e′′), and w′′ = (⟨α + e + e′⟩_{L}, e′′) such that ⟨α⟩_{L}, ⟨α + e⟩_{L} and ⟨α + e + e′′⟩_{L} are different; so are ⟨α⟩_{L}, ⟨α + e′⟩_{L} and ⟨α + e′ + e′′⟩_{L}; and ⟨α + e + e′⟩_{L} ≠ ⟨α + e + e′ + e′′⟩_{L} (see the diagram). Further, (⟨α⟩_{L}, e′′) is not a redex since w is a created redex. Hence either α + e′′ ∉ L_{fin}(C), or α + e′′ ∈ L_{fin}(C) and α ≈ α + e′′; but the latter would imply by [P2] that α + e + e′′ ≈ α + e, contradicting the fact that w is a non-empty redex. Thus α + e + e′′ and α + e′ + e′′ are both configurations, but their intersection α + e′′ is not – a contradiction, since the intersection of left-closed subsets remains left-closed.

[figure: ⟨α⟩_{L}; u; ⟨α + e⟩_{L}; w; ⟨α + e + e′′⟩_{L}]
[figure: ⟨α + e′⟩_{L}; v; u′; ⟨α + e + e′⟩_{L}; v′]
[figure: w′′]
[figure: ⟨α + e′ + e′′⟩_{L}; w′; ⟨α + e + e′ + e′′⟩_{L}]

The theorem is now proved.

Clearly, an initial reduction in an ASDRS R_{C} can be represented as a leftclosed enumeration e_{1}, …, e_{k} of a configuration α where no event e_{i} in the sequence is vacuous, i.e., ∀i : {e_{1}, …, e_{i−1}} ⋫e_{i}; the event e_{i} represents the non-empty redex ({e_{1}, …, e_{i−1}}, e_{i}). We call such a sequence also an initial reduction or an α-reduction in the DEES C, written [α]. Thus we have the following lemma:

Lemma 38 Let C be a DEES, and let R_{C} be its corresponding ASDRS. Then there is a 1 − 1 correspondence between initial reductions in C and R_{C}.

Note that, unlike PESs, not every configuration in a DEES has a reduction. For example, consider the DEES consisting of four events {e_{1}, e_{2}, e′_{1}, e′_{2}}, ordered as follows: e_{1} < e′_{1} and e_{2} < e′_{2}, and let ⊳ be given by: α ⊳ e′_{1} iff e_{2} ∈ α, and α ⊳ e′_{2} iff e_{1} ∈ α. Then {e_{1}, e_{2}, e′_{1}, e′_{2}} is a configuration, but any of its left-closed enumerations, such as e_{1}, e_{2}, e′_{1}, e′_{2}, ends either with e′_{1} or with e′_{2}, and we have {e_{1}, e_{2}, e′_{2}} ⊳ e′_{1} and {e_{1}, e_{2}, e′_{1}} ⊳ e′_{2}. This is not surprising as the vacuous events in left-closed sequences correspond to empty reductions in the corresponding ASDRS, performed in the ‘garbage’ (erased redexes). However, we have the following lemma:

Lemma 39 Let α ∈ L_{fin}(E), in a DEES. Then any left-closed enumeration of ST (α) is a reduction.

Proof Let e_{0}, …, e_{n} be a left-closed enumeration of ST (α). If there was an i such that e_{0}, …, e_{i−1} ⊳ e_{i}, then α ⊳ e_{i} by [E1], contradicting e_{i} ∈ ST (α).

Definition 40 With a DEES C = (E, ≤, ⊳, ≈), we associate a DFS F_{C} = (R_{C}, ≃_{C}, ↪_{C}) as follows:

• R_{C} is the DRSs defined in Definition 36.

• ∀e ∈ E, we define the ≃_{C}-family ϕ_{e} corresponding to e, or the e-family, as the set of all e-redexes ([α], e). That is, ([α], e) ≃_{C} ([β], e′) iff e = e′.

• Define ↪_{C} by: ϕ_{e} ↪_{C} ϕ_{e′} iff e < e′.

Theorem 41 Let C = (E, ≤, ⊳, ≈) be a DEES, let F_{C} = (R_{C}, ≃_{C}, ↪_{C}), and let F_{R_{C}} = (R_{C}, ≃_{z}, ↪_{z}). Then F_{C} = F_{R_{C}}, hence F_{C} is an AZDFS.

Proof We need to show that (a) ≃_{z}=≃_{C} and (b) ↪_{z}=↪_{C}.

(a) By Definition 36, ([α], e) ≃_{z} ([β], e′) ⇒ e = e′, implying ≃_{z}⊆≃_{C}. For the converse, consider two redexes ([α], e) ≃_{C} ([β], e). Then ([α ∩ β], e) is also a redex since α ∩ β + e = α + e ∩ β + e ∈ L_{fin}(E), and ([α], e) and ([β], e) are its residuals. (Note that (⟨α ∩ β⟩_{L}, e) ≠ ∅ since (⟨α ∩ β⟩_{L}, e) = ∅ ⇒ (⟨α⟩_{L}, e) = ∅ by [P2].) Hence ([α], e) ≃_{z} ([β], e).

(b) In order to show that ϕ_{e} ↪_{C} ϕ_{e′} ⇔ ϕ_{e} ↪_{z} ϕ_{e′}, we need to show that e < e′ iff e ∈ [γ] for any ([γ], e′) ∈ ϕ_{e′} (by (a), ϕ_{e}, ϕ_{e′} are families both w.r.t. ≃_{C} and ≃_{z}). Sufficiency is immediate since γ + e′ is left closed. For the converse, we have from Theorem 13 that ([⌈e′⌉^{<}], e′) is a canonical element of ϕ_{e′} (when ϕ_{e′} is considered as a ≃_{z}-family), hence e < e′.

4.3 Equivalence of the transition and event models

We now establish an equivalence between DEESs and AZDFSs, implying together with the results of previous sections equivalence of the considered four transition and event models – ASDRSs, AZDFSs, DEESs and DPESs.

Let R be a DRS. Let us define the reduction tree of R to be a tree whose nodes are labelled with terms in R, whose root is labelled with t_{∅}, the initial term of R, and whose arcs correspond to redexes in R. 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 R has cycles, its reduction tree is a tree. Thus the branches of the reduction tree of R are in 1 − 1 correspondence with initial reductions in R. We call two such trees isomorphic if the trees obtained by removing all labels are identical. Hence, we can define two DRSs to be isomorphic if there is an isomorphism between their reduction trees preserving the residual relation. An isomorphism between two DFSs must further preserve the family and contribution relations.

Lemma 42 Let F be an AZDFS and let C_{F} be its corresponding DEES.

(1) For any initial reduction [α] = e_{0}, e_{1}, …, e_{n} in C_{F} there is a unique initial reduction g([α]) = P : t_{∅} = t_{0}→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{n−1}}t_{n} in F such that

F am(P_{i}u_{i}) = e_{i}, where P_{i} : t_{∅} = t_{0}→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i}. (Thus F AM(P) = α.)

(2) Let P : t_{∅} = t_{0}→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{n−1}}t_{n} in F, and let e_{i} = ϕ_{i} = F am(P_{i}u_{i}), where

P_{i} : t_{∅} = t_{0}→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i}. Then f(P) = e_{0}, e_{1}, …, e_{n} is a reduction

in C_{F}.

(3) the translation functions g and f between reductions in F and C_{F} commute: for any initial reduction P in F, g(f(P)) = P, and for any reduction [α] in C_{F}, f(g([α])) = [α].

Proof

(1) By definition of a reduction in a DEES, e_{0}, e_{1}, …, e_{n} is left-closed, and {e_{0}, …, e_{j−1}} ⋫e_{j} for any j = 0, …, n. Take for u_{0} the redex in t_{∅} such that F am(∅u_{0}) = e_{0}; existence of such a redex is immediate from the definition of C_{F}, and uniqueness follows from [initial]. Suppose u_{1}, …, u_{i−1} are already defined so that F am(P_{k}u_{k}) = e_{k} for all 1 ≤ k < i. We need to show that ∃u_{i} ∈ t_{i} such that F am(P_{i}u_{i}) = e_{i}; uniqueness of such a redex follows from the separability of F (see Theorem 12) 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 [18], or Lemma 5.2 in [20]). Let N_{i}v_{i} be a canonical element of e_{i} which exists by the Affine Extraction Theorem. By the same theorem, N_{i} contracts exactly one redex in every contributor family of e_{i} (and does not contract any other redex). Thus, by [contribution], F AM(N_{i}) ⊆ F AM(P_{i}), and N_{i} ⊴ P_{i} by Proposition 11. Now we can take u_{i} = v_{i}/(P_{i}/N_{i}). If on the contrary u_{i} = ∅, then P_{i} would discard N_{i}v_{i} (since P_{i}/N_{i} is external to v_{i} as F am(N_{i}v_{i}) ∉ F AM(P_{i})), and we would have by Definition 27 that {e_{0}, …, e_{i−1}}⊳e_{i}, contradicting the assumption. Thus a reduction P as above exists, and is unique.

(2) We need to show that f(P) = e_{0}, e_{1}, …, e_{n} is left-closed and does not contain vacuous events (by Definition 27, ϕ_{i} = e_{i} are events in C_{F}). By [contribution], P_{i} contracts at least one redex in every contributor family of ϕ_{i}, hence f(P) is left-closed. If on the contrary say ϕ_{j} is vacuous, i.e., {ϕ_{0}, …, ϕ_{j−1}} ⊳ ϕ_{j}, then by Definition 27 there is an initial reduction Q such that F AM(Q) ⊆ {ϕ_{0}, …, ϕ_{j−1}} and Q discards a canonical element N_{j}v_{j} of ϕ_{j}. By Proposition 11, N_{j}, Q ⊴ P_{j}, and by Definition 6, P_{j} erases N_{j}v_{j}, i.e., v_{j}/(P_{j}/N_{j}) = ∅. Hence u_{j}/((N_{j} + v_{j})/P_{j}) = u_{j}/∅ = u_{j}, contradicting Lemma 33 (since N_{j}v_{j} ≃_{z} P_{j}u_{j}).

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

Theorem 43 (Equivalence of AZDFSs and DEESs)

(1) For any DEES C, C and C_{F_{C}} are isomorphic.

(2) For any AZDFS F, F and F_{C_{F}} are isomorphic.

Proof

(1) Let C = (E, ≤, ⊳, ≈) and C′ = C_{F_{C}} = (E′, ≤′, ⊳′, ≈′). By Definitions 40 and 27, E′ = {ϕ_{e}|e ∈ E}, where ϕ_{e} is the e-family of F_{C}. We show that f : e ↦ ϕ_{e} is an isomorphism between C and C′. Since f clearly an isomorphism between E and E′, and since C′ is a DEES by Theorems 35 and 41, we need to show that (a) e ≤ e′ iff ϕ_{e} ≤′ ϕ_{e′}; and (b) α ≈ β iff ϕ_{α} ≈′ ϕ_{β}, where ϕ_{α} = {ϕ_{e}|e ∈ α} and ϕ_{β} = {ϕ_{e}|e ∈ β}.

(a) Immediate from Definitions 40 and 27.

(b) By Definition 27, ϕ_{α} ≈′ ϕ_{β} iff ∀e ∈ α ∪ β \ α ∩ β, there is a reduction [γ] in F_{C} such that F AM([γ]) ⊆ ϕ_{α} ∩ ϕ_{β} and [γ] discards a canonical element [⌈e⌉^{<}]e of ϕ_{e} (see Theorem 13). By Definitions 6 and 36, the latter means that e ∉ γ, γ ⊆ α ∩ β, and γ ∪ ⌈e⌉^{<} ≈ γ ∪ ⌈e⌉^{≤}, thus by Definition 16, and Lemmas 39 and 19 we need to prove that α ≈ β iff ∃ standard γ : γ ⊆ α ∩ β ∧ γ ⊳ α ∪ β \ α ∩ β. But this is immediate from Proposition 21 (since ≈=≈_{⊳}) and Lemma 19.

(2) By Theorem 41 and Theorem 35, F_{C_{F}} is an AZDFS, hence it is enough to show that the underlying ASDRSs R and R_{C_{F}} of F and F_{C_{F}} are isomorphic. This follows immediately from Lemmas 42 and 38.

5 Lévy’s Configuration Domains

Next we define Lévy’s configuration domains in DEESs and show that they are isomorphic to Lévy’s reduction spaces in corresponding ASDRSs.

Definition 44 (1) Let C be a DEES. Then Lévy’s configuration domain L_{fin}^{⊴}(C) = (L_{fin}^{≈}(C), ⊴), where L_{fin}^{≈}(C) = L_{fin}(C)/_{≈} = {⟨α⟩_{L}|α ∈ L_{fin}(C)} and ⊴ is a partial order defined by: ⟨α⟩_{L} ⊴ ⟨β⟩_{L} iff ∃β′ ∈ ⟨β⟩_{L} : α ⊆ β′.

(2) Let R be an ASDRS, and let L_{fin}(R) be the set of initial reductions in R. Then Lévy’s reduction space L_{fin}^{⊴}(R) = (L_{fin}^{≈}(R), ⊴), where L_{fin}^{≈}(R) = L_{fin}(R)/_{≈} = {⟨P ⟩_{L}|P ∈ L_{fin}(R)}, and ⟨P ⟩_{L} ⊴ ⟨Q⟩_{L} iff P ⊴ Q.

Note that if ⟨α⟩_{L} ⊴ ⟨β⟩_{L}, α ≈ α′ and β ≈ β′, then ⟨α′⟩_{L} ⊴ ⟨β′⟩_{L}, implying that Definition 44.(1) is correct: Indeed, ⟨α⟩_{L} ⊴ ⟨β⟩_{L} iff ∃β′′ ≈ β : α ⊆ β′′, and by Proposition 21 and [E1], α ≈ α′ ⇒ α ⊳ (α′ \ α) ⇒ β′′ ⊳ (α′ \ α) ⇒ β′ ≈ β ≈ β′′ ≈ β′′ ∪ (α′ \ α) = β′′ ∪ α′, thus ⟨α′⟩_{L} ⊴ ⟨β′⟩_{L}.

Lemma 45 Let P be an initial reduction in an AZDFS F. Then, in the corresponding DEES C_{F}, F AM(ST (P)) = ST (F AM(P)).

Proof First note that, by [contribution] and the definition of ≤ (Definition 27), for any initial reduction Q, F AM(Q) is indeed a configuration.

(⊆) Let ϕ ∈ F AM(ST (P)). By Proposition 11, ϕ ∈ SF AM(P), i.e., there is P′v′ ∈ ϕ that is contracted in P and is P -needed, thus is P -essential. Let P^{∗}v^{∗} be a canonical element of ϕ. Then it is P -essential by Lemma 32. For any initial reduction Q with F AM(Q) ⊆ F AM(P), Q⊴P by Proposition 11, thus P^{∗}v^{∗} is Q-essential too. Hence Q does not discard P^{∗}v^{∗}, implying by Definition 27 that F AM(P) ⋫ϕ, i.e., ϕ ∈ ST (F AM(P)).

(⊇) Let ϕ ∈ ST (F AM(P)). Then ϕ ∈ F AM(P) and F AM(P) ⋫ϕ, which by Definition 27 means that there is no initial Q with F AM(Q) ⊆ F AM(P) such that Q discards a canonical element P^{∗}v^{∗} of ϕ. In particular, ST (P) does not discard P^{∗}v^{∗}, and by Lemmas 32 and 7.(1), the redex P′v′ ∈ ϕ contracted in P is P -needed, i.e., ϕ ∈ SF AM(P); thus ϕ ∈ F AM(ST (P)) by Proposition 11.

Lemma 46 Let Q, Q′ be initial reductions in an AZDFS F. Then Q ≈ Q′ in F iff F AM(Q) ≈ F AM(Q′) in the corresponding DEES C_{F} = (E_{F}, ≤, ⊳, ≈).

Proof

(⇒) By Definition 27, we need to show that ∀ϕ ∈ F AM(Q) ∪ F AM(Q′) \ F AM(Q)∩F AM(Q′), an initial reduction P with F AM(P) ⊆ F AM(Q)∩ F AM(Q′) discards a canonical element Nv of ϕ. Take P = ST (Q). By Proposition 11, F AM(P) ⊆ F AM(Q) ∩ F AM(Q′). Let Q^{∗}v^{∗} be an element of ϕ contracted in Q. Since by Proposition 11 ϕ ∉ F AM(P) = SF AM(Q), Q^{∗}v^{∗} is Q-unneeded, hence Q-inessential by Lemma 7.(1). Hence, by Lemma 30, P discards Q^{∗}v^{∗}. By the Affine Extraction Theorem, ∃N′ : N + N′ ≈ Q^{∗} and v^{∗} = v/N′. Since Q^{∗} ≤ Q ≈ P, N′/(P/N) = ∅, hence v/(P/N) = v^{∗}/(P/Q^{∗}) = ∅ by the Cube Lemma. Since ϕ ∉ F AM(P), P/N is external to v, thus P discards Nv.

(⇐) By Proposition 25, F AM(Q) ≈ F AM(Q′) implies that ST (F AM(Q)) = ST (F AM(Q′)); hence, by Lemma 45, F AM(ST (Q)) = F AM(ST (Q′)), implying by Proposition 11 that Q ≈ Q′.

Lemma 47 Let F be an AZDFS, let e_{0}, e_{1}, …, e_{n} be a left-closed enumeration of α ∈ L_{fin}(C_{F}), and let e_{i_{0}}, …, e_{i_{m}} be obtained from e_{0}, e_{1}, …, e_{n} by eliminating all vacuous events, i.e., e_{j} ∈ {e_{i_{0}}, …, e_{i_{m}}} iff {e_{0}, …, e_{j−1}} ⋫e_{j}.

Then e_{i_{0}}, …, e_{i_{m}} is a reduction in C_{F} and {e_{i_{0}}, …, e_{i_{m}}} ≈ {e_{0}, …, e_{n}}.

Proof If there were l, k such that e_{l} < e_{i_{k}} (hence l < i_{k}) and l ≠ i_{0}, …, i_{k−1}, then {e_{0}, …, e_{l−1}} ⊳ e_{l}, {e_{0}, …, e_{i_{k}−1}} ⋫e_{i_{k}}, and by [E1], {e_{0}, …, e_{i_{k}−1}} ⊳ e_{l}, contradicting [E3]. Hence e_{i_{0}}, …, e_{i_{m}} is left-closed. Since {e_{0}, …, e_{i_{k}−1}} ⋫e_{i_{k}}, {e_{i_{0}}, …, e_{i_{k−1}}} ⋫e_{i_{k}} by [E1], thus e_{i_{0}}, …, e_{i_{m}} is a reduction in C_{F}. Finally, {e_{i_{0}}, …, e_{i_{m}}} ≈ {e_{0}, …, e_{n}} follows from Proposition 21.

Proposition 48 Let P, Q be initial reductions in an ASDRS R. Then ⟨P ⟩_{L} ⊴ ⟨Q⟩_{L} iff ⟨F AM(P)⟩_{L} ⊴ ⟨F AM(Q)⟩_{L} in C_{R}.

Proof

(⇒) By Proposition 11, ⟨P ⟩_{L} ⊴ ⟨Q⟩_{L} iff ∃Q′ ≈ Q : F AM(P) ⊆ F AM(Q′), which by Definition 44 holds iff ⟨F AM(P)⟩_{L} ⊴ ⟨F AM(Q′)⟩_{L} in C_{R}. But Q ≈ Q′ implies F AM(P) ≈ F AM(Q′) in C_{R} by Lemma 46, and therefore

⟨F AM(P)⟩_{L} ⊴ ⟨F AM(Q)⟩_{L} in C_{R}.

(⇐) By Definition 44, ∃α : α ≈ F AM(Q)∧F AM(P) ⊆ α; thus by Lemma 47 ∃[β] : F AM(P) ⊆ β ⊆ α ∧ β ≈ α (assuming that say e_{0}, e_{1}, …, e_{n} is an enumeration of α whose initial part is an enumeration of F AM(P), we can take e_{i_{0}}, …, e_{i_{m}} as in Lemma 47 for [β]). By Lemma 42, there is a Q′ such that F AM(Q′) = β and P is an initial part of Q′. By Lemma 46, Q ≈ Q′, hence P ⊴ Q, therefore ⟨P ⟩_{L} ⊴ ⟨Q⟩_{L}.

Theorem 49 Let R be an ASDRS and let C = C_{R} be its corresponding DEES. Then f : ⟨P ⟩_{L} ↦ ⟨F AM(P)⟩_{L} is the isomorphism between L_{fin}^{⊴}(R) and L_{fin}^{⊴}(C), with the inverse f^{−1} : ⟨α⟩_{L} ↦ ⟨[ST (α)]⟩_{L}. Moreover, reductions in ⟨P ⟩_{L} and ⟨F AM(P)⟩_{L} are in one-to-one correspondence.

Proof By Lemmas 46 and 39 and Proposition 25, f and f^{−1} are well defined. The rest is immediate from Lemma 42 and Proposition 48.

A similar statement is valid when C is an arbitrary DEES and R = R_{C}: We only need to replace F AM(P) in the definition of f with EV N(P), where EV N(P) is the set of events fired in P.

6 Preservation of Neededness and Stability by the Translations

This section develops a normalization-by-neededness theory for DEESs, and relates it with that in affine SDRSs, establishing a relationship between the concepts of stability intrinsic to the above models, and between neededness and stability in each model.

In order to extend the theory of Relative Normalization [9–11] from SDRSs to DEESs, we can restrict ourselves to ASDRSs of the form R_{C}, where C is a DEES: by Theorem 49, such ASDRSs contain an isomorphic copy of any ASDRS.

Definition 50 ([9]) Let S be a set of terms in a DRS R.

(1) We call a redex u ⊆ t S-needed if t ∉ S and at least one residual of u is contracted in any reduction from t to a term in S; we and call u S-unneeded otherwise.

(2) We call S stable^{5} if:

(a) S is closed under reduction; and

(b) S is closed under unneeded expansion: for any e→^{u}o such that e ∉ S and o ∈ S, u is S-needed.

All interesting sets of ‘finite results’, such as of normal forms, head-normal forms, weak-head-normal forms, etc. are stable [10]. It has been shown in [11] (a corollary of the so called Relative Normalization theorem) that, for any stable set S of terms in an ASDRS R and any S-normalizable term t ∉ S, t contains at least one S-needed redex, and repeated contraction of S-needed redexes is S-normalizing, which justifies the concept of stable sets.

Our translation of AZDFSs into DEESs suggests the following definition of relative neededness and stability in DEESs.

Definition 51 Let S′ be a set of configurations in a DEES C = (E, ≤, ⊳, ≈).

(1) We call e ∈ E S′-needed, written NE_{S′}(e) if, for any α ∈ S′, e ∈ α, and call it S′-unneeded otherwise.

(2) We call S′ stable if:

(a) S′ is closed under inclusion.

(b) S′ is closed under unneeded expansion: α + e ∈ S′ ∧ α ∉ S′ ⇒ NE_{S′}(e); and

(c) S′ is closed under permutation equivalence.

Note that the relative neededness concept already makes sense for PESs.

The next theorem gives two equivalent definitions of stability in DEESs, more in the spirit of the definition of stability in PESs [37], and more convenient to generalize to the case of infinite configurations.

Theorem 52 Equivalent definitions of stability of sets of finite configurations in a DEES can be obtained from Definition 51 by replacing the condition (b) with either of the following two conditions (b′) or (b′′):

5 Our definition follows [9] rather than [10,11]; in the latter papers, the definition of stability of sets allows a slightly weaker condition than closure under reduction.

(b′) S′ is closed under intersection. (b′′) S′ is has a unique ⊆-minimal element α_{S′}.

Proof We show that (i) (b) ⇒ (b′); (ii) (b′) ⇒ (b′′) and (iii) (a), (b′′) ⇒ (b).

(i) Let α, β ∈ S′, and suppose on the contrary that α ∩ β ∉ S′. Further, let e_{1}, …, e_{m}, …, e_{n} be a left-closed enumeration of α such that e_{1}, …, e_{m} is a left-closed enumeration of α ∩ β (such an enumeration exists since α ∩ β is left-closed). Then there is m ≤ j < n such that {e_{1}, …, e_{j}} ∉ S′ and {e_{1}, …, e_{j+1}} ∈ S′. By (b), e_{j+1} is S′-needed, which is not possible since e_{j+1} ∉ β ∈ S′.

(ii) If S′ does not have a unique ⊆-minimal element, then it has at least two different ⊆-minimal elements α and β (i.e., ∄γ ⊂ α : γ ∈ S′, and similarly for β). By (b′), α ∩ β ∈ S′. But α ∩ β ⊂ α, contradicting the minimality of α.

(iii) Let α, e be such that α ∉ S′ ∧ α + e ∈ S′. By (a) and (b′′), this means that α_{S′} ⊈ α ∧ α_{S′} ⊆ α + e. Hence e ∈ α_{S′}, and therefore ∀δ ∈ S′ : e ∈ δ (since α_{S′} ⊆ δ by (b′′)).

The proof of the following proposition is routine, and therefore omitted.

Proposition 53 Let S′ be a set of configurations, in a DEES C, closed under permutation equivalence, and let S be the set of corresponding terms in the corresponding ASDRS R_{C} (which are Lévy-equivalence classes of configurations in C). Then S′ is stable in C iff S is stable in R_{C}. Further, if S′ is stable, an event e is S′-needed in C iff any e-redex is S-needed in R_{C}.

We conclude this section with a theorem expressing the relationship between concepts of stability and neededness in DEESs, analogous to the Relative Normalization Theorem for ASDRSs [11]:

Theorem 54 Let S′ be a stable set of configurations in a DEES C. Then a repeated execution of S′-needed events in any configuration α ∉ S′, possibly interleaved by finite sequences of S′-unneeded steps, eventually yields a configuration in S′.

Proof Immediate from closure of S′ under inclusion (since S′ consists of finite configurations, hence there are only a finite number of S′-needed events).

7 Relativized Information Domains

In this section, we introduce orderings on configurations relativized w.r.t. stable sets of results, in a DEES C, and show that they form finitary prime algebraic complete lattices. Unlike the previous sections, we will now allow for infinite configurations – (countably) infinite left-closed sets of events in C. The set of finite and infinite configurations in C will be denoted by L(C).

We start by some preliminary lattice theoretic definitions; we follow [37].

Definition 55 • A complete lattice is a partial order L = (L, ⊑) which has least upper bounds (joins or suprema) ⊔X and greatest lower bounds (meets or infima) ⊓X of arbitrary subsets X ⊆ L. We write x ⊔ y and x ⊓ y for the join and meet respectively of two elements x, y ∈ L.

• A directed subset of a partial order L is a subset Y ⊆ L with the property that for any finite set X ⊆ Y there is an element y ∈ Y such that ∀x ∈ X.x ⊑ y.

• A finite element of a complete lattice is an element z with the property that, for all directed subsets Y, if z ⊑ ⊔Y, then there is some y ∈ Y for which z ⊑ y.

• A complete lattice L is algebraic if for any element d ∈ L the set {x ⊑ d | x is finite} is directed and has least upper bound d.

• A complete prime of a complete lattice L is an element p ∈ L such that p ⊑ ∪X ⇒ ∃x ∈ X.p ⊑ x for any subset X ⊆ L. L is prime algebraic if, for all x ∈ L, x = ⊔{p ⊑ x | p is a complete prime}.

• An algebraic lattice is finitary iff every finite element dominates only a finite number of elements, i.e., {x | x ⊑ d} is finite for every finite element d.

• A complete lattice L is distributive if x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z), for all elements x, y, z ∈ L.

Theorem 56 ([37]) Let L be a finitary algebraic lattice. Then L is prime algebraic iff it is distributive.

We now extend some of the previously introduced concepts from finite to infinite configurations. The concepts of an α-reduction and a S′-needed event generalize immediately.

Definition 57 Let C = (E, ⊴, ⊳, ≈) be a DEES.

(1) Let α ∈ L(C). Then α ⊳ e iff ∃β ⊆_{fin} α : β ⊳ e.

(2) Let α, β ∈ L(C). Then α ≈ β iff α ⊳ β \ α ∧ β ⊳ α \ β.

(3) We call S′ ⊆ L(C) stable if it is closed under ⊆, has a unique ⊆-minimal element α_{S′}, and is closed under permutation equivalence.

It is easy to check that Definitions 57.(1)-(2) do not conflict with the definitions of the corresponding concepts for finite configurations. Further, it is an easy consequence of Definition 57.(1) and [E1] that:

Lemma 58 Let α ⊳ e and α ⊆ β ∈ L(C). Then β ⊳ e.

We call a reduction in a DEES S′-needed-fair, or simply S′-fair, if it fires at least all S′-needed events. S′-fair configurations are defined similarly.

Theorem 59 Let S′ be a stable set of configurations in a DEES C. Then its ⊆-minimal element α_{S′} consists of all S′-needed events of C. Consequently, S′ consists of all S′-fair configurations, and any S′-fair reduction generates a configuration in C.

Proof Since α_{S′} ∈ S′, all S′-needed events of C are in α_{S′}. If on the contrary α_{S′} contains an S′-unneeded event e, then ∃β ∈ S′ : e ∉ β, hence β ⊈ α_{S′}, contradicting the minimality of α_{S′}. The rest is immediate.

For example, firing all events at any state, or all S′-needed events, in parallel yields an S′-fair reduction since any finite configuration not yet in S′ can fire at least one S′-needed event.

Note that the set of all fair configurations – configurations α ∈ C such that ∀e ∈ C : e ∉ α ⇒ α ⊳ e – need not be stable for every DEES C. The reason is that, unlike the finite case, a configuration α need not be equivalent to its standard variant ST_{⊳}(α) = {e ∈ α | α ⋫e}. Indeed, consider the DEES corresponding to the ASDRS from [17] demonstrating the failure of the infinitary standardization theorem: there are infinitely many events e_{0}, e′_{1}, e_{1}, e′_{2}, e_{2}, …, the causal dependency is the transitive reflexive closure of dependencies e_{i} < e_{i+1}, e′_{i+1} (i = 0, 1, …), and the erasure relation is defined by α ⊳ e′_{j} iff e′_{k} ∈ α for some k > j, k = 2, 3, . . .. Then any fair configuration consists of all non-erasable events e_{i}, and at least one infinite sequence of erasable events e′_{i_{l}}, and it is immediate that the set of all fair configurations does not have the ⊆-minimal element. Note that for any fair configuration α in that DEES, ST (α) consists of all non-erasable events e_{i}, and α ≉ ST (α) since ST (α) ⋫e′_{k} for any k. Thus ST (α) = ST (β) does not imply α ≈ β as ST (ST (α)) = ST (α). However, the converse is always true:

Lemma 60 Let α, β ∈ L(C). Then α ≈ β implies ST (α) = ST (β).

Proof By Definition 57.(2), α⊳β\α∩β and β⊳α\α∩β. Hence ST (α), ST (β) ⊆ α ∩ β. Suppose on the contrary that ∃e ∈ ST (α) \ ST (β). Then α ⋫e and β ⊳ e, i.e., ∃β_{0} ⊆_{fin} β : β_{0} ⊳ e, implying by Lemma 58 that α ∩ β ⋫e and β′ = β_{0}∩(α∩β) ⋫e. Therefore, by Proposition 21, ∃e′ ∈ β_{0}\β′ : β′ ⋫e′. Thus α ⋫e′ by Lemma 58 (since β′ ⊆ α ∩ β ⊆ α) and e′ ∈ β \ α ∩ β, contradicting α ⊳ β \ α ∩ β.

Definition 61 Let α, β ∈ L(C), and let S′ be a stable set of configurations in C. We define α ⊴_{S′} β if [α]_{S′} ⊆ [β]_{S′}, where [α]_{S′} denotes the set of S′-needed events of α. We write α ≈_{S′} β iff α ⊴_{S′} β and β ⊴_{S′} α, i.e., [α]_{S′} = [β]_{S′}. We call ⊴_{S′} a stable embedding or S′-embedding, and call ≈_{S′} a stable equivalence or S′-equivalence. ⟨α⟩_{S′} will denote the ≈_{S′}-equivalence class of α. We write ⟨α⟩_{S′} ⊴_{S′} ⟨β⟩_{S′} if α ⊴_{S′} β. Finally, we define L^{≈_{S′}}(C) = L(C)/_{≈_{S′}} = {⟨α⟩_{S′} | α ∈ L(C)} and L^{⊴_{S′}}(C) = (L^{≈_{S′}}(C), ⊴_{S′}).

Note that ≈_{S′} does not satisfy [P0], although it does satisfy the other permutation axioms [P1] - [P3]. This means that for permutation equivalence ‘progress in any direction’ is equally important, while for a stable equivalence ≈_{S′} only ‘progress towards S′’ matters. Actually, ≈ is a special case of ≈_{S′}: the two coincide when C is a PES and S′ is the set of all events.

Definition 62 Let S′ be a stable set of configurations in a DEES C. The meet and join operations ⊔_{S′}, ⊓_{S′} on L^{⊴_{S′}}(C) are defined by:

• α ⊔_{S′} β = [α]_{S′} ∪ [β]_{S′} and ⟨α⟩_{S′} ⊔_{S′} ⟨β⟩_{S′} = ⟨α ⊔_{S′} β⟩_{S′};

• α ⊓_{S′} β = [α]_{S′} ∩ [β]_{S′} and ⟨α⟩_{S′} ⊓_{S′} ⟨β⟩_{S′} = ⟨α ⊓_{S′} β⟩_{S′};

It is immediate from the definition of ≈_{S′} that the above definition is correct.

Lemma 63 Let β ⊳ e, in a DEES C. Then β ≈ β \ ⌈e⌉^{≥}.

Proof If β is finite, then the lemma follows from Proposition 21. Otherwise, we have from Definition 57.(1)-(2) and [E3] that β ⊳e ⇒ ∃β_{0} ⊆_{fin} β : β_{0}⊳e ⇒ β_{0} ⊳ ⌈e⌉^{≥} ⇒ β ⊳ ⌈e⌉^{≥} ⇒ β ≈ β \ ⌈e⌉^{≥}.

Lemma 64 Let S′ be a stable set of configurations in a DEES C, and let e be S′-needed. Then e is non-erasable: ∀α ∈ L(C) : α ⋫e.

Proof Suppose on the contrary that ∃α ∈ L(C) : α ⊳ e. We can assume that α ∈ L_{fin}(C). By [E3] and [E2], α \ ⌈e⌉^{≥} ⊳ e. But since e is S′-needed, α\⌈e⌉^{≥} ∉ S′. Hence β = α_{S′} ∪(α\⌈e⌉^{≥}) ∈ S′ by closure of S′ under inclusion. But β ⊳e by Lemma 58, and β ≈ β \⌈e⌉^{≥} by Lemma 63. Thus, by closure of S′ under permutation equivalence, β \ ⌈e⌉^{≥} ∈ S′, and e ∉ β \ ⌈e⌉^{≥}, contradicting S′-neededness of e.

The following proposition shows that ≈⊆≈_{S′}, which agrees with our intuition that a concurrent semantics must not discriminate between permutation equivalent configurations/reductions.

Proposition 65 Let α, β be configurations in a DEES C, and let S′ be a stable set of configurations in C. Then α ≈ β implies α ≈_{S′} β.

Proof By Definition 57.(1), α ⊳ β \ α and β ⊳ α \ β. Hence, by Lemma 64, [α]_{S′}, [β]_{S′} ⊆ α ∩ β, and by Theorem 59, [α]_{S′} = α ∩ α_{S′} = (α ∩ β) ∩ α_{S′} = β ∩ α_{S′} = [β]_{S′}.

Theorem 66 Let S′ be a stable set of configurations in a DEES C. Then L^{⊴_{S′}}(C) = (L^{≈_{S′}}(C), ⊴_{S′}) is a finitary prime algebraic complete lattice.

Proof Immediate from Definition 62 and Theorem 59, since the set of subsets of any non-empty set (in our case, α_{S′}) ordered by the subset relation is a finitary prime algebraic complete lattice with intersection and union as meet and join operations [37].

In an ASDRS R, stability of a set S of initial (finite or infinite) reductions can be defined via stability of the corresponding set S′ of configurations in C_{R}. For any initial reductions P, Q, and any stable set of reductions S, in an ASDRS R, we can define P ⊴_{S} Q iff F AM_{S}(P)⊴_{S′} F AM_{S}(Q) in C_{R}, where F AM_{S}(P) denotes the set of S-needed families contracted in P (and hence coincides with the set of S′-needed events in the configuration corresponding to P). Further, we define P ≈_{S} Q iff P ⊴_{S}Q and Q⊴_{S}P. We call ⊴_{S} and ≈_{S} a stable embedding or S-embedding and a stable equivalence or S-equivalence, respectively. ⟨P ⟩_{S} denotes the ≈_{S}-equivalence class of P. We write ⟨P ⟩_{S} ⊴_{S} ⟨Q⟩_{S} if P ⊴_{S} Q. Now, if L(R) is the set of (finite or infinite) initial reductions in R, we can define L^{≈_{S}}(R) = L(R)/_{≈_{S}} = {⟨P ⟩_{S} | P ∈ L(R)} and L^{⊴_{S}}(R) = (L^{≈_{S}}(R), ⊴_{S}).

Lemma 67 Let α ∈ L(C). Then [α]_{S′} ∈ L(C). Moreover, [α]_{S′} is standard, and any of its left-closed enumerations is a reduction.

Proof Let e, e′ ∈ α, let e < e′ and let e′ be S′-needed. We need to show that e is S′-needed too. By Theorem 59, e′ ∈ α_{S′} ∈ L(C), implying that e ∈ α_{S′}. Thus [α]_{S′} ∈ L(C) ([α]_{S′} is left-closed). The rest is immediate from Lemma 64.

Theorem 68 Let R be an ASDRS and let C = C_{R} be its corresponding DEES. Further, let S′ be a set of configurations in C, and let S be the set of corresponding reductions in R. Then f : ⟨P ⟩_{S} → ⟨F AM(P)⟩_{S′} is an isomorphism between L^{⊴_{S}}(R) and L^{⊴_{S′}}(C), with the inverse f^{−1} : ⟨α⟩_{S′} → ⟨[[α]_{S′}]⟩_{S}.

Proof By Lemma 67, [[α]_{S′}] and hence f^{−1} are well defined. The rest is immediate from the definitions above.

Hence we can define on L^{⊴_{S}}(R) that ⟨P ⟩_{S} ⊔_{S} ⟨Q⟩_{S} = f^{−1}(f(⟨P ⟩_{S})⊔_{S′} f(⟨Q⟩_{S})) and ⟨P ⟩_{S} ⊓_{S} ⟨Q⟩_{S} = f^{−1}(f(⟨P ⟩_{S}) ⊓_{S′} f(⟨Q⟩_{S})), and we get from Theorem 66 that L^{⊴_{S}}(R) with ⊔_{S′} and ⊓_{S′} as join and meet is a finitary prime algebraic domain. It is not difficult to define stability of a set of reductions S, as well as the relations ⊴_{S}, ⊔_{S} and ⊓_{S}, on (corresponding equivalence classes of) reductions in R directly.

8 Conclusions

We have established an equivalence between deterministic stable operational (ASDRS) and domain-theoretic (DEES) models of computation, and based on this, constructed a fully adequate event style concurrent semantics for orthogonal rewrite systems. The correspondence between Event Structures and other models of concurrency, as well as with denotational semantics, are well studied [37,38], 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 [25], but they still use the syntax of the rewrite system essentially (axioms depend on the syntax).

Although we have restricted attention to orthogonal rewriting, it would be interesting to extend our axiomatization to partial orders with conflicts, to enable modelling of non-deterministic calculi as well.

Acknowledgments We thank R. Kennaway for useful comments.

References

[1] Asperti A., Guerrini S. The Optimal Implementation of Functional Programming Languages (Cambridge Tracts in Theoretical Computer Science, vol. 45, Cambridge University Press, 1998).

[2] A. Asperti and H.G. Mairson, Parallel beta reduction is not elementary recursive, in: Proc. 15th ACM Symposium on Principles of Programming Languages (1998) 303-315.

[3] H. P. Barendregt, The Lambda Calculus, its Syntax and Semantics (North-Holland, Amsterdam, 1984).

[4] G. Berry and J.-J. Lévy, Minimal and optimal computations of recursive programs, J. of the Association for Computing Machinery 26 (1979) 148-175.

[5] G. Boudol, Computational semantics of term rewriting systems. in: M. Nivat, J. C. Reynolds, eds., Algebraic methods in semantics (Cambridge University Press, 1985) 169-236.

[6] G. Boudol and I. Castellani, A non-interleaving semantics for CCS based on proved transitions, Fundamenta Informaticae 11(4) (1988) 433-452.

[7] D. Clark and J.R. Kennaway, Event structures and non-orthogonal term graph rewriting, Mathematical Structures in Computer Science 6 (1996) 545-578.

[8] A. Corradini, F. Gadduchi and U. Montanari, Relating two categorical models of term rewriting, in: Proc. RTA’95, Lecture Notes in Computer Science, vol. 914 (Springer, Berlin, 1995) 225-240.

[9] J.R.W. Glauert, J.R. Kennaway and Z. Khasidashvili, Stable results and relative normalization, Journal of Logic and Computation, 10(3) (2000). Special Issue on Type Theory and Term Rewriting, F. Kamareddine and J.W. Klop, eds. Oxford University Press.

[10] J.R.W. Glauert and Z. Khasidashvili, Relative normalization in orthogonal expression reduction systems, in: Proc. CTRS’94, Lecture Notes in Computer Science, vol. 968 (Springer, Berlin, 1994) 144-165.

[11] J.R.W. Glauert and Z. Khasidashvili, Relative normalization in deterministic residual structures. in: Proc. CAAP’96, Lecture Notes in Computer Science, vol. 1059 (Springer, Berlin, 1996) 180-195.

[12] G. Gonthier, J.-J. Lévy and P.-A. Melliès, An abstract standardisation theorem, in: Proc. 7th IEEE Symp. on Logic in Computer Science (1992) 72-81.

[13] R.J. Hindley, An abstract form of the Church-Rosser theorem I, Journal of Symbolic Logic 34(4) (1969) 545-560.

[14] G. Huet and J.-J. Lévy, Computations in Orthogonal Rewriting Systems, in: J.-L. Lassez and G. Plotkin, eds.,Computational Logic, Essays in Honor of Alan Robinson (MIT Press, 1991) 394-443.

[15] V. Kathail, Optimal interpreters for lambda-calculus based functional languages, Ph.D. Thesis, MIT, 1990.

[16] J.R. Kennaway, J.W. Klop, M.R. Sleep and F.-J. de Vries, Event structures and orthogonal term graph rewriting, in: M.R. Sleep, M.J. Plasmeijer, M.C.J.D. van Eekelen, eds., Term Graph Rewriting: Theory and Practice (John Wiley, 1993) 141-156.

[17] Z. Khasidashvili and J.R.W. Glauert, Discrete normalization and standardization in deterministic residual structures, in: Proc. ALP’96, Lecture Notes in Computer Science, vol. 1139 (Springer, Berlin, 1996) 135-149.

[18] Z. Khasidashvili and J.R.W. Glauert, Zig-zag, extraction and separable families in non-duplicating stable deterministic residual structures, Technical Report IR-420, Free University, 1997.

[19] Z. Khasidashvili and J.R.W. Glauert, Relating conflict-free stable transition and event models (extended abstract), in: Proc. MFCS’97, Lecture Notes in Computer Science, vol. 1295, (Springer, Berlin, 1997) 269-278.

[20] Z. Khasidashvili and J.R.W. Glauert, An abstract concept of optimal implementation, Technical Report SYS-C97-01, UEA Norwich, 1997.

[21] J. W. Klop, Combinatory reduction systems (Mathematical Centre Tracts n. 127, Amsterdam, 1980).

[22] J. W. Klop, Term rewriting systems in: S. Abramsky, D. Gabbay and T. Maibaum, eds., Handbook of Logic in Computer Science, vol. 2I (Oxford University Press, 1992) 1-116.

[23] J. Lamping, An algorithm for optimal lambda calculus reduction, in: Proc. 7th ACM Symp. on Principles of Programming Languages (1990) 6-30.

[24] C. Laneve, Distributive evaluations of λ-calculus, Fundamenta Informaticae 20(4) (1994) 333-352.

[25] C. Laneve and U. Montanari, Axiomatizing permutation equivalence, Mathematical Structures in Computer Science 6 (1994) 219 - 249.

[26] J.-J. Lévy, Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université de Paris VII, 1978.

[27] J.-J. Lévy, Optimal reductions in the Lambda-calculus, in: J. P. Seldin, J. R. Hindley, eds., To H. B. Curry: Essays on Combinatory Logic, Lambdacalculus and Formalism (Academic Press, 1980) 159-192.

[28] L. Maranget, Optimal derivations in weak λ-calculi and in orthogonal term rewriting systems, in: Proc. 18th ACM Symp. on Principles of Programming Languages (1991) 255-269.

[29] P.-A. Melliès, Description Abstraite des Systèmes de Réécriture, Thèse de l’Université Paris 7, 1996.

[30] P.-A. Melliès, A factorization theorem in rewriting theory, in; Proc. CTCS’97, Lecture Notes in Computer Science, vol. 1290 (Springer, Berlin, 1997) 49-68.

[31] R. Milner, Communication and Concurrency (Prentice Hall, 1989).

[32] M. Nielsen, G. Plotkin and G. Winskel, Petri nets, event structures and domains, Part 1, Theoret. Comput. Sci. 13 (1981) 85-108.

[33] D. Sangiorgi, Expressing mobility in process algebras: first-order and higherorder paradigms, Ph.D. Thesis, Edinburgh University, 1993.

[34] G. Schied, On relating rewrite systems and graph grammars to event structures, in: Proc. GTCS’94, Lecture Notes in Computer Science, vol. 776, (Springer, Berlin, 1994) 326-340.

[35] E.W. Stark, Concurrent transition systems, Theoret. Comput. Sci. 64(3) (1989) 221-269.

[36] Winskel G. Events in Computation, Ph.D. Thesis, Edinburgh University, 1980.

[37] Winskel G. An introduction to event structures, In Proc. ‘Linear time, branching time and partial order in logics and models of concurrency’, Lecture Notes in Computer Science, vol. 354, (Springer, Berlin, 1989) 364-397. Extended version appears as Cambridge University Computer Laboratory Report n. 95, 1986.

[38] G. Winskel and M. Nielsen, Models for concurrency, in: S. Abramsky, D. Gabbay, and T. Maibaum, eds., Handbook of Logic in Computer Science, vol. 4 (Oxford University Press, 1995) 1-148.