Domains and Event Structures for Fusions

TL;DR

This paper extends the theory of event structures to include 'fusion' phenomena by introducing weak prime domains and connected event structures, enabling semantics for non-linear graph rewriting systems with merging steps.

Contribution

It introduces weak prime domains and connected event structures, generalizing stable event structures to handle fusion in concurrent computations.

Findings

Connected event structures correspond to semantics of non-linear graph rewriting.

Weak prime domains generalize prime algebraic domains for fusion scenarios.

Category of unstable event structures coreflects into weak prime domains.

Abstract

Stable event structures, and their duality with prime algebraic domains arising as partial orders of configurations, are a landmark of concurrency theory, providing a clear characterisation of causality in computations. They have been used for defining a concurrent semantics of several formalisms, from Petri nets to (linear) graph rewriting systems, which in turn lay at the basis of many visual modelling frameworks. Stability however is restrictive when dealing with formalisms with "fusion", i.e., where a computational step can not only consume and produce but also merge parts of the state. This happens, e.g., for graph rewriting systems with non-linear rules, which are needed to cover some relevant applications (such as the graphical encoding of calculi with name passing). Guided by the need of capturing the semantics of formalisms with fusion we leave aside stability and we characterise, as a natural generalisation of prime algebraic domains, a class of domains, referred to as weak prime domains. We then identify a corresponding class of event structures, that we call connected event structures, via a duality result formalised as an equivalence of categories. We show that connected event structures are exactly the class of event structures that arise as the semantics of non-linear graph rewriting systems. Interestingly, the category of general unstable event structures coreflects into our category of weak prime domains, so that our result provides a characterisation of the partial orders of configurations of such event structures.

Equations

$$f(d_1\sqcap d_1^{\prime })=$$

$$=f((e_1\sqcap d_1^{\prime })\bigsqcup (f_1\sqcap d_1^{\prime }))$$

$$\bigsqcup$$

$$=f(e_1\sqcap d_1^{\prime })\bigsqcup f(f_1\sqcap d_1^{\prime })$$

$$=(f(e_1)\sqcap f(d_1^{\prime }))\bigsqcup (f(f_1)\sqcap f(d_1^{\prime }))$$

$$=(f(e_1)\bigsqcup f(f_1))\sqcap f(d_1^{\prime })$$

$$\bigsqcup$$

$$=f(e_1\bigsqcup f_1)\sqcap f(d_1^{\prime })=$$

$$=f(d_1)\sqcap f(d_1^{\prime })$$

$$p(d_1)=d_1\sqcap (p(d_1)\bigsqcup d_1^{\prime })$$

$$f(d_1\sqcap d_1^{\prime })=$$

$$=f(p(d_1)\sqcap d_1^{\prime })$$

$$=f(p(d_1))\sqcap f(d_1^{\prime })$$

$$=f(d_1\sqcap (p(d_1)\bigsqcup d_1^{\prime }))\sqcap f(d_1^{\prime })$$

$$=f(d_1)\sqcap f(p(d_1)\bigsqcup d_1^{\prime }))\sqcap f(d_1^{\prime })$$

$$\bigsqcup$$

$$=f(d_1)\sqcap f(d_1^{\prime })$$

$$⨆X^{\prime }=⨆X\cup \{i\}=⨆X\cup \{i^{\prime }\}=⨆X.$$

$$⨆X=⨆X^{\prime }\cup \{i\}=⨆X^{\prime }\cup \{i^{\prime }\}=⨆X^{\prime }.$$

$$f(p(i_1))\bigsqcup i_2=f(i_1)f(p(i_1^{\prime }))\bigsqcup i_2^{\prime }=f(i_1^{\prime })$$

$$[ir(i_2)\setminus \{i_2\}{]}_{{\leftrightarrow }^{\ast }}=[ir(p(i_2)){]}_{{\leftrightarrow }^{\ast }}\subseteq \mathcal{E}(f)(C_1)$$

$$[ir(f(p(i_1^{\prime }))){]}_{{\leftrightarrow }^{\ast }}\subseteq \mathcal{E}(f)(C_1)$$

$$[ir(p(i_1^{\prime })){]}_{{\leftrightarrow }^{\ast }}=[\{j_1^{\prime 1},\dots ,j_1^{\prime m}\}{]}_{{\leftrightarrow }^{\ast }}$$

$$[ir(f(p(i_1^{\prime }))){]}_{{\leftrightarrow }^{\ast }}=\mathcal{E}(f)([ir(p(i_1^{\prime })){]}_{{\leftrightarrow }^{\ast }}).$$

$$y_1{y}_{2}z\simeq y_1^{\prime }{y}_2^{\prime }z$$

$$L\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$p_i:$$

$$L_1\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$I_e\cup (\bigcup _{\begin{array}{c}{e}^{\prime }\in E\\ e\#e^{\prime }\end{array}}{C}_{e,e^{\prime }})\cup (\bigcup _{e^{\prime }\in E}(S_{e^{\prime }}\uplus \underset{\begin{array}{c}{u}^{\prime }\in U_{e^{\prime }}\\ e\in u^{\prime }\end{array}}{⨄}{L}_{u^{\prime },e^{\prime }}))\cup (S_e\cup \bigcup _{u\in U_e}{L}_{u,e})$$

$$(S_e\cup \bigcup _{u\in U_e}{L}_{u,e})\cup (\bigcup _{e^{\prime }\in E}(S_{e^{\prime }}\cup \bigcup _{\begin{array}{c}{u}^{\prime }\in U_{e^{\prime }}\\ e\in u^{\prime }\end{array}}{L}_{u^{\prime },e^{\prime }}))$$

$$G_s=(\bigcup _{e\#e^{\prime }}{C}_{e,e^{\prime }})\cup \bigcup _{e\in E}(I_e\cup S_e\uplus \underset{u\in U_e}{⨄}{L}_{u,e})$$

$$T=(\bigcup _{e\#e^{\prime }}{C}_{e,e^{\prime }})\cup \bigcup _{e\in E}(I_e\cup S_e\cup \bigcup _{u\in U_e}{L}_{u,e})$$

$$L\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

Full text

I Introduction

For a long time stable/prime event structures and their duality with prime algebraic domains have been considered one of the landmarks of concurrency theory, providing a clear characterisation of causality in software systems. They have been used to provide a concurrent semantics to a wide range of foundational formalisms, from Petri nets [1] to linear graph rewriting systems [2, 3, 4] and process calculi [5, 6, 7]. They are one of the standard tools for the formal treatment of (true, i.e., non-interleaving) concurrency. See, e.g., [8] for a reasoned survey on the use of such causal models. Recently, they have been used in the study of concurrency in weak memory models [9, 10, 11] and for process mining and differencing [12].

In order to endow a chosen formalism with an event structure semantics, a standard construction consists in viewing the class of computations as a partial order. An element of the order is some sort of configuration, i.e., an execution trace up to an equivalence that identifies traces differing only for the order of independent steps (e.g., interchange law [13] in term rewriting, shift equivalence [14] in graph rewriting or permutation equivalence [15] in $\lambda$-calculus), and the order relates two computations when the latter is an extension of the former. Events are then identified with configurations consisting of a maximal computation step (e.g., a transition of a CCS process or a firing for a Petri net) with all its causes. As a simple example, consider the CCS process $a.c\mid b$. The corresponding transition system is depicted in Fig. 1(a). We can identify the states of the computation with the sets of actions executed and obtain the partial order depicted in Fig. 1(b). The fact that each computation step in a configuration has a uniquely determined set of causes, a property that for event structures is called stability, allows one to characterise such elements, order theoretically, as the prime elements: if they are included in a join they must be included in one of the elements that are joined. For example, in Fig. 1(b), the events correspond to configurations $\{a\}$ (transition $a$ with empty set of causes), $\{a,c\}$ (transition $c$ caused by $a$) and $\{b\}$ (transition $b$ with empty set of causes). Each element of the partial order of configurations can be reconstructed uniquely as the join of the primes under it, so that the partial order is prime algebraic. This duality between event structures and domains of configurations can be nicely formalised in terms of an equivalence between the categories of prime event structures and prime algebraic domains [1, 16].

The set up described so far fails when moving to formalisms where a computational step can merge parts of the state. This happens, e.g., in nominal calculi where, as a result of name passing, the received name is identified with a local one at the receiver [17, 18] or in the modelling of bonding in biological/chemical processes [19]. Whenever we think of the state of the system as some kind of graph with the dynamics described by graph rewriting, this means that rewriting rules are non-linear (more precisely, in the jargon of the double pushout approach [20], left-linear but possibly not right-linear). In general terms, the point is that, in the presence of fusions, the same event can be enabled by different minimal sets of events, thus preventing the identification of a proper notion of causality.

As an example, consider the graph rewriting system in Fig. 2. The start graph $G_{s}$ and the rewriting rules $p_{a}$, $p_{b}$, and $p_{c}$ are reported in Fig. 2(a). Observe that rules $p_{y}$, where $y$ can be either $a$ or $b$, delete edge $\bar{y}$ and merge nodes $c$ and $\nu$. The possible rewrites are depicted in Fig. 2(b). For instance, applying $p_{a}$ to $G_{s}$ we get the graph $G_{b}$. Now, $p_{b}$ can still be applied to $G_{b}$ matching its left-hand side non-injectively, thus getting graph $G_{ab}$. Similarly, we can apply first $p_{b}$ and then $p_{a}$, obtaining again $G_{ab}$. Observe that at least one between $p_{a}$ and $p_{b}$ must be applied to enable $p_{c}$, since the latter rule requires nodes $c$ and $\nu$ to be merged. Note also that in a situation where all the three rules $p_{a}$, $p_{b}$, and $p_{c}$ are applied, since $p_{a}$ and $p_{b}$ are independent, it is not possible to define a proper notion of causality. We only know that at least one between $p_{a}$ and $p_{b}$ must be applied before $p_{c}$. The corresponding domain of configurations, reported in Fig. 2(c), is naturally derived from the possible rewrites in Fig. 2(b).

The graph rewriting system of Fig. 2(a) is a (simplified) representation of the $\pi$-calculus process $(\nu c)(\bar{a}(c)\mid\bar{b}(c)\mid c())$. Rules $p_{y}$, for $y\in\{a,b\}$, represent the execution of $\bar{y}(c)$ that outputs on channel $y$ the restricted name $c$. The first rule that is executed extrudes name $c$, while the second is just a standard output. The name $c$ is available outside the scope only after the extrusion, and after that the input prefix $c()$ can be consumed. Figure 3 shows the possible transitions of the process, which correspond one-to-one to the possible rewrites of Fig. 2(b).

The impossibility of modelling these situations with stable event structures is well-known (see, e.g., [16] for a general discussion, [2] for graph rewriting systems or [17] for the $\pi$-calculus). One has to drop the stability requirement and replace causality by an enabling relation $\vdash$. More precisely, in the specific case we would have $\emptyset\vdash a$, $\emptyset\vdash b$, $\{a\}\vdash c$, $\{b\}\vdash c$.

The questions that we try to answer is: what can be retained of the duality between events structures and domains, when dealing with formalisms with fusions? Which are the properties of the domain of computations that arise in this setting? What are the event structure counterparts?

The domain of configurations of the example suggests that in this context an event is still a computation that cannot be decomposed as the join of other computations. Hence, in order theoretical terms, it is an irreducible. However, due to unstability, irreducibles are not necessarily primes: two different irreducibles can represent the same computation step with different minimal enablings, in a way that an irreducible can be included in a computation that is the join of two computations without being included in any of the two. For instance, in the example above, $\{a,c\}$ is an irreducible, corresponding to the execution of $c$ enabled by $a$, and it is included in $\{a\}\sqcup\{b,c\}=\{a,b,c\}$, although neither $\{a,c\}\subseteq\{a\}$ nor $\{a,c\}\subseteq\{b,c\}$. Uniqueness of decomposition of an element in terms of (downward closed sets of) irreducibles also fails, e.g., $\{a,b,c\}=\{a\}\sqcup\{b\}\sqcup\{a,c\}=\{a\}\sqcup\{b\}\sqcup\{b,c\}$: the irreducibles $\{a,c\}$ and $\{b,c\}$ can be used interchangeably in the decomposition of $\{a,b,c\}$.

Building on the previous observation, we introduce an equivalence on irreducibles identifying those that can be used interchangeably in the decompositions of an element (intuitively, different minimal enablings of the same computation step). This is used to define a weaker notion of primality (up to interchangeability) that allows us to characterise the class of domains suited for modelling the semantics of formalisms with fusions as the class of weak prime algebraic domains.

Given a weak prime algebraic domain, a corresponding event structure can be obtained by taking as events the set of irreducibles, quotiented under the (transitive closure of the) interchangeability relation. The resulting class of event structures is a (mild) restriction of the general event structures in [16] that we call connected event structures. Categorically, we get an equivalence between the category of weak prime algebraic domains and the one of connected event structures, generalising the equivalence between prime algebraic domains and prime event structures.

We also show that, in the same way as prime algebraic domains/prime event structures are exactly what is needed for Petri nets/linear graph rewriting systems, weak prime algebraic domains/connected event structures are exactly what is needed for non-linear graph rewriting systems: each rewriting system maps to a connected event structure and conversely each connected event structure arises as the semantics of some rewriting system. This supports the adequateness of weak prime algebraic domains and connected event structures as semantics structures for formalisms with fusions.

Interestingly, we can also show that the category of general event structures [16] coreflects into our category of weak prime algebraic domains. Therefore our notion of weak prime algebraic domain can be seen as a novel characterisation of the partial order of configurations of such event structures that is alternative to those based on intervals in [21, 22]. It represents a natural generalisation of the one for prime event structures, with irreducibles (instead of primes) having a tight connection with events. The correspondence is established, at a categorical level, as a coreflection of categories: to the best of our knowledge, this has not been done before in the literature.

As mentioned above, weak prime domains, corresponding to possibly unstable event structures, satisfy the same conditions as prime domains, corresponding to stable event structures, up to an equivalence on irreducibles. This suggests the possibility of viewing unstable event structures as stable ones up to an equivalence on events. We show how this can be formalised with a set up closely related to the framework of prime event structures with equivalence recently devised in [23, 24].

Event structures and their domains have been also studied in relation with automata with concurrency [25, 26], a form of automata endowed with a concurrency relation on transitions (local to each state). On a similar line, the transition graphs of prime event structures have been given a characterisation in terms of local axioms in [27], answering a question posed in [28]. Recently, in connection with the abstract theory of rewriting and concurrent games, a slightly different but equivalent characterisation has been rediscovered in [29], where prime event structures are shown to correspond exactly to a suitable class of asynchronous graphs. Roughly, an asynchronous graph is a transition system where some squares are declared to commute, meaning that the coinitial edges of the square are concurrent and each one can follow the other. Asynchronous graphs correspond to prime event structures that satisfy the cube axiom, consisting of two parts: the forward and the backward cube axioms, the latter often referred to as the stability axiom. We show that asynchronous graphs that verify only the forward part of the cube axiom are exactly the transition systems of weak prime domains.

The rest of the paper is structured as follows. In Section II we recall the basics of (prime) event structures and their correspondence with prime algebraic domains. In Section III we introduce weak prime algebraic domains and connected event structures, and we characterise their relation categorically. In Section IV we present a characterisation of our proposal in terms of a formalism reminiscent of prime event structures with equivalence of [23, 24]. We also discuss and formalise the relation of our work with alternative characterisations of the domains of event structures based on intervals and on asynchronous graphs. In Section V we show the intimate connection between weak prime algebraic domains (or equivalently, connected event structures) and non-linear graph rewriting systems. Finally, in Section VI we wrap up the main contributions of the paper and we sketch further advances and some connections with related works.

The paper is rounded up with an appendix extending our characterisation results to event structures with non-binary conflict [22]. We also discuss the relation with a proposal based on labelled event structures for modelling the concurrent computations of name passing process calculi [17].

This is a revised and extended version of the conference paper [30].

II Background: Domains and Event Structures

In this section we review the basics of event structures, as introduced in [16], and their duality with partial orders.

II-A Event Structures

For the sake of presentation, we focus on event structures with binary conflict. Most results can be easily rephrased for event structures with non-binary conflict expressed by means of a consistency predicate (This is explicitly discussed in Appendix -A). Given a set $X$ we denote by $\mathbf{2}^{X}$ and $\mathbf{2}_{\mathit{fin}}^{X}$ the powerset and the set of finite subsets of $X$, respectively. For $m,n\in\mathbb{N}$, we denote by $[{m},{n}]$ the set $\{m,m+1,\ldots,n\}$.

Definition 1** (event structure)**

An event structure (es for short) is a tuple $\langle E,\vdash,\#\rangle$ such that

• •

$E$ is a set of events;

• •

${\vdash}\subseteq\mathbf{2}_{\mathit{fin}}^{E}\times E$ is the enabling relation, satisfying $X\vdash e$ and $X\subseteq Y$ implies $Y\vdash e$;

• •

$\#\subseteq E\times E$ is the conflict relation.

A subset $X\subseteq E$ is consistent if $\neg(e\#e^{\prime})$ for all $e,e^{\prime}\in X$. □

An es $\langle E,\vdash,\#\rangle$ is often denoted simply by $E$. Computations are captured by the notion of configuration.

Definition 2** (configuration, live event structure)**

Let $\langle E,\vdash,\#\rangle$ be an es. A configuration of $E$ is a consistent subset $C\subseteq E$ that is secured, i.e., such that for all $e\in C$ there are $e_{1},\ldots,e_{n}\in C$ with $e_{n}=e$ such that $\{e_{1},\ldots,e_{k-1}\}\vdash e_{k}$ for all $k\in[{1},{n}]$ (in particular, $\emptyset\vdash e_{1}$). The set of configurations of an es $E$ is denoted by $\mathit{Conf}({E})$ and the subset of finite configurations by $\mathit{Conf_{F}}({E})$. An es is live if conflict is saturated, i.e., for all $e,e^{\prime}\in E$, if there is no $C\in\mathit{Conf}({E})$ such that $\{e,e^{\prime}\}\subseteq C$ then $e\#e^{\prime}$, and moreover for all $e\in E$ it holds $\neg(e\#e)$. □

Remark 1

In live es, the fact that conflict is saturated corresponds to inheritance of conflict in prime event structures. Moreover, the absence of self-conflicts implies that each event appears in some configuration (intuitively, it is executable). In the rest of the paper, we restrict to live es, hence the qualification “live” is omitted. □

In this setting, two events are concurrent when they are consistent and enabled by the same configuration.

Since the enabling predicate is over finite sets of events, we can consider minimal sets of events enabling a given one.

Definition 3** (minimal enabling)**

Let $\langle E,\vdash,\#\rangle$ be an es. Given a configuration $C\in\mathit{Conf}({{E}})$ and an event $e\in E$ we write $C\vdash_{0}e$ and call it a minimal enabling for $e$, when $C\cup\{e\}\in\mathit{Conf}({E})$ (hence $C\cup\{e\}$ consistent and $C\vdash e$), and for any other configuration $C^{\prime}\subseteq C$, if $C^{\prime}\vdash e$ then $C^{\prime}=C$. □

The classes of stable and prime es represent our starting point and play an important role in the paper.

Definition 4** (stable and prime event structures)**

An es $\langle E,\vdash,\#\rangle$ is stable if $X\vdash e$, $Y\vdash e$, and $X\cup Y\cup\{e\}$ consistent imply $X\cap Y\vdash e$. It is prime if $X\vdash e$ and $Y\vdash e$ imply $X\cap Y\vdash e$. □

For stable es, given a configuration $C$ and an event $e\in C$, there is a unique minimal configuration $C^{\prime}\subseteq C$ such that $C^{\prime}\vdash_{0}e$. The set $C^{\prime}$ can be seen as the set of causes of the event $e$ in the configuration $C$. This gives a well-defined notion of causality that is local to each configuration. In a prime es, for any event $e$ there is a unique minimal enabling $C\vdash_{0}e$, thus providing a global notion of causality. In general, in possibly unstable es, due to the presence of consistent or-enablings, there might be distinct minimal enablings in the same configuration.

Example 1

A simple example of unstable es is the one associated with the running example discussed in the introduction (see Fig. 2). The set of events is $\{a,b,c\}$, the conflict relation $\#$ is the empty one and the minimal enablings are $\emptyset\vdash_{0}a$, $\emptyset\vdash_{0}b$, $\{a\}\vdash_{0}c$, and $\{b\}\vdash_{0}c$. Thus, event $c$ has two minimal enablings and these are consistent, hence $\{a,b\}\vdash c$. The corresponding configurations are reported in Fig. 2(c). □

The class of es can be turned into a category.

Definition 5** (category of event structures)**

A morphism of es $f:{E}_{1}\to{E}_{2}$ is a partial function $f:E_{1}\to E_{2}$ such that for all $C_{1}\in\mathit{Conf}({E_{1}})$ and $e_{1},e_{1}^{\prime}\in E_{1}$ with $f(e_{1})$, $f(e_{1}^{\prime})$ defined

• •

if $f(e_{1})\#f(e_{1}^{\prime})$ then $e_{1}\#e_{1}^{\prime}$;

• •

if $f(e_{1})=f(e_{1}^{\prime})$ then $e_{1}=e_{1}^{\prime}$ or $e_{1}\#e_{1}^{\prime}$;

• •

if $C_{1}\vdash_{1}e_{1}$ then $f(C_{1})\vdash_{2}f(e_{1})$.

We denote by $\mathsf{ES}$ the category of es and their morphisms and by $\mathsf{sES}$ and $\mathsf{pES}$, respectively, the full subcategories of stable and prime es. □

II-B Domains

A preordered or partially ordered set $\langle D,\sqsubseteq\rangle$ is often denoted simply as $D$, omitting the (pre)order relation. We denote by $\preceq$ the immediate predecessor relation, i.e., for $x,y\in D$, we write $x\preceq y$ whenever $x\sqsubseteq y$ and for all $z\in D$ if $x\sqsubseteq z\sqsubseteq y$ then $z\in\{x,y\}$. A subset $X\subseteq D$ is consistent if it has an upper bound $d\in D$ (i.e., $x\sqsubseteq d$ for all $x\in X$), while it is pairwise consistent if every two elements subset of $X$ is consistent. A subset $X\subseteq D$ is directed if $X\neq\emptyset$ and every pair of elements in $X$ has an upper bound in $X$. We say that $D$ is complete if every directed subset has a least upper bound in $D$.

A subset $X\subseteq D$ is an ideal if it is directed and downward closed. Given an element $x\in D$, we write $\mathop{\downarrow\!{x}}$ to denote the principal ideal $\{y\in D\mid y\sqsubseteq x\}$ generated by $x$. Given a partial order $D$, its ideal completion, denoted by $\mathsf{Idl}({D})$, is the set of ideals of $D$, ordered by subset inclusion. The least upper bound and the greatest lower bound of a subset $X\subseteq D$ (if they exist) are denoted by $\bigsqcup X$ and $\bigsqcap X$, respectively.

Definition 6** (domains)**

A partial order $D$ is coherent if for all pairwise consistent $X\subseteq D$ the least upper bound $\bigsqcup X$ exists. An element $d\in D$ is compact if for all directed $X\subseteq D$, $d\sqsubseteq\bigsqcup X$ implies $d\sqsubseteq x$ for some $x\in X$. The set of compact elements of $D$ is denoted by $\mathop{\mathsf{K}({D})}$. A coherent partial order $D$ is algebraic if for every $x\in D$ we have $x=\bigsqcup(\mathop{\downarrow\!{x}}\cap\mathop{\mathsf{K}({D})})$. We say that $D$ is finitary if for every element $a\in\mathop{\mathsf{K}({D})}$ the set $\mathop{\downarrow\!{a}}$ is finite. We refer to algebraic finitary coherent partially ordered sets as domains. □

Note that every domain has a bottom element (indeed $\bot=\bigsqcup\emptyset$), and that in a domain all non-empty subsets have a meet. In fact, if $\emptyset\neq X\subseteq D$, then $\bigsqcap X=\bigsqcup L(X)$ where $L(X)=\{y\mid\forall x\in X.\,y\sqsubseteq x\}$ is the set of lowerbounds of $X$, which is pairwise consistent since it is dominated by any $x\in X$. And it is easy to see that finite joins of compact elements are compact.

For a domain $D$ we can think of its elements as “pieces of information” expressing the states of evolution of a process. Compact elements represent states that are reached after a finite number of steps. Thus algebraicity essentially says that infinite computations can be approximated with arbitrary precision by finite ones. More formally, when $D$ is algebraic, it is determined by $\mathop{\mathsf{K}({D})}$, i.e., $D\simeq\mathsf{Idl}({\mathop{\mathsf{K}({D})}})$.

For an es, the configurations ordered by subset inclusion form a domain. When the es is stable, if a minimal enabling is included in the join of different configurations, then it is necessarily included in one of the configurations. In order-theoretic terms, minimal enablings are prime elements, and thus they represent the building blocks of computations.

Definition 7** (primes and prime algebraicity)**

Let $D$ be a domain. A complete prime is an element $p\in D$ such that for any pairwise consistent $X\subseteq D$, if $p\sqsubseteq\bigsqcup X$ then $p\sqsubseteq x$ for some $x\in X$. The set of complete prime elements of $D$ is denoted by $\mathop{\mathit{pr}({D})}$. The domain $D$ is prime algebraic (or simply prime) if for all $x\in D$ we have $x=\bigsqcup(\mathop{\downarrow\!{x}}\cap\mathop{\mathit{pr}({D})})$. □

Prime domains can be also characterised as coherent finitary distributive complete partial orders [16]. Note that complete primes are compact (since each directed set is pairwise consistent). Since we will only use complete primes, the qualification “complete” will be omitted.

Prime domains are the domain theoretical counterpart of stable and prime es. For a stable es $\langle E,\#,\vdash\rangle$, the partial order $\langle\mathit{Conf}({{E}}),\subseteq\rangle$ is a prime domain, denoted $\mathcal{D}_{S}({{E}})$. Conversely, given a prime domain $D$, the triple $\langle\mathop{\mathit{pr}({D})},\#,\vdash\rangle$, where $p\#p^{\prime}$ if $\{p,p^{\prime}\}$ is not consistent and $X\vdash p$ when $(\mathop{\downarrow\!{p}}\cap\mathop{\mathit{pr}({D})})\setminus\{p\}\subseteq X$, is a prime es, denoted $\mathcal{E}_{S}({D})$.

This correspondence can be elegantly formulated at the categorical level [16]. We recall the notion of domain morphism.

Definition 8** (category of prime domains)**

Let $D_{1}$, $D_{2}$ be prime domains. A morphism $f:D_{1}\to D_{2}$ is a total function such that for all consistent $X_{1}\subseteq D_{1}$ and $d_{1},d_{1}^{\prime}\in D_{1}$

if $d_{1}\preceq d_{1}^{\prime}$ then $f(d_{1})\preceq f(d_{1}^{\prime})$; 2. 2.

$f(\bigsqcup X_{1})=\bigsqcup f(X_{1})$; 3. 3.

if $X_{1}\neq\emptyset$ then $f(\bigsqcap X_{1})=\bigsqcap f(X_{1})$;

We denote by $\mathsf{pDom}$ the category of prime domains and their morphisms. □

The correspondence is then captured by the result below.

Theorem 1** (duality)**

There are functors $\mathcal{D}_{S}:\mathsf{sES}\to\mathsf{pDom}$ and $\mathcal{E}_{S}:\mathsf{pDom}\to\mathsf{sES}$ establishing a coreflection. It restricts to an equivalence of categories between $\mathsf{pDom}$ and $\mathsf{pES}$. □

III Weak Prime Domains and Connected Event Structures

In this section we show that, relaxing the stability assumption, we can generalise the duality result described in the previous section, linking suitably defined classes of domains and es. These can be proven to properly capture the semantics of computational formalisms with fusions.

III-A Weak Prime Algebraic Domains

We show that domains arising in absence of stability can be characterised by resorting to a weakened notion of prime element. We start recalling the notion of irreducible element.

Definition 9** (irreducibles)**

Let $D$ be a domain. A complete irreducible of $D$ is an element $x\in D$ such that, for any pairwise consistent $X\subseteq D$, if $x=\bigsqcup X$ then $x\in X$. The set of complete irreducibles of $D$ is denoted by $\mathop{\mathit{ir}({D})}$ and, for $d\in D$, we define $\mathop{\mathit{ir}({d})}=\mathop{\downarrow\!{d}}\cap\mathop{\mathit{ir}({D})}$. □

Observe that complete irreducibles in a domain are compact. In fact, if $i$ is a complete irreducible, by algebraicity, $i=\bigsqcup\mathop{\downarrow\!{i}}\cap\mathop{\mathsf{K}({D})}$ whence $i\in\mathop{\downarrow\!{i}}\cap\mathop{\mathsf{K}({D})}$. Conversely, we have the following.

Lemma 1** (irreducibility and compactness)**

Let $D$ be a domain. If $d\in\mathop{\mathsf{K}({D})}$ then $d$ is a complete irreducible iff for all $x,y\in D$, consistent, $d=x\sqcup y$ implies $d=x$ or $d=y$. □

Proof

Let $d\in\mathop{\mathsf{K}({D})}$. Assume that for all $x,y\in D$, consistent, $d=x\sqcup y$ implies $d=x$ or $d=y$. Assume that $d=\bigsqcup X$ for some pairwise consistent $X$. It is easy to see that $X^{\prime}=\{\bigsqcup Y\mid Y\in\mathbf{2}_{\mathit{fin}}^{X}\}$ is directed and moreover $\bigsqcup X^{\prime}=\bigsqcup X=d$. Since $d$ is compact, there is $x^{\prime}\in X^{\prime}$ such that $d\sqsubseteq x^{\prime}$, hence $d=x^{\prime}$. By definition of $X^{\prime}$, this means that there exists $Y\in\mathbf{2}_{\mathit{fin}}^{X}$ such that $d=\bigsqcup Y$. Now, using the hypothesis, an inductive reasoning allows us to conclude that $d\in Y\subseteq X$, as desired.

The converse implication is trivial: if $d\in\mathop{\mathit{ir}({D})}$ and $d\sqsubseteq x\sqcup y$ then, by definition of complete irreducible, $d\in\{x,y\}$, i.e., either $d=x$ or $d=y$, as desired. ■

Since in this paper we will refer only to complete irreducibles, the qualification “complete” will be omitted.

Irreducibles in domains have a simple characterisation.

Lemma 2** (unique predecessor for irreducibles)**

Let $D$ be a domain and $i\in D$. Then $i\in\mathop{\mathit{ir}({D})}$ iff it has a unique immediate predecessor. □

Proof

Assume that $i\in D$ has a unique immediate predecessor $d\prec i$, and let $X\subseteq D$ be pairwise consistent and such that $i=\bigsqcup X$. Hence for any $x\in X$ we have $x\sqsubseteq i$. Assume by contradiction that $i\not\in X$. This implies that for all elements $x\in X$ we have $x\sqsubseteq d$, and therefore $i=\bigsqcup X\sqsubseteq d\prec i$, which is a contradiction. Hence it must be $i\in X$, which means that $i$ is irreducible.

Vice versa, let $i$ be irreducible and let $d_{1},d_{2}\prec i$ be immediate predecessors. Since $D$ is a domain and $\{d_{1},d_{2}\}$ is consistent, we can take $d=d_{1}\sqcup d_{2}$ and we know $d_{1}\sqsubseteq d\sqsubseteq i$. Since $i$ is irreducible it cannot be $d=i$, therefore $d=d_{1}$ and thus $d_{1}=d_{2}$. Thus we conclude that $i$ has a unique immediate predecessor. ■

The unique predecessor of an irreducible will play an important role, hence we introduce a notation.

Definition 10** (immediate predecessor)**

Let $D$ be a domain and $i\in\mathop{\mathit{ir}({D})}$. We denote by $\mathit{p}({i})$ the (unique) immediate predecessor of $i$. □

We next observe that any domain is actually irreducible algebraic, namely it can be generated by the irreducibles.

Proposition 1** (domains are irreducible algebraic)**

Let $D$ be a domain. Then for any $d\in D$ it holds $d=\bigsqcup\mathop{\mathit{ir}({d})}$. □

Proof

We first prove that for any compact element $d\in\mathop{\mathsf{K}({D})}$ it holds that $d=\bigsqcup(\mathop{\downarrow\!{d}}\cap\mathop{\mathit{ir}({D})})$. The thesis then immediately follows from algebraicity of $D$. Since $D$ is a domain, $\mathop{\downarrow\!{d}}$ is finite, hence we can proceed by induction on $|\mathop{\downarrow\!{d}}|$. When $|\mathop{\downarrow\!{d}}|=1$, we have that $d=\bot$, hence $\mathop{\downarrow\!{d}}\cap\mathop{\mathit{ir}({D})}=\emptyset$ and indeed $\bot=\bigsqcup\emptyset$. When $|\mathop{\downarrow\!{d}}|=k>1$ consider the immediate predecessors of $d$ and denote them $d_{1},\ldots,d_{n}\prec d$. Since $D$ is a domain and $\{d_{1},\ldots,d_{n}\}$ is consistent, there exists $\bigsqcup\{d_{1},\ldots,d_{n}\}=d^{\prime}$ and $d_{i}\sqsubseteq d^{\prime}\sqsubseteq d$. There are two cases

• •

$d^{\prime}=d_{i}$, for all $i\in[{1},{n}]$, i.e., $d$ has a unique immediate predecessor, hence it is an irreducible and thus clearly $d=\bigsqcup(\mathop{\downarrow\!{d}}\cap\mathop{\mathit{ir}({D})})$ or

• •

$d=d^{\prime}=\bigsqcup\{d_{1},\ldots,d_{n}\}$. Since, in turn, by inductive hypothesis $d_{i}=\bigsqcup(\mathop{\downarrow\!{d_{i}}}\cap\mathop{\mathit{ir}({D})})$ and $\mathop{\downarrow\!{d}}\cap\mathop{\mathit{ir}({D})}=\bigcup_{i=1}^{n}(\mathop{\downarrow\!{d_{i}}}\cap\mathop{\mathit{ir}({D})})$, we immediately get the thesis.

■

We next observe that every prime is an irreducible and, if $D$ is a prime domain, then also the converse holds, i.e., irreducibles coincide with primes.

Proposition 2** (irreducibles vs. primes)**

Let $D$ be a domain. Then $\mathop{\mathit{pr}({D})}\subseteq\mathop{\mathit{ir}({D})}$. Moreover, $D$ is a prime domain iff $\mathop{\mathit{pr}({D})}=\mathop{\mathit{ir}({D})}$. □

Proof

Let $D$ be a domain. We show that $\mathop{\mathit{pr}({D})}\subseteq\mathop{\mathit{ir}({D})}$. Let $d\in\mathop{\mathit{pr}({D})}$. Assume that $d=\bigsqcup X$ for some pairwise consistent set $X$. By primality, since $d\sqsubseteq\bigsqcup X$ there must be $x\in X$ such that $d\sqsubseteq x$. We have also $x\sqsubseteq\bigsqcup X=d$ and thus $d=x\in X$.

For the second part, let us assume that $D$ is a prime domain. We have to prove that $\mathop{\mathit{pr}({D})}=\mathop{\mathit{ir}({D})}$. We already know that $\mathop{\mathit{pr}({D})}\subseteq\mathop{\mathit{ir}({D})}$. For the converse inclusion, let $i\in\mathop{\mathit{ir}({D})}$. By prime algebraicity $i=\bigsqcup(\mathop{\downarrow\!{i}}\cap\mathop{\mathit{pr}({D})})$. Since $i$ is irreducible, there exists $p\in\mathop{\downarrow\!{i}}\cap\mathop{\mathit{pr}({D})}$ such that $i=p$, hence $i$ is a prime.

Vice versa, if $D$ is a domain, by Proposition 1 we know that $D$ is irreducible algebraic. Hence, if $\mathop{\mathit{pr}({D})}=\mathop{\mathit{ir}({D})}$, we immediately conclude that $D$ is prime. ■

Quite intuitively, in the domain of configurations of an es the irreducibles are minimal enablings of events. For instance, in the domain depicted in Fig. 2(c) the irreducibles are $\{a\}$, $\{b\}$, $\{a,c\}$, and $\{b,c\}$. For stable es, the domain is prime and thus, as observed above, irreducibles coincide with primes. This fails in unstable es, as we can see in our running example: while $\{a\}$ and $\{b\}$ are primes, the two minimal enablings of $c$, namely $\{a,c\}$ and $\{b,c\}$, are not. In fact, $\{a,c\}\subseteq\{a\}\sqcup\{b,c\}$, but neither $\{a,c\}\subseteq\{a\}$ nor $\{a,c\}\subseteq\{b,c\}$.

The key observation is that in general an event corresponds to a class of irreducibles, like $\{a,c\}$ and $\{b,c\}$ in our example. Additionally, two irreducibles corresponding to the same event can be used, to a certain extent, interchangeably for building the same configuration. For instance, $\{a,b,c\}=\{a,b\}\sqcup\{a,c\}=\{a,b\}\sqcup\{b,c\}$. We next formalise this intuition, i.e., we interpret irreducibles in a domain as minimal enablings of some event and we identify classes of irreducibles corresponding to the same event.

We start by observing that, in a prime domain, any element admits a unique decomposition in terms of downward closed sets of irreducibles (or, equivalently, of primes).

Lemma 3** (unique decomposition in prime domains)**

Let $D$ be a prime domain and let $X,X^{\prime}\subseteq\mathop{\mathit{ir}({D})}$ be downward closed sets of irreducibles. If $\bigsqcup X=\bigsqcup X^{\prime}$ then $X=X^{\prime}$. □

Proof

Let $X,X^{\prime}\subseteq\mathop{\mathit{ir}({D})}$ be downward closed sets of irreducibles such that $\bigsqcup X=\bigsqcup X^{\prime}$. Take any $i^{\prime}\in X^{\prime}$. Then $i^{\prime}\sqsubseteq\bigsqcup X$. Since the domain is prime algebraic, and thus $i^{\prime}$ is prime, there must exist $i\in X$ such that $i^{\prime}\sqsubseteq i$ and thus $i^{\prime}\in X$. Therefore $X^{\prime}\subseteq X$. By symmetry also the converse inclusion holds, whence equality. ■

The result above no longer holds in domains arising in the presence of fusions. For instance, in the domain in Fig. 2(c), $X=\{\{a\},\{b\},\{a,c\}\}$, $X^{\prime}=\{\{a\},\{b\},\{b,c\}\}$ and $X^{\prime\prime}=\{\{a\},\{b\},\{b,c\},\{a,c\}\}$ are all decompositions for $\{a,b,c\}$. The idea is to identify irreducibles that can be used interchangeably in a decomposition.

Definition 11** (interchangeability)**

Let $D$ be a domain and $i,i^{\prime}\in\mathop{\mathit{ir}({D})}$. We write $i\leftrightarrow i^{\prime}$ if $\{i,i^{\prime}\}$ consistent and for all $X\subseteq\mathop{\mathit{ir}({D})}$ such that $X\cup\{i\}$ and $X\cup\{i^{\prime}\}$ are downward closed and consistent we have $\bigsqcup(X\cup\{i\})=\bigsqcup(X\cup\{i^{\prime}\})$. □

In words, $i\leftrightarrow i^{\prime}$ means that $i$ and $i^{\prime}$ produce the same effect when added to a decomposition that already includes their predecessors. Hence, intuitively, $i$ and $i^{\prime}$ correspond to the execution of the same event with different and consistent enablings.

We first observe that distinct irreducibles related by the interchangeability relation are necessarily incomparable.

Lemma 4** ($\leftrightarrow$ vs $\sqsubseteq$)**

Let $D$ be a domain and let $i,i^{\prime}\in\mathop{\mathit{ir}({D})}$. If $i\leftrightarrow i^{\prime}$ and $i\sqsubseteq i^{\prime}$ then $i=i^{\prime}$. □

Proof

Let $i\leftrightarrow i^{\prime}$ and $i\sqsubseteq i^{\prime}$. If $i\neq i^{\prime}$ and we let $X=\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}$, it turns out that $X\cup\{i\}=X$ and $X\cup\{i^{\prime}\}$ are consistent and downward closed. Moreover $\bigsqcup X\cup\{i\}=\bigsqcup X=\mathit{p}({i^{\prime}})\neq\bigsqcup X\cup\{i^{\prime}\}=i^{\prime}$, contradicting $i\leftrightarrow i^{\prime}$. ■

We next give some characterisations of interchangeability.

Lemma 5** (characterising $\leftrightarrow$)**

Let $D$ be a domain and $i,i^{\prime}\in\mathop{\mathit{ir}({D})}$. Then the following are equivalent

$i\leftrightarrow i^{\prime}$; 2. 2.

$\{i,i^{\prime}\}$* consistent and for all $d\in\mathop{\mathsf{K}({D})}$ if $\mathit{p}({i}),\mathit{p}({i^{\prime}})\sqsubseteq d$ then $d\sqcup i=d\sqcup i^{\prime}$;* 3. 3.

$\{i,i^{\prime}\}$* consistent and $i\sqcup\mathit{p}({i^{\prime}})=\mathit{p}({i})\sqcup i^{\prime}$.*

□

Proof

(1 $\to$ 2) Assume that $i\leftrightarrow i^{\prime}$. By definition, $\{i,i^{\prime}\}$ is consistent. Let $d\in\mathop{\mathsf{K}({D})}$ be such that $\mathit{p}({i}),\mathit{p}({i^{\prime}})\sqsubseteq d$. If we let $X=\mathop{\mathit{ir}({d})}$ we have that $\mathop{\mathit{ir}({i})}\setminus\{i\}\subseteq X$ and similarly $\mathop{\mathit{ir}({i^{\prime}})}\setminus\{i^{\prime}\}\subseteq X$. This implies that $X\cup\{i\}$ and $X\cup\{i^{\prime}\}$ are downward closed and consistent. Hence $d\sqcup i=\bigsqcup X\sqcup i=\bigsqcup(X\cup\{i\})=\bigsqcup(X\cup\{i^{\prime}\})=\bigsqcup X\sqcup i^{\prime}=d\sqcup i^{\prime}$.

(2 $\to$ 3) Assume (2). Let $p=\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})$, which is in $\mathop{\mathsf{K}({D})}$ since $\mathit{p}({i}),\mathit{p}({i^{\prime}})\in\mathop{\mathsf{K}({D})}$. Clearly, $\mathit{p}({i}),\mathit{p}({i^{\prime}})\sqsubseteq p$. Therefore $i\sqcup\mathit{p}({i^{\prime}})=i\sqcup\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})=i\sqcup p=p\sqcup i^{\prime}=\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})\sqcup i^{\prime}=\mathit{p}({i})\sqcup i^{\prime}$.

(3 $\to$ 1) Assume (3). Let $X\subseteq\mathop{\mathit{ir}({D})}$ be such that $X\cup\{i\}$ and $X\cup\{i^{\prime}\}$ are downward closed and consistent sets of irreducibles. This implies that $\mathop{\mathit{ir}({\mathit{p}({i})})}\subseteq X$ and similarly $\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}\subseteq X$. Hence, if we let $P=\mathop{\mathit{ir}({\mathit{p}({i})})}\cup\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}$, we have

$P\subseteq X$  and  $\bigsqcup P=\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})$.

Therefore

\begin{array}[]{ll}\bigsqcup(X\cup\{i\})=\\ \quad=(\bigsqcup X\setminus P)\sqcup\bigsqcup P\sqcup i=\\ \quad=(\bigsqcup X\setminus P)\sqcup\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})\sqcup i=\\ \quad=(\bigsqcup X\setminus P)\sqcup i\sqcup\mathit{p}({i^{\prime}})=\\ \quad=(\bigsqcup X\setminus P)\sqcup\mathit{p}({i})\sqcup i^{\prime}=\\ \quad=(\bigsqcup X\setminus P)\sqcup\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})\sqcup i^{\prime}=\\ \quad=(\bigsqcup X\setminus P)\sqcup\bigsqcup P\sqcup i^{\prime}=\\ \quad=\bigsqcup(X\cup\{i^{\prime}\})\end{array}

■

The interchangeability relation is clearly reflexive and symmetric, but not transitive in general: in the domain of Fig. 4, using the characterisation in Lemma 5(3) one can easily see that $i\leftrightarrow i_{1}$ and $i_{1}\leftrightarrow i^{\prime}$ but not $i\leftrightarrow i^{\prime}$, simply because $\{i,i^{\prime}\}$ is not consistent. More interestingly, in the domain of Fig. 5, we have $i\leftrightarrow i_{1}$, $i_{1}\leftrightarrow i_{2}$, $i_{2}\leftrightarrow i^{\prime}$, hence $i\leftrightarrow^{*}i^{\prime}$. However, despite the fact that $\{i,i^{\prime}\}$ is consistent, it does not hold $i\leftrightarrow i^{\prime}$, since $\mathit{p}({i})\sqcup i^{\prime}\neq i\sqcup\mathit{p}({i^{\prime}})$. This shows that the intuition that interchangeable irreducibles correspond to the execution of the same event with different and consistent enablings is still not properly captured. Since $i$ and $i^{\prime}$ represent the execution of the same event and they are consistent, one would expect that they are interchangeable.

The next definition formalises two additional properties that a domain must enjoy to provide $\leftrightarrow$ the intended meaning.

Definition 12** (interchangeable domain)**

Let $D$ be a domain. We say that $D$ is interchangeable when

for all $i,i^{\prime}\in\mathop{\mathit{ir}({D})}$, if $\{\mathit{p}({i}),\mathit{p}({i^{\prime}})\}$ consistent and $i\leftrightarrow^{*}i^{\prime}$ then $i\leftrightarrow i^{\prime}$; 2. 2.

for all $i,i^{\prime},j,j^{\prime}\in\mathop{\mathit{ir}({D})}$, if $i\leftrightarrow^{*}i^{\prime}$, $j\leftrightarrow^{*}j^{\prime}$, and $\{i^{\prime},j^{\prime}\}$, $\{\mathit{p}({i}),j\}$, $\{\mathit{p}({j}),i\}$ consistent then $\{i,j\}$ consistent.

□

Property (1) is motivated by the discussion above. It intuitively asks that whenever $i$ and $i^{\prime}$ represents the execution of the same event and they are consistent, then they are interchangeable. Property (2) can be read as follows: if $i,i^{\prime}$ and $j,j^{\prime}$ represent the same events and $i^{\prime},j^{\prime}$ are consistent, the only source of inconsistency between $i$ and $j$ is in their enablings. In other words, either $i$ and $j$ are consistent or it must be that $\mathit{p}({i})$ is inconsistent with $j$, or $i$ is inconsistent with $\mathit{p}({j})$. A situation in which this property fails is illustrated in Fig. 6.

We now introduce weak primes: they weaken the property of prime elements, requiring that it holds up to interchangeability.

Definition 13** (weak prime)**

Let $D$ be a domain. A weak prime of $D$ is an element $i\in\mathop{\mathit{ir}({D})}$ such that for all pairwise consistent $X\subseteq D$, if $i\sqsubseteq\bigsqcup X$ then there exist $i^{\prime}\in\mathop{\mathit{ir}({D})}$ and $d\in X$ such that $i\leftrightarrow i^{\prime}$ and $i^{\prime}\sqsubseteq d$. We denote by $\mathop{\mathit{wpr}({D})}$ the set of weak primes of $D$. □

Clearly, since interchangeability is reflexive, any prime is a weak prime. Moreover, in prime domains interchangeability turns out to be the identity and thus also the converse holds.

Lemma 6** (weak primes in prime domains)**

Let $D$ be a prime domain. Then $\leftrightarrow$ is the identity and $\mathop{\mathit{wpr}({D})}=\mathop{\mathit{pr}({D})}$. □

Proof

Let $i,i^{\prime}\in\mathop{\mathit{ir}({D})}$ be such that $i\leftrightarrow i^{\prime}$.

If $i$ and $i^{\prime}$ are comparable, i.e., $i\sqsubseteq i^{\prime}$ or $i^{\prime}\sqsubseteq i$, by Lemma 4 we deduce $i=i^{\prime}$ and we are done.

Otherwise, let $X=(\mathop{\mathit{ir}({i})}\setminus\{i\})\cup(\mathop{\mathit{ir}({i^{\prime}})}\setminus\{i^{\prime}\})$. Note that $X\cup\{i\}$ and $X\cup\{i^{\prime}\}$ are consistent, since, by definition of $\leftrightarrow$, $i$ and $i^{\prime}$ are so. Moreover $X\cup\{i\}$ and $X\cup\{i^{\prime}\}$ are downward closed, and thus, from $i\leftrightarrow i^{\prime}$, we deduce $\bigsqcup(X\cup\{i\})=\bigsqcup(X\cup\{i^{\prime}\})$. Since $D$ is prime, by Lemma 3, this implies that $X\cup\{i\}=X\cup\{i^{\prime}\}$. Since $i$ and $i^{\prime}$ are uncomparable, $i,i^{\prime}\not\in X$ and we conclude $i=i^{\prime}$. ■

We argue that the domain of configurations arising in the presence of fusions can be characterised domain-theoretically as interchangeable domains where all irreducibles are weak primes, i.e., that the domain is algebraic with respect to weak primes.

Definition 14** (weak prime algebraic domains)**

Let $D$ be an interchangeable domain. It is weak prime algebraic (or simply weak prime) if for all $d\in D$ it holds $d=\bigsqcup(\mathop{\downarrow\!{d}}\cap\mathop{\mathit{wpr}({D})})$. □

Observe that weak prime domains are assumed to be interchangeable. This hypothesis will actually play a role only when relating weak prime domains and event structures in Section III-C. However, in order to simplify the presentation we preferred to assume it since the beginning.

In the same way as prime domains are domains where all irreducibles are primes (see Proposition 2), we can provide a characterisation of weak prime domains in terms of coincidence between irreducibles and weak primes.

Proposition 3** (weak prime domains, again)**

Let $D$ be an interchangeable domain. It is weak prime iff all irreducibles are weak primes. □

Proof

Let $D$ be an interchangeable domain. We know, by Lemma 1, that $D$ is irreducible algebraic. If all irreducibles are weak primes, then clearly $D$ is also weak prime algebraic. Conversely, if it is weak prime algebraic, then for any irreducible $i\in\mathop{\mathit{ir}({D})}$, we have that $i=\bigsqcup(\mathop{\downarrow\!{i}}\cap\mathop{\mathit{wpr}({D})})$. Since $i$ is irreducible, this implies $i\in\mathop{\downarrow\!{i}}\cap\mathop{\mathit{wpr}({D})}\subseteq\mathop{\mathit{wpr}({D})}$, as desired. ■

A domain is often built as the ideal completion of its compact elements. We next provide a characterisation of domains and weak prime domains based on the generators.

Lemma 7** (weak prime domains from generators)**

Let $(P,\sqsubseteq)$ be a finitary partial order such that for all $d,d^{\prime},d^{\prime\prime}\in P$, if $\{d,d^{\prime},d^{\prime\prime}\}$ is pairwise consistent then $d\sqcup d^{\prime}$ exists and is consistent with $d^{\prime\prime}$. Then $\mathsf{Idl}({P})$ is a domain with $\mathop{\mathsf{K}({\mathsf{Idl}({P})})}=\{\mathop{\downarrow\!{d}}\mid d\in P\}\simeq P$.

Additionally, let $P$ be interchangeable and for all $i\in\mathop{\mathit{ir}({P})}$, $d,d^{\prime}\in P$ consistent, if $i\sqsubseteq d\sqcup d^{\prime}$ then there is $i^{\prime}\in\mathop{\mathit{ir}({P})}$, $i\leftrightarrow i^{\prime}$ such that $i^{\prime}\sqsubseteq d$ or $i^{\prime}\sqsubseteq d^{\prime}$. Then $\mathsf{Idl}({P})$ is a weak prime domain. □

Proof

Let $(P,\sqsubseteq)$ be a finitary partial order such that for all $d,d^{\prime},d^{\prime}\in P^{\prime}$, if $\{d,d^{\prime},d^{\prime\prime}\}$ is pairwise consistent then $d\sqcup d^{\prime}$ exists and is consistent with $d^{\prime\prime}$.

The fact that $\mathsf{Idl}({P})$ is a complete algebraic finitary partial order with $\mathop{\mathsf{K}({\mathsf{Idl}({P})})}=\{\mathop{\downarrow\!{d}}\mid d\in P\}\simeq P$ is a standard result. Moreover, let $X\subseteq\mathsf{Idl}({P})$ pairwise consistent. Consider $A=\bigcup\{I\mid I\in X\}$. Observe that for any finite $Y\subseteq A$ there exists $\bigsqcup Y$ in $P$. In fact, let $Y=\{y_{1},\ldots,y_{n}\}$. This means that there are $I_{1},\ldots,I_{n}$ such that $y_{i}\in I_{i}$ for each $i\in[{1},{n}]$. Since $X$ is pairwise consistent in $\mathsf{Idl}({P})$, we deduce that $Y$ is pairwise consistent in $P$. Since $y_{1},y_{2}$ are consistent and both are consistent with $y_{3},\ldots,y_{n}$, by hypothesis there exists $y_{1}\sqcup y_{2}$ and it is consistent with $y_{3},\ldots,y_{n}$, i.e., $\{y_{1}\sqcup y_{2},y_{3},\ldots,y_{n}\}$ is again pairwise consistent. Iterating the reasoning we get the existence of $y_{1}\sqcup y_{2}\sqcup\ldots\sqcup y_{n}=\bigsqcup Y$, as desired. Now, if we define $I^{\prime}=\{\bigsqcup Y\mid Y\subseteq_{\mathit{fin}}A\}$, then $I^{\prime}$ is an ideal and $I^{\prime}=\bigsqcup X$.

Let us consider the second part. It is easy to see that $\mathop{\mathit{ir}({\mathsf{Idl}({P})})}=\{\mathop{\downarrow\!{i}}\mid i\in\mathop{\mathit{ir}({P})}\}$. Moreover, for $i,i^{\prime}\in\mathop{\mathit{ir}({P})}$ we have $i\leftrightarrow i^{\prime}$ in $P$ if and only if $\mathop{\downarrow\!{i}}\leftrightarrow\mathop{\downarrow\!{i^{\prime}}}$ in $\mathsf{Idl}({P})$. This immediately implies that $\mathsf{Idl}({P})$ is interchangeable, because so is $P$ by assumption.

We need to show that, under the hypotheses, if $I\in\mathop{\mathit{ir}({\mathsf{Idl}({P})})}$ and $X\subseteq\mathsf{Idl}({P})$ pairwise consistent and $I\subseteq\bigsqcup X$ then there exists $I^{\prime}\leftrightarrow I$ and $A\in X$ such that $I^{\prime}\subseteq A$. Thus let $I=\mathop{\downarrow\!{i}}$ for some $i\in\mathop{\mathit{ir}({P})}$. The fact that $I=\mathop{\downarrow\!{i}}\subseteq\bigsqcup X=\bigsqcup\{\mathop{\downarrow\!{d}}\mid d\in\bigcup X\}$, since $\mathop{\downarrow\!{i}}$ is finite, means that $\mathop{\downarrow\!{i}}\subseteq\mathop{\downarrow\!{d_{1}}}\cup\ldots\cup\mathop{\downarrow\!{d_{n}}}$ for some finite subset $\{d_{1},\ldots,d_{n}\}\subseteq\bigcup X$ and thus $i\sqsubseteq\bigsqcup\{d_{1},\ldots,d_{n}\}$. Since $i\sqsubseteq d_{1}\sqcup\bigsqcup\{d_{2},\ldots,d_{n}\}$, by the hypothesis there is $i_{1}\leftrightarrow i$ such that $i_{1}\sqsubseteq d_{1}$ or $i_{1}\sqsubseteq\bigsqcup\{d_{2},\ldots,d_{n}\}=d_{2}\sqcup\bigsqcup\{d_{3},\ldots,d_{n}\}$. In the second case, again by the hypotheses, there are two possibilities. The first is that there is $i_{2}\leftrightarrow i_{1}$, such that $i_{2}\sqsubseteq d_{2}$. Note that, since $\mathit{p}({i})$ and $\mathit{p}({i_{2}})$ are clearly consistent (they are dominated by $\bigsqcup\{d_{1},\ldots,d_{n}\}$), by property (1) of well-interchangeability (Definition 12), we get $i_{2}\leftrightarrow i$. The second possibility is that ${i_{2}}\sqsubseteq\bigsqcup\{d_{3},\ldots,d_{n}\}$, and we can iterate the reasoning. In the end, we get the existence of some $i^{\prime}\leftrightarrow i$ and $j\in[{1},{n}]$ such that $i^{\prime}\sqsubseteq d_{j}$. Recalling that $d_{j}\in\bigcup X$, there is ${A}\in X$ such that $d_{j}\in{A}$, hence $\mathop{\downarrow\!{{i^{\prime}}}}\subseteq\mathop{\downarrow\!{d_{j}}}\subseteq{A}$. Since $i\leftrightarrow{i^{\prime}}$ in $P$ implies $\mathop{\downarrow\!{i}}\leftrightarrow\mathop{\downarrow\!{{i^{\prime}}}}$ in $\mathsf{Idl}({P})$, we conclude. ■

We finally introduce a category of weak prime domains by defining a notion of morphism.

Definition 15** (category of weak prime domains)**

Let $D_{1}$, $D_{2}$ be weak prime domains. A weak prime domain morphism $f:D_{1}\to D_{2}$ is a total function such that for all consistent $X_{1}\subseteq D_{1}$ and $d_{1},d_{1}^{\prime}\in D_{1}$

if $d_{1}\preceq d_{1}^{\prime}$ then $f(d_{1})\preceq f(d_{1}^{\prime})$; 2. 2.

$f(\bigsqcup X_{1})=\bigsqcup f(X_{1})$; 3. 3.

if $d_{1},d_{1}^{\prime}$ consistent and $d_{1}\sqcap d_{1}^{\prime}\preceq d_{1}$ then $f(d_{1}\sqcap d_{1}^{\prime})=f(d_{1})\sqcap f(d_{1}^{\prime})$;

We denote by $\mathsf{wDom}$ the category of weak prime domains and their morphisms. □

Compared with the notion of morphism for prime domains in Definition 8 (from [16]), we still require the preservation of $\preceq$ and $\sqcup$ of consistent sets (conditions (1) and (2)). However, the third condition, i.e., preservation of $\sqcap$, is weakened to preservation in some cases. General preservation of meets is indeed not expected in the presence of fusions. Consider, e.g., the es in Example 1. Take another es $E^{\prime}=\{c\}$ with $\emptyset\vdash c$ and the morphism $f:E\to E^{\prime}$ that forgets $a$ and $b$, i.e., $f(c)=c$ and $f(a)$, $f(b)$ undefined. Then $f(\{a,c\})\sqcap f(\{b,c\})=\{c\}\sqcap\{c\}=\{c\}\neq f(\{a,c\}\sqcap\{b,c\})=f(\emptyset)=\emptyset$. Intuitively, the condition $d_{1}\sqcap d_{1}^{\prime}\prec d_{1}$ means that $d_{1}^{\prime}$ includes the computation modelled by $d_{1}$ apart from a final step, hence $d_{1}\sqcap d_{1}^{\prime}$ coincides with $d_{1}$ when such step is removed. Since domain morphisms preserve immediate precedence (i.e., single steps), also $f(d_{1})$ differs from $f(d_{1}^{\prime})$ for the execution of a final step and the meet $f(d_{1})\sqcap f(d_{1}^{\prime})$ is $f(d_{1})$ without such step, and thus it coincides with $f(d_{1}\sqcap d_{1}^{\prime})$.

In general we only have

$f(\bigsqcap X_{1})\sqsubseteq\bigsqcap f(X_{1})$

In fact, for all $x_{1}\in X_{1}$, we have $\bigsqcap X_{1}\sqsubseteq x_{1}$, hence $f(\bigsqcap X_{1})\sqsubseteq f(x_{1})$ and thus $f(\bigsqcap X_{1})\sqsubseteq\bigsqcap f(X_{1})$. Still, when restricted to prime domains, also the converse inequality holds and our notion of morphism boils down to the original one, i.e., the full subcategory of $\mathsf{wDom}$ having prime domains as objects is $\mathsf{pDom}$.

Theorem 2** ($\mathsf{pDom}$ as a subcategory of $\mathsf{wDom}$)**

The category of prime domains $\mathsf{pDom}$ is the full subcategory of $\mathsf{wDom}$ having prime domains as objects. □

Proof

We just need to show that weak prime domain morphisms preserve meets on prime domains, i.e., that if $D_{1}$, $D_{2}$ are prime domains and $f:D_{1}\to D_{2}$ is a weak prime domain morphism then $f(\bigsqcap X_{1})=\bigsqcap f(X_{1})$ for all $X_{1}\subseteq D_{1}$ pairwise consistent.

We first show that for $d_{1},d_{1}^{\prime}\in\mathop{\mathsf{K}({D_{1}})}$, consistent, it holds that $f(d_{1}\sqcap d_{1}^{\prime})=f(d_{1})\sqcap f(d_{1}^{\prime})$. We proceed by induction on $k=|\mathop{\downarrow\!{d_{1}}}\cap\mathop{\mathit{pr}({D})}|$.

When $k=0$ we have $d_{1}=\bot$. Since $f$ preserves joins, we have that $f(\bot)=f(\bigsqcup\emptyset)=\bigsqcup f(\emptyset)=\bigsqcup\emptyset=\bot$. Hence

$f(d_{1}\sqcap d_{1}^{\prime})=f(\bot\sqcap d_{1}^{\prime})=f(\bot)=\bot=\bot\sqcap f(d_{1}^{\prime})=f(\bot)\sqcap f(d_{1}^{\prime})=f(d_{1})\sqcap f(d_{1}^{\prime})$.

Suppose now $k>0$. We distinguish two subcases. If $d_{1}$ is not prime then, recalling that in a prime domain, primes and irreducibles coincide, $d_{1}$ is not irreducible and thus $d_{1}=e_{1}\sqcup f_{1}$ with $d_{1}\neq e_{1},f_{1}\neq\bot$. It is immediate to see that $|\mathop{\downarrow\!{e_{1}}}\cap\mathop{\mathit{pr}({D})}|<k$ and $|\mathop{\downarrow\!{f_{1}}}\cap\mathop{\mathit{pr}({D})}|<k$. Moreover, since any prime algebraic domain is distributive we have $d_{1}\sqcap d_{1}^{\prime}=(e_{1}\sqcup f_{1})\sqcap d_{1}^{\prime}=(e_{1}\sqcap d_{1}^{\prime})\sqcup(f_{1}\sqcap d_{1}^{\prime})$. Summing up

[TABLE]

If instead $d_{1}$ is prime then note that if $d_{1}\sqsubseteq d_{1}^{\prime}$ the thesis is immediate: by monotonicity $f(d_{1})\sqsubseteq f(d_{1}^{\prime})$. Thus $f(d_{1}\sqcap d_{1}^{\prime})=f(d_{1})=f(d_{1})\sqcap f(d_{1}^{\prime})$ as desired. Therefore, let us assume that $d_{1}\not\sqsubseteq d_{1}^{\prime}$. In this case $d_{1}\sqcap d_{1}^{\prime}=\mathit{p}({d_{1}})\sqcap d_{1}^{\prime}$, since the set of lower bounds of $\{d_{1},d_{1}^{\prime}\}$ and of $\{\mathit{p}({d_{1}}),d_{1}^{\prime}\}$ is the same. Observe that

[TABLE]

In fact, the join exists since $d_{1}$, $d_{1}^{\prime}$ are consistent. Moreover, by distributivity, $d_{1}\sqcap(\mathit{p}({d_{1}})\sqcup d_{1}^{\prime})=(d_{1}\sqcap\mathit{p}({d_{1}}))\sqcup(d_{1}\sqcap d_{1}^{\prime})=\mathit{p}({d_{1}})\sqcup(\mathit{p}({d_{1}})\sqcap d_{1}^{\prime})=\mathit{p}({d_{1}})$.

Therefore

[TABLE]

as desired. This extends to the meet of finite sets of compact elements, by associativity of $\sqcap$, and to infinite sets of compacts by observing that, given an infinite set $X$, by finitariness we can identify a finite subset $F\subseteq X$ such that $\bigsqcap X=\bigsqcap F$. The last assertion can be proved by induction on $k=\min\{|\mathop{\downarrow\!{d}}|:d\in X\}$. In fact, let $d\in X$ be an element such that $|\mathop{\downarrow\!{d}}|=k$. If $k=1$ then $d=\bot$ and thus $\bigsqcap X=\bot=\bigsqcap\{d\}$, as desired. If $k>1$, then we distinguish two possibilities. If for all $d^{\prime}\in X$ it holds $d\sqcap d^{\prime}=d$ then $\bigsqcap X=d=\bigsqcap\{d\}$. If instead, there is $d^{\prime}\in X$ such that $d\sqcap d^{\prime}\sqsubset d$ then recall that the meet of compact elements is compact and consider $X^{\prime}=X\cup\{d\sqcap d^{\prime}\}$. We have that $\bigsqcap X=\bigsqcap X^{\prime}$. Moreover $|\mathop{\downarrow\!{d\sqcap d^{\prime}}}|<k$, hence we can apply the inductive hypothesis to $X^{\prime}$ and get a finite subset $F^{\prime}\subseteq X^{\prime}$ such that $\bigsqcap X^{\prime}=\bigsqcap F^{\prime}$. We conclude observing that $\bigsqcap X=\bigsqcap X^{\prime}=\bigsqcap F^{\prime}=\bigsqcap((F^{\prime}\setminus\{d\sqcap d^{\prime}\})\cup\{d,d^{\prime}\})$. Therefore we can take $F=(F^{\prime}\setminus\{d\sqcap d^{\prime}\})\cup\{d,d^{\prime}\}$ and we conclude. ■

III-B From Event Structures to Weak Prime Domains

We show that the set of configurations of an es, ordered by subset inclusion, is a weak prime domain where the compact elements are the finite configurations. Moreover, the correspondence can be lifted to a functor. We also identify a subclass of es that we call connected es and that are the exact counterpart of weak prime domains (in the same way as prime es correspond to prime algebraic domains).

Definition 16** (configurations of an event structure, ordered)**

Let ${E}$ be an es. We define $\mathcal{D}({{E}})=\langle\mathit{Conf}({{E}}),\subseteq\rangle$. Given an es morphism $f:{E}_{1}\to{E}_{2}$, its image $\mathcal{D}({f}):\mathcal{D}({{E}_{1}})\to\mathcal{D}({{E}_{2}})$ is defined as $\mathcal{D}({f})(C_{1})=\{f(e_{1})\mid e_{1}\in C_{1}\}$. □

We need some technical facts, collected in the following lemma. Recall that in the setting of unstable es we can have distinct consistent minimal enablings for an event. The following notation will be useful.

Definition 17** (connected enablings)**

Let $E$ be an es, $C,C^{\prime}\in\mathit{Conf}({E})$ and $e\in E$. When $C\vdash_{0}e$, $C^{\prime}\vdash_{0}e$, and $C\cup C^{\prime}\cup\{e\}$ is consistent, we write $C\stackrel{{\scriptstyle e}}{{\frown}}C^{\prime}$. We denote by $\stackrel{{\scriptstyle e}}{{\frown}}^{*}$ the transitive closure of the relation $\stackrel{{\scriptstyle e}}{{\frown}}$. □

Note that, whenever $C\vdash_{0}e$ and $C^{\prime}\vdash_{0}e$, requiring $C\cup C^{\prime}\cup\{e\}$ consistent amounts to require $C\cup C^{\prime}$ consistent, since conflict is binary.

Lemma 8** (properties of the domain of configurations)**

Let $\langle E,\vdash,Con\rangle$ be an es. Then

$\mathcal{D}({{E}})$* is a domain, $\mathop{\mathsf{K}({\mathcal{D}({{E}})})}=\mathit{Conf_{F}}({{E}})$, join is union and $C\prec C^{\prime}$ iff $C^{\prime}=C\cup\{e\}$ for some $e\in E\setminus C$;* 2. 2.

$C\in\mathit{Conf}({{E}})$* is irreducible iff $C=C^{\prime}\cup\{e\}$ and $C^{\prime}\vdash_{0}e$; in this case we denote $C$ as $\langle{C^{\prime}},{e}\rangle$;* 3. 3.

for $C\in\mathit{Conf}({{E}})$, we have $\mathop{\mathit{ir}({C})}=\{\langle{C^{\prime}},{e^{\prime}}\rangle\mid e^{\prime}\in C\ \land\ C^{\prime}\subseteq C\ \land\ C^{\prime}\vdash_{0}e^{\prime}\}$; moreover $\mathit{p}({\langle{C^{\prime}},{e^{\prime}}\rangle})=C^{\prime}$; 4. 4.

for $\langle{C_{1}},{e_{1}}\rangle,\langle{C_{2}},{e_{2}}\rangle\in\mathop{\mathit{ir}({\mathcal{D}({{E}})})}$, we have $\langle{C_{1}},{e_{1}}\rangle\leftrightarrow\langle{C_{2}},{e_{2}}\rangle$ iff $e=e_{1}=e_{2}$ and $C_{1}\stackrel{{\scriptstyle e}}{{\frown}}C_{2}$; 5. 5.

$\mathcal{D}({E})$* is interchangeable.*

□

Proof

We first observe that, given a pairwise consistent set of configurations $X\subseteq\mathit{Conf}({E})$, the join is the union $\bigsqcup X=\bigcup X$. The fact that $\bigcup X$ is a configuration, i.e., that it is consistent and secured immediately follows from the fact that each $C\in X$ is.

Let $C\in\mathit{Conf}({E})$ be a configuration. For every event $e\in E$, since $C$ is secured, we can consider a set $C_{e}=\{e_{1},\ldots,e_{n}\}\subseteq C$ such that $e_{n}=e$ and $\{e_{1},\ldots,e_{k-1}\}\vdash e_{k}$ for all $k\in[{1},{n}]$. It is immediate to see that $C_{e}\in\mathit{Conf_{F}}({E})$ and clearly $C=\bigsqcup_{e\in C}C_{e}$.

From the above it is almost immediate to conclude that the compact elements of $\mathcal{D}({{E}})$ are the finite configurations $\mathop{\mathsf{K}({\mathcal{D}({E})})}=\mathit{Conf_{F}}({E})$ and that $\mathcal{D}({{E}})$ is algebraic. Moreover, $\mathcal{D}({E})$ is finitary, since the number of subsets of a finite configurations is clearly finite. Hence $\mathcal{D}({{E}})$ is a domain.

Concerning immediate precedence, let $C,C^{\prime}\in\mathit{Conf_{F}}({E})$. If $C^{\prime}=C\cup\{e\}$ with $e\not\in C$ then clearly $C\prec C^{\prime}$, since the order is subset inclusion. Conversely, if $C\prec C^{\prime}$ by definition $C\subseteq C^{\prime}$ and it must be $|C^{\prime}\setminus C|=1$. In fact, $C\subseteq C^{\prime}$ and $C\neq C^{\prime}$, hence $C^{\prime}\setminus C\neq\emptyset$. Let $e,e^{\prime}\in C^{\prime}\setminus C$. Let us prove that $e=e^{\prime}$. Since $C^{\prime}$ is secured there is a set of events $D=\{e_{1},\ldots,e_{n}\}\subseteq C^{\prime}$, such that $e_{n}=e$ and $\{e_{1},\ldots,e_{k-1}\}\vdash e_{k}$ for all $k\in[{1},{n}]$. Now, if $e^{\prime}\not\in D$, observe that $C\cup D$ is a configuration and $C\subset C\cup D\subset C^{\prime}$, contradicting $C\prec C^{\prime}$. Assume that, instead, $e^{\prime}\in D$. If $e^{\prime}=e_{k}$ for $k<n$ we would have that $D^{\prime}=\{e_{1},\ldots,e_{k}\}$ is a configuration and we could replace $D$ by $D^{\prime}$ in the contradiction above. Hence it must be $e=e^{\prime}$, as desired. 2. 2.

Let $C\in\mathit{Conf}({{E}})$ be a configuration and assume that $C=C^{\prime}\cup\{e\}$ with $C^{\prime}\vdash_{0}e$. Then $C$ is a finite configuration, and thus a compact element. Moreover, if $C=C_{1}\cup C_{2}$ for $C_{1},C_{2}\in\mathit{Conf}({{E}})$, then $e$ must occur either in $C_{1}$ or in $C_{2}$. If $e\in C_{1}$, since $C_{1}$ is secured, there exists $C_{1}^{\prime}\subseteq C_{1}\setminus\{e\}$ such that $C_{1}^{\prime}\vdash e$. Hence, by monotonicity of enabling, $C_{1}\setminus\{e\}\vdash e$. Since $C^{\prime}\vdash_{0}e$ and $C_{1}\setminus\{e\}\subseteq C^{\prime}$ it follows that $C_{1}\setminus\{e\}=C^{\prime}$ and thus $C_{1}=C$. Therefore, by Lemma 1, $C$ is an irreducible.

Vice versa, let $C\in\mathit{Conf}({{E}})$ be an irreducible. It is compact, hence finite. Hence we can consider a secured execution $\langle e_{1},\ldots,e_{n}\rangle$ of configuration $C$. Note that for any $k\in[{1},{n-1}]$ it must be $\{e_{1},\ldots,e_{k-1}\}\not\vdash e_{n}$. Otherwise, if it were $\{e_{1},\ldots,e_{k-1}\}\vdash e_{n}$ for some $k\in[{1},{n-1}]$, we would have that $C^{\prime}=\{e_{1},\ldots,e_{k},e_{n}\}$ and $C^{\prime\prime}=\{e_{1},\ldots,e_{n-1}\}$ are two proper subconfigurations of $C$ such that $C=C^{\prime}\cup C^{\prime\prime}$, violating the fact that $C$ is irreducible. But this means exactly that $\{e_{1},\ldots,e_{n-1}\}\vdash_{0}e_{n}$, as desired. 3. 3.

Immediate. 4. 4.

Let $I_{j}=\langle{C_{j}},{e_{j}}\rangle\in\mathop{\mathit{ir}({\mathcal{D}({{E}})})}$ for $j\in\{1,2\}$ be irreducibles. Assume $I_{1}\leftrightarrow I_{2}$. By Lemma 5(3), observing that $\mathit{p}({I_{j}})=C_{j}$, we must have $I_{1}\cup C_{2}=C_{1}\cup I_{2}$, namely $C_{1}\cup\{e_{1}\}\cup C_{2}=C_{1}\cup C_{2}\cup\{e_{2}\}$, from which we conclude that it must be $e_{1}=e_{2}$, i.e., as desired $I_{j}=\langle{C_{j}},{e}\rangle$, where $e=e_{1}=e_{2}$ for $j\in\{1,2\}$. Additionally, $I_{1}$ and $I_{2}$ are consistent, by definition of $\leftrightarrow$, meaning that $C_{1}\stackrel{{\scriptstyle e}}{{\frown}}C_{2}$.

For the converse, consider two irreducibles $I_{1}=\langle{C_{1}},{e}\rangle$ and $I_{2}=\langle{C_{2}},{e}\rangle$, such that $C_{1}\stackrel{{\scriptstyle e}}{{\frown}}C_{2}$. Hence $C_{1}\vdash_{0}e$, $C_{2}\vdash_{0}e$ and $C=C_{1}\cup C_{2}\cup\{e\}$ is consistent. Since $I_{1},I_{2}\subseteq C$, they are consistent in $\mathcal{D}({{E}})$. Moreover, $\mathit{p}({I_{1}})=C_{1}$, $\mathit{p}({I_{2}})=C_{2}$ and $I_{1}\cup C_{2}=I_{2}\cup C_{1}=C$. Hence by Lemma 5(3) we have $I_{1}\leftrightarrow I_{2}$, as desired. 5. 5.

We have to show that $\mathcal{D}({E})$ satisfies the conditions of Definition 12. Concerning condition (1), let $I_{1}=\langle{C_{1}},{e_{1}}\rangle$ and $I_{2}=\langle{C_{2}},{e_{2}}\rangle$ such that $I_{1}\leftrightarrow^{*}I_{2}$ and $\mathit{p}({I_{1}})=C_{1},\mathit{p}({I_{2}})=C_{2}$ consistent. From $I_{1}\leftrightarrow^{*}I_{2}$, by the above result, we deduce $e_{1}=e_{2}$. Since, $C_{1},C_{2}$ consistent, we deduce $C_{1}\stackrel{{\scriptstyle e}}{{\frown}}C_{2}$ and thus, again by the same result, $I_{1}\leftrightarrow I_{2}$.

As for Condition (2), consider the irreducibles $I$, $I^{\prime}$, $J$ and $J^{\prime}$ such that $I\leftrightarrow^{*}I^{\prime}$, $J\leftrightarrow^{*}J^{\prime}$, and $\{I^{\prime},J^{\prime}\}$, $\{\mathit{p}({I}),J\}$ and $\{\mathit{p}({J}),I\}$ consistent. From $I\leftrightarrow^{*}I^{\prime}$ and $J\leftrightarrow^{*}J^{\prime}$ we deduce that $I=\langle{C},{e}\rangle$, $I^{\prime}=\langle{C^{\prime}},{e}\rangle$, $J=\langle{D},{f}\rangle$ and $J^{\prime}=\langle{D^{\prime}},{f}\rangle$. Moreover, we have $\mathit{p}({I})=C$ and $\mathit{p}({J})=D$, hence the hypotheses say $\{C,J\}$ and $\{D,I\}$ consistent. From the consistency of $\{I^{\prime},J^{\prime}\}$ we deduce that $\{e,f\}$ consistent. Therefore we have that $I=\langle{C},{e}\rangle$ and $J=\langle{D},{f}\rangle$ are consistent.

■

Concerning point 1, observe that the meet in the domain of configurations is $C\sqcap C^{\prime}=\bigcup\{C^{\prime\prime}\in\mathit{Conf}({{E}})\mid C^{\prime\prime}\subseteq C\ \land\ C^{\prime\prime}\subseteq C^{\prime}\}$, which is usually smaller than the intersection. For instance, in Fig. 2, $\{a,c\}\sqcap\{b,c\}=\emptyset\neq\{c\}$. Point 2 says that irreducibles are configurations of the form $C\cup\{e\}$ that admits a secured execution in which the event $e$ appears as the last one and cannot be switched with any other. In other words, irreducibles are minimal enablings of events. Point 3 characterises the irreducibles in a configuration. According to point 4, two irreducibles are interchangeable when they are different minimal enablings for the same event.

Proposition 4** (the domain of configurations is weak prime)**

Let ${E}$ be an es. Then $\mathcal{D}({{E}})$ is a weak prime domain. Moreover, given two es $E_{1}$ and $E_{2}$, and a morphism $f:{E}_{1}\to{E}_{2}$, its image $\mathcal{D}({f}):\mathcal{D}({{E}_{1}})\to\mathcal{D}({{E}_{2}})$ is a weak prime domain morphism. □

Proof

We know that $\mathcal{D}({{E}})$ is a domain (Lemma 8(1)) and that it is interchangeable (Lemma 8(5)).

In order to show that $\mathcal{D}({{E}})$ is a weak prime domain, we exploit the characterisation in Proposition 3, i.e., we prove that all irreducibles are weak primes. Consider an irreducible $I$, which by Lemma 8(2) is of the shape $I=\langle{C},{e}\rangle$ with $C\vdash_{0}e$, and suppose that $I\subseteq\bigsqcup X$ for some $X\subseteq\mathcal{D}({{E}})$. In particular, this means that $e\in\bigsqcup X$ and thus there is $C^{\prime}\in X$ such that $e\in C^{\prime}$. In turn, we can consider a minimal enabling of $e$ in $C^{\prime}$, i.e., a minimal $C^{\prime\prime}\subseteq C^{\prime}$ such that $C^{\prime\prime}\vdash_{0}e$, and we have that $I^{\prime\prime}=\langle{C^{\prime\prime}},{e}\rangle$ is an irreducible $I^{\prime\prime}\subseteq C^{\prime}$. Since $I$ and $I^{\prime\prime}$ are consistent, as they are both included in $\bigsqcup X$, then $C\stackrel{{\scriptstyle e}}{{\frown}}C^{\prime\prime}$ and by Lemma 8(4) $I\leftrightarrow I^{\prime\prime}$.

We next prove that given an es morphism $f:{E}_{1}\to{E}_{2}$, its image $\mathcal{D}({f}):\mathcal{D}({{E}_{1}})\to\mathcal{D}({{E}_{2}})$ is a weak prime domain morphism.

• •

$C_{1}\preceq C_{1}^{\prime}$ implies $\mathcal{D}({f})(C_{1})\preceq\mathcal{D}({f})(C_{1}^{\prime})$

Since $\mathcal{D}({f})(C_{i})=\{f(d_{i})\mid d_{i}\in C_{i}\}$ and by Lemma 8(1) $C_{1}\preceq C_{1}^{\prime}$ iff $C_{1}^{\prime}=C_{1}\cup\{e_{1}\}$ for some event $e_{1}$, the result follows immediately.

• •

for $X_{1}\subseteq\mathcal{D}({{E}_{1}})$ consistent, $\mathcal{D}({f})(\bigsqcup X_{1})=\bigsqcup\mathcal{D}({f})(X_{1})$

Since $\mathcal{D}({f})$ takes the image as set and $\bigsqcup$ on consistent sets is union, the result follows.

• •

for $C_{1},C_{1}^{\prime}\in\mathcal{D}({{E}_{1}})$ consistent such that $C_{1}\sqcap C_{1}^{\prime}\prec C_{1}$ it holds $f(C_{1}\sqcap C_{1}^{\prime})=f(C_{1})\sqcap f(C_{1}^{\prime})$

Since $C_{1}\sqcap C_{1}^{\prime}\prec C_{1}$, by Lemma 8(1) we have that $C_{1}=(C_{1}\sqcap C_{1}^{\prime})\cup\{e_{1}\}$ for some $e_{1}\not\in C_{1}\sqcap C_{1}^{\prime}$. Clearly $e_{1}\not\in C_{1}^{\prime}$, otherwise we would have $C_{1}\subseteq C_{1}^{\prime}$ and thus $C_{1}\sqcap C_{1}^{\prime}=C_{1}$. Therefore in this case, the meet coincides with intersection, $C_{1}\sqcap C_{1}^{\prime}=C_{1}\cap C_{1}^{\prime}=C_{1}\setminus\{e_{1}\}$. Since for the events in $C_{1}\cup C_{1}^{\prime}$, by definition of event structure morphism, $f$ is injective, we have that $f(C_{1})\cap f(C_{1}^{\prime})=f(C_{1}\cap C_{1}^{\prime})$. As a general fact, $f(C_{1})\sqcap f(C_{1}^{\prime})\subseteq f(C_{1})\cap f(C_{1}^{\prime})$. Therefore, putting things together, we conclude

$f(C_{1})\sqcap f(C_{1}^{\prime})\subseteq f(C_{1})\cap f(C_{1}^{\prime})=f(C_{1}\cap C_{1}^{\prime})=f(C_{1}\sqcap C_{1}^{\prime})$

The converse inequality holds in any domain (as observed after Definition 15) and thus the result follows.

■

A special role is played by the subclass of connected es which will be shown to be exact counterpart of weak prime domains.

Definition 18** (connected event structure)**

An es is connected if whenever $C\vdash_{0}e$ and $C^{\prime}\vdash_{0}e$ then $C\stackrel{{\scriptstyle e}}{{\frown}}^{*}C^{\prime}$. We denote by $\mathsf{cES}$ the full subcategory of $\mathsf{ES}$ having connected es as objects. □

In words, different minimal enablings for the same event must be pairwise connected by a chain of consistency. Equivalently, for each event $e$ the set of minimal enablings, say $M_{e}=\{C\mid C\vdash_{0}e\}$, endowed with the relation $\stackrel{{\scriptstyle e}}{{\frown}}$ is a connected graph. Intuitively, as discussed in more detail below, if $M_{e}$ were not connected, then we could split event $e$ into different instances, one for each connected component, without changing the associated domain.

For instance, the es in Example 1 is a connected es. Only event $c$ has two minimal enablings $\{a\}\vdash_{0}c$ and $\{b\}\vdash_{0}c$ and obviously $\{a\}\stackrel{{\scriptstyle c}}{{\frown}}\{b\}$. Clearly, prime es are also connected es. More precisely, we have the following.

Proposition 5** (primality = stability + connectedness)**

Let ${E}$ be an es. Then $E$ is prime iff it is stable and connected. □

Proof

The fact that a prime es is stable and connected follows immediately from the definitions. Conversely, let ${E}$ be a stable and connected es. We show that $E$ is prime, i.e., each $e\in E$ has a unique minimal enabling. Let $C,C^{\prime}\in\mathit{Conf}({E})$ be minimal enablings for $e$, i.e., $C\vdash_{0}e$ and $C^{\prime}\vdash_{0}e$. Since $E$ is connected $C\stackrel{{\scriptstyle e}}{{\frown}}^{*}C^{\prime}$. Let $C\stackrel{{\scriptstyle e}}{{\frown}}C_{1}\stackrel{{\scriptstyle e}}{{\frown}}\ldots\stackrel{{\scriptstyle e}}{{\frown}}C_{n}\stackrel{{\scriptstyle e}}{{\frown}}C^{\prime}$. Then by stability we get that $C=C_{1}=\ldots=C_{n}=C^{\prime}$. ■

The defining property of connected es allows one to recognise that two minimal enablings are relative to the same event by only looking at the partially ordered structure and thus, as we will see, from the domain of configurations of a connected es we can recover an es isomorphic to the original one and vice versa (see Theorem 3). In general, this is not possible. For instance, consider the es ${E}^{\prime}$ with events $E^{\prime}=\{a,b,c\}$, and where $a\#b$ and the minimal enablings are again $\emptyset\vdash_{0}a$, $\emptyset\vdash_{0}b$, $\{a\}\vdash_{0}c$, and $\{b\}\vdash_{0}c$. Namely, event $c$ has two minimal enablings, but differently from what happens in the running example, these are not consistent, hence $\{a,b\}\not\vdash c$. The resulting domain of configurations is depicted on the left of Fig. 7. Intuitively, it is not possible to recognise that $\{a,c\}$ and $\{b,c\}$ are different minimal enablings of the same event. In fact, we would get an isomorphic domain of configurations by considering the es ${E}^{\prime\prime}$ with events $E^{\prime\prime}=\{a,b,c_{1},c_{2}\}$ such that $a\#b$ and the minimal enablings are again $\emptyset\vdash_{0}a$, $\emptyset\vdash_{0}b$, $\{a\}\vdash_{0}c_{1}$, and $\{b\}\vdash_{0}c_{2}$.

III-C From Weak Prime Domains to Connected Event Structures

We show how to get an es from a weak prime domain. As anticipated, events are equivalence classes of irreducibles, where the equivalence is (the transitive closure of) interchangeability.

In order to properly relate domains to the corresponding es we need to prove some properties of irreducibles and of the interchangeability relation in weak prime domains.

Domains are irreducible algebraic (see Proposition 1), hence any element is determined by the irreducibles under it. The difference between two elements is thus somehow captured by the irreducibles that are under one element and not under the other. This motivates the following definition.

Definition 19** (irreducible difference)**

Let $D$ be a domain and $d,d^{\prime}\in\mathop{\mathsf{K}({D})}$ such that $d\sqsubseteq d^{\prime}$. Then we define $\delta({d^{\prime}},{d})=\mathop{\mathit{ir}({d^{\prime}})}\setminus\mathop{\mathit{ir}({d})}$. □

The immediate precedence relation intuitively relates domain elements corresponding to configurations that differ for the execution of a single event. In order to formalise this fact we first need a preliminary technical lemma.

Lemma 9** (immediate precedence and irreducibles/1)**

Let $D$ be a weak prime domain, $d\in\mathop{\mathsf{K}({D})}$, and $i\in\mathop{\mathit{ir}({D})}$ such that $d$, $i$ are consistent and $\mathit{p}({i})\sqsubseteq d$. Then

for all $i^{\prime}\in\delta({d\sqcup i},{d})$ minimal, it holds $i\leftrightarrow i^{\prime}$; 2. 2.

$d\preceq d\sqcup i$.

□

Proof

Clearly, if $d=d\sqcup i$ then $\delta({d\sqcup i},{d})=\emptyset$ and the property trivially holds. Assume $d\neq d\sqcup i$ and take $i^{\prime}\in\delta({d\sqcup i},{d})$ minimal. Note that minimality implies that $\mathit{p}({i^{\prime}})\sqsubseteq d$. In fact, for all $i_{1}^{\prime}\in\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}$ we have $i_{1}^{\prime}\sqsubset i^{\prime}\sqsubseteq d\sqcup i$. Hence $i_{1}^{\prime}\sqsubseteq d$, otherwise ${i_{1}^{\prime}}\in\delta({d\sqcup i},{d})$, violating minimality of $i^{\prime}$. Therefore $\mathit{p}({i^{\prime}})=\bigsqcup\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}\sqsubseteq d$.

Now, from $i^{\prime}\sqsubseteq d\sqcup i$, since $D$ is a weak prime domain and thus irreducibles are weak primes, there must be $i^{\prime\prime}\in\mathop{\mathit{ir}({D})}$, $i^{\prime\prime}\leftrightarrow i^{\prime}$ such that $i^{\prime\prime}\sqsubseteq d$ or $i^{\prime\prime}\sqsubseteq i$. We first note that it cannot be $i^{\prime\prime}\sqsubseteq d$, otherwise $d=d\sqcup i^{\prime\prime}=d\sqcup i^{\prime}$, the last equality motivated by Lemma 5(2), which implies that $i^{\prime}\sqsubseteq d$, contradicting the hypothesis. Hence it must be $i^{\prime\prime}\sqsubseteq i$, which by Lemma 2 means that either $i^{\prime\prime}=i$ or $i^{\prime\prime}\sqsubseteq\mathit{p}({i})$. Since $\mathit{p}({i})\sqsubseteq d$ by hypothesis, the latter case would contradict $i^{\prime\prime}\not\sqsubseteq d$, hence $i^{\prime\prime}=i$ which means that $i^{\prime}\leftrightarrow i$, as desired. 2. 2.

Let us assume that $d\not=d\sqcup i$ (otherwise the property is trivial), and consider $d^{\prime}$ such that $d\prec d^{\prime}\sqsubseteq d\sqcup i$: we prove that $d^{\prime}=d\sqcup i$. Since $d\prec d^{\prime}$, hence $d\neq d^{\prime}$, we know that $\delta({d^{\prime}},{d})$ is not empty. Take a minimal $i^{\prime}\in\delta({d^{\prime}},{d})$. Thus $i^{\prime}$ is minimal also in $\delta({d\sqcup i},{d})$, and thus, by point (1), $i\leftrightarrow i^{\prime}$. By minimality of $i^{\prime}$ we deduce also that $\mathit{p}({i^{\prime}})\sqsubseteq d$. Since also $\mathit{p}({i})\sqsubseteq d$ by hypothesis, using Lemma 5(2), we have $d\sqcup i=d\sqcup i^{\prime}$. Observing that $d\sqcup i^{\prime}\sqsubseteq d^{\prime}\sqsubseteq d\sqcup i$ we conclude that $d^{\prime}=d\sqcup i$, as desired.

■

We can now show that whenever $d\prec d^{\prime}$ the irreducible difference of $d^{\prime}$ and $d$ consists of a set of irreducibles which are pairwise interchangeble, hence, intuitively corresponding to the same event.

Lemma 10** (immediate precedence and irreducibles/2)**

Let $D$ be a weak prime domain and $d,d^{\prime}\in D$ such that $d\preceq d^{\prime}$. Then for all $i,i^{\prime}\in\delta({d^{\prime}},{d})$

$d^{\prime}=d\sqcup i$; 2. 2.

if $i\sqsubseteq i^{\prime}$ then $i=i^{\prime}$; 3. 3.

$i\leftrightarrow i^{\prime}$.

□

Proof

If $d=d^{\prime}$ all properties hold trivially.

1. 1)

Let $i\in\delta({d^{\prime}},{d})$. Then $d\sqsubseteq d\sqcup i\sqsubseteq d^{\prime}$. It follows that either $d\sqcup i=d$ or $d\sqcup i=d^{\prime}$. The first possibility can be excluded for the fact that it would imply $i\sqsubseteq d$, while we know that $i\not\in\mathop{\mathit{ir}({d})}$. Hence we get the thesis. 2. 2)

Let $i,i^{\prime}\in\delta({d^{\prime}},{d})$, with $i\sqsubseteq i^{\prime}$. Let us first assume $i$ minimal in $\delta({d^{\prime}},{d})$, hence $\mathit{p}({i})\sqsubseteq d$. Then $i^{\prime}\sqsubseteq d^{\prime}=d\sqcup i$. Since $i^{\prime}$ is a weak prime, there exists $i^{\prime\prime}\in\mathop{\mathit{ir}({D})}$ such that $i^{\prime}\leftrightarrow i^{\prime\prime}$ and either $i^{\prime\prime}\sqsubseteq i$ or $i^{\prime\prime}\sqsubseteq d$. The second possibility is excluded. In fact, if $i^{\prime\prime}\sqsubseteq d$, then we would have $\mathit{p}({i}),\mathit{p}({i^{\prime\prime}})\sqsubseteq d$ and thus, by Lemma 5(2), $d^{\prime}=d\sqcup i=d\sqcup i^{\prime\prime}=d$, contradicting $d\neq d^{\prime}$. Hence it must be $i^{\prime\prime}\sqsubseteq i$. Since $i\sqsubseteq i^{\prime}$, by transitivity $i^{\prime\prime}\sqsubseteq i^{\prime}$ and since $i^{\prime}\leftrightarrow i^{\prime\prime}$, by Lemma 4, $i^{\prime\prime}=i^{\prime}$ and thus $i^{\prime\prime}=i=i^{\prime}$.

If instead, $i$ is not minimal in $\delta({d^{\prime}},{d})$, take $i_{1}\sqsubseteq i$ minimal. By the argument above, we have that $i_{1}\leftrightarrow i^{\prime}$, and thus, by Lemma 4, $i_{1}=i^{\prime}$. Recalling that $i_{1}\sqsubseteq i\sqsubseteq i^{\prime}$ we conclude $i=i^{\prime}$, as desired. 3. 3)

Let $i,i^{\prime}\in\delta({d^{\prime}},{d})$ be irreducibles. By (1) we have $d^{\prime}=d\sqcup i$, hence $i^{\prime}\in\delta({d\sqcup i},{d})$. By (2) $i^{\prime}$ is minimal in $\delta({d\sqcup i},{d})$. Therefore, by Lemma 9(1), we conclude $i\leftrightarrow i^{\prime}$ .

■

We next show another technical result, i.e., that chains of immediate precedence are generated in essentially a unique way by sequences of irreducibles. Given a domain $D$ and an irreducible $i\in\mathop{\mathit{ir}({D})}$, we denote by $[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ the corresponding equivalence class. For $X\subseteq\mathop{\mathit{ir}({D})}$ we define $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=\{[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\mid i\in X\}$.

Lemma 11** (chains of immediate precedence)**

Let $D$ be a weak prime domain, $d\in\mathop{\mathsf{K}({D})}$ and $\mathop{\mathit{ir}({d})}=\{i_{1},\ldots,i_{n}\}$ such that the sequence $i_{1},\ldots,i_{n}$ is compatible with the order (i.e., for all $h,k$ if $i_{h}\sqsubseteq i_{k}$ then $h\leq k$). If we let $d_{k}=\bigsqcup_{h=1}^{k}i_{h}$ for $k\in\{1,\ldots,n\}$ we have

$\bot=d_{0}\preceq d_{1}\preceq\ldots\preceq d_{n}=d$**

Vice versa, given a chain $\bot=d_{0}\prec d_{1}\prec\ldots\prec d_{n}$ and taking $i_{h}\in\delta({d_{h}},{d_{h-1}})$ for $h\in\{1,\ldots,n\}$ we have

$d_{n}=\bigsqcup_{h=1}^{n}i_{h}$*   and   $\forall i\in\mathop{\mathit{ir}({d_{n}})}.\ \exists h\in[{1},{n}].\ i\leftrightarrow i_{h}$.*

Therefore $[{\{i_{1},\ldots,i_{n}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d_{n}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. □

Proof

For the first part, observe that for $k\in\{1,\ldots,n\}$ we have that

$\mathit{p}({i_{k}})\sqsubseteq d_{k-1}$

In fact, recalling that $\mathop{\mathit{ir}({i_{k}})}\subseteq\mathop{\mathit{ir}({d})}$, we have that irreducibles in $\mathop{\mathit{ir}({\mathit{p}({i_{k}})})}=\mathop{\mathit{ir}({i_{k}})}\setminus\{i_{k}\}$, which are smaller than $i_{k}$, must occur before in the list hence

$\mathop{\mathit{ir}({\mathit{p}({i_{k}})})}=\mathop{\mathit{ir}({i_{k}})}\setminus\{i_{k}\}\subseteq\{i_{1},\ldots,i_{k-1}\}$.

Therefore $\mathit{p}({i_{k}})=\bigsqcup\mathop{\mathit{ir}({\mathit{p}({i_{k}})})}\sqsubseteq\bigsqcup\{i_{1},\ldots,i_{k-1}\}=d_{k-1}$. Thus we use Lemma 9(2) to infer $d_{k-1}\preceq d_{k-1}\sqcup i_{k}=d_{k}$.

For the second part, we proceed by induction on $n$.

• •

($n=0$) Note that $d_{0}=\bigsqcup\emptyset=\bot$ and $\mathop{\mathit{ir}({\bot})}=\emptyset$, hence the thesis trivially holds.

• •

($n>0$) By induction hypothesis

$d_{n-1}=\bigsqcup_{h=1}^{n-1}i_{h}$   and   $\forall i\in\mathop{\mathit{ir}({d_{n-1}})}.\ \exists h\in[{1},{n-1}].\ i\leftrightarrow i_{h}$.

Since by construction $i_{n}\in\delta({d_{n}},{d_{n-1}})$, by Lemma 10(1) we deduce

$d_{n}=i_{n}\sqcup d_{n-1}={\bigsqcup_{h=1}^{n}i_{h}}$

Moreover, for all $i\in\delta({d_{n}},{d_{n-1}})$, we have $i\sqsubseteq d_{n}=i_{n}\sqcup d_{n-1}$. By definition of weak prime domain, there exists $i^{\prime}\leftrightarrow i$ such that $i^{\prime}\sqsubseteq d_{n-1}$ or $i^{\prime}\sqsubseteq i_{n}$. In the first case, since $i^{\prime}\sqsubseteq d_{n-1}$, by the inductive hypothesis there is $h\in[{1},{n-1}]$ such that $i^{\prime}\leftrightarrow i_{h}$. Since $i\leftrightarrow i^{\prime}\leftrightarrow i_{h}$, and $i,i_{h}\sqsubseteq d_{n}$ are consistent, by using the fact that $D$ is interchangeable we deduce $i\leftrightarrow i_{h}$, as desired. If, instead, we are in the second case, namely $i^{\prime}\sqsubseteq i_{n}$, by Lemma 10(2) it follows that $i_{n}=i^{\prime}\leftrightarrow i$, as desired.

■

In a prime domain, an element admits a unique decomposition in terms of primes (see Lemma 3). Here the same holds for irreducibles but only up to interchangeability.

Proposition 6** (unique decomposition up to $\leftrightarrow$)**

Let $D$ be a weak prime domain, let $d\in\mathop{\mathsf{K}({D})}$, and let $X\subseteq D$ be a downward closed and consistent set such that $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Then $d=\bigsqcup X$ iff $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. □

Proof

($\Rightarrow$) Let $d=\bigsqcup X$. By hypothesis $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Hence we only need to prove that $[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Let $i\in\mathop{\mathit{ir}({d})}$. Hence $i\sqsubseteq d=\bigsqcup X$. By definition of weak prime domain, this implies that there exists $i^{\prime}\leftrightarrow i$ and $x\in X$ such that $i^{\prime}\sqsubseteq x$. Since $X$ is downward closed, necessarily $i^{\prime}\in X$ and thus $[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, as desired.

($\Leftarrow$) Let $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. We can prove that $\bigsqcup X=d$ by induction on $k(X)=|(\mathop{\mathit{ir}({d})}\setminus X)\cup(X\setminus\mathop{\mathit{ir}({d})}|$. If $k(X)=0$ then $X=\mathop{\mathit{ir}({d})}$ and thus, by Proposition 1, we conclude that $d=\bigsqcup X$. If $k(X)>0$ we distinguish two subcases.

• •

First assume $\mathop{\mathit{ir}({d})}\setminus X\neq\emptyset$. Then take a minimal element $i\in\mathop{\mathit{ir}({d})}\setminus X$. Therefore $X^{\prime}=X\cup\{i\}$ is downward closed and, by minimality of $i$, we have $\mathit{p}({i})\sqsubseteq\bigsqcup X$. Since $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, there is $i^{\prime}\in X$ such that $i\leftrightarrow^{*}i^{\prime}$ and thus, since $\mathit{p}({i}),\mathit{p}({i^{\prime}})\sqsubseteq\bigsqcup X$ are consistent and $D$ is interchangeable, $i\leftrightarrow i^{\prime}$. Therefore

[TABLE]

Since $[{X^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and $|\mathop{\mathit{ir}({d})}\setminus X^{\prime}|=|\mathop{\mathit{ir}({d})}\setminus X|-1$, we have $k(X^{\prime})<k(X)$, and thus by inductive hypothesis $\bigsqcup X^{\prime}=d$. Hence, using (2), we get $\bigsqcup X=d$, as desired.

• •

If instead $\mathop{\mathit{ir}({d})}\setminus X=\emptyset$, i.e., $\mathop{\mathit{ir}({d})}\subseteq X$, since $k(X)>0$, it must be $X\setminus\mathop{\mathit{ir}({d})}\neq\emptyset$. Consider a maximal element $i\in X\setminus\mathop{\mathit{ir}({d})}$, and let $X^{\prime}=X\setminus\{i\}$. Clearly, $X^{\prime}$ is downward closed because so are $X$ and $\mathop{\mathit{ir}({d})}$. Since $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, there is $i^{\prime}\in\mathop{\mathit{ir}({d})}\subseteq X$ such that $i\leftrightarrow^{*}i^{\prime}$. Since $X$ is consistent and $D$ is interchangeable, $i\leftrightarrow i^{\prime}$. Therefore

[TABLE]

Since by construction $k(X^{\prime})=k(X)-1$, the inductive hypothesis gives us $\bigsqcup X^{\prime}=d$. Hence, using (3), we get $\bigsqcup X=d$, as desired.

■

We explicitly observe that, by the above result, whenever $X=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ for some $d\in\mathop{\mathsf{K}({D})}$ then $d$ is uniquely determined by $X$.

We now have all the tools needed for mapping our domains to an es.

Definition 20** (event structure for a weak prime domain)**

Let $D$ be a weak prime domain. The es $\mathcal{E}({D})=\langle E,\#,\vdash\rangle$ is defined as follows

• •

$E=[{\mathop{\mathit{ir}({D})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$;

• •

$e\#e^{\prime}$ if there is no $d\in\mathop{\mathsf{K}({D})}$ such that $e,e^{\prime}\in[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$;

• •

$X\vdash e$ if there is $i\in e$ such that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq X$.

Given a morphism $f:D_{1}\to D_{2}$, its image $\mathcal{E}({f}):\mathcal{E}({D_{1}})\to\mathcal{E}({D_{2}})$ is defined for $[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in{E_{1}}$ as $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, where $i_{2}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$, and $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is undefined if $f(\mathit{p}({i_{1}}))=f(i_{1})$. □

The events in $\mathcal{E}({D})$ are equivalence classes of irreducibles. Two events $e$, $e^{\prime}$ are consistent (not in conflict) when there is some compact element $d$ such that $e,e^{\prime}\in[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Spelled out, this means that there are irreducibles $i\in e$ and $i^{\prime}\in e^{\prime}$ such that $i,i^{\prime}\sqsubseteq d$, i.e., there are minimal enablings of the events $e$ and $e^{\prime}$ in the same configuration. Finally, an event $e$ is enabled by a set $X$ when $X$ includes, up to intechangeability, all the predecessors of $e$.

Note that the definition above is well-given: in particular, there is no ambiguity in the definition of the image of a morphism, since by Lemma 10(3) we easily conclude that for all $i_{2},i_{2}^{\prime}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$, it holds $i_{2}\leftrightarrow i_{2}^{\prime}$ (this is argued in detail in the proof of Lemma 13).

In the following we often use a technical lemma that holds in any domain.

Lemma 12

Let $D$ be a domain and $a,b,c\in D$ such that $c\sqsubseteq a$ and $c\preceq b$. Then either $b\sqsubseteq a$ or $c=a\sqcap b$. □

Proof

Recall that in a domain the meet of non-empty sets exists. Since $c$ is a lower bound for $a$ and $b$, necessarily $c\sqsubseteq a\sqcap b\sqsubseteq b$. If it were $c\neq a\sqcap b$ then we would have $a\sqcap b=b$, hence $b\sqsubseteq a$, as desired. ■

Lemma 13** (from weak prime domains to event structures)**

Let $D$ be a weak prime domain. Then $\mathcal{E}({D})$ is an es. Moreover, given two weak prime domains $D_{1}$, $D_{2}$ and a morphism $f:D_{1}\to D_{2}$, its image $\mathcal{E}({f}):\mathcal{E}({D_{1}})\to\mathcal{E}({D_{2}})$ is an es morphism. □

Proof

We first show that $\mathcal{E}({D})$ is a live es. In fact, it is an es: if $X\vdash e$ and $X\subseteq Y$ then $Y\vdash e$. In fact, by definition, if $X\vdash e$ then there exists $i\in e$ such that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq X$. Hence if $X\subseteq Y$ it immediately follows that $Y\vdash e$. Moreover $\mathcal{E}({D})$ is live. The fact that conflict is saturated follows immediately by the definition of conflict and the characterisation of configurations provided later in Lemma 14. Conflict is irreflexive since for any $e\in\mathcal{E}({D})$, if $e=[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ then $e\in[{\mathop{\mathit{ir}({i})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, which is a configuration again by Lemma 14.111This forward reference is only useful to simplify the structure of the presentation and to avoid breaking the statement in two parts, but it introduces no cyclic dependency.

Given a morphism $f:D_{1}\to D_{2}$, its image $\mathcal{E}({f}):\mathcal{E}({D_{1}})\to\mathcal{E}({D_{2}})$ is defined for $[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in{E_{1}}$ as $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, where $i_{2}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$, and $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is undefined if $f(\mathit{p}({i_{1}}))=f(i_{1})$. First observe that $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ does not depend on the choice of the representative. In fact, let $i_{2},i_{2}^{\prime}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$. Since $\mathit{p}({i_{1}})\prec i_{1}$, by definition of domain morphism, $f(\mathit{p}({i_{1}}))\prec f(i_{1})$. Thus, by Lemma 10(3), $i_{2}\leftrightarrow i_{2}^{\prime}$.

We next show that $\mathcal{E}({f})$ is an es morphism.

• •

If $\mathcal{E}({f})(e_{1})\#\mathcal{E}({f})(e_{1}^{\prime})$ then $e_{1}\#e_{1}^{\prime}$.

We prove the contronominal, namely if $e_{1},e_{1}^{\prime}$ consistent then $\mathcal{E}({f})(e_{1}),\mathcal{E}({f})(e_{1}^{\prime})$ consistent.

The fact that $e_{1},e_{1}^{\prime}$ consistent means that there exists $d_{1}\in\mathop{\mathsf{K}({D_{1}})}$ such that $e_{1},e_{1}^{\prime}\in[{\mathop{\mathit{ir}({d_{1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. We show that $\mathcal{E}({f})(e_{1}),\mathcal{E}({f})(e_{1}^{\prime})\in[{\mathop{\mathit{ir}({f(d_{1})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ (note that $f(d_{1})$ is a compact, since $f$ is a domain morphism).

Let us show, for instance, that $\mathcal{E}({f})(e_{1})\in[{\mathop{\mathit{ir}({f(d_{1})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. The fact that $e_{1}\in[{\mathop{\mathit{ir}({d_{1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ means that $e_{1}=[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ for some $i_{1}\sqsubseteq d_{1}$. By definition $\mathcal{E}({f})(e_{1})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, where $i_{2}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$ (since $\mathcal{E}({f})(e_{1})$ is defined the irreducible difference cannot be empty). Now, since $i_{1}\sqsubseteq d_{1}$ we have that $f(i_{1})\sqsubseteq f(d_{1})$, whence $i_{2}\sqsubseteq f(i_{1})\sqsubseteq f(d_{1})$ and $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in[{\mathop{\mathit{ir}({f(d_{1})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, as desired.

• •

If $\mathcal{E}({f})(e_{1})=\mathcal{E}({f})(e_{1}^{\prime})$ and $e_{1}\neq e_{1}^{\prime}$ then $e_{1}\#e_{1}^{\prime}$.

We prove the contronominal, namely if $e_{1},e_{1}^{\prime}$ consistent and $\mathcal{E}({f})(e_{1})=\mathcal{E}({f})(e_{1}^{\prime})$ then $e_{1}=e_{1}^{\prime}$.

Assume $e_{1},e_{1}^{\prime}$ consistent and $\mathcal{E}({f})(e_{1})=\mathcal{E}({f})(e_{1}^{\prime})$. By the first condition and the definition of conflict, there must be $d_{1}\in\mathop{\mathsf{K}({D_{1}})}$ such that $e_{1},e_{1}^{\prime}\in[{\mathop{\mathit{ir}({d_{1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, namely $e_{1}=[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and ${e_{1}^{\prime}}=[{i_{1}^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ with $i_{1},i_{1}^{\prime}\sqsubseteq d_{1}$.

Moreover, $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and $\mathcal{E}({f})([{i_{1}^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ where $i_{2}$ and $i_{2}^{\prime}$ are in $\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$ and $\delta({f(i_{1}^{\prime})},{f(\mathit{p}({i_{1}^{\prime}}))})$, respectively, and $[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{i_{2}^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, which means $i_{2}\leftrightarrow^{*}i_{2}^{\prime}$, and in turn, being $i_{2}$ and $i_{2}^{\prime}$ consistent, by the fact that $D$ is interchangeable, implies $i_{2}\leftrightarrow i_{2}^{\prime}$.

We distinguish two cases.

1. A.

If $i_{1}$ and $i_{1}^{\prime}$ are comparable, e.g., if $i_{1}\sqsubseteq i_{1}^{\prime}$, then $i_{1}=i_{1}^{\prime}$ and we are done. In fact, otherwise, if $i_{1}\neq i_{1}^{\prime}$ we have $\mathit{p}({i_{1}})\prec i_{1}\sqsubseteq\mathit{p}({i_{1}^{\prime}})\prec i_{1}^{\prime}$. By monotonicity of $f$ we have $f(\mathit{p}({i_{1}}))\prec f(i_{1})\sqsubseteq f(\mathit{p}({i_{1}^{\prime}}))\prec f(i_{1}^{\prime})$ (where strict inequalities $\prec$ are motivated by the definition of $\mathcal{E}({f})$, since both $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ and $\mathcal{E}({f})([{i_{1}^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ are defined). Now notice that $\mathit{p}({i_{2}})\sqsubseteq i_{2}\sqsubseteq f(i_{1})\sqsubseteq f(\mathit{p}({i_{1}^{\prime}}))$. Moreover, $i_{2}^{\prime}\in\delta({f(i_{1}^{\prime})},{f(\mathit{p}({i_{1}^{\prime}}))})$, therefore $\mathit{p}({i_{2}^{\prime}})\sqsubseteq i_{2}^{\prime}\sqsubseteq f(\mathit{p}({i_{1}^{\prime}}))$. Hence, using the fact that $i_{2}\leftrightarrow i_{2}^{\prime}$, by Lemma 5(2) we have

$f(\mathit{p}({i_{1}^{\prime}}))=f(\mathit{p}({i_{1}^{\prime}}))\sqcup i_{2}=f(\mathit{p}({i_{1}^{\prime}}))\sqcup i_{2}^{\prime}=f(i_{1}^{\prime})$

contradicting the fact that $f(\mathit{p}({i_{1}^{\prime}}))\prec f(i_{1}^{\prime})$. 2. B.

Assume now that $i_{1}$ and $i_{1}^{\prime}$ are uncomparable: we show that this leads to a contradiction. Let $p=\mathit{p}({i_{1}})\sqcup\mathit{p}({i_{1}^{\prime}})$. We can also assume $i_{1},i_{1}^{\prime}\not\sqsubseteq p$. In fact, otherwise, e.g., if $i_{1}\sqsubseteq p$, then, by the defining property of weak prime domains, we derive the existence of $i_{1}^{\prime\prime}\leftrightarrow i_{1}$ such that $i_{1}^{\prime\prime}\sqsubseteq\mathit{p}({i_{1}})$ or $i_{1}^{\prime\prime}\sqsubseteq\mathit{p}({i^{\prime}_{1}})$. The first possibility can be excluded because it would imply $i_{1}^{\prime\prime}\sqsubseteq i_{1}$. Hence, since $i_{1}^{\prime\prime}\leftrightarrow i_{1}$, by Lemma 4, we would get $i_{1}=i_{1}^{\prime\prime}$, contradicting $i_{1}^{\prime\prime}\sqsubseteq\mathit{p}({i_{1}})$. Then it should be $i_{1}^{\prime\prime}\sqsubseteq\mathit{p}({i_{1}^{\prime}})\sqsubseteq i_{1}^{\prime}$. Therefore, if we take $i_{1}^{\prime\prime}$ as representative of the equivalence class we are back to case A above.

Using the fact that $i_{1},i_{1}^{\prime}\not\sqsubseteq p$ and $\mathit{p}({i_{1}}),\mathit{p}({i_{1}^{\prime}})\sqsubseteq p$, by Lemma 9(2) we deduce that $p\prec p\sqcup i_{1}$ and $p\prec p\sqcup i_{1}^{\prime}$. Hence $f(p)\prec f(p\sqcup i_{1})$ with strict inequality again motivated by the definition of $\mathcal{E}({f})$, since $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is defined.

By Lemma 10(1), since $i_{2}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$ and $i_{2}^{\prime}\in\delta({f(i_{1}^{\prime})},{f(\mathit{p}({i_{1}^{\prime}}))})$, we have

[TABLE]

Now, observe that

\begin{array}[]{lll}f(p\sqcup i_{1})=\\ =f(\mathit{p}({i_{1}})\sqcup\mathit{p}({i_{1}^{\prime}})\sqcup i_{1})\\ =f(\mathit{p}({i_{1}^{\prime}})\sqcup i_{1})\\ =f(\mathit{p}({i_{1}^{\prime}}))\sqcup f(i_{1})&\mbox{[preservation of \sqcup]}\\ =f(\mathit{p}({i_{1}^{\prime}}))\sqcup f(\mathit{p}({i_{1}}))\sqcup i_{2}&\mbox{[by~{}(\ref{eq:adding})]}\\ =f(\mathit{p}({i_{1}^{\prime}}))\sqcup f(\mathit{p}({i_{1}}))\sqcup i_{2}^{\prime}&\mbox{[by Lemma~{}\ref{le:eq-char}(\ref{le:eq-char:3}),}\\ &\mbox{\ since i_{2}\leftrightarrow i_{2}^{\prime}]}\\ =f(i_{1}^{\prime})\sqcup f(\mathit{p}({i_{1}}))&\mbox{[by~{}(\ref{eq:adding})]}\\ =f(\mathit{p}({i_{1}})\sqcup i_{1}^{\prime})&\mbox{[preservation of \sqcup]}\\ =f(\mathit{p}({i_{1}})\sqcup\mathit{p}({i_{1}^{\prime}})\sqcup i_{1}^{\prime})\\ =f(p\sqcup i_{1}^{\prime})\\ \end{array}

Since $p\prec p\sqcup i_{1}$ and $p\prec p\sqcup i_{1}^{\prime}$, by Lemma 12, we have $(p\sqcup i_{1})\sqcap(p\sqcup i_{1}^{\prime})=p$. Therefore, on the one hand $f((p\sqcup i_{1})\sqcap(p\sqcup i_{1}^{\prime}))=f(p)$. On the other hand, since the meet is an immediate predecessor, by definition of weak domain morphism (Definition 15), it is preserved: $f((p\sqcup i_{1})\sqcap(p\sqcup i_{1}^{\prime}))=f(p\sqcup i_{1})\sqcap f(p\sqcup i_{1}^{\prime})=f(p\sqcup i_{1})=f(p\sqcup i_{1}^{\prime})$. Putting things together, $f(p)=f(p\sqcup i_{1})=f(p\sqcup i_{1}^{\prime})$, contradicting the fact that $f(p)\prec f(p\sqcup i_{1})$.

• •

if $C_{1}\vdash_{1}[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is defined then $\mathcal{E}({f})(C_{1})\vdash_{2}\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$

Recall that $C_{1}\vdash_{1}[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ means that $[{\mathop{\mathit{ir}({i_{1}^{\prime}})}\setminus\{i_{1}^{\prime}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({\mathit{p}({i_{1}^{\prime}})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq C_{1}$ for some $i_{1}^{\prime}\leftrightarrow i_{1}$.

By definition, $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ where $i_{2}\in\delta({f(i_{1}^{\prime})},{f(\mathit{p}({i_{1}^{\prime}}))})$. We show that $\mathcal{E}({f})(C_{1})\vdash_{2}[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, namely that

[TABLE]

Observe that since $i_{2}\in\delta({f(i_{1}^{\prime})},{f(\mathit{p}({i_{1}^{\prime}}))})$ and distinct elements in $\delta({f(i_{1}^{\prime})},{f(\mathit{p}({i_{1}^{\prime}}))})$ are incomparable by Lemma 10(2), it holds $\mathit{p}({i_{2}})\sqsubseteq f(\mathit{p}({i_{1}^{\prime}}))$. Therefore, we have

$\mathop{\mathit{ir}({\mathit{p}({i_{2}})})}\subseteq\mathop{\mathit{ir}({f(\mathit{p}({i_{1}^{\prime}}))})}$

Hence, in order to conclude (5), it suffices to show that

[TABLE]

In order to reach this result, first note that, by Lemma 11, if $\mathop{\mathit{ir}({\mathit{p}({i_{1}^{\prime}})})}=\{j_{1}^{1},\ldots,j_{1}^{n}\}$ is a sequence of irreducibles compatible with the order, we can obtain a $\preceq$-chain

$\bot=d_{1}^{0}\preceq d_{1}^{1}\preceq\ldots\preceq d_{1}^{n}=\mathit{p}({i_{1}^{\prime}})\prec i_{1}^{\prime}$

We can extract a strictly increasing subsequence

$\bot=d_{1}^{\prime 0}\prec d_{1}^{\prime 1}\prec\ldots\prec d_{1}^{\prime m}=\mathit{p}({i_{1}^{\prime}})\prec i_{1}^{\prime}$

and, if we take irreducibles $j_{1}^{\prime 1},\ldots,j_{1}^{\prime m}$ in $\delta({d_{1}^{\prime i}},{d_{1}^{\prime i-1}})$, again by Lemma 11 we know that

[TABLE]

Since $f$ is a domain morphism, it preserves $\preceq$, namely

$\bot=f(d_{1}^{\prime 0})\preceq f(d_{1}^{\prime 1})\preceq\ldots\preceq f(d_{1}^{\prime m})=f(\mathit{p}({i_{1}^{\prime}}))\prec f(i_{1}^{\prime})$

where the last inequality is strict since $\mathcal{E}({f})([{i_{1}^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ is defined. Moreover, whenever $f(d_{1}^{\prime h-1})\prec f(d_{1}^{\prime h})$, then $\mathcal{E}({f})([{j_{1}^{\prime h}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{\ell_{2}^{h}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ where $\ell_{2}^{h}$ is any irreducible in $\delta({f(d_{1}^{\prime h})},{f(d_{1}^{\prime h-1})})$, otherwise $\mathcal{E}({f})([{j_{1}^{\prime h}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is undefined.

Once more by Lemma 11 we know that

$[{\mathop{\mathit{ir}({f(\mathit{p}({i_{1}^{\prime}}))})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\{\ell_{2}^{1},\ldots,\ell_{2}^{m}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=\mathcal{E}({f})([{\{j_{1}^{\prime 1},\ldots,j_{1}^{\prime m}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$,

thus, using (7)

[TABLE]

Hence, recalling that, by hypothesis, $[{\mathop{\mathit{ir}({\mathit{p}({i_{1}^{\prime}})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq C_{1}$, we conclude the desired inclusion (6).

■

Since in a prime domain irreducibles coincide with primes (Proposition 2), $\leftrightarrow$ is the identity (Lemma 6) and $\delta({d^{\prime}},{d})$ is a singleton when $d\prec d^{\prime}$, the construction above produces the prime es $\mathsf{pES}(D)$ as defined in Section II.

Given a weak prime domain $D$, the finite configurations of the es $\mathcal{E}({D})$ exactly correspond to the elements in $\mathop{\mathsf{K}({D})}$. Moreover, in such es we have a minimal enabling $C\vdash_{0}e$ when there is an irreducible in $e$ (recall that events are equivalence classes of irreducibles) such that $C$ contains all and only (the equivalence classes of) its predecessors.

Lemma 14** (compacts vs. configurations)**

Let $D$ be a weak prime domain and $C\subseteq\mathcal{E}({D})$ a finite set of events. Then $C$ is a configuration in the es $\mathcal{E}({D})$ iff there exists a unique $d\in\mathop{\mathsf{K}({D})}$ such that $C=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Moreover, for any $e\in\mathcal{E}({D})$ we have that $C\vdash_{0}e$ iff $C=[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ for some $i\in e$. □

Proof

The left to right implication of the first part follows by proving that, given a configuration $C\in\mathit{Conf_{F}}({\mathcal{E}({D})})$, there exists $X\subseteq\mathop{\mathit{ir}({D})}$ downward closed and consistent such that $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=C$. Hence, if we let $d=\bigsqcup X$, by Proposition 6, we have that $C=[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Moreover, $d$ is uniquely determined, since, by the same proposition we have that for any other $X^{\prime}$ such that $[{X^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=C$, since $[{X^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=C=[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, necessarily $d=\bigsqcup X^{\prime}$.

Let us thus prove the existence of $X\subseteq\mathop{\mathit{ir}({D})}$ consistent and downward closed such that $[{X}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=C$. We proceed by induction on the cardinality of $C$.

• •

if $|C|=0$, namely $C=\emptyset$ then we can take $X=\emptyset$, and trivially conclude.

• •

if $|C|>0$, since $C$ is secured, there is $[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in C$ such that $C^{\prime}=C\setminus\{[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\}\vdash[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. By inductive hypothesis there is $X^{\prime}\subseteq\mathop{\mathit{ir}({D})}$, downward closed and consistent such that $[{X^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=C^{\prime}$.

The fact that $C^{\prime}=C\setminus\{[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\}\vdash[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ means that for some $i^{\prime}\in\mathop{\mathit{ir}({D})}$ such that $i^{\prime}\leftrightarrow^{*}i$, it holds $[{\mathop{\mathit{ir}({i^{\prime}})}\setminus\{i^{\prime}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq C^{\prime}$. Therefore, there is $X^{\prime\prime}\subseteq X^{\prime}$ such that $[{X^{\prime\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({\mathit{p}({i})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and thus, by Proposition 6, $\mathit{p}({i^{\prime}})\sqsubseteq\bigsqcup X^{\prime}$. We can assume, without loss of generality that $\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}\subseteq X^{\prime}$. If not, we can replace $X^{\prime}$ by $X^{\prime}\cup\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}$. By the consideration above, it is consistent and it has the same join of $X^{\prime}$.

Now, an induction on the cardinality $k$ of $X^{\prime}\setminus\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}$ allows us to show that $\{i^{\prime},j\}$ consistent for all $j\in X^{\prime}$. If $k=0$ then $X^{\prime}\setminus\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}=\emptyset$ and the thesis is trivial. Otherwise, consider $j^{\prime}\in X^{\prime}\setminus\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}$ maximal and $X^{\prime\prime}=X^{\prime}\setminus\{j^{\prime}\}$. Since $|X^{\prime}\setminus\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}|=k-1$, by inductive hypothesis, for all $j\in X^{\prime\prime}$, we have $\{j,i^{\prime}\}$ consistent. Now, since $j,\mathit{p}({i})\sqsubseteq\bigsqcup X^{\prime}$, we have that $\{j,\mathit{p}({i})\}$ is consistent. Moreover, since $\mathop{\mathit{ir}({j^{\prime}})}\setminus\{j^{\prime}\}=\mathop{\mathit{ir}({\mathit{p}({j^{\prime}})})}\subseteq X^{\prime\prime}$, we have that $\{i,\mathit{p}({j^{\prime}})\}$ is consistent.

Finally, recalling that, since $C$ is consistent, we have that $\neg([{j^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\#[{i^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$, i.e., there is $d\in\mathop{\mathsf{K}({D})}$ such that $\{[{j^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}},[{i^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\}\subseteq[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. More explicitly, this means that there are $j^{\prime\prime},i^{\prime\prime}\in\mathop{\mathit{ir}({D})}$ such that $j^{\prime\prime}\leftrightarrow^{*}j^{\prime}$, $i^{\prime\prime}\leftrightarrow^{*}i^{\prime}$ and $j^{\prime},i^{\prime\prime}$ consistent. Since $D$ is interchangeable, by condition (2) of Definition 12, we conlcude $j^{\prime},i^{\prime}$ consistent.

We can thus conclude that $X=X^{\prime}\cup\{i^{\prime}\}$ is consistent, and downward closed since $\mathop{\mathit{ir}({\mathit{p}({i^{\prime}})})}\subseteq X^{\prime}$. Hence we conclude.

For the converse, let $C=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Let $\bot=d_{0}\prec d_{1}\prec\ldots d_{n-1}\prec d_{n}=d$ be a chain of immediate precedence and for each $h\in\{1,\ldots,n\}$ take $i_{h}\in\delta({d_{h}},{d_{h-1}})$. By Lemma 11, $d=\bigsqcup\{i_{1},\ldots,i_{n}\}$ and $[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\{i_{1},\ldots,i_{n}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Moreover, for all $h\in\{1,\ldots,n\}$, we have $[{\mathop{\mathit{ir}({i_{h}})}\setminus\{i_{h}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq[{\mathop{\mathit{ir}({d_{h-1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, hence $[{\mathop{\mathit{ir}({d_{h-1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\vdash[{i_{h}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Therefore $C$ is secured. Moreover, it is clearly consistent and thus $C\in\mathit{Conf}({\mathcal{E}({D})})$.

The second part follows immediately by Definition 20. ■

Given the lemma above, it is now possible to state how weak prime domains relate to connected es.

Proposition 7** (from weak prime domains to connected ES)**

Let $D$ be a weak prime domain. Then $\mathcal{E}({D})$ is a connected es. □

Proof

We have to show that if $X\vdash_{0}e$ and $X^{\prime}\vdash_{0}e$, then $X\stackrel{{\scriptstyle e}}{{\frown}}^{*}X^{\prime}$. Note that, by Lemma 14, from $X\vdash_{0}e$ and $X^{\prime}\vdash_{0}e$, we deduce that there exists $i,i^{\prime}\in e$ such that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=X$ and $[{\mathop{\mathit{ir}({i^{\prime}})}\setminus\{i^{\prime}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=X^{\prime}$. Since $i,i^{\prime}\in e$ we deduce that $i\leftrightarrow^{*}i^{\prime}$, namely $i=i_{0}\leftrightarrow i_{1}\leftrightarrow\ldots\leftrightarrow i_{n}=i^{\prime}$. We proceed by induction on $n$. The base case $n=0$ is trivial. If $n>0$ then from $i\leftrightarrow i_{1}\leftrightarrow^{*}i^{\prime}$ we have that $i_{1}\in e$ and, if we let $X_{1}=[{\mathop{\mathit{ir}({i_{1}})}\setminus\{i_{1}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, then $X_{1}\vdash_{0}e$. By inductive hypothesis, we know that $X_{1}\stackrel{{\scriptstyle e}}{{\frown}}^{*}X^{\prime}$. Moreover, since $i\leftrightarrow i_{1}$, the irreducibles $i$ and $i_{1}$ are consistent. Hence, by definition of conflict in $\mathcal{E}({D})$, also $X\cup X_{1}\cup\{e\}$ is consistent and hence $X\stackrel{{\scriptstyle e}}{{\frown}}X_{1}$. Therefore $X\stackrel{{\scriptstyle e}}{{\frown}}^{*}X^{\prime}$, as desired. ■

III-D Relating Categories of Models

We show that, at a categorical level, the constructions taking a weak prime domain to an es and an es to a domain (the domain of its configurations) establish a coreflection between the corresponding categories. This becomes an equivalence when it is restricted to the full subcategory of connected es.

Theorem 3** (coreflection of $\mathsf{ES}$ and $\mathsf{wDom}$)**

The functors $\mathcal{D}:\mathsf{ES}\to\mathsf{wDom}$ and $\mathcal{E}:\mathsf{wDom}\to\mathsf{ES}$ form a coreflection $\mathcal{E}\dashv\mathcal{D}$. It restricts to an equivalence between $\mathsf{wDom}$ and $\mathsf{cES}$. □

Proof

Let ${E}$ be an es. Recall that the corresponding domain of configurations is $\mathcal{D}({{E}})=\langle\mathit{Conf}({{E}}),\subseteq\rangle$. Then, $\mathcal{E}({\mathcal{D}({{E}})})=\langle E^{\prime},\#^{\prime},\vdash^{\prime}\rangle$, where the set of events $E^{\prime}$ is defined as

$E^{\prime}=[{\mathop{\mathit{ir}({\mathcal{D}({{E}})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=\{[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\mid C\vdash_{0}e\}$

By Lemma 8(4), the equivalence class of an irreducible $\langle{C},{e}\rangle$ consists of all minimal enablings of event $e$ which are connected. Therefore we can define a morphism, which is the counit of the adjunction, as follows:

\begin{array}[]{lccc}\theta_{{E}}:&\mathcal{E}({\mathcal{D}({{E}})})&\to&{E}\\ &[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}&\mapsto&e\end{array}

Observe that $\theta_{{E}}$ is surjective. In fact ${E}$ is live and thus any event $e\in E$ has at least a minimal enabling $C\vdash_{0}e$. If we let $I=\langle{C},{e}\rangle$, then $[{I}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in\mathcal{E}({\mathcal{D}({{E}})})$ and $\theta_{{E}}([{I}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=e$. The mapping $\theta_{E}$ is clearly a morphism of event structures. In fact, observe that

• •

For $I_{1},I_{2}\in\mathop{\mathit{ir}({\mathcal{D}({{E}})})}$, if $\theta_{{E}}([{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})\#\theta_{{E}}([{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ then $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\#^{\prime}[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$.

Let $I_{1}=\langle{C_{1}},{e_{1}}\rangle$ and $I_{2}=\langle{C_{2}},{e_{2}}\rangle$. If $\theta_{{E}}([{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=e_{1}\#e_{2}=\theta_{{E}}([{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$, then there cannot be any configuration $C\in\mathit{Conf}({{E}})$ such that $I_{1},I_{2}\subseteq C$. Hence, by definition of conflict in $\mathcal{E}({\mathcal{D}({{E}})})$, we have $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\#^{\prime}[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$.

• •

For $I_{1},I_{2}\in\mathop{\mathit{ir}({\mathcal{D}({{E}})})}$, with $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\neq[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, we have that $\theta_{{E}}([{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=\theta_{{E}}([{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ implies $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\#^{\prime}[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$.

In fact, by Lemma 8(2), the irreducibles $I_{1}$ and $I_{2}$ are of the kind $I_{1}=\langle{C_{1}},{e_{1}}\rangle$ and $I_{2}=\langle{C_{2}},{e_{2}}\rangle$. We show that if $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and $[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ are consistent and $\theta_{{E}}([{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=\theta_{{E}}([{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ then $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$.

Assume $\theta_{{E}}([{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=\theta_{{E}}([{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$, hence $e_{1}=e_{2}$. Since $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and $[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ are consistent, there exists $k\in\mathop{\mathsf{K}({\mathcal{D}({{E}})})}$ such that $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}},[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in[{\mathop{\mathit{ir}({k})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Compacts in $\mathcal{D}({{E}})$ are finite configurations, hence the condition amounts to the existence of $C\in\mathit{Conf_{F}}({{E}})$ such that $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}},[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in[{\mathop{\mathit{ir}({C})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, i.e., there are $I_{1}^{\prime},I_{2}^{\prime}$ with $I_{i}\leftrightarrow^{*}I_{i}^{\prime}$ for $i\in\{1,2\}$, such that $I_{1}^{\prime},I_{2}^{\prime}\subseteq C$. Since the choice of the representatives is irrelevant, we can assume that $I_{1}=I_{1}^{\prime}$ and $I_{2}=I_{2}^{\prime}$. Summing up, $I_{1}$ and $I_{2}$ are consistent minimal enablings of the same event, hence by Lemma 8(4), $I_{1}\leftrightarrow I_{2}$, i.e., $[{I_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{I_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, as desired.

• •

For the enabling relation, we have to show that if $X\vdash^{\prime}[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ then $\theta_{E}(X)\vdash\theta([{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=e$. Assume $X\vdash^{\prime}[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. According to the definition of the functor ${\mathcal{E}}$, this means that there exists $i\in[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ such that ${[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq X}$. Let such $i\in[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ be $i=\langle{C^{\prime}},{e}\rangle$ with $C^{\prime}\vdash_{0}{e}$. We have

$\mathop{\mathit{ir}({\langle{C^{\prime}},{e}\rangle})}\setminus\{\langle{C^{\prime}},{e}\rangle\}=\mathop{\mathit{ir}({C^{\prime}})}=\{[{\langle{C^{\prime\prime}},{e^{\prime\prime}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\mid\langle{C^{\prime\prime}},{e^{\prime\prime}}\rangle\subseteq C^{\prime}\}$.

Therefore from $[{\mathop{\mathit{ir}({\langle{C^{\prime}},{e^{\prime}}\rangle})}\setminus\{\langle{C^{\prime}},{e^{\prime}}\rangle\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq X$ we deduce

$\theta_{E}([{\mathop{\mathit{ir}({\langle{C^{\prime}},{e^{\prime}}\rangle})}\setminus\{\langle{C^{\prime}},{e^{\prime}}\rangle\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=C^{\prime}\subseteq\theta_{E}(X)$.

Since $C^{\prime}\vdash_{0}e$, by monotonicity of enabling, we conclude $\theta_{E}(X)\vdash e$, as desired.

We prove the naturality of $\theta$ by showing that the diagram below commutes.

{\mathcal{E}({\mathcal{D}({{E}_{1}})})}$${{{E}_{1}}}$${\mathcal{E}({\mathcal{D}({{E}_{2}})})}$${{{E}_{2}}}$$\scriptstyle{\mathcal{E}({\mathcal{D}({f})})}$$\scriptstyle{\theta_{{E}_{1}}}$$\scriptstyle{f}$$\scriptstyle{\theta_{{E}_{2}}}

Consider $[{\langle{C_{1}},{e_{1}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in\mathcal{E}({\mathcal{D}({{E}_{1}})})$. Recall that $\mathcal{E}({\mathcal{D}({f})})([{\langle{C_{1}},{e_{1}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is computed by considering the image of the irreducible $\langle{C_{1}},{e_{1}}\rangle$ and of its predecessor, namely

$\mathcal{D}({f})(C_{1})=f(C_{1})$ and $\mathcal{D}({f})(\langle{C_{1}},{e_{1}}\rangle)=f(C_{1}\cup\{e_{1}\})$

If $f(e_{1})$ is defined, then $f(C_{1})\prec f(C_{1}\cup\{e_{1}\})$ and $\mathcal{E}({\mathcal{D}({f})})([{\langle{C_{1}},{e_{1}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=f(e_{1})$, otherwise $\mathcal{E}({\mathcal{D}({f})})([{\langle{C_{1}},{e_{1}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is undefined. This means that in all cases, as desired

$\mathcal{E}({\mathcal{D}({f})})([{\langle{C_{1}},{e_{1}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=f(e_{1})=f(\theta_{{E}_{1}}([{\langle{C_{1}},{e_{1}}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}))$.

Vice versa, let $D$ be a weak prime domain. Recall from Definition 20 that $\mathcal{E}({D})=\langle E,\#,\vdash\rangle$ is defined as:

• •

$E=[{\mathop{\mathit{ir}({D})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$

• •

$e\#e^{\prime}$ if there is no $d\in\mathop{\mathsf{K}({D})}$ such that $e,e^{\prime}\in[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$;

• •

$X\vdash e$ if there exists $i\in e$ such that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq X$.

and consider $\mathcal{D}({\mathcal{E}({D})})$. Elements of $\mathop{\mathsf{K}({\mathcal{D}({\mathcal{E}({D})})})}$ are configurations of $C\in\mathit{Conf_{F}}({\mathcal{E}({D})})$. We can define the unit of the adjunction as

\begin{array}[]{lccc}\eta_{D}:&\mathop{\mathsf{K}({D})}&\to&\mathop{\mathsf{K}({\mathcal{D}({\mathcal{E}({D})})})}\\ &d&\mapsto&[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\end{array}

Observe that it is well defined, since by Lemma 14, $[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ is a finite configuration of $\mathcal{E}({D})$ and thus a compact element in $\mathop{\mathsf{K}({\mathcal{D}({\mathcal{E}({D})})})}$. The function is clearly monotone and bijective with inverse $\eta_{D}^{-1}:\mathop{\mathsf{K}({\mathcal{D}({\mathcal{E}({D})})})}\to\mathop{\mathsf{K}({D})}$ defined, for $C\in\mathop{\mathsf{K}({\mathcal{D}({\mathcal{E}({D})})})}=\mathit{Conf_{F}}({\mathcal{E}({D})})$ by letting $\eta_{D}^{-1}(C)=d$, where $d$ is the unique element, given by Lemma 14, such that $C=[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. By algebraicity of the domains, this function thus uniquely extends to an isomorphism $\eta_{D}:D\to\mathcal{D}({\mathcal{E}({D})})$.

Finally, we prove the naturality of $\eta_{D}$. It is convenient to prove the naturality of the inverse, i.e., to show that the diagram below commutes.

{\mathcal{D}({\mathcal{E}({D_{1}})})}$${D_{1}}$${\mathcal{D}({\mathcal{E}({D_{2}})})}$${D_{2}}$$\scriptstyle{\mathcal{D}({\mathcal{E}({f})})}$$\scriptstyle{\eta_{D_{1}}^{-1}}$$\scriptstyle{f}$$\scriptstyle{\eta_{D_{2}}^{-1}}

Let $C_{1}\in\mathop{\mathsf{K}({\mathcal{D}({\mathcal{E}({D_{1}})})})}$, namely $C_{1}\in\mathit{Conf_{F}}({\mathcal{E}({D_{1}})})$, and let $\eta_{D_{1}}^{-1}(C_{1})=d_{1}$ be the element such that $C_{1}=[{\mathop{\mathit{ir}({d_{1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$.

The construction offered by Lemma 11 provides a chain

${d^{0}_{1}}=\bot\prec d_{1}^{1}\prec d_{1}^{2}\prec\ldots\prec d_{1}^{n}=d_{1}$

and, by the same lemma, if we take an irreducible $i_{1}^{h}\in\delta({d_{1}^{h}},{d_{1}^{h-1}})$ for $1\leq h\leq n$ we have that $C_{1}=[{\mathop{\mathit{ir}({d_{1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\{i_{1}^{1},\ldots,i_{1}^{n}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Therefore the image

$\mathcal{D}({\mathcal{E}({f})})(C_{1})=\{\mathcal{E}({f})([{j_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})\mid[{j_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in C_{1}\}=\{\mathcal{E}({f})([{i_{1}^{h}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})\mid h\in[{1},{n}]\}$

is the set of equivalence classes of irreducibles $i_{2}^{1},\ldots,i_{2}^{k}$ corresponding to

$f(d_{1}^{0})=\bot\prec f(d_{1}^{1})\prec f(d_{1}^{2})\prec\ldots\prec f(d_{1}^{n})=f(d_{1})$

namely $i_{2}^{j}\in\delta({f(d_{1}^{j})},{f(d_{1}^{j-1})})$, and, again, by Lemma 11, $[{\{i_{2}^{1},\ldots,i_{2}^{k}\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{\mathop{\mathit{ir}({f(d_{1})})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Summing up

$\eta_{D_{2}}^{-1}(\mathcal{D}({\mathcal{E}({f})})(C_{1}))=\eta_{D_{2}}^{-1}(\{[{i_{2}^{h}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\mid 1\leq h\leq k\}\})=f(d_{1})=f(\eta_{D_{1}}^{-1}(C_{1}))$

as desired.

We finally show that the above coreflection restricts to an equivalence between $\mathsf{wDom}$ and $\mathsf{cES}$. For this, just observe that, in the proof above, when ${E}$ is a connected es, then the morphism $\theta_{E}$ defined as

\begin{array}[]{lccc}\theta_{{E}}:&\mathcal{E}({\mathcal{D}({{E}})})&\to&{E}\\ &[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}&\mapsto&e\end{array}

is an isomorphism. We already know that it is surjective. We next show that it is also injective. In fact, if $\theta_{{E}}([{I}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=\theta_{{E}}([{I^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ then $I$ and $I^{\prime}$ are minimal enablings of the same event, i.e., $I=[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and $I^{\prime}=[{\langle{C^{\prime}},{e}\rangle}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Since ${E}$ is a weak prime domain, $C\stackrel{{\scriptstyle e}}{{\frown}}^{*}C^{\prime}$ and thus, by Lemma 8(4), $I\leftrightarrow^{*}I^{\prime}$, i.e., $[{I}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=[{I^{\prime}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$. Proving that also the inverse is an es morphism is immediate, by exploiting the fact that the es is live. ■

The above result indirectly provides a way of turning a general es into a connected es.

Corollary 1** (from general to connected es)**

The functors $\mathcal{C}:\mathsf{ES}\to\mathsf{cES}$ defined by $\mathcal{C}=\mathcal{E}\circ\mathcal{D}$ and the inclusion $\mathcal{I}:\mathsf{cES}\to\mathsf{ES}$ form a coreflection. □

Proof

Immediate consequence of Theorem 3. ■

Explicitly, for any event structure $E$ the corresponding connected es $\mathcal{C}(E)=\langle E^{\prime},\vdash^{\prime},\#^{\prime}\rangle$ is defined as follows. The set of events is $E^{\prime}=\{[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\sim}}\mid C\vdash_{0}e\}$, where $\sim$ is the least equivalence such that $\langle{C},{e}\rangle\sim\langle{C^{\prime}},{e}\rangle$ if $\langle{C},{e}\rangle$ and $\langle{C^{\prime}},{e}\rangle$ are consistent. Moreover $[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\sim}}\#^{\prime}[{\langle{C^{\prime}},{e^{\prime}}\rangle}]_{\scriptscriptstyle{\sim}}$ if for all $\langle{C_{1}},{e}\rangle\sim\langle{C},{e}\rangle$ and $\langle{C_{1}^{\prime}},{e^{\prime}}\rangle\sim\langle{C^{\prime}},{e^{\prime}}\rangle$ the minimal enablings $\langle{C_{1}},{e}\rangle$ and $\langle{C_{1}^{\prime}},{e_{1}^{\prime}}\rangle$ are not consistent. Finally, for $X\subseteq E^{\prime}$, $X\vdash^{\prime}[{\langle{C},{e}\rangle}]_{\scriptscriptstyle{\sim}}$ if there exists $\langle{C^{\prime}},{e}\rangle\sim\langle{C},{e}\rangle$ such that $C^{\prime}\subseteq\{e^{\prime\prime}\mid[{\langle{C^{\prime\prime}},{e^{\prime\prime}}\rangle}]_{\scriptscriptstyle{\sim}}\in X\}$.

An overall picture of the results discussed up to now can be found in Fig. 8. The arrows from classes of event structures to domains are restrictions of the functor $\mathcal{D}({\cdot})$, while the converse arrows are restrictions of the functor $\mathcal{E}({\cdot})$. The Venn diagram stresses the fact that prime es are exactly the es which are stable and connected (see Lemma 5) showing how the notion of connectedness naturally emerges in the framework.

IV Related Characterisations

In this section we present a characterisation of our proposal in terms of a formalism reminiscent of the prime event structures with equivalence of [23, 24]. Moreover, we discuss and formalise the relation of our work with alternative characterisations of the domains of (prime) event structures proposed in the literature, based on intervals and on asynchronous graphs.

IV-A Prime Event Structures with Equivalence

The previous sections showed that the domains of configurations of unstable es are weak prime domains, i.e., they satisfy the same conditions as those of prime domains but only up to the equivalence induced by interchangeability. Symmetrically, this suggests the possibility of viewing unstable es as stable ones up to some equivalence on events. In this section we consider a formalisation for such a view, leading to a set up that is closely related to the framework devised in [23, 24], which we also call prime event structures with equivalence for the space of this article, since no confusion can arise.

In Section II-A we mentioned that in prime es a global notion of causality can be used in place of the enabling. We next recall the formal definition. We also introduce a notation for direct (i.e., non-inherited) conflict that will play a role later.

Definition 21** (causality/direct conflict in prime event

structures)**

Let $P=\langle E,\vdash,\#\rangle$ be a prime es. Given an event $e\in E$, the unique $C\in\mathit{Conf}({P})$ such that $C\vdash_{0}e$ is called the set of strict causes of $e$ and denoted by \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,, while the set of causes is \,\downarrow\!\!{e}=\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\{e\}. The strict causality relation $<$ is defined by $e^{\prime}<e$ if e^{\prime}\in\,\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,, and, as usual, we denote by $\leq$ the reflexive closure of $<$. We say that $e,e^{\prime}\in E$ are in direct conflict, written $e\#_{d}e^{\prime}$, when $e\#e^{\prime}$ and \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\{e^{\prime}\}, \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\,\cup\{e\} are consistent. □

We next introduce our notion of prime es with equivalence. Given a prime es $P$ with an equivalence over the set of events ${\sim}\subseteq E\times E$, we say that a subset $X\subseteq E$ is $\sim$-saturated if for all $e\in X$ and $e^{\prime}\in E$, if $e\sim e^{\prime}$ and \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\,\subseteq X then $e^{\prime}\in X$. Since the intersection of saturated sets is saturated, given a set $X$ we can always consider the smallest saturated superset of $X$, called the saturation of $X$ and denoted $\tilde{X}$.

Definition 22** (prime event structures with equivalence)**

A prime es with equivalence (epes for short) is a pair $\langle P,\sim\rangle$ where $P=\langle E,\vdash,\#\rangle$ is a prime es and $\sim$ is an equivalence on $E$ such that for all $e,e^{\prime},e_{1},e_{1}^{\prime}\in E$

if $[{\,\downarrow\!\!{e}}]_{\scriptscriptstyle{\sim}}\subseteq[{\,\downarrow\!\!{e^{\prime}}}]_{\scriptscriptstyle{\sim}}$ then $e\leq e^{\prime}$; if in addition $e\sim e^{\prime}$ then $e=e^{\prime}$; 2. 2.

if $e\sim e^{\prime}$ and \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\, consistent then $\neg(e\#e^{\prime})$. 3. 3.

if $e\sim e^{\prime}$, $e_{1}\sim e_{1}^{\prime}$, and $e\#_{d}e_{1}$ then $e^{\prime}\#e_{1}^{\prime}$.

We say that $\langle P,\sim\rangle$ is connected if ${\sim}=(\sim\setminus\#)^{*}$. A morphism of epes $f:\langle P_{1},\sim_{1}\rangle\to\langle P_{{2}},\sim_{2}\rangle$ is an es morphism $f:P_{1}\to P_{2}$ such that for all $e_{1},e_{1}^{\prime}\in P_{1}$, $e_{1}\sim_{1}e_{1}^{\prime}$ iff $f(e_{1})\sim_{2}f(e_{1}^{\prime})$. We denote by $\mathsf{epES}$ the corresponding category. □

An es with equivalence is thus just an es equipped with an equivalence on events. Condition (1) essentially says that an event is determined by the equivalence classes of events in its causal history. In particular, as a consequence, if \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\subseteq\,\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\, and $e\sim e^{\prime}$ then $e=e^{\prime}$, which intuitively means that distinct equivalent events must correspond to different enablings of the same event. Moreover, it implies that the set $\,\downarrow\!\!{e}$ is $\sim$-saturated and thus it is a configuration (see Definition 23 and Lemma 15). Conditions (2) and (3) essentially say that equivalent events can have different conflicts only for the fact that their minimal enablings have different conflicts. Connectedness amounts to the fact that equivalent events must be connected by a chain of equivalences going through consistent events. We next introduce a notion of configuration.

Definition 23** (configurations)**

Let $\langle P,\sim\rangle$ be an epes. Then \mathit{Conf}({\langle P,\sim\rangle})=\{C\mid C\in\mathit{Conf}({P})\ \land\ C\mbox{ \sim-saturated}\}. □

In words, a configuration of a prime es with equivalence is a configuration $C$ of the underlying event structure, where all events enabled in $C$ that are equivalent to some event already in $C$ are also in $C$. Thus equivalent events may have different minimal enablings, but whenever a configuration contains the causes of two equivalent events, their executions cannot be taken apart.

Lemma 15** (histories are configurations)**

Let $\langle P,\sim\rangle$ be a epes. For all $e\in E$, $\,\downarrow\!\!{e}$ is a configuration. □

Proof

Let $e\in E$ be any event. We have to show that $\,\downarrow\!\!{e}$ is saturated. If there are $e^{\prime}\in\,\downarrow\!\!{e}$ and $e^{\prime\prime}\sim e^{\prime}$ such that \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime\prime}}\,\subseteq\,\downarrow\!\!{e} then $[{\,\downarrow\!\!{e^{\prime\prime}}}]_{\scriptscriptstyle{\sim}}\subseteq[{\,\downarrow\!\!{e}}]_{\scriptscriptstyle{\sim}}$ and hence, by condition (1) in Definition 22, $e^{\prime\prime}\leq e$ which means $e^{\prime\prime}\in\,\downarrow\!\!{e}$. ■

As an example, the connected es of our running example (see Fig. 2), corresponds to the prime es with equivalence in Fig. 9(a), where we have two distinct copies of event $c$, namely $c_{a}\sim c_{b}$, corresponding to the possibile minimal enablings. Graphically, causality is represented by a straight directed line. The corresponding domain of configurations is depicted in Fig. 9(b). Note that $C=\{a,b,c_{a}\}$ is not a configuration despite the fact that it is downward closed, since it is not $\sim$-saturated: event $c_{b}$ is missing, but its causes $\{b\}$ are in $C$.

Our definition of epes is similar to that in [23, 24]. Concerning configurations, while [23, 24] identifies unambiguous configurations where there is a unique representative for each equivalence class, here instead we saturate including all equivalent events that are not in conflict.

We finally observe that the constructions above can be “translated” into constructions that relate directly epes and weak prime domains.

Proposition 8** (weak prime domain for epes)**

Let $\langle P,\sim\rangle$ be a epes. Then $\mathcal{D}_{eq}({\langle P,\sim\rangle})=\langle\mathit{Conf}({\langle P,\sim\rangle}),\subseteq\rangle$ is a weak prime domain. Conversely, if $D$ is a weak prime domain then $\mathcal{E}_{eq}({D})=\langle\langle\mathop{\mathit{ir}({D})},\#,\vdash\rangle,\leftrightarrow^{*}\rangle$ with conflict and enabling defined by

• •

$i_{1}\#i_{2}$* if $\{i_{1},i_{2}\}$ not consistent;*

• •

$X\vdash i$* if $X\supseteq\mathop{\mathit{ir}({i})}\setminus\{i\}$.*

is an epes. □

Proof

Let $\langle P,\sim\rangle$ be a epes. Then it is easy to see that the irreducibles of $\mathcal{D}_{eq}({\langle P,\sim\rangle})$ are the minimal enablings $\,\downarrow\!\!{e}$ for $e\in E$. Moreover, given a set of pairwise consistent configurations $X\subseteq\mathit{Conf}({\langle P,\sim\rangle})$, the join $\bigsqcup X$ is the saturation of their union. Interchangeability is given by $\,\downarrow\!\!{e}\leftrightarrow\,\downarrow\!\!{e^{\prime}}$ if $e\sim e^{\prime}$ and $\neg(e\#e^{\prime})$. Using these fact it is almost immediate to conclude that $\mathcal{D}_{eq}({\langle P,\sim\rangle})$ is a weak prime domain. Let us first observe that $\mathcal{D}_{eq}({\langle P,\sim\rangle})$ is interchangeable (Definition 12):

• •

Condition (1) requires that for all $e,e^{\prime}\in P$ if $\,\downarrow\!\!{e}\leftrightarrow^{*}\,\downarrow\!\!{e^{\prime}}$ and \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\, consistent then $\,\downarrow\!\!{e}\leftrightarrow\,\downarrow\!\!{e^{\prime}}$. Observe that $\,\downarrow\!\!{e}\leftrightarrow^{*}\,\downarrow\!\!{e^{\prime}}$ implies $e\sim e^{\prime}$. Moreover, by condition (2) in Definition 22, \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\, consistent implies $\neg(e\#e^{\prime})$. Hence we conclude $\,\downarrow\!\!{e}\leftrightarrow\,\downarrow\!\!{e^{\prime}}$.

• •

Condition (2) is an easy consequence of condition (3) of Definition 22. In fact, let $e,e^{\prime},e_{1},e_{1}^{\prime}\in E$ such that $\,\downarrow\!\!{e}\leftrightarrow^{*}\,\downarrow\!\!{e^{\prime}}$, $\,\downarrow\!\!{e_{1}}\leftrightarrow^{*}\,\downarrow\!\!{e_{1}^{\prime}}$, i.e., $e\sim e^{\prime}$ and $e_{1}\sim e_{1}^{\prime}$. Assume moreover that the sets $\{\,\downarrow\!\!{e^{\prime}},\,\downarrow\!\!{e_{1}^{\prime}}\}$, \{\,\downarrow\!\!{e},\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e_{1}}\,\}, \{\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,,\,\downarrow\!\!{e_{1}}\} are consistent, meaning that $\,\downarrow\!\!{e^{\prime}}\cup\,\downarrow\!\!{e_{1}^{\prime}}$, \,\downarrow\!\!{e}\cup\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e_{1}}\,, \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\,\downarrow\!\!{e_{1}} are so. From the consistency of $\,\downarrow\!\!{e^{\prime}}\cup\,\downarrow\!\!{e_{1}^{\prime}}$ we have $\neg(e^{\prime}\#e_{1}^{\prime})$. Moreover, the consistency of \,\downarrow\!\!{e}\cup\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e_{1}}\,, \mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,\cup\,\downarrow\!\!{e_{1}} implies that if $e\#e_{1}$ then the conflict would be direct and this would violate condition (3) of Definition 22. Hence we must have $\neg(e\#e_{1})$, i.e., $\{\,\downarrow\!\!{e},\,\downarrow\!\!{e_{1}}\}$ consistent, as desired.

Finally, we show that all irreducibles are weak prime. Let $e\in P$, consider the irreducible $\,\downarrow\!\!{e}$ and a consistent set of configurations $X\subseteq\mathit{Conf}({\langle P,\sim\rangle})$. Assume that $\,\downarrow\!\!{e}\subseteq\bigsqcup X$. This means that $e$ is in the saturation of $\bigcup X$, which in turn means that there is $C\in X$ and $e^{\prime}\in C$, whence $\,\downarrow\!\!{e^{\prime}}\subseteq C$, such that $e^{\prime}\sim e$. Since $e,e^{\prime}\in\bigsqcup X$, they are consistent, hence $\,\downarrow\!\!{e}\leftrightarrow\,\downarrow\!\!{e^{\prime}}$. Summing up $\,\downarrow\!\!{e^{\prime}}\subseteq C$ and $e\sim e^{\prime}$, as desired.

Conversely, let $D$ be a weak prime domain. Observe that the causal order in $\mathcal{E}_{eq}({D})$ is the restriction of the domain order to irreducibles. Condition (1) in Definition 22 is an immediate consequence of Proposition 6.

Condition (2) is immediately implied by condition (1) in the definition of interchangeable domain (Definition 12).

Concerning condition (3), observe that it becomes: for $i,i^{\prime},i_{1},i_{1}^{\prime}\in\mathop{\mathit{ir}({D})}$, if $i\leftrightarrow^{*}i^{\prime}$, $i_{1}\leftrightarrow^{*}i_{1}^{\prime}$, $i,i_{1}$ not consistent and $i^{\prime},i_{1}^{\prime}$ consistent then either $\mathop{\mathit{ir}({\mathit{p}({i})})}\cup\{i_{1}\}$ or $\mathop{\mathit{ir}({\mathit{p}({i_{1}})})}\cup\{i\}$ not consistent. In turn this is easily seen to be equivalent to condition (2) in the definition of interchangeable domain (Definition 12). ■

The correspondence above can be translated to an analogous correspondence between epes and unstable es. It is however impossible to make such correspondence functorial essentially for the same reason why [23, 24] resorts to a pseudo-adjunction. We try to enucleate the problem by showing a correspondence between (unstable) event structures and epes.

Definition 24** (from es to epes and back)**

Let $\langle P,\sim\rangle$ be an epes, where $P=\langle E,\vdash,\#\rangle$. The corresponding es is $\mathcal{M}({\langle P,\sim\rangle})=\langle{E}_{\scriptscriptstyle{\sim}},{\vdash}_{\scriptscriptstyle{\sim}},{\#}_{\scriptscriptstyle{\sim}}\rangle$, with ${\vdash}_{\scriptscriptstyle{\sim}}$ and ${\#}_{\scriptscriptstyle{\sim}}$ defined by

• •

$[{X}]_{\scriptscriptstyle{\sim}}{\vdash}_{\scriptscriptstyle{\sim}}[{e}]_{\scriptscriptstyle{\sim}}$ when $X\vdash e$;

• •

$[{e}]_{\scriptscriptstyle{\sim}}{\#}_{\scriptscriptstyle{\sim}}[{e^{\prime}}]_{\scriptscriptstyle{\sim}}$ when $e_{1}\#e_{1}^{\prime}$ for all $e_{1}\in[{e}]_{\scriptscriptstyle{\sim}}$ and $e_{1}^{\prime}\in[{e^{\prime}}]_{\scriptscriptstyle{\sim}}$.

Conversely, given an es $P=\langle E,\vdash,\#\rangle$ the corresponding epes is $\mathcal{U}({P})=\langle Q,\sim\rangle$, with $Q=\langle E^{\prime},\vdash^{\prime},\#^{\prime}\rangle$ defined by

• •

$E^{\prime}=\{\langle{C},{e}\rangle\mid C\in\mathit{Conf}({E})\ \land\ e\in E\ \land\ C\vdash_{0}e\}$;

• •

$X\vdash^{\prime}\langle{C},{e}\rangle$ if $C\subseteq\bigcup\{C^{\prime}\cup\{e^{\prime}\}\mid\langle C^{\prime},e^{\prime}\rangle\in X\}$;

• •

$\langle{C},{e}\rangle\#^{\prime}\langle{C^{\prime}},{e^{\prime}}\rangle$ if $C\cup C^{\prime}\cup\{e,e^{\prime}\}$ is not consistent.

and the equivalence is defined by $\langle{C},{e}\rangle\sim\langle{C^{\prime}},{e}\rangle$ for all $C,C^{\prime}$ such that $C\vdash_{0}e$ and $C^{\prime}\vdash_{0}e$. □

We can easily show, exploiting Proposition 8, that the constructions above produce well-defined structures and map connected structures to connected structures. Moreover, the two constructions are inverse of each other.

Proposition 9

Let $\langle P,\sim\rangle$ be an epes. Then $\langle P,\sim\rangle$ and $\mathcal{U}({\mathcal{M}({\langle P,\sim\rangle})})$ are isomorphic. Dually, let $P=\langle E,\vdash,\#\rangle$ be an es. Then $\mathcal{M}({\mathcal{U}({P})})$ and $P$ are isomorphic. □

Proof

Let $\langle P,\sim\rangle$ be an epes. Recall that events in $\mathcal{U}({\mathcal{M}({\langle P,\sim\rangle})})$ are minimal enablings in $\mathcal{M}({\langle P,\sim\rangle})$. By definitions of $\mathcal{M}({\langle P,\sim\rangle})$, for all $e\in P$ we have $[{X}]_{\scriptscriptstyle{\sim}}\vdash_{\mathcal{M}({\langle P,\sim\rangle})}[{e}]_{\scriptscriptstyle{\sim}}$ when $X\vdash e$. Therefore [{\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,}]_{\scriptscriptstyle{\sim}}\vdash_{\mathcal{M}({\langle P,\sim\rangle})}[{e}]_{\scriptscriptstyle{\sim}}, and this enabling is minimal since, by Definition 22(1), whenever $e^{\prime}\sim e$ and [{\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e^{\prime}}\,}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq[{\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,}]_{\scriptscriptstyle{\leftrightarrow^{*}}} we have $e=e^{\prime}$. And, again relying on the definition of enabling, one sees that all minimal enablings are of this shape. Therefore we can define $c:\langle P,\sim\rangle\to\mathcal{U}({\mathcal{M}({\langle P,\sim\rangle})})$ by c(e)=\langle{[{\mathrel{\raisebox{0.8pt}{\rotatebox{270.0}{\twoheadrightarrow}}}\!\!{e}\,}]_{\scriptscriptstyle{\sim}}},{[{e}]_{\scriptscriptstyle{\sim}}}\rangle. By the previous arguments it is a bijection and it can be shown $c$ to be an isomorphism of epes.

Conversely, let $\langle E,\vdash,\#\rangle$ be an an es. According to the definition, events in $\mathcal{U}({E})$ are minimal enablings $\langle{C},{e}\rangle$ in $E$, and they are equivalent when they are minimal enablings of the same event. Then events in $\mathcal{M}({\mathcal{U}({E})})$ are just equivalence classes of events in $\mathcal{U}({E})$. Therefore we can define $u:E\to\mathcal{M}({\mathcal{U}({E})})$ by $u(e)=\{\langle{C},{e}\rangle\mid C\in\mathit{Conf}({E})\ \land\ C\vdash_{0}e\}$. It is immediate to see that it is a bijection and an isomorphism of es. ■

Observe that the construction from epes to es can be easily turned into a functor $\mathcal{M}:\mathsf{epES}\to\mathsf{ES}$. In fact, given a morphism $f:\langle P_{1},\sim_{1}\rangle\to\langle P_{2},\sim_{2}\rangle$ we can let $\mathcal{M}({f})([{e_{1}}]_{\scriptscriptstyle{\sim_{1}}})=[{f(e_{1})}]_{\scriptscriptstyle{\sim_{2}}}$.

Instead, making the converse construction from es to epes functorial is problematic. In fact, consider the es of the running example $E=\{a,b,c\}$, with $\emptyset\vdash_{0}a$, $\emptyset\vdash_{0}b$ and $\{a,b\}\vdash_{0}c$ and the es with events $E^{\prime}=\{a^{\prime},b^{\prime},c^{\prime}\}$ with $\emptyset\vdash_{0}a^{\prime}$, $\emptyset\vdash_{0}b^{\prime}$ and $\{a^{\prime}\}\vdash_{0}c^{\prime}$ and $\{b^{\prime}\}\vdash_{0}c^{\prime}$ and the morphism $f:E\to E^{\prime}$ with $f(x)=x^{\prime}$ for $x\in\{a,b,c\}$. Then $\mathcal{U}({E})=\{\langle{\emptyset},{a}\rangle,\langle{\emptyset},{b}\rangle,\langle{\{a,b\}},{c}\rangle\}$ and $\mathcal{U}({E^{\prime}})=\{\langle{\emptyset},{a^{\prime}}\rangle,\langle{\emptyset},{b^{\prime}}\rangle,\langle{\{a^{\prime}\}},{c^{\prime}}\rangle,\langle{\{b^{\prime}\}},{c^{\prime}}\rangle\}$. Observe that, while clearly $\mathcal{U}({f})(\langle{\emptyset},{a}\rangle)=\langle{\emptyset},{a^{\prime}}\rangle$ and $\mathcal{U}({f})(\langle{\emptyset},{b}\rangle)=\langle{\emptyset},{b^{\prime}}\rangle$, when we come to $\mathcal{U}({f})(\langle{\{a,b\}},{c}\rangle)$ we can define it as one of the two equivalent events $\langle{\{a^{\prime}\}},{c^{\prime}}\rangle$ and $\langle{\{b^{\prime}\}},{c^{\prime}}\rangle$.

The solution offered by [23, 24] is to move towards pseudo-functors, i.e., considering two epes morphisms $g,g^{\prime}:P_{1}\to P_{2}$ equivalent if $g(e_{1})\sim_{2}g^{\prime}(e_{1})$ for all $e_{1}\in P_{1}$ and requiring that functors are defined only up-to morphism equivalence. Indeed, it is easy to see that the two possible choices for $f$ above lead to equivalent morphisms.

IV-B Relation with Interval Based Characterisations

The correspondence between event structures and domains has been often studied in the literature by relying on the notion of interval [21, 1, 16, 22].

Definition 25** (interval)**

Let $D$ be a domain. An interval is a pair $[{d},{d^{\prime}}]$ of elements of $D$ such that $d\prec d^{\prime}$. The set of intervals of $D$ is denoted by $\mathop{\mathit{Int}({D})}$. Given two intervals $[{c},{c^{\prime}}],[{d},{d^{\prime}}]\in\mathop{\mathit{Int}({D})}$ we define

$[{c},{c^{\prime}}]\leq[{d},{d^{\prime}}]$  if $(c=c^{\prime}\sqcap d)\ \wedge\ (c^{\prime}\sqcup d=d^{\prime})$,

and we let $\sim$ be the equivalence obtained as the symmetric and transitive closure of $\leq$. □

It can be shown that $\leq$ is a partial order on intervals and thus $\sim$ is indeed an equivalence. An interval represents a pair of elements differing only for a “quantum” of information, intuitively the execution of an event. The equivalence $\sim$ is intended to identify intervals corresponding to the execution of the same event in diffent states. Indeed, in [1] it is shown that for prime domains there is a bijective correspondence between $\sim$-classes of intervals and complete primes. In weak prime domains we can establish a similar correspondence, with $\leftrightarrow^{*}$-classes of irreducibles playing the role of the primes.

Lemma 16** (intervals vs. irreducibles)**

Let $D$ be a weak prime domain. Define $\mathop{\mathit{\zeta}}:{\mathop{\mathit{Int}({D})}}_{\scriptscriptstyle{\sim}}\to{\mathop{\mathit{ir}({D})}}_{\scriptscriptstyle{\leftrightarrow^{*}}}$ by

$\mathop{\mathit{\zeta}}([{d},{d^{\prime}}]_{\sim})=[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$,

where $i$ is any element in $\delta({d^{\prime}},{d})$. Then $\mathop{\mathit{\zeta}}$ is a bijection, whose inverse is $\mathop{\mathit{\iota}}:{\mathop{\mathit{ir}({D})}}_{\scriptscriptstyle{\leftrightarrow^{*}}}\to{\mathop{\mathit{Int}({D})}}_{\scriptscriptstyle{\sim}}$ defined by

$\mathop{\mathit{\iota}}([{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{\mathit{p}({i})},{i}]_{\sim}$.

□

Proof

We first observe that $\mathop{\mathit{\zeta}}$ is well-defined, i.e., if $[{c},{c^{\prime}}]\sim[{d},{d^{\prime}}]$ are equivalent intervals then for all $i\in\delta({c^{\prime}},{c})$, $i^{\prime}\in\delta({d^{\prime}},{d})$ it holds $i\leftrightarrow i^{\prime}$. This follows by noting that if $[{c},{c^{\prime}}]\leq[{d},{d^{\prime}}]$, $i\in\delta({c^{\prime}},{c})$ and $i^{\prime}\in\delta({d^{\prime}},{d})$ then $i\leftrightarrow i^{\prime}$. In order to prove the last assertion, observe that since $i\in\mathop{\mathit{ir}({c^{\prime}})}$ we have $i\sqsubseteq c^{\prime}\sqsubseteq d^{\prime}$, thus $i\in\mathop{\mathit{ir}({d^{\prime}})}$. Moreover, $i\not\in\mathop{\mathit{ir}({d})}$, otherwise, by $i\sqsubseteq d$, $i\sqsubseteq c^{\prime}$ and $c=d\sqcap c^{\prime}$, we would get $i\sqsubseteq c$, contradicting the assumption that $i\in\delta({c^{\prime}},{c})$. Hence $i\in\delta({d^{\prime}},{d})$ and by Lemma 10(3) we conclude.

Also the converse map $\mathop{\mathit{\iota}}$ is well-defined. This follows from the observation that for all irreducibles $i,i^{\prime}\in\mathop{\mathit{ir}({D})}$ if $i\leftrightarrow i^{\prime}$ then $[{\mathit{p}({i})},{i}],[{\mathit{p}({i^{\prime}})},{i^{\prime}}]\leq[{\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})},{i\sqcup i^{\prime}}]$ and thus $[{\mathit{p}({i})},{i}]\sim[{\mathit{p}({i^{\prime}})},{i^{\prime}}]$. Let us prove, for instance, that

$[{\mathit{p}({i})},{i}]\leq[{\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})},{i\sqcup i^{\prime}}]$.

Since $i\leftrightarrow i^{\prime}$, surely $\mathit{p}({i})\sqsubseteq\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})$ and $\mathit{p}({i})\prec i$, hence by Lemma 12, we deduce $i\sqsubseteq\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})$ or $\mathit{p}({i})=i\sqcap(\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}}))$. The first possibility, $i\sqsubseteq\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})$, by the fact that $i$ is irreducible leads to $i\sqsubseteq\mathit{p}({i^{\prime}})$ (since $i\sqsubseteq\mathit{p}({i})$ is clearly false). Thus $i\sqcup\mathit{p}({i^{\prime}})=\mathit{p}({i^{\prime}})\prec i^{\prime}\sqsubseteq\mathit{p}({i})\sqcup i^{\prime}$, that, by Lemma 5(3), contradicts $i\leftrightarrow i^{\prime}$. Hence the second possibility must hold, i.e., $\mathit{p}({i})=i\sqcap(\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}}))$. Moreover, again by Lemma 5(3), we have $i\sqcup(\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}}))=i\sqcup i^{\prime}$. Hence $[{\mathit{p}({i})},{i}]\leq[{\mathit{p}({i})\sqcup\mathit{p}({i^{\prime}})},{i\sqcup i^{\prime}}]$ as desired.

The two maps are inverse each other.

• •

If $[{d},{d^{\prime}}]\in\mathop{\mathit{Int}({D})}$ and $i\in\delta({d^{\prime}},{d})$ then $[{d},{d^{\prime}}]\sim[{\mathit{p}({i})},{i}]$.

Observe that $d\sqcup i=d^{\prime}$ by Lemma 10(1). Moreover, in order to show that $d\sqcap i=\mathit{p}({i})$, note that, since $i\in\delta({d^{\prime}},{d})$ and, by Lemma 10(2), the set $\delta({d^{\prime}},{d})$ is flat, we have that $\mathit{p}({i})\sqsubseteq d$. Moreover $\mathit{p}({i})\prec i$, therefore by Lemma 12, $\mathit{p}({i})=d\sqcap i$, as desired.

• •

If $i\in\mathop{\mathit{ir}({D})}$ and $i^{\prime}\in[{\mathit{p}({i})},{i}]$ then $i\leftrightarrow i^{\prime}$.

Just observe that $i\in[{\mathit{p}({i})},{i}]$ and then use Lemma 10(3).

■

In  [21, 22] the domain of configurations of general event structures with binary conflict is characterised in terms of intervals. It is shown (see, e.g., [21, Theorem 3.3.3]), that given a an event structure with binary conflict, the domain of configuration is an algebraic complete partial order where the following axioms hold

(F)

for all $d\in\mathop{\mathsf{K}({D})}$ the set $\mathop{\downarrow\!{d}}$ is finite;

(C)

for all $x,y,z\in\mathop{\mathsf{K}({D})}$, if $x\prec y$, $x\prec z$, $\{y,z\}$ consistent, and $y\neq z$ then there exists $y\sqcup z$ and $y\prec y\sqcup z$ and $z\prec y\sqcup z$;

(R)

for all intervals $[{x},{y}]$, $[{x},{z}]$ if $[{x},{y}]\sim[{x},{z}]$ then $y=z$;

(V)

for all $x,x^{\prime},y,y^{\prime},x^{\prime\prime},y^{\prime\prime}\in\mathop{\mathsf{K}({D})}$ if $[{x},{x^{\prime}}]\sim[{y},{y^{\prime}}]$, $[{x},{x^{\prime\prime}}]\sim[{y},{y^{\prime\prime}}]$, and $\{x^{\prime},x^{\prime\prime}\}$ consistent then $y^{\prime},y^{\prime\prime}$ consistent.

Conversely, in [22] an explicit construction of the es corresponding to a domain is provided. Given $d\in\mathop{\mathsf{K}({D})}$, let $s(d)=\{[{c},{c^{\prime}}]_{\sim}\mid c^{\prime}\sqsubseteq d\}$.

Definition 26** (event structure from a domain [22])**

Given a domain $D$ satisfying the axioms (F), (C), (R), (V), the corresponding es with binary conflict is defined as $\mathcal{E}_{wd}({D})=(E,\#,\vdash)$ where

• •

$E={\mathop{\mathit{Int}({D})}}_{\scriptscriptstyle{\sim}}$;

• •

$[{c},{c^{\prime}}]_{\sim}\#[{d},{d^{\prime}}]_{\sim}$ if for all $[{c_{1}},{c_{1}^{\prime}}]$, $[{d_{1}},{d_{1}^{\prime}}]$ such that $[{c_{1}},{c_{1}^{\prime}}]\sim[{c},{c^{\prime}}]$ and $[{d_{1}},{d_{1}^{\prime}}]\sim[{d},{d^{\prime}}]$ the set $\{c_{1}^{\prime},d_{1}^{\prime}\}$ is not consistent;

• •

for $X\subseteq E$, $X\vdash[{c},{c^{\prime}}]_{\sim}$ if $s(c_{1})\subseteq X$ for some interval $[{c_{1}},{c_{1}^{\prime}}]\sim[{c},{c^{\prime}}]$.

□

The above construction produces an event structure with binary conflict that is mapped back to the original domain (see, e.g., [22, Corollary 2.10]).

Theorem 4

Let $D$ be a domain satisfying axioms (F), (C), (R), (V). Then $\mathcal{D}({\mathcal{E}_{wd}({D})})$ is isomorphic to $D$. □

We can build on the above results to show that the domains satisfying axioms (F), (C), (R) and (V) are exactly the weak prime domains.

Proposition 10** (weak prime domains and intervals)**

Let $D$ be a domain. Then $D$ is a weak prime domain iff $D$ satisfies axioms (F), (C), (R) and (V). □

Proof

Let $D$ be a domain satisfying axioms (F), (C), (R) and (V). By Theorem 4, $\mathcal{D}({\mathcal{E}_{wd}({D})})\simeq D$. Since, by Proposition 4, the set of configurations of any event structure forms a weak prime domain, we conclude that $D$ is weak prime.

For the converse, let $D$ be a weak prime domain. By Theorem 3, we have that $\mathcal{D}({\mathcal{E}({D})})\simeq D$ and thus, since by [21, 22], the domain of configuration of an event structure with binary conflict satisfies axioms (F), (C), (R) and (V), we conclude. ■

Moreover, relying on Lemma 16, we can show that the event structures associated with a domain in [22] (Definition 26) and in our work (Definition 20) coincide.

Proposition 11

Let $D$ be a weak prime domain. Then $\mathcal{E}({D})$ and $\mathcal{E}_{wd}({D})$ are isomorphic. □

Proof

By Lemma 16, the function $\mathop{\mathit{\zeta}}:{\mathop{\mathit{Int}({D})}}_{\scriptscriptstyle{\sim}}\to{\mathop{\mathit{ir}({D})}}_{\scriptscriptstyle{\leftrightarrow^{*}}}$ is a bijection. Note that ${\mathop{\mathit{Int}({D})}}_{\scriptscriptstyle{\sim}}$ and ${\mathop{\mathit{ir}({D})}}_{\scriptscriptstyle{\leftrightarrow^{*}}}$ are the sets of events respectively of $\mathcal{E}({D})$ and $\mathcal{E}_{wd}({D})$. We next show that $\mathop{\mathit{\zeta}}$ is an isomorphism of event structures.

Let $e_{1},e_{2}$ be events in $\mathcal{E}_{wd}({D})$. We show that $e_{1}\#e_{2}$ iff $\mathop{\mathit{\zeta}}(e_{1})\#\mathop{\mathit{\zeta}}(e_{2})$.

If $\neg(e_{1}\#e_{2})$, from Definition 26, we get that there exist $[{c_{1}},{c_{1}^{\prime}}]\in e_{1}$ and $[{c_{2}},{c_{2}^{\prime}}]\in e_{2}$ such that $\{c_{1}^{\prime},c_{2}^{\prime}\}$ is consistent. Let $d\in D$ be an upper bound, i.e., $c_{1}^{\prime},c_{2}^{\prime}\sqsubseteq d$. Now, $\mathop{\mathit{\zeta}}(e_{j})=[{i_{j}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ for $i_{j}\in\delta({c_{j}},{c_{j}^{\prime}})$, for $j\in\{1,2\}$. Clearly, $i_{1},i_{2}\in\mathop{\mathit{ir}({d})}$ whence $[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}},[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ and thus, according to Definition 20, we have $\neg([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\#[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$, as desired. The argument can be reversed to prove that if $\neg(\mathop{\mathit{\zeta}}(e_{1})\#\mathop{\mathit{\zeta}}(e_{2}))$ then $\neg(e_{1}\#e_{2})$.

Concerning the enabling relation, we show that $X\vdash e$ in $\mathcal{E}_{wd}({D})$ iff $\mathop{\mathit{\zeta}}(X)\vdash\mathop{\mathit{\zeta}}(e)$ in $\mathcal{E}({D})$. Assume that $X\vdash e$ in $\mathcal{E}_{wd}({D})$. This means that there exists $[{c},{c^{\prime}}]\in e$ such that $s(c)=\{[{d},{d^{\prime}}]_{\sim}\mid d^{\prime}\sqsubseteq c\}\subseteq X$. Now, recall that $\mathop{\mathit{\zeta}}(e)=[{i}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$ with $i\in\delta({c^{\prime}},{c})$. In order to show that $\mathop{\mathit{\zeta}}(X)\vdash\mathop{\mathit{\zeta}}(e)$, according to Definition 20, we prove that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq\mathop{\mathit{\zeta}}(X)$. Let $j\in\mathop{\mathit{ir}({i})}\setminus\{i\}$. Clearly $j\in\delta({j},{\mathit{p}({j})})$ and thus $[{j}]_{\scriptscriptstyle{\leftrightarrow^{*}}}=\mathop{\mathit{\zeta}}([{\mathit{p}({j})},{j}]_{\sim})$. Moreover, by Lemma 10(2) the set $\delta({c^{\prime}},{c})$ is flat and thus, since $j\sqsubset i$ necessarily $j\not\in\delta({c^{\prime}},{c})$. Since $j\in\mathop{\mathit{ir}({c^{\prime}})}$ we conclude that $j\in\mathop{\mathit{ir}({c})}$, namely $j\sqsubseteq c$. This implies that $[{\mathit{p}({j})},{j}]_{\sim}\in s(c)$ and thus

\begin{array}[]{lll}[{j}]_{\scriptscriptstyle{\leftrightarrow^{*}}}&=\mathop{\mathit{\zeta}}([{\mathit{p}({j})},{j}]_{\sim})&\\ &\subseteq\mathop{\mathit{\zeta}}(s(c))&\\ &\subseteq\mathop{\mathit{\zeta}}(X)&\mbox{[since s(c)\subseteq X]}\end{array}

We thus conclude that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq\mathop{\mathit{\zeta}}(X)$ as desired.

Also in this case, the argument can be easily reversed to prove the converse implication. ■

The paper by Droste [22] considers also the case of event structures with a general consistency relation (rather than a binary conflict). The correspondence with our approach can be extended to this setting, as further detailed in Appendix -A.

IV-C Relation with Asynchronous Graphs

A characterisation of prime es in terms of their transition graph has been given in [27]. A slightly different, yet equivalent formalisation has been rediscovered in [29], in the context of the work on the abstract theory of rewriting and concurrent games. Here we show that an analogous characterisation can be obtained for (connected) event structures. For our development we refer to the formalisation in [29]. Given a graph $G=\langle N,U,s,t\rangle$, a sequence of edges $w=u_{1};\ldots;u_{n}\in U^{*}$ is a path whenever each edge has a target that coincide with the source of the subsequent edge, i.e., for all $i\in[{1},{n-1}]$, $t(u_{i})=s(u_{i+1})$. Let us denote by $P_{2}(G)$ the set of paths of length $2$, i.e., $P_{2}(G)=\{u_{1};u_{2}\mid u_{1},u_{2}\in E\}$. Note that two paths of length 2 with the same source and target can be seen as a “square” in the graph. An asynchronous graph is then a transition system where some squares are declared to commute.

Definition 27** (asynchronous graph)**

An asynchronous graph is a tuple $A=\langle G,n_{0},\simeq\rangle$ where $G=\langle N,U,s,t\rangle$ is a directed graph, $n_{0}\in N$ is the origin and ${\simeq}\subseteq P_{2}(G)\times P_{2}(G)$ is an equivalence relation on coinitial and cofinal paths of length $2$ (i.e., if $u_{1};u_{2}\simeq v_{1};v_{2}$ then $s(u_{1})=s(v_{1})$ and $t(u_{2})=t(v_{2})$) such that the following axioms hold (in pictures, all squares depicted are assumed to commute)

if $u_{1};u_{2}\simeq v_{1};v_{2}$ and $u_{2}\neq v_{2}$ then $u_{1}\neq v_{1}$;

\bullet$$\bullet$$\bullet$$\bullet$$u_{1}$$v_{1}$$u_{2}$$v_{2} 2. 2.

if $u;u_{1}\simeq v_{1};v_{2}$ and $u;u_{1}^{\prime}\simeq v_{1}^{\prime};v_{2}^{\prime}$ then ($u_{1}=u_{1}^{\prime}$ iff $v_{1}=v_{1}^{\prime}$);

\bullet$$\bullet$$\bullet$$\bullet$$u$$v_{1}$$u_{1}$$v_{2}

and

\bullet$$\bullet$$\bullet$$\bullet$$u$$v_{1}^{\prime}$$u_{1}^{\prime}$$v_{2}^{\prime} 3. 3.

Cube

\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$u_{1}$$v_{1}$$u_{2}$$v_{2}$$u_{3}$$v_{3}

\begin{array}[]{c}\stackrel{{\scriptstyle(a)}}{{\Rightarrow}}\\ \stackrel{{\scriptstyle(b)}}{{\Leftarrow}}\end{array}

\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$u_{1}$$v_{1}$$u_{2}$$v_{2}$$u_{3}$$v_{3} 4. 4.

Coherence axiom

\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$u_{1}$$v_{1}$$u_{2}$$v_{2}

$\Rightarrow$

\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$u_{1}$$v_{1}$$u_{2}$$v_{2}

□

Given an asynchronous graph, we denote by the same symbol $\simeq$ the extension of the equivalence to all paths by contextual closure, i.e., $w_{1};w;w_{2}\simeq w_{1};w^{\prime};w_{2}$ for all $w_{1},w_{2},w,w^{\prime}\in U^{*}$ with $w\simeq w^{\prime}$. The equivalence classes of paths from the origin can be ordered by prefix, leading to a partial order $P(A)$. Then it can be shown that the partial orders of finite configurations of prime es exactly correspond to asynchronous graphs such that all cofinal paths from the origin are equivalent.

Definition 28** (prime asynchronous graph)**

An asynchronous graph $A=\langle G,n_{0},\simeq\rangle$ is called prime if all cofinal paths from the origin $n_{0}$ are equivalent. □

It can be seen that the requirement of having all cofinal paths equivalent amounts to that of having all coinitial and cofinal paths of length $2$ (squares) equivalent. This is indeed how the condition is formalised in [27].

Theorem 5** (asynchronous graphs/prime es [29])**

Let $A$ be a prime asynchronous graph. The ideal completion $\mathsf{Idl}({P(A)})$ is a prime domain. Conversely, each prime domain is isomorphic to $\mathsf{Idl}({P(A)})$ for some prime asynchronous graph $A$. □

With respect to [29], we added the coherence axiom (4) in the definition of asynchronous graph, which is going to be pivotal in our later characterisation of weak prime domains (Proposition 12). This is actually necessary already for having a correspondence with prime domains and es.222In a personal communication, Paul Andrée Melliès agreed that condition (4) is necessary for the correctness of Theorem 3 of Section 2.6 of [29], rephrased here as Theorem 5.

The correspondence established by Theorem 5 generalises to connected es and what we call weak asynchronous graphs, i.e., asynchronous graphs where only the forward part of the cube axiom holds, while the converse implication (indeed sometimes referred to as stability axiom) may fail.

Definition 29** (weak asynchronous graphs)**

A weak asynchronous graph is defined as in Definition 27, but omitting the stability axiom (3a). It is called weak prime if additionally all cofinal paths from the origin are equivalent. □

Then we can prove that weak prime domains are exactly the partial orders generated by weak prime asynchronous graphs (which in turn correspond to connected es).

Proposition 12** (weak asynchronous graphs and domains)**

Let $A$ be a weak prime asynchronous graph. The ideal completion $\mathsf{Idl}({P(A)})$ is a weak prime domain. Conversely, each weak prime domain is isomorphic to $\mathsf{Idl}({P(A)})$ for some weak prime asynchronous graph $A$. □

Proof

First observe that in a weak asynchronous graph $A=\langle G,n_{0},\simeq\rangle$ with $G=\langle N,U,s,t\rangle$ such that all the cofinal paths from the origin are equivalent we have that all the squares are commuting. Thus axioms (1) and  (2) imply that the graph is simple, that there are at most two different paths of length $2$ with the same source and target, and that there is at most one way of closing a square.

Now, let $D$ be a weak prime domain and consider the subset of compact elements $\mathop{\mathsf{K}({D})}$. It can be seen as an (acyclic) graph by taking compact elements as nodes and intervals as edges, with source and target functions being the obvious ones $s([{c},{c^{\prime}}]{)}=c$ and $t([{c},{c^{\prime}}])=c^{\prime}$. Then taking $\emptyset$ as origin and letting all the squares commute, we get a weak asynchronous graph where all the paths are equivalent. In detail, as observed above, axiom (1) follows from the fact that the graph is simple. Axiom (2) says that there are at most two paths of length $2$ between the same source and target. Assume that this is not the case, i.e., $\mathop{\mathsf{K}({D})}$ contains a substructure as below, with $y_{1},y_{2},y_{3}$ pairwise distinct.

z$$y_{1}$$y_{2}$$y_{3}$$x

Then we would have that $y_{1}$ is an irreducible which is not a weak prime. In fact $y_{1}\sqsubseteq y_{2}\sqcup y_{3}$, but it is not the case that either $y_{1}\leftrightarrow y_{2}$ or $y_{1}\leftrightarrow y_{3}$.

Axiom (3a) follows from bounded completeness and the fact that if $x\prec y_{1}$ and $x\prec y_{2}$, with $y_{1}\neq y_{2}$ then $y_{1}\prec y_{1}\sqcup y_{2}$ and $y_{2}\prec y_{1}\sqcup y_{2}$.

Axiom (4) is an immediate consequence of coherence.

Finally, we have to prove that all the paths from $\emptyset$ to the same target are equivalent. We prove more generally that all coinitial and cofinal paths are equivalent. First notice that given two paths $w=y_{1}\ldots y_{n}$ and $w^{\prime}=y_{1}^{\prime}\ldots y_{m}^{\prime}$ with $y_{1}=y_{1}^{\prime}$ and $y_{n}=y_{m}^{\prime}$ then $n=m=|[{\mathop{\mathit{ir}({y_{n}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\setminus[{\mathop{\mathit{ir}({y_{1}})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}|$, by Lemma 11. We prove by induction on $n=m$ that the two paths are equivalent. The base cases $n=1$ and $n=2$ are obvious. In the inductive case, consider $z=y_{2}\sqcup y_{2}^{\prime}$.

y_{n}=y_{n}^{\prime}$$y_{3}$$y_{3}^{\prime}$$z$$y_{2}$$y_{2}^{\prime}$$y_{1}=y_{1}^{\prime}

Then, as already observed, $y_{2}\prec z$ and $y_{2}^{\prime}\prec z$. Then

[TABLE]

Moreover, since $z\sqsubseteq y_{n}=y_{n}^{\prime}$ there is a path $y_{2}z\ldots y_{n}$ of length $n-1$ in a way that we can apply the inductive hypothesis to prove that $y_{2}y_{3}\ldots y_{n}\simeq y_{2}z\ldots y_{n}$. Similarly, on the left side, we get $y_{2}^{\prime}y_{3}^{\prime}\ldots y_{n}\simeq y_{2}^{\prime}z\ldots y_{n}^{\prime}$. Therefore, together with (9), we conclude that $w=y_{1}y_{2}y_{3}\ldots y_{n}\simeq y_{1}y_{2}z\ldots y_{n}\simeq y_{1}^{\prime}y_{2}^{\prime}z\ldots y_{n}^{\prime}\simeq y_{1}^{\prime}y_{2}^{\prime}y_{3}^{\prime}\ldots y_{n}^{\prime}=w^{\prime}$.

Conversely, let $A=\langle G,n_{0},\simeq\rangle$ where $G=\langle N,U,s,t\rangle$ is a weak asynchronous graph such that all the paths from the origin are equivalent. Then, in particular, all the squares are commuting and, by axiom (1), the graph is simple, i.e., we can think of edges as a relation on nodes. This allows us to view $A$ as a concurrent automata $(Q,\Sigma,T,(\parallel_{q})_{q\in Q})$ in the sense of [25] as follows. Define an equivalence on edges by $u\equiv u^{\prime}$ if there are $v,v^{\prime}\in U$ such that $uv\sim v^{\prime}u^{\prime}$ (namely, $u,u^{\prime}$ are the opposite edges of a square). Then take nodes as states $Q=N$, equivalence classes of edges as labels $\Sigma={U}_{\scriptscriptstyle{\equiv}}$, transition relation $T=\{(s(u),u,t(u))\mid u\in U\}$ and local concurrency given by $[{u}]_{\scriptscriptstyle{\equiv}}\parallel_{n}[{v}]_{\scriptscriptstyle{\equiv}}$ when $u,v$ are such that $s(u)=s(v)=n$ and there are $u^{\prime},v^{\prime}\in E$ such that $uu^{\prime}\sim vv^{\prime}$. The fact that $\parallel_{n}$ is well-defined uses in an essential way axioms (3a) and (4). Then an immediate adaptation of [25, Theorem 10] to asynchronous graphs shows that $P(A)$ is a domain that satisfies axioms (F), (C), and (R) in Subsection IV-B. Finally, observe that axiom (V) is a “global” version of the axiom (1). The fact that the latter implies the former can be proved by exploiting the fact that each bounded subset of $P(A)$ is a semimodular lattice [26, Theorem 3.1]. Hence $D$ is a weak prime domain. ■

V Domain and event structure semantics for graph rewriting

In this section we consider graph rewriting systems where rules are left-linear but possibly not right-linear and thus, as an effect of a rewriting step, some items can be merged. We argue that weak prime domains and connected es are the right tool for providing a concurrent semantics to this class of rewriting systems. More precisely, in Subsection V-A we review the basics of graph rewriting and we generalise the notion of independence between rule applications to graph rewriting with left-linear rules. Then in Subsections V-B and V-C we show that the domain associated with a graph rewriting system by a generalisation of a classical construction is a weak prime domain and vice versa that each connected es and thus each weak prime domain arise as the semantics of some graph rewriting system. Finally, in Subsection V-D we show how a prime event structure semantics for a graph rewriting system can be recovered by imposing suitable restriction on rule application.

V-A Graph rewriting and concatenable traces

We first review the basic definitions about graph rewriting in the double-pushout approach [20]. We recall graph grammars and then introduce a notion of trace, which provides a representation of a sequence of rewriting steps that abstracts from the order of independent rewrites. This requires an original generalisation of the notion of independence between rewriting steps to the case of left-linear rules. Traces are then turned into a category $\mathsf{Tr}({\mathcal{G}})$ of concatenable derivation traces [31].

Definition 30

A (directed) graph is a tuple $G=\langle N,E,s,t\rangle$, where $N$ and $E$ are sets of nodes and edges, and $s,t:E\rightarrow N$ are the source and target functions. The components of a graph $G$ are often denoted by $N_{G}$, $E_{G}$, $s_{G}$, $t_{G}$. A graph morphism $f:G\rightarrow H$ is a pair of functions $\langle f_{N}:N_{G}\rightarrow N_{H},f_{E}:E_{G}\rightarrow E_{H}\rangle$ such that $f_{N}\circ s=s^{\prime}\circ f_{E}$ and $f_{N}\circ t=t^{\prime}\circ f_{E}$. We denote by $\mathsf{Graph}$ the category of graphs and graph morphisms

□

An abstract graph $[G]$ is an isomorphism class of graphs. We work with typed graphs, i.e., graphs which are “labelled” over some fixed graph. Formally, given a graph $T$, the category of graphs typed over $T$, as introduced in [32], is the slice category $({\mathsf{Graph}}\downarrow{T})$, also denoted $\mathsf{Graph}_{T}$.

Definition 31** (graph grammar)**

A ($T$-typed graph) rule is a span $(L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle r}}{{\rightarrow}}R)$ in $\mathsf{Graph}_{T}$ where $l$ is mono and not epi. The typed graphs $L$, $K$, and $R$ are called the left-hand side, the interface, and the right-hand side of the rule, respectively. A ($T$-typed) graph grammar is a tuple $\mathcal{G}=\langle T,G_{s},P,\pi\rangle$, where $G_{s}$ is the start (typed) graph, $P$ is a set of rule names, and $\pi$ maps each rule name in $P$ into a rule. □

Sometimes we write $p:(L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle r}}{{\rightarrow}}R)$ for denoting the rule $\pi(p)$. When clear from the context we omit the word “typed” and the typing morphisms. Note that we consider only consuming grammars, i.e., grammars where for every rule $\pi(p)$ the morphism $l$ is not epi. Also note that rules are, by default, left-linear, i.e., the morphism $l$ is mono. When also the morphism $r$ is mono, the rule is called right-linear.

An example of graph grammar has been discussed in the introduction (see Fig. 2(a)). The type graph was left implicit: it can be found in the top part of Fig. 10. The typing morphisms for the start graph and the rules are implicitly represented by the labelling. Also observe that for the rules only the left-hand side $L$ and the right-hand side $R$ were reported. The same rules with the interface graph explicitly represented are in Fig. 10.

Definition 32** (direct derivation)**

Let $G$ be a typed graph, let $p:(L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle r}}{{\rightarrow}}R)$ be a rule, and let $m^{L}$ be a match, i.e., a typed graph morphism $m^{L}:L\rightarrow G$. A direct derivation $\delta$ from $G$ to $H$ via $p$ (based on $m^{L}$) is a diagram as in Fig. 11, where both squares are required to be pushouts in $\mathsf{Graph}_{T}$. We write $\delta:G\stackrel{{\scriptstyle{p/m}}}{{\Longrightarrow}}H$, where $m=\langle m^{L},m^{K},m^{R}\rangle$, or simply $\delta:G\stackrel{{\scriptstyle{p}}}{{\Longrightarrow}}H$. □

Since pushouts are defined only up to isomorphism, given isomorphisms $\kappa:G^{\prime}\to G$ and $\nu:H\to H^{\prime}$, also $G^{\prime}\stackrel{{\scriptstyle{p/m^{\prime}}}}{{\Longrightarrow}}H$ with $m^{\prime}=\langle\kappa^{-1}\circ m^{L},m^{K},m^{R}\rangle$ and $G\stackrel{{\scriptstyle{p/m^{\prime\prime}}}}{{\Longrightarrow}}H^{\prime}$ with $m^{\prime\prime}=\langle m^{L},m^{K},\nu\circ m^{R}\rangle$ are direct derivations, denoted by $\kappa\cdot\delta$ and $\delta\cdot\nu$, respectively. Informally, the rewriting step removes (the image of) the left-hand side from $G$ and replaces it by (the image of) the right-hand side $R$. The interface $K$ (the common part of $L$ and $R$) specifies what is preserved. For example, the transitions in Fig. 2(b) are all direct derivations. When rules are not right-linear, some items in the (image of the) interface are merged. This happens, e.g., for $p_{a}$ and $p_{b}$.

Definition 33** (derivations)**

Let $\mathcal{G}=\langle T,G_{s},P,\pi\rangle$ be a graph grammar. A derivation $\rho:G_{0}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}_{\mathcal{G}}G_{n}$ over ${\mathcal{G}}$ is a (possibly empty) sequence of direct derivations $\{G_{i-1}\stackrel{{\scriptstyle{p_{i}}}}{{\Longrightarrow}}G_{i}\}_{i\in[{1},{n}]}$ where $p_{i}\in P$ for $i\in[{1},{n}]$. The graphs $G_{0}$ and $G_{n}$ are called the source and the target of $\rho$, and denoted by $\mathsf{s}({\rho})$ and $\mathsf{t}({\rho})$, respectively. The length of $\rho$ is $|\rho|=n$. The derivation is called proper if $|\rho|>0$. Given two derivations $\rho$ and $\rho^{\prime}$ such that $\mathsf{t}({\rho})=\mathsf{s}({\rho^{\prime}})$, their sequential composition $\rho\,;\,\rho^{\prime}:\mathsf{s}({\rho})\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}\mathsf{t}({\rho^{\prime}})$ is defined in the obvious way. □

When irrelevant/clear from the context, the subscript $\mathcal{G}$ is omitted. If $\rho:G\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}H$ is a proper derivation and $\kappa:G^{\prime}\to G$, $\nu:H\to H^{\prime}$ are graph isomorphisms, then $\kappa\cdot\rho:G^{\prime}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}H$ and $\rho\cdot\nu:G\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}H^{\prime}$ are defined as expected.

In the double pushout approach to graph rewriting, it is natural to consider graphs and derivations up to isomorphism. However some structure must be imposed on the start and end graphs of an abstract derivation in order to have a meaningful notion of sequential composition. In fact, isomorphic graphs are, in general, related by several isomorphisms, while in order to concatenate derivations keeping track of the flow of causality one must specify how the items of the source and target isomorphic graphs should be identified. We follow [2], inspired by the theory of Petri nets [33]: we choose for each class of isomorphic typed graphs a specific graph, named the canonical graph, and we decorate the source and target graphs of a derivation with isomorphisms from the corresponding canonical graphs to such graphs.

Let $\mathsf{C}$ denote the operation that associates with each ($T$-typed) graph its canonical graph, thus satisfying $\mathsf{C}({G})\simeq G$ and if $G\simeq G^{\prime}$ then $\mathsf{C}({G})=\mathsf{C}({G^{\prime}})$.

Definition 34** (decorated derivation)**

A decorated derivation $\psi:G_{0}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}G_{n}$ is a triple $\langle\alpha,\rho,\omega\rangle$, where $\rho:G_{0}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}G_{n}$ is a derivation and $\alpha:\mathsf{C}({G_{0}})\to G_{0}$, $\omega:\mathsf{C}({G_{n}})\to G_{n}$ are isomorphisms. We define $\mathsf{s}({\psi})=\mathsf{C}({\mathsf{s}({\rho})})$, $\mathsf{t}({\psi})=\mathsf{C}({\mathsf{t}({\rho})})$ and $|\psi|=|\rho|$. □

Definition 35** (sequential composition)**

Let $\psi=\langle\alpha,\rho,\omega\rangle$, $\psi^{\prime}=\langle\alpha^{\prime},\rho^{\prime},\omega^{\prime}\rangle$ be decorated derivations such that $\mathsf{t}({\psi})=\mathsf{s}({\psi^{\prime}})$. Their sequential composition $\psi;\psi^{\prime}$ is defined, if $\psi$ and $\psi^{\prime}$ are proper, as $\langle\alpha,(\rho\cdot\omega^{-1});(\alpha^{\prime}\cdot\rho^{\prime}),\omega^{\prime}\rangle$. Otherwise, if $|\psi|=0$ then $\psi;\psi^{\prime}=\langle\alpha^{\prime}\circ\omega^{-1}\circ\alpha,\rho^{\prime},\omega^{\prime}\rangle$, and similarly, if $|\psi^{\prime}|=0$ then $\psi;\psi^{\prime}=\langle\alpha,\rho,\omega\circ{\alpha^{\prime}}^{-1}\circ\omega^{\prime}\rangle$. □

We next define an abstraction equivalence that identifies derivations that differ only in representation details.

Definition 36** (abstraction equivalence)**

Let $\psi=\langle\alpha,\rho,\omega\rangle$, $\psi^{\prime}=\langle\alpha^{\prime},\rho^{\prime},\omega^{\prime}\rangle$ be decorated derivations with $\rho:G_{0}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}G_{n}$ and $\rho^{\prime}:G^{\prime}_{0}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}G^{\prime}_{n^{\prime}}$ (whose $i^{th}$ step is depicted in the lower rows of Fig. 12). They are abstraction equivalent, written $\psi\equiv^{a}\psi^{\prime}$, if $n=n^{\prime}$, $p_{i}=p_{i}^{\prime}$ for all $i\in[{1},{n}]$, and there exists a family of isomorphisms $\{\theta_{X_{i}}:X_{i}\rightarrow X^{\prime}_{i}\mid X\in\{G,D\},$ $i\in[{1},{n}]\}\cup\{\theta_{G_{0}}\}$ between corresponding graphs in the two derivations such that (1) the isomorphisms relating the source and target commute with the decorations, i.e., $\theta_{G_{0}}\circ\alpha=\alpha^{\prime}$ and $\theta_{G_{n}}\circ\omega=\omega^{\prime}$; and (2) the resulting diagram (whose $i^{th}$ step is represented in Fig. 12) commutes.

□

Equivalence classes of decorated derivations with respect to $\equiv^{a}$ are called abstract derivations and denoted by $[\psi]_{a}$, where $\psi$ is an element of the class.

From a concurrent perspective, also derivations that only differ for the order in which two independent direct derivations are applied should not be distinguished. This is classically formalised by a notion of sequential independence between rewrites inducing the so-called shift equivalence on derivations. When working with rules which are only left-linear, we need to refine the notion of independence as discussed below.

Definition 37** (sequential independence)**

Consider a derivation $G\stackrel{{\scriptstyle{p_{1}/m_{1}}}}{{\Longrightarrow}}H\stackrel{{\scriptstyle{p_{2}/m_{2}}}}{{\Longrightarrow}}M$ as in Fig. 13. Then, its components are weakly sequentially independent if there exists an independence pair among them, i.e., two graph morphisms $i_{1}:R_{1}\rightarrow D_{2}$ and $i_{2}:L_{2}\rightarrow D_{1}$ such that $l_{2}^{*}\circ i_{1}=m_{R_{1}}$, $r_{1}^{*}\circ i_{2}=m_{L_{2}}$. They are sequentially independent if the independence pair is unique. □

Intuitively, when the independence pair is not unique, we can think that the first rewrite has performed some fusions that the second rewrite is using in an essential way. Hence the steps should not considered independent. Note that when dealing with linear rules, the independence pair, if it exists, is always unique. Hence the two notions independence coincide and reduce to the classical one in [14].

Proposition 13** (interchange operator)**

Let $\rho={G}\stackrel{{\scriptstyle{p_{1}/m_{1}}}}{{\Longrightarrow}}{H}\stackrel{{\scriptstyle{p_{2}/m_{2}}}}{{\Longrightarrow}}{M}$ be a derivation whose components are sequentially independent via an independence pair $\xi$. Then, a derivation $IC_{\xi}(\rho)={G}\stackrel{{\scriptstyle{p_{2}/m^{*}_{2}}}}{{\Longrightarrow}}{H^{*}}\stackrel{{\scriptstyle{p_{1}/m^{*}_{1}}}}{{\Longrightarrow}}{M}$ can be uniquely constructed. The interchange is called proper when it produces a derivation that is again sequentially independent. □

We explicitly observe that the result of the interchange of two sequentially independent rewrites is still weak sequentially independent, but, differently from what happens for linear rules, it could fail to be sequentially independent due to non-uniqueness of the independence pair. This motivates the notion of proper interchange.

The interchange operator is used to introduce a notion of shift equivalence [14], identifying (as for the analogous permutation equivalence of $\lambda$-calculus) those derivations which differ only for the scheduling of independent steps. Due to the fact that the interchange of a sequential independence derivation is not necessarily sequential independent some care must be put for making the relation symmetric.

Definition 38** (shift equivalence)**

The derivations $\rho$ and $\rho^{\prime}$ are shift equivalent, written $\rho\equiv^{sh}\rho^{\prime}$, if $\rho^{\prime}$ can be obtained from $\rho$ by repeated proper interchanges of pairs of sequentially independent rewrite steps. □

If we are interested in the way $\rho^{\prime}$ is obtained from $\rho$, we write $\rho\equiv^{sh}_{\sigma}\rho^{\prime}$, for $\sigma:[{1},{n}]\to[{1},{n}]$ the associated permutation. It is easy to see that, due to the requirement that interchanges are proper, the relation $\equiv^{sh}$ is indeed symmetric.

For instance, in Fig. 2(b) it is easy to see that the derivation $G_{s}\stackrel{{\scriptstyle{p_{a}}}}{{\Longrightarrow}}G_{b}\stackrel{{\scriptstyle{p_{b}}}}{{\Longrightarrow}}G_{ab}$ consists of sequentially independent direct derivations. It is shift equivalent to $G_{s}\stackrel{{\scriptstyle{p_{b}}}}{{\Longrightarrow}}G_{a}\stackrel{{\scriptstyle{p_{a}}}}{{\Longrightarrow}}G_{ab}$, via the permutation $\sigma=\{(1,2),(2,1)\}$.

Two decorated derivations are said to be shift equivalent when the underlying derivations are, i.e., $\langle\alpha,\rho,\omega\rangle\equiv^{sh}\langle\alpha,\rho^{\prime},\omega\rangle$ if $\rho\equiv^{sh}\rho^{\prime}$. Then the equivalence of interest arises by joining abstraction and shift equivalence.

Definition 39** (concatenable traces)**

We denote by $\equiv^{c}$ the equivalence on decorated derivations arising as the transitive closure of the union of the relations $\equiv^{a}$ and $\equiv^{sh}$. Equivalence classes of decorated derivations with respect to $\equiv^{c}$ are denoted as $[\psi]_{c}$ and are called concatenable (derivation) traces. □

We will sometimes annotate $\equiv^{c}$ with the permutation relating the equivalent permutations. Formally, $\equiv^{c}_{\sigma}$ can be defined inductively as: if $\psi\equiv^{a}\psi^{\prime}$ then $\psi\equiv^{c}_{id}\psi^{\prime}$ , if $\psi\equiv^{sh}_{\sigma}\psi^{\prime}$ then $\psi\equiv^{c}_{\sigma}\psi^{\prime}$, and if $\psi\equiv^{c}_{\sigma}\psi^{\prime}$ and $\psi^{\prime}\equiv^{c}_{\sigma^{\prime}}\psi^{\prime\prime}$ then $\psi\equiv^{c}_{\sigma^{\prime}\circ\sigma}\psi^{\prime\prime}$.

Several proofs concerning concatenable traces exploit a property of equivalence $\equiv^{c}$ presented in [2, Sec. 3.5], that we summarize and adapt here to our framework.

If $\psi$ and $\psi^{\prime}$ are decorated derivations, then a consistent permutation between their steps relates two direct derivations if they consume and produce the same items, up to an isomorphism that is consistent with the decorations.

Definition 40** (consistent permutation)**

Given a decorated derivation $\psi=\langle\alpha,\rho,\omega\rangle:G_{0}\stackrel{{\scriptstyle{}}}{{\Longrightarrow}}^{*}G_{n}$, we denote by $\mathsf{col}({\psi})$ the colimit of the corresponding diagram in category $\mathsf{Graph}_{T}$, and by $in^{X}_{\mathsf{col}({\psi})}$ the injection of $X$ into the colimit, for any graph $X$ in $\rho$. Given two such decorated derivations $\psi$ and $\psi^{\prime}$ of equal length $n$, a consistent permutation $\sigma$ from $\psi$ to $\psi^{\prime}$ is a permutation $\sigma$ on $[{1},{n}]$ such that

there exists an isomorphism $\xi:\mathsf{col}({\psi})\to\mathsf{col}({\psi^{\prime}})$; 2. 2.

for each $i\in[{1},{n}]$ the direct derivations $\delta_{i}$ of $\psi$ and $\delta_{\sigma(i)}$ of $\psi^{\prime}$ use the same rule; 3. 3.

for each $i\in[{1},{n}]$, let $p:(L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle r}}{{\rightarrow}}R)$ be the rule used by direct derivations $\delta_{i}:G_{i-1}\stackrel{{\scriptstyle{p/m}}}{{\Longrightarrow}}G_{i}$ and $\delta^{\prime}_{\sigma(i)}:G^{\prime}_{\sigma(i)-1}\stackrel{{\scriptstyle{p/m^{\prime}}}}{{\Longrightarrow}}G^{\prime}_{\sigma(i)}$; then

• •

$\xi\circ in^{G_{i-1}}_{\mathsf{col}({\psi})}\circ m^{L}=in^{G_{\sigma(i)-1}}_{\mathsf{col}({\psi^{\prime}})}\circ m^{\prime L}$, and

• •

$\xi\circ in^{G_{i}}_{\mathsf{col}({\psi})}\circ m^{R}=in^{G_{\sigma(i)}}_{\mathsf{col}({\psi^{\prime}})}\circ m^{\prime R}$; 4. 4.

[$\alpha$-consistency] $\xi\circ in^{G_{0}}_{\mathsf{col}({\phi})}\circ\alpha=in^{G^{\prime}_{0}}_{\mathsf{col}({\phi^{\prime}})}\circ\alpha^{\prime}$; 5. 5.

[$\omega$-consistency] $\xi\circ in^{G_{n}}_{\mathsf{col}({\phi})}\circ\omega=in^{G^{\prime}_{n}}_{\mathsf{col}({\phi^{\prime}})}\circ\omega^{\prime}$;

A permutation $\sigma$ from $\psi$ to $\psi^{\prime}$ is called left-consistent if it satisfies conditions (1)-(4), but possibly not $\omega$-consistency. It is easy to show, by induction on the length of derivations, that the isomorphism $\xi:\mathsf{col}({\psi})\to\mathsf{col}({\psi^{\prime}})$ is uniquely determined by conditions (2)-(4), if it exists.

□

In the case of linear rules the existence of a consistent permutation is a characterisation of equivalence $\equiv^{c}$. Here, it just provides a necessary condition.

Lemma 17

Let $\psi$, $\psi^{\prime}$ be decorated derivations.

if $\psi\equiv^{c}_{\sigma}\psi^{\prime}$ then $|\psi|=|\psi^{\prime}|$ and $\sigma$ is a consistent permutation on $[{1},{|\psi|}]$ between them. We write $\psi\equiv^{c}_{\sigma}\psi^{\prime}$ in this case. 2. 2.

If $\psi;\psi_{1}\equiv^{c}_{\sigma}\psi^{\prime};\psi^{\prime}_{1}$ and $\psi\equiv^{c}_{\sigma_{0}}\psi^{\prime}$, then $\sigma_{0}$ is the restriction of $\sigma$ to $[{1},{|\psi|}]$. In this case it also holds $\psi_{1}\equiv^{c}_{\sigma_{1}}\psi^{\prime}_{1}$, with $\sigma_{1}(i)=\sigma(i+|\psi|)-|\psi|$. 3. 3.

If $\psi\equiv^{c}\psi^{\prime}$, then there is a unique consistent permutation $\sigma$ such that $\psi\equiv^{c}_{\sigma}\psi^{\prime}$.

□

Proof

[sketch]

This holds by [2, Thm. 3.5.3]. Just note that the proof of this direction does not use linearity of rules. 2. 2.

Suppose by absurd that $j$ be the smallest index in $[{1},{|\psi|}]$ such that $\sigma(j)\not=\sigma_{0}(j)$. Let $p:(L\stackrel{{\scriptstyle l}}{{\leftarrow}}K\stackrel{{\scriptstyle r}}{{\rightarrow}}R)$ be the rule used in $\delta_{j}$ and let $x\in L\setminus{l(K)}$ be an item consumed by it, which exists because all rules are consuming. By Definition 40 we deduce that both direct derivations $\delta^{\prime}_{\sigma(j)}$ and $\delta^{\prime}_{\sigma_{0}(j)}$ of $\psi^{\prime};\psi^{\prime}_{1}$ use the same rule $p$ (say, with matches $m^{\prime}$ and $m^{\prime\prime}$), and that the items ${m^{\prime}}^{L}(x)\in G^{\prime}_{\sigma(j)-1}$ and ${m^{\prime\prime}}^{L}(x)\in G^{\prime}_{\sigma_{0}(j)-1}$ which are consumed by $\delta^{\prime}_{\sigma(j)}$ and $\delta^{\prime}_{\sigma_{0}(j)}$, respectively, are identified in the colimit $\mathsf{col}({\psi^{\prime};\psi^{\prime}_{1}})$ (actually, from $\psi\equiv^{c}_{\sigma_{0}}\psi^{\prime}$ we know that there is a morphism $G^{\prime}_{\sigma_{0}(j)-1}\to\mathsf{col}({\psi^{\prime}})$, but we can compose it with the obvious – not necessarily injective – morphism $\mathsf{col}({\psi^{\prime}})\to\mathsf{col}({\psi^{\prime};\psi^{\prime}_{1}})$). But given the shape of the derivation diagram determined by the left-linearity of rules, and the properties of colimits in $\mathsf{Graph}$, this is not possible, because there is no undirected path of morphisms relating the images of element $x\in L$ in $G^{\prime}_{\sigma(j)-1}$ and $G^{\prime}_{\sigma_{0}(j)-1}$ respectively. Therefore $\sigma$ and $\sigma_{0}$ must coincide on $[{1},{|\psi|}]$.

For the second part, by the fact just proved clearly $\sigma_{1}$ is a well-defined permutation on $[{1},{|\psi_{1}|}]$. Then the fact that $\psi_{1}\equiv^{c}_{\sigma_{1}}\psi^{\prime}_{1}$ is almost immediate. Only commutation of the source decorations is not obvious, but it follows from commutation of the target for $\psi\equiv^{c}_{\sigma_{0}}\psi^{\prime}$ and Definition 35. 3. 3.

Direct consequence of the previous point, considering zero-length decorated derivations $\psi_{1}$ and $\psi_{1}^{\prime}$.

■

The sequential composition of decorated derivations lifts to composition of derivation traces so that we can consider the corresponding category.

Definition 41** (category of concatenable traces)**

Let $\mathcal{G}$ be a graph grammar. The category of concatenable traces of $\mathcal{G}$, denoted by $\mathsf{Tr}({\mathcal{G}})$, has abstract graphs as objects and concatenable traces as arrows. □

V-B A weak prime domain for a grammar

For a grammar $\mathcal{G}$ we obtain a partially ordered representation of its derivations starting from the initial graph by considering the concatenable traces ordered by prefix. Formally, as done in [2, 3] for linear grammars, we consider the category $({[G_{s}]}\downarrow{\mathsf{Tr}({\mathcal{G}})})$, which, by definition of sequential composition between traces, is easily shown to be a preorder.

Proposition 14

Let $\mathcal{G}$ be a graph grammar. Then the category $({[G_{s}]}\downarrow{\mathsf{Tr}({\mathcal{G}})})$ is a preorder. □

Proof

Let $[\psi]:[G_{s}]\to[G]$, $[\psi^{\prime}]:[G_{s}]\to[G^{\prime}]$ be concatenable traces and let $[\psi_{1}],[\psi_{2}]:[\psi]\to[\psi^{\prime}]$ be arrows in the slice category. Spelled out, this means that $\psi_{1},\psi_{2}:G\to G^{\prime}$ are such that $\psi;\psi_{1}\equiv^{c}\psi;\psi_{2}\equiv^{c}\psi^{\prime}$. By point (2) of Lemma 17, using the fact that $\psi\equiv^{c}\psi$ we can conclude that $\psi_{1}\equiv^{c}\psi_{2}$, as desired. ■

Explicitly, elements of the preorder are concatenable traces $[\psi]_{c}:[G_{s}]\to[G]$ and, for $[\psi^{\prime}]_{c}:[G_{s}]\to[G^{\prime}]$, we have $[\psi]_{c}\sqsubseteq[\psi^{\prime}]_{c}$ if there is $\psi^{\prime\prime}:G\to G^{\prime}$ such that $\psi;\psi^{\prime\prime}\equiv^{c}\psi^{\prime}$. Note that, given two concatenable traces $[\psi]_{c}:[G_{s}]\to[G]$ and $[\psi^{\prime}]_{c}:[G_{s}]\to[G^{\prime}]$, if $[\psi]_{c}\sqsubseteq[\psi^{\prime}]_{c}\sqsubseteq[\psi]_{c}$ then $\psi$ can be obtained from $\psi^{\prime}$ by composing it with a zero-length trace. Hence the elements of the partial order induced by $({[G_{s}]}\downarrow{\mathsf{Tr}({\mathcal{G}})})$ intuitively consist of classes of concatenable traces whose decorated derivations are related by an isomorphism that has to be consistent with the decoration of the source. Once applied to the grammar in Fig. 2(a), this construction produces a domain isomorphic to that in Fig. 2(c).

Lemma 18

Let $\mathcal{G}$ be a graph grammar. The partial order induced by $({[G_{s}]}\downarrow{\mathsf{Tr}({\mathcal{G}})})$, denoted $\mathcal{P}({\mathcal{G}})$, has as elements $\langle{\psi}\rangle_{c}=\{[\psi\cdot\nu]_{c}\mid\nu:\mathsf{t}({\psi})\stackrel{{\scriptstyle\sim}}{{\to}}\mathsf{t}({\psi})\}$ and $\langle{\psi}\rangle_{c}\sqsubseteq\langle{\psi^{\prime}}\rangle_{c}$ if $\psi;\psi^{\prime\prime}\equiv^{c}\psi^{\prime}$ for some decorated derivation $\psi^{\prime\prime}$. □

Proof

Immediate. ■

The domain of interest is then obtained by ideal completion of $\mathcal{P}({\mathcal{G}})$, with (the principal ideals generated by) the elements in $\mathcal{P}({\mathcal{G}})$ as compact elements. In order to give a proof for this, we need a preliminary technical lemma that essentially proves the existence and provides the shape of the least upper bounds in the domain of traces.

Lemma 19** (properties of $\equiv^{c}$)**

Let $\psi$ and $\psi^{\prime}$ be decorated derivations. Then the following hold:

Let $\psi_{1},\psi_{1}^{\prime}$ be such that $\psi;\psi_{1}\equiv^{c}_{\sigma}\psi^{\prime};\psi_{1}^{\prime}$ and let $n=|\{j\in[{|\psi|},{|\psi;\psi_{1}|-1}]\mid\sigma(j)<|\psi^{\prime}|\}|$. Then for all $\phi_{2},\phi_{2}^{\prime}$ such that $\psi;\phi_{2}\equiv^{c}\psi^{\prime};\phi_{2}^{\prime}$ it holds $|\phi_{2}|\geq n$ and there are $\psi_{2},\psi_{2}^{\prime},\psi_{3}$ such that

• •

$\psi;\psi_{1}\equiv^{c}\psi;\psi_{2};\psi_{3}$**

• •

$\psi;\psi_{2}\equiv^{c}\psi^{\prime};\psi_{2}^{\prime}$**

• •

$|\psi_{2}|=n$** 2. 2.

Let $\psi_{1},\psi_{1}^{\prime}$, $\psi_{2},\psi_{2}^{\prime}$ be such that $\psi;\psi_{1}\equiv^{c}_{\sigma_{1}}\psi^{\prime};\psi_{1}^{\prime}$ and $\psi;\psi_{2}\equiv^{c}_{\sigma_{2}}\psi^{\prime};\psi_{2}^{\prime}$ with $\psi_{1},\psi_{2}$ of minimal length. Then $\psi_{1}\equiv^{c}_{\sigma}\psi_{2}\cdot\nu$, where $\nu:\mathsf{t}({\psi_{2}})\to\mathsf{t}({\psi_{2}})$ is some graph isomorphism and $\sigma(j)=\sigma_{2}^{-1}(\sigma_{1}(j+|\psi|))-|\psi|$ for $j\in[{0},{|\psi_{1}|-1}]$.

□

Proof

We first observe that if $\psi,\psi^{\prime}$ are derivation traces and $\psi_{1},\psi_{1}^{\prime}$ are such that $\psi;\psi_{1}\equiv^{c}_{\sigma}\psi^{\prime};\psi_{1}^{\prime}$, with $|\psi|=k$, $|\psi^{\prime}|=k^{\prime}$, $|\psi;\psi_{1}|=|\psi^{\prime};\psi_{1}^{\prime}|=h$ then there is a $\phi_{1}$ such that $\psi;\psi_{1}\equiv^{c}\psi;\phi_{1}\equiv^{c}_{\sigma_{1}}\psi^{\prime};\psi_{1}^{\prime}$ and

for $i,j\in[{|\psi|},{h-1}]$, $i\leq j$ implies $\sigma_{1}(i)\leq\sigma_{1}(j)$. (†)

In order to prove this, we can proceed by induction on the number of inversions $x=|\{(i,j)\in[{|\psi|},{h-1}]\mid i\leq j\ \land\ \sigma(i)>\sigma(j)\}|$, i.e., on the number of pairs $(i,j)$ in the interval of interest that do not respect the monotonicity condition. When $x=0$ the thesis immediately holds. Assume that $x>0$. Then there are certainly indices $j\in[{|\psi|},{h-2}]$ such that $\sigma(j)>\sigma(j+1)$. Among these, take the index $i$ such that $\sigma(i+1)$ is minimal. Then it can be shown that direct derivations at position $i$ and $i+1$ in $\psi_{1}$ are sequentially independent, and thus they can be switched, i.e., there is $\phi_{2}$ such that $\psi;\phi_{2}\equiv^{c}_{id[i\mapsto i+1,i+1\mapsto i]}\psi;\psi_{1}$. Therefore $\psi;\phi_{2}\equiv^{c}_{\sigma\circ id[i\mapsto i+1,i+1\mapsto i]}\psi^{\prime};\psi_{1}^{\prime}$. This reduces the number of inversions and thus the inductive hypothesis allows us to conclude.

In the same way, we can prove that there is a $\phi^{\prime}_{1}$ such that $\psi;\phi_{1}\equiv_{\sigma_{2}}^{c}\psi^{\prime};\phi^{\prime}_{1}\equiv^{c}\psi^{\prime};\psi_{1}^{\prime}$ and

for $i,j\in[{|\psi^{\prime}|},{h\!-\!1}]$, if $i\leq j$ then $\sigma^{-1}_{2}(i)\leq\sigma^{-1}_{2}(j)$ (‡)

Putting conditions (†) and (‡) together we derive that $\psi;\psi_{1}\equiv^{c}\psi;\phi_{1}\equiv^{c}_{\sigma^{\prime}}=\psi^{\prime};\phi^{\prime}_{1}\equiv^{c}\psi^{\prime};\psi^{\prime}_{1}$. Now let $y\in[{|\psi|},{h-1}]$ be the largest index such that $\sigma^{\prime}(y)<|\psi^{\prime}|$ (or $y=|\psi|$ if it does not exist), let $l_{3}=h-y$ and consider decorated derivations $\psi_{2},\psi_{3},\psi_{2}^{\prime},\psi_{3}^{\prime}$ such that $|\psi_{3}|=|\psi^{\prime}_{3}|=l_{3}$ and $\psi;\psi_{2};\psi_{3}=\psi;\phi_{1}\equiv^{c}_{\sigma^{\prime}}\psi^{\prime};\phi^{\prime}_{1}=\psi^{\prime};\psi^{\prime}_{2};\psi^{\prime}_{3}$. By construction we obtain that $|\psi_{2}|=n$ and that $\sigma^{\prime}$ restricts to a permutation $\sigma^{\prime}_{2}$ on $[{0},{|\psi;\psi_{2}|-1}]$. Commutation with the target decoration can be obtained, if necessary, by changing the $\omega$ decoration of $\psi_{2}$, affecting only the $\alpha$ decoration of $\psi_{3}$. Thus we conclude that $\psi;\psi_{2}\equiv^{c}\psi^{\prime};\psi_{2}^{\prime}$.

Finally, notice that by the definition of $y$ and the properties of $\sigma^{\prime}$, it follows that $\sigma^{\prime}(j)<|\psi^{\prime}|$ for all $j\in[{|\psi|},{|\psi;\psi_{2}|-1}]$ and $\sigma^{\prime}(j)\geq|\psi^{\prime}|$ for all $j\in[{|\psi;\psi_{2}|},{h-1}]$. That is, the direct derivations in $\psi_{2}$ match all direct derivations of $\psi^{\prime}$ that are not matched in $\psi$. This implies that there cannot exist a derivation $\phi_{2}$ shorter than $n$ such that $\psi;\phi_{2}\equiv^{c}\psi^{\prime};\phi_{2}^{\prime}$ for some $\phi_{2}^{\prime}$. 2. 2.

Let $n=|\psi|$ and $m=|\psi_{1}|=|\psi_{2}|$, which must have the same length. By the last part of the proof of the previous point, since both $\psi_{1}$ and $\psi_{2}$ are of minimal length, we have that for all $j\in[{n},{n+m-1}]$ it holds $\sigma_{1}(j)<|\psi^{\prime}|$ and $\sigma_{2}(j)<|\psi^{\prime}|$. Furthermore, $\sigma_{1}([{n},{n+m-1}])=\sigma_{2}([{n},{n+m-1}])$, because both $\psi_{1}$ and $\psi_{2}$ consist of direct derivation that match those of $\psi^{\prime}$ which are not matched in $\psi$.

Thus $\sigma(j)=\sigma_{2}^{-1}(\sigma_{1}(j+|\psi|))-|\psi|$ is a well-defined permutation on $[{0},{|\psi_{1}|-1}]$ from $\psi_{1}$ to $\psi_{2}$. It is easy to see that the only condition that can be violated for concluding $\psi_{1}\equiv^{c}_{\sigma}\psi_{2}$ is commutation of the target decorations. This can be reestablished by post-composing $\psi_{2}$ with a graph isomorphism.

■

Relying on the results above we can easily prove that the ideal completion of the partial order of traces is a domain.

Proposition 15** (domain of traces)**

Let $\mathcal{G}$ be a graph grammar. Then $\mathcal{D}({\mathcal{G}})=\mathsf{Idl}({\mathcal{P}({\mathcal{G}})})$ is a domain. □

Proof

By Lemma 7 it is sufficient to prove (1) that $\mathop{\downarrow\!{\langle{\psi}\rangle_{c}}}$ is finite for every $\langle{\psi}\rangle_{c}\in\mathcal{P}({\mathcal{G}})$, and (2) that if $\{\langle{\psi_{1}}\rangle_{c},\langle{\psi_{2}}\rangle_{c},\langle{\psi_{3}}\rangle_{c}\}$ is pairwise consistent then $\langle{\psi_{1}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$ exists and is consistent with $\langle{\psi_{3}}\rangle_{c}$.

Let $\langle{\psi^{\prime}}\rangle_{c}\sqsubseteq\langle{\psi}\rangle_{c}$. By Lemma 18 we know that $\psi^{\prime};\psi^{\prime\prime}\equiv^{c}_{\sigma}\psi$ for some decorated derivation $\psi^{\prime\prime}$ and a permutation $\sigma$. Now suppose that $\psi^{\prime}_{1}$ and $\psi^{\prime}_{2}$ are decorated derivations such that $\psi^{\prime}_{1};\psi^{\prime\prime}_{1}\equiv^{c}_{\sigma_{1}}\psi$ and $\psi^{\prime}_{2};\psi^{\prime\prime}_{2}\equiv^{c}_{\sigma_{2}}\psi$ for some $\psi^{\prime\prime}_{1}$, $\psi^{\prime\prime}_{2}$, and that $\sigma_{1}([{0},{|\psi^{\prime}_{1}|}])=\sigma_{2}([{0},{|\psi^{\prime}_{2}|}])\subseteq[{0},{|\psi|}]$. Then $\sigma_{2}^{-1}\circ\sigma_{1}$ is a permutation on $[{0},{|\psi^{\prime}_{1}|}]$ from $\psi^{\prime}_{1}$ to $\psi^{\prime}_{2}$ witnessing $\psi^{\prime}_{1}\equiv^{c}_{\sigma_{2}^{-1}\circ\sigma_{1}}\psi^{\prime}_{2};\nu$ for some isomorphism $\nu$. Therefore $\langle{\psi^{\prime}_{1}}\rangle_{c}=\langle{\psi^{\prime}_{2}}\rangle_{c}$. As a consequence, the cardinality of $\mathop{\downarrow\!{\langle{\psi}\rangle_{c}}}$ is bound by $2^{|\psi|}$. 2. 2.

Given two consistent elements $\langle{\psi_{1}}\rangle_{c}$ and $\langle{\psi_{2}}\rangle_{c}$ of $\mathcal{P}({\mathcal{G}})$, there exists $\langle{\psi}\rangle_{c}=\langle{\psi_{1}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$, where $\psi$ is the minimal common extension of $\psi_{1}$ and $\psi_{2}$, provided by Lemma 19(1). Uniqueness of $\langle{\psi}\rangle_{c}$ follows by Lemma 19(2) because minimal common are essentially unique (up to $\equiv^{c}$ and right-composition with isomorphisms). Suppose further that $\langle{\psi_{3}}\rangle_{c}$ is compatible with both $\langle{\psi_{1}}\rangle_{c}$ and $\langle{\psi_{2}}\rangle_{c}$: we have to show that it is compatible with $\langle{\psi}\rangle_{c}$. Let $\langle{\psi^{\prime}}\rangle_{c}=\langle{\psi_{2}}\rangle_{c}\sqcup\langle{\psi_{3}}\rangle_{c}$. Then there exist $\phi_{1}$, $\phi$ and $\phi^{\prime}$ such that $\psi_{1};\phi_{1}\equiv^{c}_{\sigma_{1}}\psi_{2};\phi\equiv^{c}_{\sigma}\psi$ and $\psi_{2};\phi^{\prime}\equiv^{c}_{\sigma^{\prime}}\psi^{\prime}$ for suitable permutations $\sigma_{1}$, $\sigma$ and $\sigma^{\prime}$.

We conclude by showing that either $\langle{\psi}\rangle_{c}$ and $\langle{\psi^{\prime}}\rangle_{c}$ are compatible, or $\langle{\psi_{1}}\rangle_{c}\sqcup\langle{\psi_{3}}\rangle_{c}$ and $\langle{\psi^{\prime}}\rangle_{c}$ are compatible, both of which are equivalent and imply the thesis. We proceed by induction on $k=|\psi_{1}|+|\psi_{3}|$. If $|\psi_{1}|=0$, i.e. $\psi_{1}$ is a zero-length decorated derivation, hence, by Lemma 19, also $\phi$ is so and thus $\langle{\psi}\rangle_{c}=\langle{\psi_{2}}\rangle_{c}$, and the latter is compatible with $\langle{\psi^{\prime}}\rangle_{c}$. If $|\psi_{3}|=0$ we conclude analogously. If $k>0$, let $\delta$ be the last derivation step in $\psi_{1}$, i.e., $\psi_{1}=\psi_{1}^{\prime};\delta$. If $\sigma_{1}(|\psi_{1}|-1)<|\psi_{2}|$, namely if step $\delta$ is already in $\psi_{2}$, then by Lemma 19 we get that $\langle{\psi}\rangle_{c}=\langle{\psi_{1}^{\prime}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$. Since $|\psi_{1}^{\prime}|<k$ we conclude by inductive hypothesis that $\psi$ and $\psi^{\prime}$ are compatible. If instead, $\sigma_{1}(|\psi_{1}|-1)\geq|\psi_{2}|$ then, again by Lemma 19, we can write $\psi$ as $\psi\equiv^{c}_{\sigma^{\prime\prime}}\psi_{2};\phi^{\prime\prime};\delta^{\prime}$, where $\langle{\psi_{2};\phi^{\prime\prime}}\rangle_{c}=\langle{\psi_{1}^{\prime}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$ and $\sigma^{\prime\prime}(|\psi_{1}|-1)=|\psi|-1$, i.e., $\delta$ is mapped to $\delta^{\prime}$. Hence, by inductive hypothesis $\psi_{2};\phi^{\prime\prime}$ and $\psi^{\prime}$ are compatible.

Now, since $\langle{\psi_{1}}\rangle_{c}$ and $\langle{\psi_{3}}\rangle_{c}$ are compatible (thus $\psi_{1};\phi^{\prime}_{1}\equiv^{c}_{\sigma_{3}}\psi_{3};\phi^{\prime}_{3}$ for suitable derivations $\phi^{\prime}_{1},\phi^{\prime}_{3}$ and permutation $\sigma_{3}$), either step $\delta$ is already in $\psi_{3}$ (thus $\sigma_{3}(|\psi_{1}|-1)<|\psi_{3}|)$, or it isn’t, and $\sigma_{3}(|\psi_{1}|-1)\geq|\psi_{3}|$. In the first case $\delta$ is related to a step in $\psi^{\prime}$, and it follows that $\langle{\psi^{\prime}}\rangle_{c}\sqcup\langle{\psi_{2};\phi^{\prime\prime}}\rangle_{c}=\langle{\psi^{\prime}}\rangle_{c}\sqcup\langle{\psi_{2};\phi^{\prime\prime};\delta^{\prime}}\rangle_{c}$ and we conclude. If instead $\delta$ is not a step in $\psi_{3}$, we can write $\psi_{3};\phi^{\prime}_{3}$ as $\psi_{3};\phi^{\prime\prime}_{3};\delta^{\prime\prime}$, where step $\delta^{\prime\prime}$ matches step $\delta$ of $\psi_{1}$. By inductive hypothesis we have that $\psi_{3};\phi^{\prime\prime}_{3}$ and $\psi^{\prime}$ are compatible, and we get $\langle{\psi_{3};\phi^{\prime\prime}_{3}}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}=\langle{\psi_{2};\phi^{\prime\prime}}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}$. Since both steps $\delta^{\prime}$ and $\delta^{\prime\prime}$ are related by suitable permutations to step $\delta$ of $\psi_{1}$, we can extend uniformly the two derivations preserving consistency, obtaining $\langle{\psi_{3};\phi^{\prime\prime}_{3};\delta^{\prime\prime}}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}=\langle{\psi_{2};\phi^{\prime\prime};\delta^{\prime}}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}=\langle{\psi}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}$, as desired.

■

We can show that $\mathcal{D}({\mathcal{G}})$ is a weak prime domain. The proof relies on the fact that irreducibles are (the principal ideals of) elements of the form $\langle{\epsilon}\rangle_{c}$, where $\epsilon=\psi;\delta$ is a decorated derivation such that its last direct derivation $\delta$ cannot be shifted back, i.e., minimal traces enabling some direct derivation. These are called pre-events in [2, 3], where graph grammars are linear and thus, consistently with Lemma 2, such elements provide the primes of the domain. Two irreducibles $\langle{\epsilon}\rangle_{c}$ and $\langle{\epsilon^{\prime}}\rangle_{c}$ are interchangeable when they are different minimal traces for the same direct derivation.

Theorem 6** (weak prime domains from graph grammars)**

Let $\mathcal{G}$ be a graph grammar. Then $\mathcal{D}({\mathcal{G}})$ is a weak prime domain. □

Proof

We know by Proposition 15 that $\mathcal{D}({\mathcal{G}})$ is a domain. Hence, recalling Definition 14, we have to show that $\mathcal{D}({\mathcal{G}})$ is weak prime algebraic.

We will exploit the characterisation in Lemma 7. First provide a characterisation of irreducibles and of the interchangeability relation among them. As usual, we confuse compact elements of $\mathcal{D}({\mathcal{G}})$ with the corresponding generators in $\mathcal{P}({\mathcal{G}})$.

As mentioned above, irreducibles in $\mathcal{D}({\mathcal{G}})$ are, in the terminology of [2, 3], pre-events, namely elements of the form $\langle{\epsilon}\rangle_{c}$, where $\epsilon=\psi;\delta$ is a decorated derivation such that its last direct derivation $\delta$ cannot be switched back. Formally, $\langle{\epsilon}\rangle_{c}$ is a pre-event if letting $n=|\epsilon|$ then for all $\epsilon=\psi;\delta\equiv^{c}_{\sigma}\psi^{\prime}$ it holds $\sigma(n)=n$.

In fact, assume that $\langle{\epsilon}\rangle_{c}=\langle{\psi_{1}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$, and let $\epsilon\equiv^{c}_{\sigma}\psi_{1};\psi_{1}^{\prime}\equiv^{c}_{\sigma^{\prime}}\psi_{2};\psi_{2}^{\prime}$ for suitable $\psi_{1}^{\prime},\psi_{2}^{\prime}$ of minimal length. Since $\epsilon$ is a pre-event, we have that if $n=|\psi;\delta|=|\psi_{1};\psi_{1}^{\prime}|=|\psi_{2};\psi_{2}^{\prime}|$, then $\sigma^{\prime}(n)=n$. This implies that $|\psi_{1}^{\prime}|=0$ (and thus $\langle{\epsilon}\rangle_{c}=\langle{\psi_{1}}\rangle_{c}$) or $|\psi_{2}^{\prime}|=0$ (and thus $\langle{\epsilon}\rangle_{c}=\langle{\psi_{2}}\rangle_{c}$), as desired.

Two irreducibles $\langle{\epsilon}\rangle_{c}$ and $\langle{\epsilon^{\prime}}\rangle_{c}$ are interchangeable iff the corresponding traces are compatible and whenever $\epsilon;\psi_{1}\equiv^{c}_{\sigma}\epsilon^{\prime};\psi_{1}^{\prime}$ with $\psi_{1},\psi_{1}^{\prime}$ of minimal length (thus $\langle{\epsilon;\psi_{1}}\rangle_{c}=\langle{\epsilon^{\prime};\psi^{\prime}_{1}}\rangle_{c}=\langle{\epsilon}\rangle_{c}\sqcup\langle{\epsilon^{\prime}}\rangle_{c}$), then $\sigma(|\epsilon|)=|\epsilon^{\prime}|$.

In fact, assume that $\langle{\epsilon}\rangle_{c}=\langle{\psi;\delta}\rangle_{c}$ and $\langle{\epsilon^{\prime}}\rangle_{c}=\langle{\psi^{\prime};\delta^{\prime}}\rangle_{c}$ are interchangeable, and $\epsilon;\psi_{1}\equiv^{c}_{\sigma}\epsilon^{\prime};\psi_{1}^{\prime}$ with $\psi_{1},\psi_{1}^{\prime}$ of minimal length. By the proof of Lemma 19(1) we have that $\sigma$ maps steps in $\psi_{1}$ to $\epsilon^{\prime}$ and, analogously, $\sigma^{-1}$ maps steps in $\psi_{1}^{\prime}$ to $\epsilon$ (formally, $\sigma(j)<|\epsilon^{\prime}|$ for $j\geq|\epsilon|$ and, dually, if $\sigma(j)\geq|\epsilon^{\prime}|$ then $j<|\epsilon|$). By Lemma 5(3) we have that $\langle{\epsilon}\rangle_{c}\sqcup\langle{\epsilon^{\prime}}\rangle_{c}=\langle{\psi}\rangle_{c}\sqcup\langle{\epsilon^{\prime}}\rangle_{c}=\langle{\epsilon}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}$. Hence we can view the previous equivalence of decorated derivations as $\psi;(\delta;\psi_{1})\equiv^{c}_{\sigma}(\psi^{\prime};\delta^{\prime});\psi_{1}^{\prime}$, with $\delta;\psi_{1}$ and $\psi_{1}^{\prime}$ of minimal length. This means that $\sigma$ maps steps in $\delta;\psi_{1}$ to $\epsilon^{\prime}$ and, with a dual argument, steps in $\delta^{\prime};\psi_{1}^{\prime}$ to $\epsilon$. Putting all this together we get that necessarily $\sigma(|\epsilon|)=|\epsilon^{\prime}|$, as desired.

For the converse, assume that $\langle{\epsilon}\rangle_{c}$, $\langle{\epsilon^{\prime}}\rangle_{c}$ are compatible, that $\langle{\psi}\rangle_{c}=\langle{\epsilon}\rangle_{c}\sqcup\langle{\epsilon^{\prime}}\rangle_{c}$, and that $\psi\equiv^{c}\epsilon;\psi_{1}\equiv^{c}_{\sigma}\epsilon^{\prime};\psi_{1}^{\prime}$ where $\sigma(|\epsilon|)=|\epsilon^{\prime}|$. Then, reverting the reasoning above, we get that $\langle{\psi}\rangle_{c}\sqcup\langle{\epsilon^{\prime}}\rangle_{c}=\langle{\epsilon}\rangle_{c}\sqcup\langle{\psi^{\prime}}\rangle_{c}$, and thus we conclude that $\langle{\epsilon}\rangle_{c},\langle{\epsilon^{\prime}}\rangle_{c}$ are interchangeable by Lemma 5(3).

We conclude that $\mathcal{D}({\mathcal{G}})$ is a weak prime domain, relying on Lemma 7. Let $\langle{\epsilon}\rangle_{c}$ with $\epsilon=\psi;\delta$ be an irreducible, and $\langle{\epsilon}\rangle_{c}\sqsubseteq\langle{\psi_{1}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$. Let $\psi_{1}^{\prime}$ and $\psi_{2}^{\prime}$ be decorated derivations of minimal length such that $\epsilon;\psi\equiv^{c}_{\sigma}\psi_{1};\psi_{1}^{\prime}\equiv^{c}_{\sigma_{1}}\psi_{2};\psi_{2}^{\prime}$ for some $\psi$. If $\sigma(|\epsilon|)\in[{0},{|\psi_{1}|-1}]$ then consider $\phi_{1}$ such that $\psi_{1};\psi_{1}^{\prime}\equiv^{c}_{\sigma^{\prime}}\phi_{1};\psi_{1}^{\prime}$ and $\sigma^{\prime}(\sigma(|\epsilon|))$ is minimal. Then $\langle{\phi_{1}}\rangle_{c}$ is an irreducible, $\langle{\phi_{1}}\rangle_{c}$ and $\langle{\epsilon}\rangle_{c}$ are interchangeable, and clearly $\langle{\phi_{1}}\rangle_{c}\sqsubseteq\langle{\psi_{1}}\rangle_{c}$. If instead $\sigma(|\epsilon|)\geq|\psi_{1}|$ we have that $\sigma_{1}(\sigma(|\epsilon|))<|\psi_{2}|$, and we can conclude, in the same way, the existence of $\langle{\phi_{2}}\rangle_{c}\sqsubseteq{\langle{\psi_{2}}\rangle_{c}}$ irreducible and interchangeable with $\langle{\epsilon}\rangle_{c}$. ■

Note that when the rules are right-linear the domain and es semantics specialises to the usual prime event structure semantics (see [2, 3, 4]), since the construction of the domain in the present paper is formally the same as in [2].

V-C Any connected es is generated by some grammar

By Theorem 6, given a graph grammar $\mathcal{G}$ the domain $\mathcal{D}({\mathcal{G}})$ is weak prime. We next show that also the converse holds, i.e., any connected es (and thus any weak prime domain) is generated by a suitable graph grammar. This shows that weak prime domains and connected es are precisely what is needed to capture the concurrent semantics of non-linear graph grammars, and thus strengthen our claim that they represent the right structure for modelling formalisms with fusions.

Construction (graph grammar for a connected es) Let $\langle E,\#,\vdash\rangle$ be a connected es. The grammar $\mathcal{G}_{E}=\langle T,P,\pi,G_{s}\rangle$ is defined as follows.

First, for every element $e\in E$, we define the following graphs, which are then used as basic building blocks

• •

$I_{e}$ and $S_{e}$ as shown in Fig. 14(14(a)) and Fig. 14(14(b));

• •

let $U_{e}$ denote the set-theoretical product of the minimal enablings of $e$, i.e., $U_{e}=\Pi\{X\subseteq E\mid X\vdash_{0}e\}$; for every tuple $u\in U_{e}$ we define the graph $L_{u,e}$ as in Fig. 14(14(c)).

Moreover, for every pair of events $e,e^{\prime}\in E$ such that $e\#e^{\prime}$, we define a graph $C_{e,e^{\prime}}$ as in Fig. 14(14(d)).

The set of productions is $P=E$, i.e., we add a rule for every event $e\in E$, and we define such rule in a way that

• •

it deletes $I_{e}$ and $C_{e,e^{\prime}}$ for each $e^{\prime}\in E$ such that $e\#e^{\prime}$.

• •

it preserves the graph $S_{e}\cup\bigcup_{u\in U_{e}}L_{u,e}$

• •

for all $e^{\prime}\in E$, for all graphs $L_{u,e^{\prime}}$ such that $e$ occurs in $u$, it merges the corresponding nodes and that of $S_{e^{\prime}}$ into one.

The graph $S_{e}\cup\bigcup_{u\in U_{e}}L_{u,e}$ arises from $S_{e}$ and $L_{u,e}$, $u\in U_{e}$ by merging all the nodes (we use $\bigcup$ and $\biguplus$ to denote union and disjoint union, respectively, with a meaning illustrated in Fig. 14(14(f)) and Fig. 14(14(g)).) Hence, there is a match for the rule $e$ only if $S_{e}$ and all $L_{u,e}$ for $u\in U_{e}$ have been merged and this happens if and only if at least one minimal enabling of $e$ has been entirely executed. The deletion of the graphs $C_{e,e^{\prime}}$ establishes the needed conflicts. The rule is consuming since it deletes the node of graph $I_{e}$.

Formally, the rule for $e$ has as left-hand side the graph

[TABLE]

while the right-hand side is

[TABLE]

The rule is schematised in Fig. 14(14(e)), where it is intended that $e$ occurs in $u_{j}^{1},\ldots,u_{j}^{n_{j}}$ for $u_{j}^{i}\in U_{e_{j}}$, $i\in[{1},{n_{j}}]$, $j\in[{1},{k}]$. Moreover $e_{1}^{\prime},\ldots,e_{h}^{\prime}$ are the events in conflict with $e$ and, finally, $U_{e}=\{u_{1},\ldots,u_{n}\}$.

The start graph is just the disjoint union of all the basic graphs introduced above

[TABLE]

Then the type graph is

[TABLE]

Note that the interfaces of the rules are not given explicitly. They can be deduced from the left and right-hand side, and the labelling. The same applies to the type graph.

It is not difficult to show that the grammar $\mathcal{G}_{E}$ generates exactly the es ${E}$.

Theorem 7** (connected ES from graph grammars)**

Let $\langle E,\#,\vdash\rangle$ be a connected es. Then, ${E}$ and $\mathcal{E}({\mathcal{D}({\mathcal{G}_{E}})})$ are isomorphic. □

Proof

First observe that any rule in $\mathcal{G}_{E}$ is executed at most once in a derivation since it consumes an item (the node of graph $I_{e}$) that is generated by no other rule. If we consider $\mathcal{D}({\mathcal{G}_{E}})$, then the irreducibles are minimal $\langle{\epsilon}\rangle_{c}$ with $\epsilon=\psi;\delta$. By the shape of rule $e$, the derivation $\psi$ must contain the occurrences of a minimal set of rules such that the graphs $S_{e}$ and $L_{u,e}$ for $u\in U_{e}$ are merged along the common node. By construction, in order to merge all such graphs, if we denote by $X_{\psi}$ the set of rules applied in $\psi$, it must be $X_{\psi}\supseteq C$ for some $C\in\mathit{Conf_{F}}({E})$ such that $C\vdash_{0}e$. Therefore by minimality we conclude that $X_{\psi}\vdash_{0}e$. Relying on this observation, a routine induction on the $|C|$ shows that minimal enablings $C\vdash_{0}e$ in $E$ are in one to one correspondence with irreducibles $\langle{\epsilon}\rangle_{c}$ in $\mathcal{D}({\mathcal{G}_{E}})$. Recalling, that, in turn, irreducibles in $\mathcal{D}({E})$ are again minimal enablings, i.e., $\langle{C},{e}\rangle$ with $C\in\mathit{Conf_{F}}({E})$ such that $C\vdash_{0}e$ we obtain a bijection between irreducibles in $\mathcal{D}({\mathcal{G}_{E}})$ and $\mathcal{D}({E})$.

The fact that the correspondence preserves and reflects the order is, again, almost immediate by construction. In fact, consider two irreducibles $\langle{\epsilon}\rangle_{c}$ and $\langle{\epsilon^{\prime}}\rangle_{c}$ in $\mathcal{D}({\mathcal{G}_{E}})$ and the corresponding irreducibles $\langle{C},{e}\rangle$ and $\langle{C^{\prime}},{e^{\prime}}\rangle$ in $\mathcal{D}({E})$. If $\langle{C},{e}\rangle\subseteq\langle{C^{\prime}},{e^{\prime}}\rangle$, take $X=\langle{C^{\prime}},{e^{\prime}}\rangle\setminus\langle{C},{e}\rangle$. Then $\epsilon$ can be extended with the rules corresponding to the events in $X$, thus showing the existence of a derivation $\psi$ such that $\epsilon;\psi\equiv^{c}\epsilon^{\prime}$. In fact, if this were not possible, there would be an event $e^{\prime\prime}\in X$ such that the corresponding rule compete for deleting some item of the start graph with a rule $e_{1}$ in $\epsilon$, hence $e_{1}\in\langle{C},{e}\rangle$. By construction, the only possibility is that the common item is $C_{e^{\prime\prime},e_{1}}$. But this would mean that $e^{\prime\prime}\#e_{1}$. This contradicts the fact that $\{e_{1},e^{\prime\prime}\}\subseteq\langle{C^{\prime}},{e^{\prime}}\rangle$. The converse, i.e., the fact that if $\langle{\epsilon}\rangle_{c}\sqsubseteq\langle{\epsilon^{\prime}}\rangle_{c}$ then $\langle{C},{e}\rangle\subseteq\langle{C^{\prime}},{e^{\prime}}\rangle$ is immediate.

Recalling that domains are irreducible algebraic (Proposition 1), we conclude that $\mathcal{D}({\mathcal{G}_{E}})$ and $\mathcal{D}({E})$ are isomorphic. Since $E$ is connected es, by Theorem 3, $E\simeq\mathcal{E}({\mathcal{D}({E})})$ and thus $\mathcal{E}({\mathcal{D}({\mathcal{G}_{E}})})$ and $E$ are isomorphic, as desired. ■

Example 2

Consider the running example es, from Example 1, with set of events $\{a,b,c\}$, empty conflict relation and the minimal enablings by $\{a\}\vdash_{0}c$ and $\{b\}\vdash_{0}c$. The associated grammar is depicted in Fig. 15.

As a further example, consider an es $E_{1}$ with events $\{a,b,c,d,e\}$. The conflict relation $\#$ is given by $e\#d$ and minimal enablings $\emptyset\vdash_{0}a$, $\emptyset\vdash_{0}b$, $\emptyset\vdash_{0}c$, $\emptyset\vdash_{0}e$, $\{a,b\}\vdash_{0}d$ and $\{c\}\vdash_{0}d$. The grammar is in Fig. 16. □

V-D A prime es semantics for grammars with fusions

A possibility for recovering a notion of causality based on prime es also for graph grammars with fusions is to introduce suitable restrictions on the concurrent applicability of rules. Indeed, the lack of stability arises essentially from considering as concurrent those fusions which act on common items. Preventing fusions to act on already merged items, one may lose some concurrency, yet gaining a definite notion of causality. Technically, a prime es can be obtained for left-linear rewriting systems by restricting the applicability condition: the match must be such that the pair $\langle l;m^{L},r\rangle$ of Fig. 11 is jointly mono. This essentially means that items which have been already fused, should not be fused again.

Formally, this means changing the applicability condition, restricting to fusion safe derivations.

Definition 42** (fusion safe (direct) derivation)**

A fusion safe direct derivation is a direct derivation as in Fig. 17 where $\langle l;m^{L},r\rangle$ is jointly mono. A derivation is fusion safe if it consists of a sequence of fusion safe direct derivations. □

Consider our running example in Fig. 2. Clearly, the derivations labelled $p_{a}$ and $p_{b}$ starting from $G_{s}$ are now in conflict, since e.g. the application of $p_{a}$ forbids the application of $p_{b}$ to $G_{a}$, since the derivation would not be anymore jointly mono. We thus end up in the situation presented by the configurations in Fig. 7, hence the applications of $p_{c}$ to $G_{a}$ and $G_{b}$ respectively must be considered as different events.

The notion of sequential independence remains unchanged. Note that the interchange operator (see Proposition 13) applied to sequential independent derivations that are fusion safe produces a new pair of fusion safe derivations. Then we can consider concatenable fusion safe traces, that form a subcategory of the category of traces.

Definition 43** (fusion safe traces)**

Let $\mathcal{G}$ be a graph grammar. The category of concatenable fusion safe traces of $\mathcal{G}$, denoted by $\mathsf{Tr}_{s}({\mathcal{G}})$, has abstract graphs as objects and concatenable fusion safe traces as arrows. □

The construction of Theorem 6 recasted on fusion safe traces now produces a prime domain (hence a prime es).

Theorem 8** (prime domain structure for graph grammars)**

Let $\mathcal{G}$ be a graph grammar. Then $\mathsf{Idl}({({[G_{s}]}\downarrow{\mathsf{Tr}_{s}({\mathcal{G}})})})$ is a prime domain. □

Proof

The proof is the same as for Theorem 6. We already know that the domain is weak prime, hence, by Proposition 3, all irreducibles are weak primes. Additionally, interchangeability, as characterised in the proof of the mentioned theorem, is the identity.

In fact, given two irreducibles $\langle{\epsilon_{i}}\rangle_{c}$ with $\epsilon_{i}=\psi_{i};\delta_{i}$ for $i\in\{1,2\}$ such that $\langle{\epsilon_{1}}\rangle_{c}\leftrightarrow\langle{\epsilon_{2}}\rangle_{c}$, by interchangeability $\langle{\psi_{1}}\rangle_{c}\sqcup\langle{\epsilon_{2}}\rangle_{c}=\langle{\epsilon_{1}}\rangle_{c}\sqcup\langle{\psi_{2}}\rangle_{c}$. Let such join be $\langle{\psi_{1};\delta_{1};\psi_{1}^{\prime}}\rangle_{c}=\langle{\psi_{2};\delta_{2};\psi_{2}^{\prime}}\rangle_{c}$ for suitable $\psi_{1}^{\prime},\psi_{2}^{\prime}$. This means that $\psi_{1};\delta_{1};\psi_{1}^{\prime}\equiv^{c}_{\sigma}\psi_{2};\delta_{2};\psi_{2}^{\prime}$ for a suitable permutation $\sigma$, with $\sigma(|\epsilon_{1}|)=\sigma(|\epsilon_{2}|)$. There are two possibilities. If $|\psi_{1}|=|\psi_{2}|$ and $\sigma$ restricts to a permutation of $[{1},{|\psi_{1}|}]$, then $\psi_{1}\equiv^{c}\psi_{2}$ and we conclude. Otherwise a step in $\psi_{2}$ is not mapped to $\psi_{1}$ or viceversa. Assume, without loss of generality, that there is $i\in[{1},{|\psi_{1}|}]$ such that $\sigma(i)>|\psi_{2}|$. This means that the $i$-th step in $\psi_{1}$ is performed in $\psi_{2}^{\prime}$. Since such step is performed after $\delta_{2}$, it cannot generate items consumed by $\delta_{1}$. Hence it must merge items that are merged by a different step in $\psi_{2}$. But this contradicts its fusion safety.

Hence all weak primes are primes and we conclude. ■

VI Conclusions and Related Work

In the paper we provided a characterisation of a class of domains, referred to as weak prime algebraic domains, which is appropriate for describing the concurrent semantics of those formalisms where a computational step can merge parts of the state. We show a categorical equivalence between weak prime algebraic domains and a suitably defined class of connected event structures. We also prove that the category of general event structures coreflects into the category of weak prime algebraic domains.

The appropriateness of the class of weak prime domains is witnessed by the results that show that weak prime algebraic domains are precisely those arising from left-linear graph rewriting systems, i.e., those systems where rules besides generating and deleting can also merge graph items. Furthermore, we show how to recover a prime event structures semantics also for rule-based formalisms with fusions by introducing suitable restrictions on the concurrent applicability of rules.

We have shown that the characterisations of prime domains and event structures in terms of intervals and asynchronous graphs naturally extend to weak prime domains. The characterisation of weak prime domains in terms of the interchangeability equivalence on irreducibles naturally suggest a presentation in terms of prime event structures endowed with an equivalence relation, allowing us to establish a link with the work in [23, 24].

Technically, the starting point for our proposal is the relaxation of the stability condition for event structures. As already noted by Winskel in [5] “[t]he stability axiom would go if one wished to model processes which had an event which could be caused in several compatible ways […]; then I expect complete irreducibles would play a similar role to complete primes here”. Indeed, the correspondence between irreducibles and weak primes, which exploits the notion of interchangeability, is the ingenious step that allows us to obtain a smooth extension of the classical duality between prime event structures and prime algebraic domains.

The coreflection between the category of general unstable event structures (with binary conflict) and the one of weak prime algebraic domains says that the latter are exactly the partial orders of configurations of the former. Such class of domains has been studied originally in [21] where, generalising the work on concrete domains and sequentiality [34], a characterisation is given in terms of a set of axioms expressing properties of prime intervals. In our paper we also provide an in depth comparison with these results, based on the observation that, roughly speaking, weak primes correspond to executions of events with their minimal enablings, while intervals can be seen as executions of events in a generic configuration. A comparison is also drawn with the more recent notions of asynchronous graph [29], an alternative representation of prime algebraic domains based on the notion of path equivalence, which we generalise in order to account for weak prime ones.

The need of resorting to unstable es for modelling the concurrent computations of name passing process calculi has been observed by several authors. In particular, in [17] an es semantics for the $\pi$-calculus is defined by relying on es with names, namely labelled es tailored for modelling parallel extrusions. An event can have various minimal enablings but with the constraint that distinct minimal enablings can differ only for one event (intuitively, the extruder). es with names are not connected es since they can have non-connected minimal enablings (roughly, because identical events in disconnected minimal enablings can be identified via the labelling). Nevertheless, a connected es semantics could be obtained by transforming es with names through the coreflection in the paper: More details are reported in Appendix -B.

We believe that our results cover a long road in establishing weak prime domains and connected event structures as a foundational concept in the event-based semantics for concurrent computational systems. Our next step will be to look at possible more general formalisms. In particular, the paper [35] studies a characterisation of the partial order of configurations for a variety of classes of event structures in terms of axiomatisability of the associated propositional theories. Even if the focus in the present paper is on event structures that generalise Winskel’s ones, we believe that our work can provide interesting suggestions for further development.

Acknowledgements

We are grateful to the anonymous referees of the conference version of the paper for their insightful comments and suggestions. We are also indebted to Paul-Andrè Melliés for insightful discussions on the relation between event structures and asynchronous graphs.

-A Event Structures with Non-Binary Conflict

In the literature also es with non-binary conflict have been considered, where the binary conflict relation is replaced by a consistency predicate [22]. It is noteworthy that the duality results of Section III easily adapt to this case.

Definition 44** (es with non-binary conflict)**

An es with non-binary conflict (esnb for short) is a tuple $\langle E,\vdash,Con\rangle$ such that

• •

$E$ is a set of events

• •

$Con\subseteq\mathbf{2}^{E}_{fin}$ is the consistency predicate, satisfying $X\in Con$ and $Y\subseteq X$ implies $Y\in Con$

• •

$\vdash\ \subseteq Con\times E$ is the enabling relation, satisfying $X\vdash e$ and $X\subseteq Y\in Con$ implies $Y\vdash e$.

The esnb ${E}$ is stable if $X\vdash e$, $Y\vdash e$, and $X\cup Y\cup\{e\}\in Con$ imply $X\cap Y\vdash e$. □

A configuration $C\subseteq E$ is just a set such that it is secured and all its finite subsets are consistent. The notion of live esnb is easily adapted to take into account non-binary conflicts and also in this case we will implicitly assume all esnb to be live.

Definition 45** (live esnb)**

An esnb ${E}$ is live if for all $X\in Con$ there is $C\in\mathit{Conf}({E})$ such that $X\subseteq C$ and moreover for all $e\in E$ we have $\{e\}\in Con$. □

The notion of the category of esnb is adapted accordingly.

Definition 46** (category of event structures)**

A morphism of esnb $f:{E}_{1}\to{E}_{2}$ is a partial function $f:E_{1}\to E_{2}$ such that for all $X_{1}\subseteq E_{1}$ and $e_{1},e_{1}^{\prime}\in E_{1}$ with $f(e_{1})$, $f(e_{1}^{\prime})$ defined

• •

if $X_{1}\in Con_{1}$ then $f(X_{1})\in Con_{2}$;

• •

if $\{e_{1},e_{1}^{\prime}\}\in Con_{1}$ and $f(e_{1})=f(e_{1}^{\prime})$ then $e_{1}=e_{1}^{\prime}$;

• •

if $X_{1}\vdash_{1}e_{1}$ then $f(X_{1})\vdash_{2}f(e_{1})$.

We denote by $\mathsf{ES_{nb}}$ the category of esnb and esnb morphisms, and by $\mathsf{cES_{nb}}$ its full subcategory having connected esnb as objects (the definition of conectedness remains unchanged). □

In the definition of domains (Definition 6), the existence of joins is now required only for consistent subsets, instead of being required for pairwise consistent.

Definition 47** (b-domains)**

A bounded complete domain (b-domain) is an algebraic finitary partial order where all consistent subsets $X\subseteq D$ admit a least upper bound $\bigsqcup X$. B-domain morphisms are as in Definition 15. We denote by $\mathsf{Dom_{b}}$ the corresponding category. □

The definition of weak prime algebraicity remains formally the same, but the underlying partial order is required to be a b-domain.

Definition 48** (weak prime algebraic b-domain)**

A weak prime algebraic b-domain (or simply weak prime b-domain) is a interchangeable b-domain $D$ such that for all $d\in D$ it holds $d=\bigsqcup(\mathop{\downarrow\!{d}}\cap\mathop{\mathit{wpr}({D})})$. We denote by $\mathsf{wDom_{b}}$ the corresponding category. □

The proof of the fact that, given an esnb ${E}$, the partial order of configurations $\mathcal{D}({{E}})=\langle\mathit{Conf}({{E}}),\subseteq\rangle$ is a weak prime b-domain, is unchanged. The same holds for the fact that if $f:E_{1}\to E_{2}$ is an esnb morphism then $\mathcal{D}({f}):\mathcal{D}({{E}_{1}})\to\mathcal{D}({{E}_{2}})$ is a weak prime b-domain morphism.

Vice versa the esnb associated with a weak prime b-domain is defined as follows.

Definition 49** (esnb for a weak prime b-domain)**

Let $D$ be a weak prime b-domain. The esnb $\mathcal{E}({D})=\langle E,Con,\vdash\rangle$ is defined as follows

• •

$E=[{\mathop{\mathit{ir}({D})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$;

• •

$Con=\{X\mid\exists d\in\mathop{\mathsf{K}({D})}.\ X\subseteq[{\mathop{\mathit{ir}({d})}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\}$;

• •

$X\vdash e$ if there exists $i\in e$ such that $[{\mathop{\mathit{ir}({i})}\setminus\{i\}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\subseteq X$.

Given a morphism $f:D_{1}\to D_{2}$, its image $\mathcal{E}({f}):\mathcal{E}({D_{1}})\to\mathcal{E}({D_{2}})$ is defined for $[{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}\in E$ as $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})=[{i_{2}}]_{\scriptscriptstyle{\leftrightarrow^{*}}}$, where $i_{2}\in\delta({f(i_{1})},{f(\mathit{p}({i_{1}}))})$, and $\mathcal{E}({f})([{i_{1}}]_{\scriptscriptstyle{\leftrightarrow^{*}}})$ is undefined if $f(\mathit{p}({i_{1}}))=f(i_{1})$. □

We then get a result corresponding to Theorem 1 for es with non-binary conflict and weak prime b-domains.

Theorem 9** (corecflection of $\mathsf{ES_{nb}}$ and $\mathsf{wDom_{b}}$)**

The functors $\mathcal{D}:\mathsf{ES_{nb}}\to\mathsf{wDom_{b}}$ and $\mathcal{E}:\mathsf{wDom_{b}}\to\mathsf{ES_{nb}}$ form a coreflection. It restricts to an equivalence between $\mathsf{wDom_{b}}$ and $\mathsf{cES_{nb}}$. □

Concerning the interval-based characterisation in Section IV-B, we recall that the paper by Droste [22] considers also the case of event structures with a general consistency relation (rather than a binary conflict) and shows that the corresponding domains can be characterised as algebraic complete partial orders where axioms (F), (C) of Section IV-B and, additionally, (I) below hold.

(I)

for all $x,x^{\prime},y,y^{\prime}\in\mathop{\mathsf{K}({D})}$ if $[{x},{x^{\prime}}]\sim[{y},{y^{\prime}}]$ and $x\sqsubseteq x^{\prime}$ then $y\sqsubseteq y^{\prime}$.

The definition of the es $\mathcal{E}_{wd}({D})$ associated with a domain $D$ (Definition 26) can be easily adapted to the non-binary case. The only thing that changes is the definition of consistency: a set $X\subseteq E$ is consistent if for all $e\in X$ there exists a representative $[{c_{e}},{c_{e}^{\prime}}]\in e$ such that $\{c_{e}\mid e\in X\}$ is bounded in $D$. Then the correspondence with our approach established in Section IV-B easily extends to this setting: algebraic complete partial orders where axioms (F), (C) and (I) hold are exactly the weak prime b-domains and the obvious rephrasing of Proposition 11 continue to hold.

Also the connection with asynchronous graphs in Section IV-C can be adapted easily. Unsurprisingly, Proposition 12 holds for connected es with non-binary conflict if we modify the definition of asynchronous graph (Definition 27) by omitting the coherence axiom (4).

-B An Event Structure Semantics for the $\pi$-calculus

The need of resorting to unstable es for modelling the concurrent computations of name passing process calculi has been observed by several authors. In particular, in [17] an es semantics for the pi-calculus is defined by relying on so-called es with names (esn for short), namely es that are tailored for parallel extrusions: labelled unstable es with the constraint that two minimal enablings can differ only for one event (intuitively, the extruder).

Given a global set of names $\mathcal{N}$, es with names (esn for short) are triples $(E,X,\lambda)$ where $E$ is a prime es, $X\subseteq\mathcal{N}$ is a set of names (intuitively, the names that are restricted), and $\lambda:E\to\{x(y),\bar{x}(y)\}$ is a function mapping each event to either an input or an output prefix.

A configuration $C$ is a configuration of the underlying prime es such that there exists a maximal $e\in C$ satisfying

• •

$C\setminus\{e\}$ is a configuration;

• •

if $\lambda(e)=x(y)$ or $\lambda(e)=\bar{x}(y)$ with $x\in X$ then there exists $e^{\prime}\in C\setminus\{e\}$ such that $\lambda(e^{\prime})=\bar{z}(x)$.

The latter requirement above boils down to ensuring that if the name were restricted, it has been extruded before. Thus, esn are unstable es with the additional constraint that two minimal enablings can differ only for one event (the extruder!): namely, if $X_{1}\vdash_{0}e$ and $X_{2}\vdash_{0}e$ then $X_{1}\cap X_{2}=X_{1}\setminus\{e_{1}\}=X_{2}\setminus\{e_{2}\}$ for suitable $e_{1},e_{2}$.

Note that, esn are not connected es since they can have non-connected minimal enablings (roughly, because identical events in disconnected minimal enablings are identified via the labelling). Consider e.g. $E=\{\bar{a}(x),\bar{b}(x),x(y)\}$, with $\bar{a}(x)\#\bar{b}(x)$, and $X=\{x\}$. Then the configurations are $\emptyset$, $\{\bar{a}(x)\}$, $\{\bar{b}(x)\}$, $\{\bar{a}(x),x(y)\}$, and $\{\bar{b}(x),x(y)\}$, hence $x(y)$ has two non-connected minimal enablings.