Relating Conflict-free Stable Transition and Event Models

Zurab Khasidashvili NTT Basic Research Laboratories

Atsugi-shi, Kanagawa-ken, 243-01, Japan zurab@theory.brl.ntt.jp

John Glauert

School of Information Systems, UEA

Norwich NR4 7TJ England jrwg@sys.uea.ac.uk ^{∗}

Abstract

We describe an Event Structure semantics for conflictfree (term and graph, first and higher order) rewrite systems, including the λ-calculus, and other stable transition systems. Our interpretation is based on interpreting redex-families as events. It treats permutation-equivalent reductions as representing the same concurrent computation, which was thought impossible as Lévy’s ordering on the reduction space is not in general a lattice (but only an upper semilattice). Further, in order to achieve a fully faithful event semantics based on the permutation-equivalence (which Winskel’s Event Structures cannot do), we extend the Prime Event Structure model by axiomatizing the permutation-equivalence on concurrent computations (configurations) in two equivalent ways (for the conflict-free case), and show that thus extended models are isomorphic to known stable transition models with axiomatized residual and family relations.

1 Introduction

The prime goal of this paper is to provide a fully adequate concurrent semantics for orthogonal rewrite systems. As an abstract model of concurrency, we chose Event Structures, the most successful and commonly accepted one [NPW81, Win89]. An Event Structure is simply a set of events ordered by causal dependency relation. The idea is to view a process as performing events (some atomic tasks), and an event can only occur if all events on which it depends already have. Causally independent events are concurrent events and can be evaluated in parallel. Stages of a computation are then represented by configurations – leftclosed event sets w.r.t. the causal order, and the same configuration represents all sequential computations executing events in that configuration, no matter in which order the concurrent events were executed.

In the theory of orthogonal rewrite systems (such as the λ-calculus) there is the well established concept of ‘redex-family’, due to Lévy [Lév80], which formalizes the idea of the ‘same work’. Therefore we want to base our interpretation on interpreting redex-families as events, hence to interpret family-reductions (contracting entire families as multisteps) as configurations of the corresponding Event Structure. This is also justified by the fact that reductions in optimal graphimplementations of orthogonal systems precisely correspond to family-reductions in the original system.

Recent advances in abstract study of orthogonal rewrite systems [Sta89, GLM92, GK96, KG96, KG96a] allows us to address the problem in an abstract setting. Stable Deterministic Residual Structures (SDRSs) and Deterministic Family Structures (DFSs) model computation in orthogonal rewrite systems. DRSs are Abstract Rewrite Systems with an axiomatized residual relation; DFSs are DRSs there in addition the concept of redex-family is axiomatized. Stable DRSs allow to prove analogs of the Normalization and Standardization Theorems [CF58] [GK96]. In DFSs one can further prove Lévy’s Optimality Theorem and the Unique Families Lemma. The latter states that any family can be contracted at most once in a familyreduction. It corresponds to the fact that any event may occur at most once in the course of a computation, and is needed for event structure interpretation of DRSs based on interpreting families as events.

Since we want to restrict our attention to familyreductions only, we define linearization of any DFS, which is a non-duplicating, also called affine SDRS, ASDRS. We have already shown [KG96a] that the latter forms a DFS with the zig-zag [Lév80] as the family relation. And family-reductions in a DFS precisely correspond to reductions in its linearization. This allows us to concentrate on construction of event semantics for affine SDRSs only.

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

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

In order for this to be possible, permutationequivalence classes of (finite) reductions must be partially ordered in a way to form distributive lattices, as the domains of (finite) configurations of an Event Structure order by inclusion are such lattices [Win89]. However, it is a well known problem that Lévy’s ordering on the reduction space is not in general a lattice (Recursive Program Schemes are exception), but only an upper semi-lattice, as the greatest lower bound of two co-initial reductions need not exist [Lév80]. This problem, caused by erasure of redexes, is well discussed in [Lan93], where it is argued that event semantics say for the λ-calculus cannot therefore be based on permutation-equivalence˙

Several authors have proposed different ways to get round of this problem. Laneve [Lan93] introduces the distributive equivalence on β-reductions which only allow permutation of steps cannot erase or duplicate on another, and consequently all equivalent sequences have the same length. Schied [Sch94] and Corradini et al [CELMR94], propose a similar solution, working with non-duplicating systems (graphs). Kennaway et al [KKSV93] do work with permutation equivalence, for orthogonal Term Graph Rewriting, but they only restrict themselves to needed events of a normalizable term do cope with problems with erasure (needed redexes cannot be erased, and all needed normalizing reductions are of the same length in affine systems). Similarly, Clark and Kennaway [CK95] work with permutation-equivalence and allow infinite reductions but restrict themselves to standard reductions only (which are unique in their permutationequivalence class).

To deal with that (lattice) problem, we introduce a different ordering on permutation classes of finite reductions in ASDRSs which makes the latter a distributive lattice (and again generates permutationequivalence.) The ideal completion of the obtained distributive lattice forms a prime algebraic domain, and an Event Structure can be associated with the ASDRS whose domain of configurations is isomorphic to the one we have constructed on reductions [Win89]. But this interpretation is still inadequate as configurations in the constructed ES cannot represent all reductions in a permutation-equivalence class (simply because the latter may contain infinitely many elements while the former has only a finite number of runs).

In order to cope with the adequacy problem we extend the PES model by axiomatizing permutationequivalence on event configurations in them in two equivalent ways. One by directly constraining the class of all equivalence relations on configurations, and another by axiomatizing the inessentiality relation expressing redundancy of an event for a configuration. We can thus identify configurations with different number of events but still representing the same permutation-equivalence class of reductions. Our ordering on reductions precisely match the inclusion order on canonical representatives of equivalence classes of configurations (which are the smallest elements in every configuration). We then show that the extended PES models are actually isomorphic to AS-DRSs, therefore give a fully adequate semantics to them.

We think that our axiomatization of permutation equivalence and the erasure relation is interesting on its own right for better understanding of permutation equivalence and its relationship with sequentiality and stability concepts, and is interesting from the lattice theory point of view. Definitions of permutation equivalence without using a residual calculus have been studied before [LM94], but they still use the syntax of the rewrite system essentially (axioms do depend on the syntax).

2 Deterministic Residual and Family Structures

In this section we recall Deterministic Residual Structures (DRSs) and Deterministic Family Structures (DFSs), introduced in [GK96]. DRSs and DFSs are Abstract Reduction Systems (ARSs) with axiomatized notions of residual. In DFSs, in addition, Lévy’s concept of redex-family is axiomatized. We also recall some of the basic theory developed for DRSs and DFSs in [GK96, KG96, KG96a].

Definition 2.1 ([Hin64]) 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. ^{1} 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. P + Q denotes the concatenation of P and Q. u also denotes the reduction that contracts u.

DRSs are similar to Stark’s Determinate Concurrent Transition Systems (DCTSs) [Sta89] and Abstract Reduction Systems of Gonthier et al. [GLM92]. Unlike DCTSs, the residual relation in DRSs may be duplicating, and unlike ARSs of [GLM92], we do not have a nesting relation on redexes. Several refined concepts of abstract rewriting are studied in [Oos94, Mel96, Raa96]. DRS are intended to model all orthogonal term and graph rewrite systems, both first and higher-order, and other conflict-free transition systems with a reasonable level of abstraction, while say ARSs of [GLM92] do not cover e.g., orthogonal term graph rewriting systems [SPE93].

Definition 2.2 (Deterministic Residual Structure) 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 of residuals of a redex under any reduction is defined by transitivity.

A development of a set U of redexes in a term t is a reduction P : t → → that only contracts residuals of redexes from U; the development P is complete if U/P, the set of residuals under P of redexes from U, is empty ∅. 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, called Finite Developments (FD) [GLM92] and acyclicity (axiom (4) in [Sta89]): • [FD] All developments are terminating; all coinitial complete developments of the same set of redexes end at the same term; and residuals of a redex under all complete co-initial developments of a set of redexes are the same.

• [acyclicity] Let u, v ∈ t, let u ≠ v, and let u/v = ∅. Then v/u ≠ ∅.

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 by u/v .

In a DRS R, the residual relation on redexes is extended to all co-initial reductions exactly as in syntactic orthogonal rewrite systems [HL91, Lév78, Lév80, Sta89]: (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 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 [Klo80, Bar84].

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

Definition 2.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}. We call P external to Q if for any i, j, u_{i}/(Q_{j}/P_{i})∩v_{j}/(P_{i}/Q_{j}) = ∅ (see the diagram, where U_{i,j} = u_{i}/(Q_{j}/P_{i}) and V_{i,j} = v_{j}/(P_{i}/Q_{j})).

1Klop’s ARSs [Klo92] are pairs (T er, →), and do not allow one to distinguish transitions with the same source and target terms.

[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 2.4 (Stability Lemma) 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 2.5 (Acyclicity Lemma) Let P, N be coinitial finite reductions in a DRS, and let P be external to N. Then N ≉ P.

Definition 2.6 (Deterministic Family Structure) 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 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] if e → →^{P} t→^{u}s and u creates v ∈ s, then F am(P u) ↪ F am((P + u)v).

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

We call a DFS F a zig-zag DFS, ZDFS, if its family relation is the zig-zag ≃_{z} (the corresponding contribution relation ↪_{z} is determined by [contribution]).

It is shown in [GK96] 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 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 ∅, by analogy with the initial state in an Event Structures. Further, in DFSs, families will always be considered relative to ∅, i.e., all histories start with ∅. Unless otherwise stated, under a reduction we mean a finite reduction. Reductions starting from ∅ will also be called initial reductions or histories.

2.1 Standardization

In this subsection, we recall some definitions and results from [KG96] concerning standardization of reductions in non-duplicating, i.e., affine, SDRSs, AS-DRSs.

Definition 2.7 • Let P : t → → o and u ∈ t, in a DRS. We call u erased in P or P -erased, written ER_{P} (u, t), if u/P = ∅. We say that P discards u if P is external to u and erases it.

• We call u P -needed, NE_{P} (u, t), if there is no Q ≈ P that is external to u, and call it P - unneeded, UN_{P} (u, t), otherwise. We call u P - essential, ES_{P} (u, t), if there is no Q ≈ P that discards u, and P -inessential, IE_{P} (u, t), otherwise.

We extend these concepts to reductions co-initial with those containing u as a redex of one of its terms.

• Let Q : t → → o, P : t → →^{P′} s → → e, and u ∈ s.

We say NE_{Q}(u, s), or more precisely NE_{Q}(P′u, s), if NE_{Q/P′}(u, s). We call P Q-needed if so is every redex contracted in P. 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. The latter property will be referred to as CR for residuals.

Lemma 2.8 Let P : s → → t→^{u}e → → o in an ASDRS. (1) NE_{P} (w, t) iff ER_{P} (w, t) and ES_{P} (w, t).

(2) If P : t → → s′→^{w}o, then NE_{P} (w, s′).

(3) If u creates v ∈ e and UN_{P} (u.t) (resp. IE_{P} (u, t), then so is v.

(4) If u ≠ v ∈ t, then NE_{P} (v, t) (resp. ES_{P} (v, t)) iff v has a P -needed (P -essential) residual in e.

Definition 2.9 Let P : t → → and Q ⊴ P. The P - needed variant of Q, written SE_{P} (Q), is defined as follows: let v ∈ t be such that it is P -needed and its residual is contracted in Q first among P -needed residuals of P -needed redexes in t. Then SE_{P} (Q) = v + SE_{P/v}(Q/v). If there is no such a redex in t, then SE_{P} (Q) = ∅.

Self-needed reductions play the role of standard reductions in SDRSs, and the above algorithm is a standardization procedure for reductions in SDRSs.

Definition 2.10 We call a reduction P in a DRS standard, written P ∈ ST A, if it is self-needed, or equivalently, self-essential. We write Q ∈ ST AP if Q ∈ ST A and Q ≈ P, and call Q a standard variant of P.

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

2.2 Families in Affine SDRSs

In this section we recall construction of DFSs from non-duplicating SDRSs from [KG96a].

Below, F AM(P) (resp. SF AM(P)) denotes the set of zig-zag classes whose member (resp. P -needed, or equivalently, P -essential) redexes are

contracted in P, in an ASDRS.

Proposition 2.12 Let P and Q be co-initial finite reductions in an affine zig-zag DFS. Then 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)).

Theorem 2.13 (Affine Extraction) Every redex P v in an ASDRS has a zig-zag related redex P′v′ in canonical form, meaning that P′ is standard 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^{∗}.

Theorem 2.14 (Affine Zig-zag Families) Let R be a non-duplicating SDRS. Then F_{R} = (R, ≃_{z}, ↪_{z}) is a zig-zag DFS, called the corresponding ZDFS of R.

3 Deterministic Permutation and Erasure Event Structures

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

A Prime Event Structure (PES) [Win80] 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. In this paper 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, denoted by F inE, and will be often omitted. Finite configurations of E are finite left-closed subsets α, β, … of E, i.e., subsets L(E) = {α ⊆ F inE | e ∈ E ∧ e′ < e ⇒ e′ ∈ α}. 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 3.1 A Deterministic Permutation Event Structure (DPES) is a triple P = (E, ≤, ≈), where E = (E, ≤) is a conflict-free Prime Event Structure and ≈⊆ L(E) × L(E) is an equivalence relation, permutationequivalence, satisfying the following axioms:

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

• [P1] α ≈ β ∧ α ∩ β ⊆ γ ⊆ α ∪ β ∧ γ ∈ L(E) ⇒ α ≈ γ;

• [P2] α ≈ β ∧α+e, β +e ∈ L(E) ⇒ α+e ≈ β +e;

• [P3] α ≈ α − e ∧ e < e′ ∧ α + e′ ∈ L(E) ⇒ α ≈ α + e′;

DEESs extend Deterministic Computation Structures (DCS) [GK96] by further erasure axioms to enable a fully adequate treatment of erasure.

Definition 3.2 A Deterministic Erasure Event Structure (DEES) is a triple C = (E, ≤, ⊳), where E = (E, ≤) is a conflict-free Prime Event Structure and ⊳ ⊆ L(C) × E is erasure relation, satisfying the following axioms:

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

• [E1] α ⊳ e ∧ α ⊆ β ∈ L(E) ⇒ β ⊳ e;

• [E2] α ⊳ e′ ∧ α ⊳ e ∧ α − e′ ∈ L(E) ⇒ α − e′ ⊳ e;

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

• [E4] α ∈ L(E) ∧ α ∪ ⌈e^{<}⌉ ⊳ e ⇒ α ⊳ e. We read α ⊳ e as: ‘e is α-inessential’.

We may write α ⊳ X if ∀e ∈ X : α ⊳ e. Sometimes we write L(P) for L(E) if E is the domain of a DPES P, and similarly for L(C). Next we define translations between DPESs and DEESs.

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

• α ⊳_{≈} e iff α ∪ ⌈e^{≤}⌉ ≈ (α ∪ ⌈e^{≤}⌉) \ ⌈e^{≥}⌉. In particular, when e ∈ α and α − e ∈ L(E),

• α ⊳_{≈} e iff α ≈ α − e.

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

• α ≈_{⊳} β iff ST_{⊳} (α) = ST_{⊳} (β), where ST_{⊳} (α) = {e ∈ α | α ⋫e} is the set of α-essential events of α. (The subscript ⊳ in ST_{⊳} (α) will often be omitted.)

ST (α) is called the standard variant of α.

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

Lemma 3.5 Let α ∈ L(C), in a DEES. Then ST (α) ∈ L(C) and ST (ST (α)) = ST (α). Proof Let e ∈ ST (α) ∧ e′ < e. Then e ∈ α and α ⋫e, implying by [E3] that α ⋫e′. Since α ∈ L(C) and e′ < e, e′ ∈ α, implying e′ ∈ ST (α). Hence ST (α) ∈ L(C). If, on the contrary, ST (ST (α)) ≠ ST (α), i.e., ∃e′′ ∈ ST (α) : ST (α) ⊳ e′′, then α ⊳ e′′ by [E1], contradicting e′′ ∈ ST (α).

Lemma 3.6 ∀e ∈ α ∈ L(C), α ⊳ 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} = α, α_{i+1} = α_{i} + e_{i+1}, and hence α = α_{n}. By the definition of ST (α), we have α_{n} ⊳ e_{i} for all i = 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].

Corollary 3.7 ∀α, β ∈ L(C), ST (α) = ST (β) ⇔ α ∩ β ⊳ α ∪ β \ α ∩ β. Proof (⇒) ST (α) = ST (β) ⇒ ST (α) ⊆ α ∩ β, and by the definition of ST (α), Lemma 3.6, and [E1], ST (α) = ST (β) ⇒ ST (α) ⊳ β \ α ∪ α \ β ⇒ α ∩ β ⊳ α ∪ β \ α ∩ β. (⇐) By [E1] and Lemma 3.8, α ∩ β ⊳ α ∪ β \ α ∩ β ⇒ α ⊳ α \ β ∧ β ⊳ β \ α ⇒ ST (α) = ST (α ∩ β) = ST (β).

Lemma 3.8 Let α, β ∈ L(E) and α ⊆ β, in a DEES C. Then ST (α) = ST (β) iff β ⊳ β \ α. Proof (⇒) By Definition 3.4. (⇐) Since β ⊳ β \ α, ST (β) ⊆ α. Let e′ ∈ ST (β). Then e′ ∈ β and β ⋫e′, implying by [E1] 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 3.6 that β ⋫e′′, i.e., e′′ ∈ ST (β). Hence ST (α) = ST (β).

Theorem 3.9 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 3.3 and [P0].

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

[E1]: Let α ⊳_{≈} e ∧ α ⊆ β ∈ L(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 3.3. 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 3.3. Finally, if e < e′, then α + e′ ∈ L(E) ⇒ e ∈ α, and α + e′ ∪ ⌈e^{≤}⌉ = α ∪ ⌈e^{≤}⌉ + e′ and α + e′ ∪ ⌈e^{≤}⌉ \ ⌈e^{≥}⌉ = α ∪ ⌈e^{≤}⌉⌈e^{≥}⌉. By [E3] which we have already proved above for ⊳_{≈}, α ⊳_{≈} e ⇒ α ⊳_{≈} e′, implying by Definition 3.3 that α = α ∪ ⌈e^{≤}⌉ ≈ α ∪ ⌈e^{≤}⌉ \ ⌈e^{≥}⌉ + e′ = α + e′. Hence α + e′ ∪ ⌈e^{≤}⌉ \ ⌈e^{≥}⌉ ≈ α + e′ ∪ ⌈e^{≤}⌉, i.e., α + e′ ⊳ e by Definition 3.3.

[E2]: We can assume that e′ ∈ α. Let α ⊳_{≈} e′, α ⊳_{≈} e and α − e′ ∈ L(E). By Definition 3.3, α ⊳_{≈} e ⇒ α ∪ ⌈e^{≤}⌉ ≈ α ∪ ⌈e^{≤}⌉ \ ⌈e^{≥}⌉ and α ⊳_{≈} e′ ⇒ α ≈ α − e′, implying by repeated application of [P2] that α ∪ ⌈e^{≤}⌉ ≈ α − e′ ∪ ⌈e^{≤}⌉. In each of the three cases of relative ordering of e and e′, one easily checks that (α∪⌈e^{≤}⌉\⌈e^{≥}⌉)∩(α−e′ ∪⌈e^{≤}⌉) = α−e′ ∪⌈e^{≤}⌉\⌈e^{≥}⌉ implying by [P1] that α−e′∪⌈e^{≤}⌉ ≈ α−e′∪⌈e^{≤}⌉\⌈e^{≥}⌉. Hence, α − e′ ⊳_{≈} e by Definition 3.3.

[E4]: Immediate from Definition 3.3.

Theorem 3.10 For any DEES C = (E, ≤, ⊳), P_{C} = (E, ≤, ≈_{⊳} ) is a DPES. Proof We need to show that ≈_{⊳} satisfies the permutation axioms [P0] – [P3].

[P0]: ⌈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 ST (⌈e^{≤}⌉) ≉_{⊳} ST (⌈e^{<}⌉) by Definition 3.4.

[P1]: Let α ≈_{⊳} β, α ∩ β ⊆ γ ⊆ α ∪ β, and γ ∈ L(E). By Definition 3.4, ST (α) = ST (β), hence ST (α) ⊆ α ∩ β ⊆ γ. Further, ∀e ∈ α ∩ β \ ST (α), α ⊳ e or β ⊳ e, hence ST (α) ⊳ e by Lemma 3.6. Hence ST (ST (β)) = ST (γ) by Lemma 3.8, and ST (β) = ST (γ) by Lemma 3.5.

[P2]: Let α ≈_{⊳} β and α + e, β + e ∈ L(E). By Definition 3.4, ST (α) = ST (β). Assume first that ST (α) ⊳ e. Then α + e ⊳ e by [E1] and ST (α + e) = ST (α) by Lemma 3.8. Similarly, ST (β + e) = ST (β). Hence, ST (α + e) = ST (β + e), implying by Definition 3.4 that α + e ≈_{⊳} β + e. Now let ST (α) ⊳e. Then, by [E3], ∀e′ ∈ α \ ST (α) : e′ ≮ e. Thus α + e ∈ L(E) ⇒ ST (α) + e ∈ L(E). Since ∀e′ ∈ α + e \ (ST (α) + e) : α + e ⊳ e′, we have by Lemma 3.8 that ST (α + e) = ST (ST (α) + e), thus α + e ≈_{⊳} ST (α) + e by Definition 3.4. Similarly, β + e ≈_{⊳} ST (β) + e, implying α + e ≈_{⊳} β + e (since ST (α) = ST (β)).

[P3]: Let α ≈_{⊳} α − e, e < e′ and α + e′ ∈ L(E). By Definition 3.4, ST (α) = ST (α − e), implying α ⊳ e. Hence, by [E3], α ⊳ e′, implying by [E1] that α + e′ ⊳ e′. Hence, by Lemma 3.8, ST (α + e) = ST (α), thus α + e ≈_{⊳} α by Definition 3.4.

Lemma 3.11 Let P = (E, ≤, ≈) be a DPES, and let α ∈ L(E). Then α ≈ ST_{⊳_{≈}} (α). Proof Let α \ ST_{⊳_{≈}} (α) = {e_{1}, …, e_{n}}, By Definition 3.3, α ⊳_{≈} e_{i} ⇒ α ≈ α \ ⌈e_{i}^{≥}⌉. Clearly, ∩_{i=1}^{n}α \ ⌈e_{i}^{≥}⌉ ⊆ ST_{⊳_{≈}} (α) ⊆ α, implying by [P1] and α ≈ α \ ⌈e_{i}^{≥}⌉ that α ≈ ∩_{i=1}^{n}α \ ⌈e_{i}^{≥}⌉ ≈ ST_{⊳_{≈}} (α).

Corollary 3.12 In a DPES P = (E, ≤, ≈), α ≈ β iff ST_{⊳_{≈}} (α) = ST_{⊳_{≈}} (β). Proof By Lemma 3.11, α ≈ β iff ST_{⊳_{≈}} (α) ≈ ST_{⊳_{≈}} (β), and (⇐) is immediate. (⇒) Suppose on the contrary that ST_{⊳_{≈}} (α) ≠ ST_{⊳_{≈}} (α). Then ∃e ∈ ST_{⊳_{≈}} (α)∪ST_{⊳_{≈}} (α)\ST_{⊳_{≈}} (α)∩ST_{⊳_{≈}} (α). Let 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 3.3 that α ⊳_{≈} e, contradicting e ∈ ST_{⊳_{≈}} (α).

Theorem 3.13 (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. Let C_{P_{C}} = (E, ≤, ⊳′) and P_{C_{P}} = (E, ≤, ≈′), and let us show that ⊳ = ⊳′ and ≈=≈′′.

(1) By [E4], [E1] and [E3], α ⊳ e iff α ∪ ⌈e^{≤}⌉ ⊳ e iff α ∪ ⌈e^{≤}⌉ ⊳ ⌈e^{≥}⌉. By Lemma 3.8, the latter holds iff ST (α ∪ ⌈e^{≤}⌉) = ST (α ∪ ⌈e^{≤}⌉ \ ⌈e^{≥}⌉), which, by Definition 3.4 means that α∪⌈e^{≤}⌉ ≈_{⊳} α∪⌈e^{≤}⌉\⌈e^{≥}⌉, meaning α ⊳′ e by Definition 3.3.

(2) By Corollary 3.12 and Definition 3.4, α ≈ β iff ST_{⊳_{≈}} (α) = ST_{⊳_{≈}} (β) iff α ≈′ β.

4 Relating Transition and Event models

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

4.1 Translation of affine SDRSs and DFSs into DPESs and DEESs

Definition 4.1 To a DFS F = (R, ≃, ↪), we associate the DPES P_{F} = (E_{F}, ≤, ≈), and the DEES C_{F} = (E_{F}, ≤, ⊳), where

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

• ϕ < ψ iff ϕ ↪ ψ;

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

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

Lemma 4.2 Let Q : t → → s, v ∈ t, IE_{Q}(v, t), and let Q′ ∈ ST AQ, in an ASDRS. Then Q′ discards v. Proof Since IE_{Q}(v, t), v/Q = ∅ and UN_{Q}(v, t). Since Q′ is Q-needed, it is external to v by Lemma 2.8, and v/Q′ = v/Q = ∅, i.e., Q′ discards v.

Lemma 4.3 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}.

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

By Lemma 2.8.(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 2.8.(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). Then by Lemma 2.8, 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}]

Corollary 4.4 Let Q : t → → s, P : t → → o, v ∈ o, IE_{Q}(P v, o), and let Q′ ∈ ST AQ, in an ASDRS. Then Q′ discards P v. Proof By Lemma 4.3, Q′/P ∈ ST AQ/P. And since v is Q/P -inessential, Q′/P discards v by Lemma 4.2.

Lemma 4.5 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 affine SDRS. Then (Q′ + u)v is P -inessential too. Proof Let P′ = ST (P), P′′ = P′/Q′, and P^{∗} = P′′/u. By Corollary 4.4, P′′ discards u. So let w be the step of P′′ that discards the residual u′ of u, and let v′ be the the corresponding residual of v along P^{∗}, see the figure. If v′ ≠ ∅, 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. IE_{P} (v, e).

[figure: P′]

[figure: Q′; w; P′′]

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

[figure: v; v′; ∅; ∅]

Lemma 4.6 Let P : t → → s, ϕ be a family in an AZDFS F, Qv, Q′v′ ∈ ϕ, let Qv be canonical, and let Qv be P -inessential. Then so is Q′v′. Proof By the Affine Extraction Theorem, there is Q′′ such that Q′ ≈ Q + Q′′ and v′ = v/Q′′. Since Qv is P -inessential, ST (P)/Q discards v by Corollary 4.4, and ST (P)/Q′ discards v′ by CR for residuals.

Lemma 4.7 Let t → →^{Q} s→^{u}s′, t → →^{P} o→^{v}o′, and let Qu ≃_{z} P v. Then v/((Q + u)/P) = ∅. Proof 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 CR for residuals, v′ = w/(N′ + P/Q). But u is the only N′-residual of w, thus v′ = u/(P/Q), implying v/((Q+u)/P) = ∅.

Lemma 4.8 Let P ∈ ST A, F AM(P) = F_{1} ∪ F_{2}, F_{1} ∩ F_{2} = ∅ and ∀ϕ ∈ F − 2, ψ ∈ F_{1} : ϕ ↛ ψ. Then ∃Q ∈ ST AP : Q = Q_{1} + Q + 2, F AM(Q_{i}) = F_{i}. 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 again a standard reduction by Lemma 2.8.(4). The resulting reduction can be transformed similarly until all steps in F_{2} are pushed to the end. Termination of the transformation follows from the fact that it does not change the length of reductions.

Theorem 4.9 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].

[E0] and [E1] follow immediately from Definitions 2.7 and 4.1.

[E2]: Let α⊳ϕ, α⊳ϕ′, and let α−ϕ ∈ L(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 4.6, 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 α − ϕ′ ⊳ ϕ.

[E3]: Immediate from Definitions 2.7 and 4.1 and Lemma 4.5.

[E4]: Let α ∪ ⌈ϕ^{<}⌉ ⊳ ϕ. By Definition 4.1, there is a Q such that F AM(Q) ⊆ α ∪ ⌈ϕ^{<}⌉ and Q discards a canonical element P v of ϕ. By Proposition 2.12 and Corollary 4.4, Q can be chosen standard. Let F_{2} = F AM(Q) ∩ (⌈ϕ^{<}⌉ \ α) and F_{1} = F AM(Q) \ F_{2}. Since α ∈ L(E), ∀ϕ ∈ F − 2, ψ ∈ F_{1} : ϕ ↛ ψ. Hence, by Lemma 4.8, ∃Q ∈ ST AP : Q′ = Q_{1} + Q + 2, F AM(Q_{i}) = F_{i}. By Corollary 4.4, Q′ discards P v, and by Lemma 4.7, Q′/P = Q_{1}/P, since ⌈ϕ^{<}⌉ ⊆ F AM(P). Hence Q_{1} too discards P v, and F AM(Q_{1}) ⊆ α, implying α ⊳ ϕ.

Theorem 4.10 For any DFS F, P_{F} = P_{C_{F}}. Proof Let F = (R, ≈, ↪). By Definition 4.1 and Definition 3.4, P_{F} = (F AM(F), \underline{↪}, ≈), C_{F} = (F AM(F), \underline{↪}, ⊳) and P_{C_{F}} = (F AM(F), \underline{↪}, ≈_{⊳} ). We need to show that ≈=≈_{⊳} . By Definition 4.1, α ≈ β iff α ∩ β ⊳ α ∪ β \ α ∩ β. By Corollary 3.12 and Theorem 4.9, the latter holds iff ST (α) = ST (β), meaning that α ≈_{⊳} β by Definition 3.4.

Now, as a corollary of Theorems 3.10, 3.13, 4.9 and 4.10, we have the following theorem.

Theorem 4.11 For any AZDFS F, P_{F} is a DPES and C_{F} = C_{P_{F}}.

Since ASDRSs are ZDFSs by Theorem 2.14, from the above results we immediately get interpretations of ASDRSs into DPESs and DEESs.

4.2 Translation of DPESs and DEESs into stable DRSs and DFSs

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

Definition 4.12 To a DPES P = (E, ≤, ≈) (resp. a DEES C = (E, ≤, ⊳)) we associate an SDRS R_{P} (resp. R_{C}) as follows:

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

• The reduction relation of R_{P} (R_{C}) consists of sets of pairs u = (⟨α⟩_{L}, e), where α, α + e ∈ L(E) and α ≉ α + e (resp.α ⋫e). Pairs u = (⟨α⟩_{L}, e) such that α ≈ α + e (α ⊳ e) are identified with the empty redex ∅ = (⟨α⟩_{L}, ∅) in ⟨α⟩_{L}.

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

It is easily seen that R_{P} = R_{C_{P}} and R_{C} = R_{P_{C}}. In [GK96], a similar translation of DCSs into SDRSs is given, and its correctness implies also the correctness of Definition 4.12, i.e., R_{P} and R_{C} are indeed SDRSs.

Note that initial reductions in R_{P} and R_{C} can be represented as event sequences e_{1}, …, e_{n} respecting the causal order – e_{i} represents the (contraction of) non-empty redex ({e_{1}, …, e_{i−1}}, e_{i}). That is, reductions are left-closed enumerations of configurations α ∈ L(E), and will be denoted by [α]. (As we will see below, not all left-closed enumerations of a configuration represent a reduction.)

Definition 4.13 To a DPES P = (E, ≤, ≈), we associate a DFS F_{P} = (R_{P}, ≃_{P}, ↪_{P}) as follows:

• R_{P} is the DRSs defined in Definition 4.12.

• ∀e ∈ E, we define the ≃_{P}-family ϕ_{e} corresponding to e by ϕ_{e} = {([α], e) | α + e ∈ L(P) ∧ (⟨α⟩_{L}, e) ≠ ∅}. That is, ([α], e) ≃_{P} ([β], e′) iff e = e′, α + e, β + e ∈ L(P), (⟨α⟩_{L}, e) ≠ ∅, (⟨β⟩_{L}, e) ≠ ∅.

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

Theorem 4.14 Let P = (E, ≤, ≈) be a DPES, let R_{P} and F_{P} = (R_{P}, ≃_{P}, ↪_{P}) be as in Definition 4.13, and let F_{R_{P}} = (R_{P}, ≃_{z}, ↪_{z}) be the corresponding ZDFS of R_{P}. Then F_{R_{P}} = F_{P} (so F_{P} is indeed a DFS). Proof We need to show that ≃_{z}=≃_{P} and ↪_{z}=↪_{P}.

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

Let ϕ_{e} = {([α], e) | α + e ∈ L(P)} and ϕ_{e′} = {([α], e′) | α+e′ ∈ L(P)}} be two families (by (a), they are families both w.r.t. ≃_{P} and ≃_{z}). Then ϕ_{e} ↪_{z} ϕ_{e′} means that for any ([α], e′) ∈ ϕ_{e′}, the sequence [α] contains e; and ϕ_{e} ↪_{P} ϕ_{e′} just means that e < e′. Hence in order to prove ϕ_{e} ↪_{z} ϕ_{e′} ⟺ ϕ_{e} ↪_{P} ϕ_{e′} it is enough to show that e < e′ ⟺ e ∈ [β] for any ([β], e′) ∈ ϕ_{e′}. (⇒) is immediate since β + e′ ∈ L(P) is left closed. (⇐) Let ([γ], e′) be a canonical element of ϕ_{e′} which exists by Theorem 2.13 (when ϕ_{e′} is considered as a zig-zag family); it has the property that γ ⊆ α for any α such that ([α], e) ∈ ϕ_{e′}. Then e ∈ γ. If on the contrary e ≮ e′, then ∃γ′L(E) : e′ ∈ γ′ ∧e ∉ γ′, and since e ∈ γ, γ + e′ is not the smallest (wrt ⊆) left-closed subset containing e′ – contradiction.

4.3 Equivalence of the four models

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

Definition 4.15 (1) We call DRSs R = (A, /) and R′ = (A′, /′) isomorphic if there is an isomorphism between reduction graphs of A and A′ respecting the residual relation.

(2) We call DFSs F = (R, ≃, ↪) and F′ = (R′, ≃′ , ↪′) isomorphic if there is an isomorphism between R and R′ respecting ≃ and ≃′ (and hence, by [contribution], respecting ↪ and ↪′).

(3) We call DPESs P = (E, ≤, ≈) and P′ = (E′, ≤′ , ≈) isomorphic if there is an isomorphism between (E, ≤) and (E′, ≤′) respecting ≈ and ≈′.

Theorem 4.16 (1) For any DPES P, P_{F_{P}} ⇀ ↽ P.

(2) For any ADFS F, F = F_{P_{F}}. Proof {Zurab: Routine.}

5 Configuration Domains

Definition 5.1 We call a left-closed enumeration (i.e, respecting the causality relation) \overline{α} = e_{1}, …, e_{k} of a configuration α = {e_{i} | i = 1, …, k} a reduction or an α-reduction if no event e_{i} in \overline{α} is vacuous, i.e., erased by the set of its preceding events: {e_{1}, …, e_{i−1}} ⋫e_{i}. An α-reduction will be denoted by [α].

Thus reductions in a DPES P precisely correspond to initial reductions in the corresponding ASDRS R_{P}, and the use of notation [α] both for reductions in P and R_{P} should not be confusing.

Note that, unlike Prime Event Structures, 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_{e} < 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 is a left-closed enumerations, such as e_{1}, e_{2}, e′_{1}, e′_{2}, ends either with e′_{1} or with e′_{2}, and we have {e_{1}, e_{2}, e′_{2}} ⊳ e′_{1} and {e_{1}, e_{2}, e′_{2}} ⊳ e′_{1}. This is not surprising as the vacuous events in left-closed sequences correspond to empty reductions in the corresponding ASDRS, performed in the ‘garbage’ (erased redexes). However, we have the following lemma.

Lemma 5.2 Let α ∈ L(C), in a DEES C. Then any left-closed enumeration of ST (α) is a reduction. Proof Let e_{o}, …, 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 5.3 Let P be a DPES, L^{≈}(P) = L(P)/_{≈} = {⟨α⟩_{L} | α ∈ L(P)}, where ⟨α⟩_{L} is the ≈- class of configurations containing α, and let L^{⪯}(P) = (L^{≈}(P), ⪯) be a partial order defined by ⟨α⟩_{L} ⪯ ⟨β⟩_{L} iff ST (α) ⊆ ST (β). Further, define ⟨α⟩_{L} ⊔ ⟨β⟩_{L} = ⟨α ∪ β⟩_{L} and ⟨α⟩_{L} ⊓ ⟨β⟩_{L} = ⟨α ∩ β⟩_{L}.

Theorem 5.4 Let P be a DPES. Then L^{⪯}(P) = (L^{≈}(P), ⪯), with the join ⊔ and meet ⊓ defined as in Definition 5.3, is a distributive lattice. Proof Easy.

Note that if P, Q are initial reductions in an ASDRS R and P_{R} is its corresponding DPES, then P ⊴Q need not imply ⟨F AM(P)⟩_{L} ⪯ ⟨F AM(Q)⟩_{L}. For example, take a term v = (λx.y)u in the λ-calculus, where u is a β-redex, and let P = u and Q = v. Then P ⊲ Q but ⟨F AM(P)⟩_{L} ⪯̸ ⟨F AM(Q)⟩_{L} since ST (F AM(P)) = {F am(u)} and ST (F AM(Q)) = {F am(v)}, and ST (F AM(P)) ⊈ ST (F AM(Q)). This is not unexpected, as it is a well known problem of Lévy’s reduction space that it is not a lattice but only an upper semi-lattice. We now define an ordering on (permutation-equivalence classes of) reductions in R that matches the embedding on configurations defined above, and makes R a distributive lattice.

Definition 5.5 Let P, Q be co-initial finite reductions in an ASDRS R. Define P ⪯ Q iff P is Q-needed. We refer to ⪯ as the embedding relation (while we call ⊴ Lévy-embedding relation).

Proposition 5.6 In an ASDRS, P ⪯ Q ⇒ P ⊴ Q, but not conversely; and P ≈ Q iff P ⪯ Q and Q ⪯ P.

Lemma 5.7 Let P, Q ∈ ST A and be initial. Them F AM(Q/P) = F AM(Q)\F AM(P). If moreover P ⊴ Q, then F AM(P) ⊆ F AM(Q), hence F AM(Q) = F AM(Q/P) ∪ F AM(P).

Lemma 5.8 Let P be Q-needed, and let P, Q ∈ ST A, in an AZDFS. Then F AM(Q) = F AM(P) ∪ F AM(Q/P). Proof Since P be Q-needed, P ⊴ Q, hence Q ≈ P + Q/P. Since Q/P is standard by Lemma 4.3 and P is P ⊔Q-needed, P ⊔Q is standard. By Proposition 2.12, F AM(Q) = F AM(P ⊔Q) = F AM(P)∪F AM(Q/P).

Lemma 5.9 Let P, Q ∈ ST A, in an AZDFS. Then P is Q-needed iff F AM(P) ⊆ F AM(Q). Proof (⇐) By Lemma 5.8. (⇒) Let F AM(P) ⊆ F AM(Q), and suppose on the contrary that P is not Q-needed. Let P = P′ + u + P′′, where u is the first Q-unneeded step of P. Since Q/P′ is standard by Lemma 4.3 and erases u, it is external to u by Lemma 4.2. Thus F am(u) ∉ F AM(Q/P′). By the Unique Families Lemma, F am(u) ∉ F AM(P′), hence F am(u) ∉ F AM(Q) by Lemma 5.8, contradiction.

Corollary 5.10 In an affine ZDFS, P ⪯ Q iff SF AM(P) ⊆ SF AM(Q). Proof By Proposition 2.12, SF AM(P) ⊆ SF AM(Q) iff F AM(ST (P)) ⊆ SF AM(ST (Q)). Further, ST (P), ST (Q) ∈ ST A by the Standardization theorem, and the statement follows from Definition 5.5 and Lemma 5.9.

Definition 5.11 Let R be an ASDRS, L^{≈}(R) = L(R)/_{≈} = {⟨P ⟩_{L} | P ∈ L(R)}, where L(R) is the set of initial reductions in R and ⟨P ⟩_{L} is the ≈- class containing P, and let L^{⪯}(R) = (L^{≈}(R), ⪯), where ⪯ is the embedding relation defined in Definition 5.5. Further, define ⟨P ⟩_{L} ⊔ ⟨Q⟩_{L} = ⟨P ⊔ Q⟩_{L} and ⟨P ⟩_{L} ⊓ ⟨Q⟩_{L} = ⟨[SF AM(P) ∩ SF AM(Q)]⟩_{L}, i.e., ⟨P ⟩_{L} ⊓ ⟨Q⟩_{L} = ⟨N⟩_{L}, where N is an initial reduction with SF AM(N) = SF AM(P) ∩ F AM(Q).

Existence of ⟨P ⟩_{L} ⊓ ⟨Q⟩_{L} follows from Lemma 5.2, but we can directly construct a canonical element P ⊓ Q ∈ ⟨P ⟩_{L} ⊓ ⟨Q⟩_{L} by the following algorithm. First, standardize P and Q. Let P′ = ST (P) and Q′ = ST (Q). Using the algorithm in Lemma 4.8, construct P′′ ∈ ST AP′ in which the steps not in F AM(Q′) form a tail. P ⊓ Q is obtained from P′′ by removing that tail. Clearly, F AM(P ⊓Q) = SF AM(P)∩SF AM(Q), hence P ⊓ Q ∈ ⟨P ⟩_{L} ⊓ ⟨Q⟩_{L}.

Theorem 5.12 Let R be an ASDRS and let P = P_{R} be its corresponding DPES. Then f : ⟨P ⟩_{L} ⟶ ⟨F AM(P)⟩_{L} is the isomorphism between L^{⪯}(R) and L^{⪯}(P), with the inverse f^{−1} : ⟨α⟩_{L} ⟶ ⟨[ST (α)]⟩_{L}.

6 Event Structure semantics for stable DRSs

Now we come to constructing event style semantics for orthogonal rewrite systems. Our interpretations will be based again on interpretation of redexfamilies as events, so we assume that if the system is duplicating, then it comes with a notion of redex-family (defined via labelling, extraction or zigzag [Lév80, Mar91, AL93, Oos96]) satisfying our family axioms. That is, we assume that the orthogonal system is given in the form of a DFS, and we discuss two event structure semantics for DFSs.

In [GK96] we gave an interpretation of DFSs into Prime Event Structures. To a DFS F = (R, ≃, ↪), we associated the PES E_{F} = (E_{F}, \underline{↪}), where E_{F} = F AM(F), the set of all families ϕ of F; and where ϕ\underline{↪}ψ means that ϕ ↪ ψ or ϕ = ψ. Since events of an event structure are supposed to correspond to all computation steps of a process, one may find the above interpretation unsatisfactory, since some of the events in E_{F} may never occur in a reduction sequence in E_{F}. This is not surprising, since events in E_{F} correspond to all computations in R, while events in reductions in E_{F} correspond to families contracted in family reductions in F. For example, consider a CRS ([Klo80]) R with rules {F [x]Z(x) → Z(Z(x)), H(x) → a, G(a) → b}, restricted to the graph of the term t = F [x]H(G(x)). Let P : F [x]H(G(x)) → H(G(H(G(x)))) → H(G(a)) and v = G(a). Then the redex P v has a corresponding event in the corresponding PES, but in no complete-family reduction redexes zig-zag related to P v can be contracted, since if one contracts the whole family of the redex H(G(x)), no redex in the family of P v will be created: F [x]H(G(x)) → H(G(H(G(x)))), F [x]H(G(x)) → H(G(H(G(x)))) → → a, and F [x]H(G(x)) → F [x]a → a are all complete family reductions in R, but neither contracts the family of P v.

To avoid this situation, we first associate an AS-DRS R_{F} to a DFS F, called the linearization of F, and interpret F in the DEES or DPES corresponding to R_{F}, which we have already defined in previous sections. The reduction steps in R_{F} correspond to multi-steps of F contracting all members of a family in parallel.

Definition 6.1 We call a multi-step reduction in a DFS a complete family-reduction, or just a familyreduction, if each multi-step is a complete development of the maximal set of redexes of some family.

Definition 6.2 Let F = (R, ≃, ↪) be a DFS. The linearization of F is the ASDRS R_{F} = (A, /), where

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

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

It is easy to check that R_{F} in the above definition is indeed an ASDRS. One first checks that if U and V are complete sets of redexes in two different families in a term s and s→^{U}o, then V/U forms a complete family too, in o. Obviously, V/V = ∅, and every family in o has at most one ancestor family in s. Finally, [acyclicity] and [stability] for R_{F} follow immediately from the Acyclicity Lemma and Stability Lemma, respectively. From the correctness of Definition 6.2 and Theorem 2.14, we have the following theorem.

Theorem 6.3 Let F = (R, ≃, ↪) be a ZDFS. Then its linearization is an AZDFS.

The extraction procedure [KG96a] in the linearization R_{F} of an Orthogonal (possibly duplicating) Rewrite System, F, first or higher order, corresponds to ‘family-extraction’ in family-reductions, eliminating all family-steps not contributing to a family. (So family-extraction is different from extraction in that the latter eliminates particular redexes in a history, which need not be a family-reduction.) If F comes equipped with the labelling concept of family, two families in different family-reductions can be familyextracted to the same canonical representative iff the families have the same label (since extraction preserves labels of every family). Here a canonical representative of a family is one whose history is a family-reduction contracting only contributor families, and is unique up to the order of contraction of causally independent families.) Since labelling and extraction families coincide in orthogonal rewrite systems [Lév80, Mar91, AL93, Oos96]) and zig-zag and extraction families coincide in ASDRSs [KG96a], families contracted in family-reductions in F are in oneto-one correspondence with zig-zag families in the corresponding linearization R_{F}.

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

Acknowledgments We thank bla for useful comments.

References

[AL93] Asperti A., Laneve C. Interaction Systems I: The theory of optimal reductions. MSCS 11:1-48, 1993.

[Bar84] Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.

[Ber79] Berry G. Modéles complétement adéquats et stables des λ-calculs typés. Thèse de l’Université de Paris VII, 1979.

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

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

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

[CELMR94] Corradini A., Ehrig H., Löwe M., Montanari U., Rossi F. An event structure semantics for safe graph grammars. In proc PROCOMET’94, IFIP Transactions A-56, 1994.

[CF58] Curry H. B., Feys R. Combinatory Logic. vol. 1, North-Holland, 1958.

[GK96] Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In: Proc. of CAAP’96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180-195.

[GK96a] Glauert J.R.W., Khasidashvili Z. Relative normalization in stable deterministic residual structures. Technical Report SYS-C96-01, UEA, Norwich, UK.

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. of LICS’92, Santa Cruz, California, 1992, p. 72-81.

[Hin64] Hindley R.J. An abstract form of the Church-Rosser theorem I. JSL, 34(4):545-560, 1969.

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

[KKSV93] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Event structures and orthogonal term graph rewriting. In [SPE93].

[KG96] Khasidashvili Z., Glauert J. R. W. Discrete normalization and Standardization in Deterministic Residual Structures. In: Proc. of ALP’96, Springer LNCS, vol. 1139, M. Hanus, M. Rodríguez-Artalejo, eds. 1996, p.135-149.

[KG96a] Khasidashvili Z., Glauert J.R.W. Zig-zag and extraction families in non-duplicating stable Deterministic Residual Structures. Submitted. (ftp://ftp.sys.uea.ac.uk/pub/zurab/LinZig.ps.gz)

[Klo80] Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980.

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

[Lan93] Laneve C. Optimality and Concurrency in Interaction Systems. Ph.D. Thesis, University of Pisa, 1993.

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

[LM94] Laneve C., Montanari U. Axiomatizing permutation equivalence. MSCS, 6:219 - 249, 1994.

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

[Lév80] Lévy J.-J. Optimal reductions in the Lambdacalculus. 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.

[Mar91] Maranget L. Optimal derivations in weak λcalculi and in orthogonal Term Rewriting Systems. In: Proc. of POPL’91, p. 255-269.

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

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

[Oos94] Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D. Thesis, Free University, Amsterdam, 1994.

[Oos96] Van Oostrom V. Higher order families. In: Proc. of RTA’96, Springer LNCS, vol. 1103, Ganzinger, H., ed., 1996, p. 392–407.

[Raa96] Van Raamsdonk F. Confluence and normalisation for higher-order rewriting. Ph.D. Thesis, Free University, Amsterdam, 1996.

[Sch94] Schied G. On relating rewrite systems and graph grammars to event structures. In [SE94], p. 326-340.

[SE94] Schneider H.-J. Ehrig H., editors. Proceedings of the Dagstuhl Seminar 9301 on Graph Transformations in Computer Science, Springer LNCS, vol. 776, 1994.

[SPE93] Sleep M. R., Plasmeijer M. J., van Eekelen M. C. J. D., eds. Term Graph Rewriting: Theory and Practice. John Wiley, 1993, p.141-156.

[Sta89] Stark E. W. Concurrent transition systems. TCS 64(3):221-270, 1989.

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

[Win89] Winskel G. An introduction to Event Structures. In proc. of School/Workshop on ‘Linear time, branching time and partial order in logics and models of concurrency’. Springer LNCS, vol. 354, 1989, p. 364-397.