Relating Conflict-free Stable Transition and Event Models (Extended Abstract, Submitted to MFCS’97)

Zurab Khasidashvili

NTT Basic Research Laboratories, A4S-220S

Atsugi, Kanagawa-pref, 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 style semantics for conflict-free (term and graph, possibly with bound variables) rewrite systems, including the λ-calculus and other stable transition systems with residual relation. Our interpretation is based on interpreting redex-families as events. It treats permutationequivalent reductions as representing the same concurrent computation. Since Event Structures are inadequate for such interpretation (because of the erasure of redexes), we extend the Prime Event Structure model by axiomatizing the permutation-equivalence on finite configurations in two different ways (for the conflictfree case), and show that thus extended models are equivalent 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, Win86/89, WN95]. Conflictfree Prime Event Structures (PESs) are sufficient for our purposes. A (conflict-free) PES is simply a set of events partially ordered by causal dependency relation (i.e., is 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 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 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 [Lév80], which formalizes the idea of the ‘same atomic task’. Therefore we want to base our interpretation on interpreting redexfamilies as events, hence to interpret family-reductions (contracting entire families as multi-steps) as configurations of the corresponding PES. This is also justified by the fact that reductions in optimal 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, KG97] allows us to address the problem (entirely!) 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 [GK96] to prove analogs of the Normalization and Standardization Theorems [Bar84]. 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 family-reduction. It corresponds to the fact that any event may occur at most once in the course of a computation, and is needed for event structure interpretation of DRSs based on interpreting families as events.

Since we want to restrict our attention to familyreductions only, we define linearization of DFSs. We show that the linearization of any DFS is a nonduplicating, also called affine, DFSs, with the zigzag [Lév80] as the family relation (AZDFS). Familyreductions in a DFS precisely correspond to reductions in its linearization, and this allows us to concentrate on construction of event semantics for AZDFSs only. We have shown in [KG97] that any affine SDRS, AS-DRS, is in fact an AZDFS.

∗The contact author. Fax: 81 462 404709.

†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 (finite) configuration (i.e., all its possible sequentializations) should be in one-to-one correspondence with all reductions in the equivalence class which the configuration is supposed to represent. Because of the huge importance of the permutation or Lévy equivalence [Lév80] to the whole theory of (not only orthogonal) rewrite systems [HL91, Bou85], which is well understood by now, and to the concurrency theory too [Sta89], we want to treat permutation-equivalent reductions as representing the same concurrent computation, as indeed permutationequivalent reductions result one from another by permuting concurrent consecutive steps. However, this is clearly impossible in the present PES framework [Win86/89], as a configuration in a PES has only a finite number of runs while a permutationequivalence class of a (finite) reduction may have an infinite number of elements.

In order for an equivalence relation to satisfy the adequacy requirement, the corresponding equivalence classes of (finite) reductions must be partially ordered in a way to form distributive lattices, as the domains of (finite) configurations of a PES ordered by inclusion are such lattices [Win86/89]. However, it is well known that Lévy’s reduction space is not in general a lattice, 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 that cannot erase or duplicate one another, and consequently all equivalent sequences have the same length. 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 to cope with problems with erasure. As needed redexes cannot be erased, all needed normalizing reductions are of the same length, and on needed reductions, the permutation and distributive equivalences coincide (since the system is affine). Similarly, Clark and Kennaway [CK95] work with permutation-equivalence and allow infinite reductions but restrict themselves to standard reductions only (which are unique in their permutation-equivalence class). Schied [Sch94] and Corradini et al [CELMR94] work with linear rewrite systems (no duplication, no erasure), mainly graph grammars, and do not therefore encounter the erasure problems.

In order to cope with the adequacy problem, we extend the PES model by axiomatizing permutationequivalence on event configurations. We do it in two different ways. One by directly constraining the class of all equivalence relations on configurations, and another by axiomatizing the 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 [GK96]. In the resulting extended models, Deterministic Permutation and Erasure Event Structures, DPESs and DEESs, we can identify configurations with different number of events but still representing the same permutation-equivalence class of reductions. We show that permutation-equivalence classes of configurations in a DPES/DEES, appropriately ordered, are isomorphic to Lévy’s reduction space of the corresponding ASDRSs, therefore the former give a fully adequate semantics to ASDRSs.

The paper is organized as follows. In the next section, we review the existing theory of DRSs and DFSs used in this paper. In section 3 we introduce DPESs and DEESs and establish their equivalence. In section 4 we relate the latter event models with affine SDRSs and zig-zag DFSs, showing the equivalence of the four models. In section 5, we define Lévy-embedding on configurations in a DPES/DEES and show its isomorphism with Lévy’s reduction space of the corresponding ASDRS. Finally, in section 6, we extend our interpretation to duplicating orthogonal rewrite systems by encoding DFSs into AS-DRSs/AZDFSs using the linearization method mentioned above. Conclusions appear in section 7.

2 Deterministic Residual and Family Structures

In this section we recall some basic theory for DRSs and DFSs developed in [GK96, KG96, KG97].^{1} We start by introducing Abstract Reductions Systems, ARSs.

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. 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]. Further, for example, Interaction Nets [Laf90], which form DRSs (when restricted to finite nets), do not have or need any nesting order on redexes (as nets are undirected, possibly cyclic, graphs).

DRSs axiomatize exactly the properties of residuals which are used in [Lév80, HL91] to define permutation equivalence on reductions and Lévy-embedding relation on permutation-equivalence classes, that is, to define Lévy’s reduction space. Hence DRSs are the minimal axiomatization of the residual concept enabling one to relate the operational and denotational semantics of orthogonal rewrite systems.

Definition 2.2 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 complete developments of a set of redexes 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] 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 along 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. 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 following two lemmas, established in [GK96, KG96], 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 contact redexes having common residuals.

1The axioms [acyclicity] and [termination] are renamed to [weak acyclicity] and [FFD], respectively, where FFD stands for finite family Developments.

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

[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) 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) Let P, N be co-initial finite reductions in a DRS, and let P be external to N. Then N ≉ P.

Definition 2.6 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).

• [FFD] 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]).

We call a DFS separable, SDFS, 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′′).

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 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 ∅, by analogy with the initial state in an Event Structure, although ∅ will also be used to denote empty reductions. Further, in DFSs, families will always be considered relative to ∅, i.e., all histories start with ∅. Unless otherwise stated, by a reduction we mean a finite reduction. Reductions starting from ∅ will also be called initial reductions.

2.1 Standardization

We recall some definitions and results from [KG96] concerning standardization of reductions in nonduplicating, i.e., affine, SDRSs, ASDRSs.

Definition 2.7 • 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 so is every redex contracted in P. We call P selfneeded 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 discards concept however does depend on the particular reduction in the permutation-equivalence class.

Lemma 2.8 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 = ∅, when so is 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 2.8). 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 2.9 (Standardization) For any finite reduction P in a stable non-duplicating DRS, ST (P) is a standard reduction Lévy-equivalent to P.

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

2.2 Families in Affine SDRSs

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

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 2.10 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.11 (Affine Extraction) Every redex P v in an ASDRS has a zig-zag related redex P′v′ in canonical form, meaning that P′ ∈ ST A 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.12 (Affine Families) Let R be a nonduplicating SDRS. Then F_{R} = (R, ≃_{z}, ↪_{z}) is a zigzag 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.

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., [San93]) processes (that can fire events) can be passed 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 (no actions can be erased or duplicated), such as CCS [Mil80] and the π-calculus [Mil92]. However, any attempt to adequately interpret higher-order process languages in Event Structures would face the same erasure problems discussed in the introduction (no such interpretation is discussed in [WN95]. As in the case of reductions, the aim of axiomatizing permutation equivalence on event configurations is to be able to equate configurations which differ only by irrelevant or inessential events.

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.

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, F in(E), and will be omitted. Finite configurations of E are finite left-closed subsets α, β, … of E, i.e., subsets L(E) = {α ⊆ F in(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, ≤) is a conflict-free PES and ≈⊆ L(E) × L(E) is an equivalence relation, called Lévy or permutationequivalence, satisfying the following axioms, where α, β, γ ∈ L(E):

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

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

• [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, ≤) is a conflict-free PES and ⊳ ⊆ L(E) × E is inessentiality or erasure relation, satisfying the following axioms, where α, β ∈ L(E):

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

• [E1] α ⊳ e ∧ α ⊆ β ⇒ β ⊳ e;

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

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

• [E4] α ∪ ⌈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 α. It is easy to show that α ∈ L(E) ⇒ ST (α) ∈ L(E).

A close inspection of the above definitions shows that the DPES axiom [P0] is a counterpart of the DEES axioms [E0] and [E4], and similarly for [P3] and [E3]. Further, the combination of [P1] and [P2] have the same effect as that of [E1] and [E2]. [E4] does not have a ‘direct’ counterpart among DPES axioms, but it corresponds to the fact that, according to Definition 2.7, a redex with history P v is Q-inessential iff v is Q/P -inessential. Similarly, [P0] corresponds to Lemma 2.8.(2).

We need the following characterization of ≈_{⊳} via ⊳ and ≈ via ⊳_{≈}, which is not difficult to prove from the erasure and permutation axioms.

Proposition 3.5 ∀α, β, γ ∈ L(C) : α ∩ β ⊆ γ ⊆ α ∪ β, α ≈_{⊳} β ⇔ ST (α) = ST (β) ⇔ γ ⊳ α ∪ β \ α ∩ β.

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

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

[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 Proposition 3.5. 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), we have by Proposition 3.5 that ST (α + e) = ST (ST (α) + e), thus α + e ≈_{⊳} ST (α) + e by Definition 3.4. Similarly, β + e ≈_{⊳} ST (β) + e, implying α + e ≈_{⊳} β + e (since ST (α) = ST (β)).

Theorem 3.8 For any DPES P = (E, ≤, ≈), C_{P} = (E, ≤, ⊳_{≈}) is a DEES. Proof We need to show that ⊳_{≈} satisfies the erasure axioms [E0] – [E4]. [E0] follows from Definition 3.3 and [P0], and [E4] is immediate from Definition 3.3. Proofs of the other axioms are not too long, but are tedious to include here.

Theorem 3.9 (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. 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 Proposition 3.5, 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 Proposition 3.6 and Definition 3.4, α ≈ β iff ST_{⊳_{≈}} (α) = ST_{⊳_{≈}} (β) iff α ≈′ β.

4 Relating Transition and Event models

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

4.1 Translation of affine SDRSs and ZDFSs into DPESs and DEESs

Definition 4.1 To an AZDFS 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 ϕ (see Theorem 2.11);

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

In order to prove the correctness of Definition 4.1, we need, among others, the following lemma, which is obtained using results in subsections 2.1 and 2.2.

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

Lemma 4.3 Let P ∈ ST A, F AM(P) = F_{1} ∪ F_{2}, F_{1} ∩ F_{2} = ∅ and ∀ϕ ∈ F_{2}, ∀ψ ∈ F_{1} : ϕ ↛ ψ. Then ∃Q ∈ ST V (P) : 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. The transformation terminates as it does not change the length of reductions.

Lemma 4.4 For any AZDFS F, C_{F} is a DEES. Proof We need to show that C_{F} = (E_{F}, \underline{↪}, ⊳) satisfies the erasure axioms. We only prove [E4].

[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.10 and Lemma 4.2, 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.3, ∃Q ∈ ST V (P) : Q′ = Q_{1} + Q_{2}, F AM(Q_{i}) = F_{i}. By Lemma 4.2, Q′ discards P v, and Q′/P = Q_{1}/P, since ⌈ϕ^{<}⌉ ⊆ F AM(P). Hence Q_{1} discards P v and F AM(Q_{1}) ⊆ α, implying α ⊳ ϕ.

It is an immediate consequence of Definitions 4.1 and 3.4, Proposition 3.6 and the above lemma that for any AZDFS F, P_{F} = P_{C_{F}}. By combining this with Theorems 3.7 and 3.9, we get the following theorem.

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

Since ASDRSs are AZDFSs by Theorem 2.12, 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), used for construction of PESs from stable families of configurations in [Win86/89].

Definition 4.6 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 P (C);

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

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.6, 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 (some of) 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. Such enumerations will be called quasi-reductions. Quasi-reductions are defined similarly in any DRS – they are ‘reductions containing empty steps corresponding to erased redexes’.

Definition 4.7 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.6.

• ∀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′.

One easily shows that translations P → F_{P} and P → R_{P} commute with the zig-zag embedding R → F_{R}, i.e., F_{R_{P}} = (R_{P}, ≃_{z}, ↪_{z}) = (R_{P}, ≃_{P}, ↪_{P}) = F_{P}, implying in particular the correctness of Definition 4.7.

Theorem 4.8 For any DPES P, F_{P} is an AZDFS.

4.3 Equivalence of the four models

For any of the four models, there is an obvious concept of isomorphism, ⇀ ↽. For example, DFSs F = (R, ≃ , ↪) and F′ = (R′, ≃′, ↪′) are isomorphic if there is an isomorphism between the underlying reduction graphs of R and R′ respecting the residual, family, and contribution relations in F and F′.

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

(2) For any AZDFS F, F ⇀ ↽ F_{P_{F}}. Proof Routine, from Definition 4.1 and Definition 4.7.

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

5 Configuration Domains

Let us call a left-closed enumeration (i.e., respecting the causality relation) e_{1}, …, e_{k} of a configuration α a reduction or an α-reduction if no event e_{i} in the sequence is vacuous, i.e., ∀i : {e_{1}, …, e_{i−1}} ⋫e_{i}. Any other left-closed enumeration of α will be called a quasi-reduction. An α-reduction will be denoted by [α]. Thus reductions in a DPES P precisely correspond to initial reductions in the corresponding AS-DRS 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_{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 is left-closed enumerations, such as e_{1}, e_{2}, e′_{1}, e′_{2}, ends either with e′_{1} or with e′_{2}, and we have {e_{1}, e_{2}, e′_{2}} ⊳ 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). Thus quasi-reductions in a DPES/DEES correspond to quasi-reductions in the corresponding ASDRS. However, we have the following lemma.

Lemma 5.1 Let α ∈ L(C), in a DEES C. 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 5.2 (1) Let P be a DPES, L^{≈}(P) = L(P)/_{≈} = {⟨α⟩_{L} | α ∈ L(P)}, and let L^{⊴} (P) = (L^{≈}(P), ⊴) be a partial order defined by ⟨α⟩_{L} ⊴ ⟨β⟩_{L} iff ∃α′ ∈ ⟨α⟩_{L}, ∃β′ ∈ ⟨β⟩_{L} : α′ ⊆ β′.

(2) 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 let L^{⊴} (R) = (L^{≈}(R), ⊴), where ⊴ is Lévy’s embedding relation.

¿From the above comparison of (quasi)-reductions in DPESs and ASDRSs, we have the following fact:

Proposition 5.3 ⟨P ⟩_{L} ⊴ ⟨Q⟩_{L} in an ASDRS R iff ⟨F AM(P)⟩_{L} ⊴ ⟨F AM(Q)⟩_{L} in P_{R}.

Theorem 5.4 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}. Moreover, (quasi-)reductions in ⟨P ⟩_{L} are in one-to-one correspondence with these in ⟨F AM(P)⟩_{L}. Proof By Proposition 5.3 and Lemma 5.1.

Note that L^{⊴} (P) is not a lattice since L^{⊴} (R) is not. However, depending on the set of ‘results’ we are interested in, we can construct a (distributive) lattice on configurations in P reflecting growth of information relative to that goal. For example, if we are interested in fair computations, we can order configurations by defining α ⪯ β iff NE(α) ⊆ NE(β), where NE(α) is the set of fairly-needed events of α. Here an event is fairly-needed in P if it belongs to every, possibly infinite, configuration in the maximal element of the ideal completion of L^{⊴} (P). Fairly-needed redexes in R coincide with Maranget-needed or essential redexes, and are contracted in all fair reductions in R, which are maximal w.r.t. ⊴ [GK94]. Note that ⪯ induces an equivalence relation which is different from the permutation-equivalence. Construction of such ‘relativized’ information domains from configurations in DPESs will be addresses in detail in a separate paper.

6 Event Structure semantics for DFSs

Now we come to constructing event semantics for orthogonal rewrite systems. Our interpretations is based on interpreting redex-families as events, so we assume that if the system is duplicating, then it comes with a notion of redex-family ([Lév78, Lév80, Mar91, AL93, Oos96]) satisfying our family axioms, i.e., it is a DFS.

Recall that a multi-step reduction in a DFS is a (complete) family-reduction if each multi-step is a complete development of the maximal set of redexes of some family. it is immediate that for any DFS F = (R, ≃, ↪), E_{F} = (F AM(F), \underline{↪}) is a PES [GK96]. Note however that some of the events in F AM(F) may never occur in reduction sequences of E_{F} that correspond to family-reductions in F. ^{2} As argued in the introduction, we want events in the corresponding DPES of F to match precisely the families contracted in family-reductions in F. Therefore, we first associate an ASDRS F_{l} to a DFS F, called the linearization of F, and interpret F in the DEES or DPES corresponding to F_{l}. The reduction steps in F_{l} correspond to family-reduction multi-steps of F.

Definition 6.1 Let F = (R, ≃, ↪) be a DFS. The linearization of F is the AZDFS F_{l} = (R_{l}, ≃_{l}, ↪_{l}), where

• the branches of the reduction graph of the underlying ARS A of R_{l} = (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 families, in a term s, and let U : s → o be the multi-step contacting U. Then V/U is the multi-step o → e contracting all members of the set V/U in a multi-step.

• the family and contribution relations ≃_{l}, ↪_{l} in F_{l} are those induced by ≃ and ↪.

It is easy to check that F_{l} in the above definition is indeed an AZDFS. 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. Further, [weak acyclicity] and [stability] for F_{l} follow immediately from the Acyclicity Lemma and Stability Lemma, respectively. The axiom [initial] in F_{l} follows immediately from [initial] in F. If P + U + V is a reduction in F_{l} such that U creates V, then the redexes in V are created along U (when P +U +V is considered as a reduction in F), i.e., F am(U) ↪ F am(V) in F, hence F am(U) ↪_{l} F am(V), implying [contribution] in F_{l}. Since family-reductions can be viewed as reduction in F (by considering multi-steps as corresponding complete developments), [contribution] for ↪_{l} follows immediately from [contribution] for ↪. Finally, [FFD] for F_{l} follows immediately from the Unique Families Lemma for F. Hence F_{l} is indeed a DFS. Note that F_{l} is separable as its steps contract entire families in F, hence it is an AZDFS by Theorem 2.12:

Theorem 6.2 For any DFS F, F_{l} is an AZDFS.

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

7 Conclusions

We have established an equivalence between deterministic stable operational (ASDRSs) and domaintheoretic (DPESs and DEESs) models of computation, and based on this, constructed a fully adequate event style concurrent semantics for orthogonal rewrite systems. The correspondence between Event Structures and the denotational semantics is well studied [Win86/89], and we hope that our results contribute to better understanding of relationship between operational and denotational semantics of sequential and concurrent languages.

2For example, consider a CRS ([Klo80]) R with rules {F [x]Z(x) → Z(Z(x)), H(x) → a, G(a) → b}, restricted to the reduction 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 (F AM(R), \underline{↪}), but no family-reduction can create redexes in F am(P v).

For example, the theory of normalization by neededness relative to stable sets of terms in ASDRSs [GK96] has a counterpart in DPESs, thus implying a concept of stable sets of configurations in DPESs, different from the concept of stable families of configurations in [Win86/89].^{3} The concept of stability of an Event Structure (E, ⊢) (with an enabling relation ⊢ instead of a causal order ≤) [Win86/89] becomes a special case of our concept of stable sets, as it is trivial to check that (E, ⊢) is stable iff for any e ∈ E, so is the set of all configurations containing e. Study of precise relationship between syntactic and semantic concepts of stability and its relationship with sequentiality (neededness) goes beyond the scope of this paper.

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

We expect that the theory developed here for conflict-free systems can be extended to the general case, so that higher order process calculi in which processes can be passed and erased can be modeled too.

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.

[CK95] Clark D., Kennaway R. Some properties of non-orthogonal term graph rewriting. ENTCS 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.

[GK94] Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in Orthogonal Expression Reduction Systems. Report SYS-C94-06, UEA, Norwich, 1994.

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

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

[KG97] Khasidashvili Z., Glauert J.R.W. Zig-zag, extraction and separable families in non-duplicating stable Deterministic Residual Structures. Free University Technical Report, Amsterdam, 1997 (in print). (ftp://ftp.sys.uea.ac.uk/pub/zurab/VU-1997.ps.Z)

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

[Laf90] Lafont Y. Interaction nets. In: Proc. of POPL’90, p. 95-108.

3A set S of configurations in a DPES P is stable if it is closed under Lévy-equivalence, α ∈ S ∧ β ∈ S ⇒ α ∩ β ∈ S, and (α ∈ S ∧ β ∈ L(P)∧ ∄γ ∈ S : γ ⊆ β) ⇒ α ∪ β ∈ S. Recall that stability of S is a sufficient and necessary condition for the S-needed strategy to be S-normalizing [GK94, GK96].

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

[Mil80] Milner R. A calculus of communicating systems. Springer LNCS, vol. 92, 1980.

[Mil92] Milner R. Functions as processes. In: Journal of Mathematical structures in Computer Science. 2(2): 1992, p. 119–141.

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

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

[Sch94] Schied G. On relating rewrite systems and graph grammars to event structures. Springer LNCS, vol. 776, Schneider H.-J. Ehrig H., eds, 1994, p. 326-340.

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

[Win86/89] Winskel G. An introduction to Event Structures. Springer LNCS, vol. 354, 1989, p. 364-397. Extended version appears as Cambr. Univ. Comp. Lab. Report n. 95, 1986.

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