Relating Conflict-free Stable Transition and Event Models (Extended Abstract)

Zurab Khasidashvili^{1} and John Glauert^{2}

1 NTT Basic Research Laboratories, Atsugi, Kanagawa, 243-01, Japan zurab@theory.brl.ntt.co.jp 2 School of Information Systems, UEA, Norwich NR4 7TJ England jrwg@sys.uea.ac.uk ^{⋆⋆⋆}

Abstract. We describe an event-style (or poset) semantics for conflictfree rewrite systems, such as the λ-calculus, and other stable transition systems with a residual relation. Our interpretation is based on considering redex-families as events. It treats permutation-equivalent reductions as representing the same concurrent computation. Due to erasure of redexes, Event Structures are inadequate for such an interpretation. We therefore extend the Prime Event Structure model by axiomatizing permutation-equivalence on finite configurations in two different ways, for the conflict-free case, and show that these extended models are equivalent to known stable transition models with axiomatized residual and family relations.

1 Introduction

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

In the theory of orthogonal rewrite systems, such as the λ-calculus, there is the well established concept of ‘redex-family’, due to Lévy [Lév80], which formalizes the idea of the ‘same atomic task’. Therefore it is natural to base our interpretation on considering redex-families as events, and to interpret (complete) family-reductions (contracting entire families as multi-steps) as configurations

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

of the corresponding PES. Indeed, reductions in optimal graph-implementations of orthogonal systems precisely correspond to family-reductions in the original system.

Recent advances in the abstract study of orthogonal rewrite systems [Sta89, GLM92, GK96, KG96, KG97] allow us to address the problem in an entirely abstract setting. Stable Deterministic Residual Structures (SDRSs) and Deterministic Family Structures (DFSs) model computation in orthogonal rewrite systems. DRSs are Abstract Rewrite Systems with an axiomatized residual relation; DFSs are DRSs where in addition the concept of redex-family is axiomatized. Stable DRSs allow [GK96, KG96] proofs of analogs of the Normalization and Standardization Theorems [Bar84]. In DFSs one can further prove Lévy’s Optimality Theorem [Lév80] and the Unique Families Lemma [GK96]. The latter states that any family can be contracted at most once in a family-reduction, and corresponds to the fact that any event may occur at most once in the course of a computation.

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

To view a process as the domain of all its configurations, an adequacy requirement is desirable. Namely, that runs of a (finite) configuration (i.e., all its possible sequentializations) should be in one-to-one correspondence with all reductions in the equivalence class which the configuration is supposed to represent. Because of the huge importance of permutation or Lévy equivalence [Lév80] to the whole theory of (not only orthogonal) rewrite systems [HL91, Bou85], and to concurrency theory as well [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, for example, a permutation-equivalence class of a (finite) reduction may have an infinite number of elements.

In order for an equivalence relation to satisfy the adequacy requirement, the corresponding equivalence classes of (finite) reductions must be partially ordered so as to form distributive lattices, since the domains of (finite) configurations of a PES ordered by inclusion are such lattices [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 [Lév80]. This problem, caused by erasure of redexes, is well discussed in [Lan94], 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 this problem. Laneve [Lan94] introduces distributive equivalence on β-reductions which only allows permutation of steps that cannot erase or duplicate one another, and consequently all equivalent sequences have the same length. Kennaway et al [KKSV93] 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 [CK96] work with permutation-equivalence and allow infinite reductions but restrict themselves to standard reductions only. 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 permutation-equivalence 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 numbers of events but still representing the same permutationequivalence 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, and therefore the former give a fully adequate semantics to ASDRSs.

2 Deterministic Residual and Family Structures

Let us first recall some basic theory for DRSs and DFSs developed in [GK96, KG96, KG97]. We start by introducing Abstract Reduction Systems [Hin69]. 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 axiomatize exactly the properties of residuals in orthogonal rewrite systems which are used in [Lév80, HL91] to define permutation equivalence on reductions, and the Lévy-embedding relation on permutation-equivalence classes, i.e., to construct 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. The most closely related models are Stark’s Determinate Concurrent Transition Systems [Sta89], where the residual relation is non-duplicating, and Abstract Reduction Systems of Gonthier et al. [GLM92], where in addition the nesting relation on redexes is axiomatized.

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

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

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

• [weak acyclicity] ([Sta89]) Let u, v ∈ t, u ≠ v, and u/v = ∅. Then v/u ≠ ∅. We call a DRS R stable (SDRS) if:

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

Non-duplicating stable DRSs will be called affine SDRSs, or ASDRSs.

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 above relations can equivalently be defined also using Klop’s method of commutative diagrams [Klo80, Bar84].

Definition 2.2 ([KG96]) • Let P : t → → o and u ∈ t, in a DRS. We call u erased in P if u/P = ∅. We call P external to u if it does not contract its residuals. 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.

• Let Q : t → → o, P : t → →^{P′} s → → e, and u ∈ s. We call u, or more precisely P′u, Q-(un)needed (resp. Q-(in)essential) if u is Q/P′-(un)needed (resp. (in)essential). We call P Q-needed if so is every redex contracted in P, and call standard if it is P -needed. The other concepts above are extended in the same way.

Definition 2.3 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] (Finite Family Developments) 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, if, for any redex P v, v cannot create two different redexes in the same family: if v creates w′, w′′ and w′ ≠ w′′, then F am((P + v)w′) ≠ F am((P + v)w′′).

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 ∅. By a reduction we mean a finite reduction. Reductions starting from ∅ will also be called initial reductions.

It is shown in [GK96] that every DFS is a stable DRS. DFSs model all known concepts of family relation [Lév78, Lév80, Klo80, KS89, Mar91, AL93, Oos96], and allow for an abstract proof [GK96] of the Optimality theorem [Lév80]. Further, we have shown in [KG97] that any ASDRS is in fact an affine ZDFS, AZDFS (i.e., for any ASDRS R, F_{R} = (R, ≃_{z}, ↪_{z}) is an AZDFS), and that F_{R} is the only separable DFS with R as the underlying SDRS. The proof of the above result is based on an abstract concept of extraction allowing to construct a canonical element P u in every family ϕ: P is standard and ∀P′u′ ∈ ϕ ∃P′′ : P′ ≈ P + P′′ ∧ u′ = u/P′′ (for any finite Q in an ASDRS, there is a standard reduction ST (Q) ≈ Q [KG96]). Further, it enables us to associate an AZDFS F_{I} to a DFS F, called the implementation of F. The reduction steps in F_{I} correspond to (complete) family-reduction multi-steps of F (i.e., multi-steps contracting maximal sets of redexes of some family).

Definition 2.4 Let F = (R, ≃, ↪) be a DFS. The Lévy implementation or simply implementation of F is the AZDFS F_{I} = (R_{I}, ≃_{I}, ↪_{I}), where

• the branches of the reduction graph of the underlying ARS A of R_{I} = (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 contracting U. Then V/U is the multi-step o → e contracting all members of the set V/U.

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

Theorem 2.5 ([KG97a]) For any DFS F, F_{I} is an AZDFS.

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 around as messages and therefore erased. Event Structures are linear in nature and consequently the configuration domains enjoy nice lattice properties; therefore Event Structures have been very successful in modelling linear process calculi (no actions can be erased or duplicated), such as CCS [Mil89]. However, any attempt to adequately interpret higher-order process languages in Event Structures would face the same erasure problems discussed in the introduction. As in the case of reductions, the aim of axiomatizing permutation equivalence on event configurations is to be able to equate configurations which differ only by irrelevant or inessential events.

A Prime Event Structure (PES) [Win86/89] 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}, 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 permutation-equivalence, 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’.

The next definition gives a translation between DPESs and DEESs:

Definition 3.3 (1) 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^{≥}⌉.

(2) 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 α.

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.2, a redex with history P v is Q-inessential iff v is Q/P -inessential.

The following theorem, which is proved using the DEES and DPES axioms, implies the correctness of Definition 3.3.

Theorem 3.4 (1) For any DEES C = (E, ≤, ⊳), P_{C} = (E, ≤, ≈_{⊳} ) is a DPES. (2) For any DPES P = (E, ≤, ≈), C_{P} = (E, ≤, ⊳_{≈}) is a DEES.

Further, the translations between DEESs and DPESs, in Definition 3.3, commute, implying the equivalence of the two event models:

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

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

4 Relating Conflict-Free 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.

Definition 4.1 To an AZDFS F = (R, ≃_{z}, ↪_{z}), 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 ϕ ↪_{z} ψ;

• α ≈ β iff ∀ϕ ∈ α ∪ β \ α ∩ β, ∃P : ∅ → → s : F AM(P) ⊆ α ∩ β and P discards a canonical element of ϕ, where F AM(P) denotes the set of families whose member redexes are contracted in P.

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

Theorem 4.2 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}}.

The following translation of DPESs and DEESs into ASDRSs resembles to the representation of events in a PES (E, ≤) as prime intervals of the configuration domain L(E) [Win86/89].

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

We show that R_{P} and R_{C} are ASDRSs, R_{P} = R_{C_{P}}, and R_{C} = R_{P_{C}}.

Let us call a left-closed enumeration (i.e., respecting the causality relation) e_{1}, …, e_{k} of a configuration α in a DEES a reduction, written [α], 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. Quasi-reductions are defined similarly in any DRS, as ‘reductions containing empty steps corresponding to erased redexes’.

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}), i.e., they correspond to reductions in C. As we will see below, not all left-closed enumerations of a configuration represent a reduction – they represent quasi-reductions.

Definition 4.4 To a DPES P = (E, ≤, ≈), we associate an affine DFS F_{P} = (R_{P}, ≃_{P}, ↪_{P}) as follows (where R_{P} is the DRSs defined in Definition 4.3):

• ≃_{P}-families are sets ϕ_{e} = {([α], e) | α + e ∈ L(P) ∧ (⟨α⟩_{L}, e) ≠ ∅}, for any e ∈ E.

• ↪_{P} is defined 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.4: F_{P} is an AZDFS.

For any of the four models, there is an obvious concept of isomorphism, ⇀ ↽. The following theorem, combined with the results of previous sections, implies equivalence of the considered four transition and event models.

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

(2) For any AZDFS F, F ⇀ ↽ F_{P_{F}}.

5 Configuration Domains

Note that, unlike PESs, not every configuration α in a DEES has a reduction. For example, consider the DEES consisting of four events {e_{1}, e_{2}, e′_{1}, e′_{2}}, ordered as follows: e_{1} < e′_{1} and e_{2} < e′_{2}, and let ⊳ be given by: α ⊳ e′_{1} iff e_{2} ∈ α, and α ⊳ e′_{2} iff e_{1} ∈ α. Then {e_{1}, e_{2}, e′_{1}, e′_{2}} is a configuration, but any of its 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). However, it is easy to see that, for any α ∈ L(C), in a DEES C, any left-closed enumeration of ST (α) is a reduction.

Definition 5.1 (1) Let P be a DPES. Then L^{≈}(P) = L(P)/_{≈} = {⟨α⟩_{L} | α ∈ L(P)} and L^{⊴} (P) = (L^{≈}(P), ⊴), where ⊴ is a partial order defined by: ⟨α⟩_{L} ⊴ ⟨β⟩_{L} iff ∃α′ ∈ ⟨α⟩_{L}, ∃β′ ∈ ⟨β⟩_{L} : α′ ⊆ β′.

(2) Let R be an ASDRS. Then 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 Lévy-equivalence class of P, and L^{⊴} (R) = (L^{≈}(R), ⊴), where ⊴ is Lévy’s embedding relation.

It has been shown in [KG97] that P ⊴ Q iff F AM(P) ⊆ F AM(Q′) for some Q′ ≈ Q, implying that ⟨P ⟩_{L} ⊴ ⟨Q⟩_{L} in an ASDRS R iff ⟨F AM(P)⟩_{L} ⊴ ⟨F AM(Q)⟩_{L} in P_{F_{R}}. Therefore Theorem 5.2 Let R be an ASDRS and let P = P_{F_{R}} be its corresponding DPES. Then f : ⟨P ⟩_{L} → ⟨F AM(P)⟩_{L} is an isomorphism between L^{⊴} (R) and L^{⊴} (P). Moreover, (quasi-)reductions in ⟨P ⟩_{L} are in one-to-one correspondence with these in ⟨F AM(P)⟩_{L}.

Note that L^{⊴} (P) is not a lattice since L^{⊴} (R) is not. However, depending on the set of ‘results’ we are interested in, one can construct a (distributive) lattice on configurations in P reflecting growth of information relative to that goal. Construction of such ‘relativized’ information domains will be addressed in a separate paper.

6 Conclusions

We have established an equivalence between deterministic stable operational (ASDRS) and domain-theoretic (DPES/DEES) models of computation, and based on this, constructed a fully adequate event style concurrent semantics for orthogonal rewrite systems. The correspondence between Event Structures and other models of concurrency is well studied [Win86/89, WN95], and we hope that our results contribute to better understanding of the relationship between operational and denotational semantics of sequential and concurrent languages. Further, we think that our axiomatization of permutation equivalence is interesting on its own right from the poset/lattice theoretic point of view.

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

Acknowledgments We thank Richard Kennaway and Fer-Jan de Vries 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. 1984.

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

[CK96] Clark D., Kennaway R. Event structures and non-orthogonal term graph rewriting. MSCS 6:545-578, 1996.

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

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

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

[Hin69] Hindley R.J. An abstract form of the Church-Rosser theorem. 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, p. 394-443, 1991.

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

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

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

[KG97a] Khasidashvili Z., Glauert J.R.W. An abstract concept of optimal implementation. Report SYS-C97-??, UEA, Norwich, 1997.

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

[Lan94] Laneve C. Distributive evaluations of λ-calculus, Fundamenta Informaticae, 20(4):333 – 352, 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 Lambda-calculus. In: To H. B. Curry:

Essays on Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.

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

[Mil89] Milner R. Communication and concurrency. Prentice Hall, 1989.

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

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

[San93] Sangiorgi D. Expressing mobility in process algebras: first-order and higherorder 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.

[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. Full version: Cambr. Univ. Comp. Lab. Report n. 95, 1986.

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

This article was processed using the L^{A}TEX macro package with LLNCS style