What is a State of a System? (an outline)

Uri Abraham Department of mathematics and computer science Ben-Gurion University, Be’er Sheva, ISRAEL.

Abstract

We try to answer this question in defining a state as a kind of a pomset. The notion of a pomset is extended by adding to the unary predicates unary functions of bounded depth. We show the equivalence of two approaches to modeling concurrency: the sequential point of view (which is based on states) and the partial-order point of view (based on events). This note points to a possible approach for defining the semantics of communicating processes. We define and show how to work with a natural subclass of information systems, which were introduced by Scott to give denotational domains.

1 Preface

For sequential processes, a state is simply the complete information on all the variables and control positions at a particular instant. For concurrent communicating processes, the notion state has no such simple definition, unless severe limitations on concurrency are imposed. Considering its central place, it is surprising that the general notion state has received so little attention.

In this note the notion ‘pomset’ is extended in such a way that a state is just a pomset with no temporal precedence relation on its events—it is the description of an instant (Section 3.3). This allows to demonstrate within a single framework the duality between two approaches to modeling concurrency: the one based on events and the other on states. For one direction in this duality, any pomset is described as a serial concatenation of its states (Section 4). And for the other direction, a sequence of abstractly given states give rise to a partial order of events (Section 2).

This approach to the notion of a state, and the construction of domains by Scott [1982], are used here to give a (denotational) semantics to a very simple language for concurrent processes. In fact, we modify to some extent the original definition of information systems of Scott, and provide (in Section 6) an account of a simplified version that suffices for our use.

2 From States to Events

The prime notion in the approach to modeling based on pomsets is the ‘event’, with its characteristics and temporal position. In this section we show how pomsets arise naturally, even if the starting point is the abstract notion of a state rather than that of an event.

Assuming global time, reality can be described as a sequence of states. A run is a structure R = ⟨N, <, F ⟩, where N (the set of integers or a finite initial segment of it) is the sequence of states, < is the usual order on the integers and is intuitively seen here as the temporal precedence order on N. F is a finite collection of unary predicates on N. The meaning of i < j is that state i appeared before state j. P (i) means that P is true at state i. Since the predicates are unary, the second-order monadic theory of ω expresses all that we may wish to say about runs.

What is an event? Usually, an event is defined as the object that caused the transition from one state to its successor. Such an approach is suitable when concurrency is modeled by interleaving atomic actions and an elementary object is the triple S_{1}⟶^{e}S_{2} which indicates that event e has caused the change from state S_{1} to state S_{2}. We take here an alternative approach: An event occurrence is a constant and continuous thread through the succession of changing states. A formal definition follows. Some predicates in F denote the occurrences of events. Given such a predicate P, P (i) indicates that the event denoted by P occurs at the i-th state. It is assumed that the description given by P is so complete that if P (i) holds, then only one event of type e_{P} (the type of P) occurs at the i-th state. The point is that if two events with property P occurred at i, then they are indistinguishable and hence are the same event. Now suppose both P (i) and P (i + 1) are true, how do we know then whether it is the same occurrence of the event that appeared in the two successive states? Could it not be that two distinct occurrences of events of type P happened at state i and i + 1? It is necessary therefore to be able to tell whether an event is new or is a continuation ot its occurrence in the previous state. There are several ways to do that, and later we will suggest one way. Let us only assume now that somehow the predicates in F can tell whether P (i) and P (i + 1) represent the same or two distinct occurrences.

This leads to the following. Let R be a run. For each P ∈ F that is supposed to describe occurrences of events of type e_{P}, let us define “an occurrence of e_{P} ” to be a maximal interval I in N such that (1) P (i) holds for all i ∈ I, and (2) for i, i + 1 ∈ I, P (i) and P (i + 1) represent the same occurrence.

Let E be the collection of all event intervals thus obtained as occurrences of e_{P} for some P ∈ F. A partial order ≺ is defined on I, J ∈ E by:

I ≺ J iff ∀x ∈ I ∀y ∈ J(x < y).

The set of event occurrences of a fixed type e_{P} are linearly ordered by ≺. That is, E is the union of finitely many chains (since F is finite).

The predicates of F can be defined on E as well: For I ∈ E of type e_{P} and for Q ∈ F that has the form “property R holds for the event of type e_{P} ”, R(I) holds iff ∀x ∈ I, Q(x). The structure (E, ≺, F) thus obtained will be defined in the following section as a pomset (Partially Ordered MultiSet).

3 On Pomsets

The pomsets defined in this paper combine features from the original definitions of Gischer [1989] and Pratt [1986], and from Lamport’s system executions [1986], with the addition of some other features (mainly the addition of functions). First, we present a restricted version of pomsets that have only predicates, and in the following section functions are added.

A partial order <_{S} on a set E_{S} is called an interval order if the following (Russell-Wiener property) holds:

a<_{S}b, b≯_{S}c, and c<_{S}d imply a<_{S}d.

By Wiener [1914], any interval order can be represented by intervals of a linear order. An outline of the proof follows (see Fishburn [1986], or Anger [1989] or Abraham, Ben David and Magidor [1990]).

The intuition of Russell and Wiener is that instants (points of time) can be retrieved from the events (which are extended in time). Recall that an antichain in a partially ordered set, (E_{S}, <_{S}), is a non empty collection of pairwise incomparable members. We are assuming that E_{S} is countable, and each e ∈ E_{S} has finitely many predecessors, and every antichain is finite.

Wiener’s representation result begins by collecting all maximal antichains of (E_{S}, <_{S}) into a set M, the set of ‘instants’. In our case, since we assume that every antichain is finite, M is countable. Then define for m_{1}, m_{2} ∈ M,

m_{1} <_{M} m_{2} iff ∃a ∈ m_{1}, ∃b ∈ m_{2} (a<_{S}b).

Assuming the Russell-Wiener property, the relation <_{M} is a linear order of M, and if M is infinite then its order-type is ω (by the finiteness of predecessors assumption).

The representation is the function μ defined on E_{S} by:

μ(e) = {m | e ∈ m}.

μ(e) is a convex interval in <_{M}, and

e_{1} <_{S} e_{2} iff μ(e_{1}) ≺ μ(e_{2}).

Where ≺ is as the order defined in Section 2, but now on the intervals of M. We claim that if m_{1} <_{M} m_{2} are maximal antichains, and m_{2} is the successor of m_{1} in <_{M}, then

∀x ∈ m_{1} − m_{2} ∀y ∈ m_{2} − m_{1} (x<_{S}y).

Indeed, if x and y as above were incomparable in <_{S}, then m_{1} ∩ m_{2} ∪ {x, y} could be extended to a maximal antichain m, and necessarily m_{1} <_{M} m <_{M} m_{2}.

Definition 3.1 A pomset (with unary predicates) is a structure P = (E_{P}, <_{P}, F_{P}) where

(1) (E_{P}, <_{P}) is an interval order. (We will use the convention that sets a≤_{P}b iff a<_{P}b or a = b.)

(2) For every e ∈ E_{P}, { x ∈ E_{P} | x≯_{P}e} is finite. (This is Lamport’s finiteness condition).

(3) F_{P} is a finite collection of unary predicates on E_{P}.

(4) There is a finite bound k on the size of antichains in (E_{P}, <_{P}). In fact, there is in F_{P} a decomposition of E_{P} into k many chains (linear subsets).

Let us emphasize that, primarily, we view a pomset as a description of reality, one world out of many possible, and not as a prescription of how things should be. Thus a<_{P}b means that a happens before b, and not that a caused b or that b is bound to follow a.

Sometimes it is convenient to include in F_{P} unary functions as well, from E_{P} into some fixed (finite) range. Since such functions can be represented with finitely many unary predicates, this is just a stylistic addition.

Condition (4) is natural when one puts a finite limit on all possible resources; for example if there are finitely many serial processors working concurrently.

In the following section and in Section 3.3 we will extend this notion of a pomset in two directions: by adding functions from E_{P} to E_{P}, and by adding initial and final events. There is clearly also the need to represent in E_{P} those fixed object for which it makes no sense to apply the precedence relation. For example, the program statements and control positions, or the possible values of the variables. However, for notational simplicity, we will not do this here.

3.1 Pomsets with functions

Experience with protocols and correctness proofs has taught us the advantage of supplementing pomsets with unary functions from E_{S} to E_{S}. However, in order not to lose the decidability of the theory of pomsets given by Büchi’s theorem, only a limited family of functions should be allowed: non-increasing functions with bounded depth (defined below). It turns out that only definable functions are thus added, and the functionless pomsets suffice—at least in theory. In practice, we find that the addition of functions can help in understanding systems. As an example, see the definition of a queue given in Section 3.4.

For simplicity, let us restrict the following discussion to the monadic theory of the order of N. Let R = ⟨N, <, F ⟩ be a monadic structure. (i.e., < is the usual order relation on the set of integers, N, and F is a collection of unary predicates and unary functions with finite range.) A function f : A → N, where A ⊆ N, is definable in R iff there is a 2nd order monadic formula φ(x, y) such that y = f(x) iff R ⊧ φ(x, y).

A decreasing function is a function satisfying f(x) < x for all x ∈ dom(f). Some decreasing functions have the following simple definition. A subset, B ⊆ N, is given, and for every x ∈ A: f(x) = y iff y ∈ B is the rightmost member of B such that y < x.

A slightly more general definition of a function allows for several such B’s. Let us define a decreasing function f to be simply definable in R if f : A → N, and there are, in F, B_{1}, …, B_{n} ⊆ N, and g : A → {1, …, n} such that: f(x) = y iff y ∈ B_{g(x)} is the rightmost member y′ ∈ B_{g(x)} such that y′ < x.

Let us say that f : A → N, A ⊆ N, is a function of depth k, if for every e ∈ N there is a set T ⊆ [0, …, e] of cardinality ≤ k such that:

∀x > e (f(x) ≤ e ⇒ f(x) ∈ T).

If for some k, f has depth k, then f is said to be “of bounded depth”. The following was confirmed in conversation with M. Magidor. For a decreasing function f : A → N, (1) implies (2) and (2) implies (3).

(1) f is definable in R .

(2) f is of bounded depth.

(3) f is simply definable in some extension of R (obtained by adding unary predicates).

We now generalize the discussion from monadic structures to the setting of a pomset S = (E_{S}, <_{S}, F_{S}). Let us say that a function f : A → E_{S}, A ⊆ E_{S}, is non-increasing if, for every e, f(e)≯_{S}e. Say f has depth k, if for every e ∈ E_{S} there is a set T of size ≤ k, such that if e≯_{S}x and f(x)≤_{S}e, then f(x) ∈ T. In this case, since there is a bound, b, on the size of the antichains, for every instant m (a maximal antichain) there is a set U of size ≤ k × b such that: If x ≥ e for some e ∈ m, and f(x) < e′ for some e′ ∈ m, then f(x) ∈ U.

Definition 3.2 A pomset (with functions) is a pomset as in Definition 3.1, but now with (finitely many) non increasing functions of bounded depth. We will call such a pomset plain to distinguish it from the full pomsets defined in Section 3.3 (by adding initial and final events).

3.2 Initial and final segments of pomsets (intuitive remarks)

An initial segment of a pomset S (with functions) represents the run up to a certain instant. A final segment is the run from some instant on. Both are subpomsets. In the following we are going to motivate the distinction between finished and unfinished events and the introduction of initial events.

Given a pomset S, and an instant m (a maximal antichain) let us form

≤ (m) = { x ∈ E_{S} | x≤_{S}a for some a ∈ m},
≥ (m) = { y ∈ E_{S} | a≤_{S}y for some a ∈ m}.

Now let m_{1} and m_{2} be a maximal antichain and its successor in the order <_{M} defined on the maximal antichains. Then the following hold:

1. ∀a ∈ m_{1} \ m_{2} ∀b ∈ m_{2} \ m_{1} (a<_{S}b)

2. ≤ (m_{1}) ∪ ≥ (m_{2}) = E_{S}.

In fact, for the ongoing discussion it suffices to assume that m_{1} and m_{2} are antichains (not necessarily maximal) that satisfy these conditions.

We wish to form the initial pomset S_{1} with set of events E_{S_{1}} =≤ (m_{1}), and the final pomset S_{2} with set of events E_{S_{2}} =≥ (m_{2}). It is required of such a definition that the concatenation S_{1}; S_{2} (to be defined later) gives back S. For that, we need to be able to identify those events that are common to S_{1} and to S_{2}, in order to unify them in the concatenation. It is easy to see that a is both in ≤ (m_{1}) and ≥ (m_{2}) iff a ∈ m_{1} ∩ m_{2}. The way we single out the events in m_{1} ∩ m_{2} is by declaring them to be ‘unfinished’ in S_{1} (this is so because any a ∈ m_{1} ∩ m_{2} in S_{1} continues to occur in S_{2}).

So we assume a predicate in F_{S} that tells us about each event whether it is finished or not. An unfinished event in an initial segment may become finished in a longer segment. (For all other predicates in F we assume that the truth value of P (x) does not change in the passage from a pomset to a subpomset —this is of course the definition of a substructure). The only role of the finished/unfinished distinction is to enable the identification of an unfinished event in a pomset with its continuation in an extension of that pomset. In an infinite pomset all events are finished, and in a finite pomset unfinished events are always maximal. So if a<_{S}b then a is finished.

Now let us look at the final segment ≥ (m_{2}) and try to generate the appropriate pomset by restricting the predicates and functions of F_{S} to E_{S_{2}}. It may well be that E_{S_{2}} is not closed under the functions in F_{S}. This shows the need for initial events. These are ‘prehistoric’ events, not present in E_{S_{2}} but used to explain its behavior. They will form the initial pomset of S_{2} which will also be the final pomset of S_{1}. Typically, the final pomset includes all the relevant information needed for the system to resume its execution. In other words, the final pomset of S_{1} is the initial pomset of any possible continuation. Since the functions in F_{S} are of bounded depth, the number of possible initial states will be finite. Let us now formally develop these intuitive considerations.

3.3 Pomsets with initial and final events

A pomset with initial and final events is a structure S = (E_{S}, I_{S}, <_{S}, F_{S}, T_{S}) consisting of

1. a set of events E_{S},

2. a (finite) set of initial events I_{S},

3. a precedence relation <_{S} (defined on E_{S} ∪ I_{S}),

4. a finite collection, F_{S}, of (partial) unary predicates and non-increasing functions of bounded depth, and

5. a finite set T_{S} ⊆ E_{S} ∪ I_{S}, of “final events”.

Let us call the events in E_{S} ‘actual’ to distinguish them from the ‘prehistoric’ events in I_{S} \ E_{S}. It is possible that the set I_{S} ∩ E_{S} is nonempty, but this intersection is always an antichain in <_{S}. If a ∈ I_{S} \E_{S} and b ∈ E_{S} \I_{S} then a<_{S}b. I_{S} is an initial segment, and E_{S} a final segment in <_{S}; that means that if x<_{S}y then x ∈ E_{S} implies y ∈ E_{S}, and y ∈ I_{S} implies x ∈ I_{S}.

The functions and relations are on E_{S} ∪ I_{S}. In all of our applications, the functions are partial functions with the property that for any set X the union of the ranges f′′X for f ∈ FS is closed (under all the functions). If T_{S} is undefined or T_{S} = ∅ then it may be omited from S. This is the case when E_{S} is infinite. The precedence relation is an interval order, and in fact all the requirements of Definition 3.1 are made here too. It is possible to omit I_{S} and T_{S} from the definition, and in this case S is called a plain pomset. For emphasize, a pomset with initial and final events may be called full.

There is a distinguished finished/unfinished predicate in F_{S} defined on the actual events. In an infinite pomset the events of E_{S} are all finished, but some events may be unfinished in a finite pomset. If a<_{S}b then a is finished (so the unfinished events form an antichain). When the predicate T_{S} is present (in a full pomset), the unfinished events of E_{S} are all in T_{S}, but it is possible for T_{S} to also have finished events. (The events in I_{S} \ E_{S} are considered to be finished.)

Definition 3.3 A pomset S in which E_{S} is an antichain (possibly empty) is called a state (a pomset state, when other notions of states are around). If E_{S} = ∅, then S is called an ‘eventless’ state (or pomset).

For each pomset with initial/final events, two plain pomsets are defined: its initial, and final pomsets. Let us first define the initial pomset of S.

Given a pomset S = (E_{S}, I_{S}, <_{S}, F_{S}, T_{S}), the initial pomset of S is the plain pomset U = (I_{S}, <_{S} |` I_{S}, F_{S}), obtained by taking E_{U} = I_{S} with <_{U} and F_{U} being the restrictions of <_{S} and F_{S} to I_{S}; except that the unfinished events of U are exactly I_{S} ∩ E_{S}. (Intuitively this is so since these events continue to be in E_{S}).

The final pomset of S is naturally defined by restricting <_{S} and F_{S} to T_{S}: That is F = (T_{S}, (<_{S} |` T_{S}), F_{S} |` T_{S}). Thus the final pomset of S is the plain pomset F obtained by transforming the final events T_{S} into the events of F. The intuition is that the final pomset of S constitutes the initial pomset of any continuation of S. The unfinished events of F are the unfinished events of S (required to be in T_{S}).

Let S be a pomset, and m_{1} and m_{2} be an instant and its successor in S (or just two antichains that satisfy 1 and 2 of Section 3.2). The initial segment, S_{1}, generated by m_{1} and the final segment, S_{2}, generated by m_{2} (that we intuitively defined in Section 3.2) can now be completely defined. The final events of S_{1} are exactly the initial events of S_{2}: these include the unfinished events of E_{S_{1}} (that is, m_{1} ∩ m_{2}), and all the events of the form f(x) for f ∈ F_{S}, where x ∈≥ (m_{2}), but f(x) ∉≥ (m_{2}). (It is assumed that the set thus obtained is closed under the functions of F_{S}.)

The initial pomset of S_{2} equals the final pomset of S_{1}, and the concatenation of S_{1} with S_{2} will be defined in Section 4 so as to give back S.

3.4 An example: specifying a queue

As an example to the use of functions in pomsets, let us specify a bounded queue for one Producer and two Consumers, where an item in the queue withdrawn by one of the Consumers is no longer available to the other. Thus if two dequeue operations are executed, by Consumer_{1} and Consumer_{2}, it is never the same item that is delivered to them (it may have the same value of course). The queue is supposed to have a bounded capacity, k. The operations of the Producer are called enqueue, and those of the Consumers are called dequeue events (thus, since we are only interested in the queue specifications, the producing and consuming events are disregarded).

The specification (or description) of the queue is given by the collection of all pomsets that behave correctly. (A collection of pomsets is called a ‘system’.) This queue specifying system is determined by the following list of ‘axioms’ concerning a pomset S = (E_{S}, <_{S}, F_{S}).

We will be using the relation a <_{S} end(b) on events in E_{S}. This means that

∀x ∈ E_{S} (b <_{S} x ⇒ a <_{S} x).

Similarly, begin(a) <_{S} b means that ∀x <_{S} a, x <_{S} b. QUEUE SPECIFICATIONS (the parenthetical explanations are only for intuition):

1. Each of the processes in S, Producer, Consumer_{1}, and Consumer_{2} (subsets of E_{S}), are serial (linearly ordered by <_{S}). Put Consumer= Consumer_{1} ∪Consumer_{2}. The events in Producer are called ‘enqueue’, and those in Consumer, ‘dequeue’.

2. There are in F_{S} a predicate ‘successful’, and two functions: f and Value. (Every event is of finite duration (i.e., it is terminating) and it returns a value indicating its status, successful or not. Intuitively, a Producer enqueue is not successful when the queue has already k items, and a dequeue event is not successful when the queue is empty. Value(e) is the data value of the enqueue or dequeue event e. The function f is defined on the successful dequeue events, and f(c) = p means that c obtained the item deposited by the (successful) enqueue event p. There is more than one way of making this intuition precise, and we have chosen one way as an example.)

3. f is defined on the successful dequeue events, and is taking values in successful enqueue events.

(a) f is one-to-one, and f(a) <_{S} a for all a.

(b) f is order-preserving:

a <_{S} b ⇒ f(a) <_{S} f(b).

(c) Value(a)=Value(f(a)).

4. For every successful enqueue event p the following set has cardinality < k: {q ∈ Producer | q <_{S} p, q is a successful enqueue, and there is no c ∈ Consumer such that q = f(c) and c <_{S} end(p)}.

5. For every unsuccessful enqueue event p the following set has cardinality ≥ k: {q ∈ Producer | q is a successful enqueue, q <_{S} p, and there is no c ∈ Consumer, c <_{S} p, such that q = f(c)}.

6. For every successful Consumer dequeue c, if p <_{S} f(c) is a successful enqueue event, then p = f(c′) for some dequeue c′.

7. For every unsuccessful dequeue event c, there is, for every successful enqueue p <_{S} c, a dequeue event a such that f(a) = p and begin(a) <_{S} c.

3.5 Environments

In the traditional view, a state is a map form the set of variables into the set of possible values. To not overload the word ‘state’, let us call such a map a ‘variable environment’. This traditional view capture an intuition not present in our definition of a state as a pomset with no precedence relation on its events; an intuition which is particularly useful when dealing with the semantics of programming languages, because the execution of a program depends on the environment.

It therefore makes sense to incorporate the traditional view in our definition, and this can be done simply by adding to a pomset S two (partial) functions

I ENV , F ENV : Var → Value

where Var is the set of variables, and Value is the set of possible values; I ENV and F ENV are the initial and final variable environments.

These functions are added to F_{S}, but for emphasize we can write them externally, so that the resulting pomset is represented as

A = (S, I ENV , F ENV ).

In an eventless pomset the initial and final environments must be the same since there are no events.

4 Operations on Pomsets: Concatenation and Concurrent unions

In this section we first define the concatenation of two pomsets and show how every pomset can be decomposed into a sequence of states. Then we define the concurrent union of two pomsets.

4.1 Concatenation

Let A and B be two pomsets (with A finite), and suppose that S is a plain pomset that occurs both as a final pomset of A and as an initial pomset of B. Then A; B, which is the concatenation of A followed by B, can be defined by identifying these two occurrences of S, and requiring that, except for this identification, all the events of A precede those of B. The initial events of A; B are the initial events of A, and its final events are those of B.

To be more specific, A; B = C is defined thus. Set I_{C} = I_{A}. To obtain E_{C}, take first the disjoint union of E_{A} with E_{B}, and then identify events in E_{A} and E_{B} as follows. Let i_{1} and i_{2} be the embeddings of S as a final pomset of A, and an initial pomset of B respectively. So i_{1} is taking E_{S} onto T_{A}, and i_{2} is onto I_{B}. Now, if s ∈ E_{S} is such that i_{2}(s) ∈ E_{B}, then i_{1}(s) and i_{2}(s) are identified. So the elements of E_{B} that are thus identified with members of A are exactly those in I_{B} ∩ E_{B}, and these were defined to be the unfinished events of the initial pomset of B. Hence it is exactly the unfinished events of A that are identified with actual elements of B. (Recall that the unfinished events in the final pomset of A, namely in S, were defined to be the unfinished events of A.)

The final events of C are defined to be T_{B}, the final events of B (in case T_{B} contains some members of I_{B}, these are identified, via S, with the corresponding members of I_{A} ∪ E_{A}). The precedence relation <_{C} is defined by first taking the union of <_{A} with <_{B} and then extending the relation so that for a ∈ (E_{A}∪I_{A})\E_{B} and b ∈ E_{B}\I_{B}, a <_{C} b holds. The Russell-Wiener property holds in A; B.

It is not difficult to prove that concatenation is an associative operation on pomsets.

In particular, it is possible now to define the concatenation of a sequence ⟨S_{i}|i < i_{0}⟩ (i_{0} is finite or ω) of states. Recall that a state is a pomset with E_{S_{i}} forming an antichain, and it has its own initial and final (plain) pomsets. It is assumed that for every i the final pomset of S_{i} equals the initial pomset of S_{i+1} in order for this concatenation sequence to be defined.

Now, any pomset can be represented as the concatenation of a sequence of its states. The coarser way to do that is to look at the sequence of instants. Each instant (maximal antichain) defines a state, and these instants are linearly ordered and their concatenation gives back the pomset. We are back to our starting point where a run was given as a sequence of states. It should be observed that there are finer ways to decompose a pomset into states. All these decompositions give back the pomset, and intuitively they correspond to decompositions obtained with clocks of varying ticking rates. Graphically, if the events of the pomset are represented by intervals, then each decomposition corresponds to a sequence of points where each point corresponds to an antichain (not necessarily maximal), and different points may correspond to the same antichain.

To take the simplest example, suppose the pomset S contains a single serial process, enumerated as e_{0}, e_{1} …, in increasing <_{S} order. The coarser decomposition of S is into the states S_{i} that contain the antichain e_{i} (a single event). Finer decompositions could be described graphically by first representing the events e_{i}’s as intervals and then picking a sequence of points that intersect each interval in one or more points and may also contain points falling in between adjacent intervals.

Let us give another example to illustrate a nonsequential process. Suppose the pomset S consists of three events, E_{S} = {a, b, c}, and the only temporal relation is a<_{S}c. There are thus only two maximal antichins, m_{1} = {a, b}, and m_{2} = {c, b}. The coarser decomposition is therefore into two states, and then no state corresponds, for example, to the moment when a has finished, c has not yet begun and b is ongoing. An example of a finer decomposition into states is S_{1}; …; S_{5}, where the actual events of the five states are: {b}, {a, b}, {b}, {c, b}, and {c}. In this concatenation, b begins before a, and ends before c ends.

4.2 Concurrent unions

We shall first define the term ‘restriction of a pomset’, and then define the concurrent union of two pomsets that have the same restrictions: it is the collection of pomsets obtained by ‘running’ the two pomsets concurrently while identifying the events in this common restriction. Restrictions: Let S = (E_{S}, I_{S}, <_{S}, F_{S}) be a pomset. If A ⊆ E_{S} ∪ I_{S}, and G is a set of relation and function symbols, then the restriction of S to A and G is the pomset obtained by restricting the functions and predicates of F_{S} with names in G to the subset A.

Let S_{1} and S_{2} be two pomsets. Put E_{i} = E_{S_{i}} ∪ I_{i} for i = 1, 2. And let L_{i} be the language of the relation and function symbols interpreted by F_{S_{i}}. Assume that for some A and G, A = E_{1} ∩ E_{2} and G = L_{1} ∩ L_{2}, and the restrictions of S_{1} and of S_{2} to A and G are the same. Then the collection (S_{1}∥S_{2}) = S is defined to be the system of all pomsets S in the language L_{1} ∪ L_{2} such that the restriction of S to E_{i} and L_{i} is S_{i} for i = 1, 2. It is not difficult to see that S is not empty (under the above assumption on the equality of the restrictions). Also, taking concurrent unions is a commutative operation.

Restrictions and concurrent unions can be used to define the semantics of communicating processes. As an example, suppose P_{1} and P_{2} are two processes that access some communication device D. Suppose D supports operations of type OP_{1}, executed in P_{1}, and OP_{2} executed in P_{2}. (For example OP_{1} is read, and OP_{2} is write.) Let Y_{1} and Y_{2} be the systems describing P_{1} and P_{2} respectively, and let Y be the system describing D.

(A system is a collection of pomsets; it represents a process.) So if A is a pomset in Y_{1}, E_{A} contains events that are executions of OP_{1} (and other events not connected to D). Similarly, pomsets in Y_{2} contain events of type OP_{2}. The pomsets in Y contain events of both types, since the pomsets of Y describe the correct behavior of the device D.

It is possible that the pomsets in Y contain functions that are not in Y_{1} or Y_{2} but are needed for the specification of the device D. This shows the need to defined concurrent unions for pomsets with different languages.

Now if A ∈ Y_{1}, B ∈ Y_{2}, C ∈ Y and it happens that:

(1) The restrictions of A and of C to operation executions of OP_{1} are the same.

(2) The restrictions of B and of C to operation executions of OP_{2} are the same.

Then the collection A∥C∥B = S can be formed. Any D ∈ S is a pomset in which P_{1} and P_{2} communicate through D. The system of all such concurrent unions is denoted Y_{1}∥Y ∥Y_{2}. This system represents the concurrent runs of P_{1} communicating with P_{2} through device D. In Section 5.3 we will use a different definition for S_{1}∥S_{2} which is applicable in case S_{1} and S_{2} are states. In this case E_{i} = E_{S_{i}} is an antichain and then it is possible to define S_{1}∥S_{2} not as a system but as a single pomset, by declaring E_{1} ∪ E_{2} to be an antichain (after the suitable identifications are made).

5 Semantics

The aim of this part is to sketch a (denotational) semantics to a very simple language which nontheless allows concurrent executions of programs and recursive calls to procedures. The use of ‘states’ makes it almost as simple (or difficult) to deal with concurrent as with sequential programs. First we describe the language, then its semantics, and finally we say a little about the construction of domains (in Section 6).

5.1 A simple language

The language contains a set of basic instructions which consists of the following:

1. Communication instructions, such as WRITE(R, x) or GET (Q, x), where R and Q are communication devices and x is a data variable.

2. Assignment instructions. These have the form x := θ, where x is a data variable and θ is a term built from the data variables with the aid of the the language functions (addition etc.).

3. Procedure calls. There is a collection PVar of Procedure identifiers (variables), and if X ∈ PVar then the statement ‘X’ is a basic instruction. (So procedures are called without parameters.)

These basic instructions can be composed into ‘compound instructions’ which are formed by the following operations:

1. Any basic instruction is also a compound instruction.

2. Concatenation: ‘(p;q)’ where p and q are compound instructions.

3. Conditional instruction: ‘IF α THEN p’ where α is a propositional statement involving data (and boolean) variables, logical connectives and the equality symbol. p is a compound instruction.

A ‘sequential program’ has the form

d_{1}; … d_{n}; p

where the d_{i}’s are procedure declarations (see below) and p is a compound instruction.

A ‘procedure declaration’ has the form

procedure X; p

where X is a procedure variable and p is a compound instruction. This procedure declaration binds the compound instruction p to the procedure name X.

Finally, a ‘concurrent program’ has the form

a_{1}∥a_{2} … ∥a_{n}

where the a_{i}’s are sequential programs. For simplicity, we assume that the set of variables used by the a_{i}’s are disjoint.

Obviously, we have swept aside some of the harder problems in language semantics. For example all our variables are globals, and procedures are parameterless. However, our aim is rather limited: only to point to the possibility of using the established tools of semantics for the description of concurrently communicating sequential programs (with the possibility of noninterleaving events).

5.2 Semantics

If the meaning of a program is its behavior (and not only the input/output relation) then the semantics should assign to a program fragment the collection of its possible behaviors (namely, a system of pomsets). It seems however more convenient to make explicit the dependency of the behavior on the (initial) environment, and let the denotation of a program construct be a map from the domain Env, of environments, to the domain Sys of all possible systems.

An environment was defined to be a map from the set of variables to the set of possible values. Let Var be the domain of variables of our language (process and data variables), and Val be the domain of possible values. So

Env = Var → Val.

In words, the domain of environments consists of the maps assigning values to the variables. There are two types of variables in our simple language: data and procedure variables, and accordingly:

Val = Data + Proc.

(It is assumed that if fεEnv, then for a data variable x, f(x) is a data value, and for a procedure variable X, f(X) is in Proc, the domain of process values.

The domain Moment contains all the pomset states (as defined in Definition 3.3). The term moment is used here rather than state, because in the context of denotational semantics ‘state’ has a different meaning.

Recall that in Section 3.5 the pomset concept was extended to include two environments (the second, only for terminating pomsets). Using the same intuition, let us define the domain State by

State = Moment×Env×Env.

In words, a state in State is a triple consisting of a pomset state and two environments—an initial and a final. If T = (m, a, b) is in State, then m is called the pomset of T; a and b are the initial and final environments of T; the initial (final) pomset of T is defined to be the initial (final) pomset of m as defined in Section 3.3. The initial part of T is defined as the pair consisting of the initial pomset and the initial environment of T. Similarly, the final part of T consists of the final pomset and final environment of T.

It is useful to also have two special states, the undefined and the null state in State. The elements of any domain are partially ordered by the information they carry. For State, the null state is less informative than any other state; otherwise the states are incomparable. The use of the undefined state will be described later.

A pomset is represented here by a concatenated sequence of states: T_{1}; T_{2} …, where T_{i} ∈ State are such that the final part (pomset and environment) of T_{i} equals the initial part of T_{i+1}. A system is a collection of pomsets, it is the formal counterpart of the notion ‘behavior’.

A simple way to represent a system is as a partial map f : ω^{+} → State. Here ω^{+} is the discret domain of all finite non empty sequences of integers, and the domain (source) of f is assumed to be closed under initial segments. It is also assumed that if ν, ν′ ∈ ω^{+} are in the domain of f and ν′ is a successor of ν (i.e., ν′ = νˆ ⟨n⟩ for some n), then the final part of f(ν) equals the initial part of f(ν′), unless F (ν) is the null state, and then we drop this requirement. In case f(ν) = null, for every extension ν′ of ν, f(ν′) = null.

Suppose that the sequence ν = ⟨n_{1} … n_{l}⟩ is in the domain of f and set ν_{i} = ⟨n_{1} … n_{i}⟩, then the sequence of states f(ν_{1}), …, f(ν_{l}) represents a pomset—the concatenation of these states. We say that the resulting pomset is ‘represented’ in f by the branch determined by ν (the branch ν_{1}, …, ν_{l}). The branches of ω^{+} (finite or infinite) thus represent the computations. I.e., we say that pomset S is represented in f (by ν) iff ν is a branch of the form ν = {ν_{i}|1 ≤ i < i_{0}}, where ν_{i} ∈ ω^{+} is of length i and is in the domain of f, and the concatenation of the states f(ν_{i})’s gives S (i_{0} can be finite or ω).

Actually, instead of dealing with partial maps, we shall take fully defined maps and allow the undefined state to be in the range (target) of f. We assume that if f(\overline{n}) = undefined for \overline{n} ∈ ω^{+}, then, for every extension \overline{m} of \overline{n}, f(\overline{m}) = undefined. The source of f is then defined to be the set of \overline{n}’s such that f(\overline{n}) ≠ undefined.

A maximal node in the source of f is called a leaf: it is a node \overline{n} ∈ ω^{+} such that f(\overline{n}) ≠ undefined but f(\overline{m}) = undefined for every extension \overline{m} of \overline{n}. It is probably a technical point, but it seems that we need to know whether \overline{n} is a leaf directly, and not only by checking that f(\overline{m}) = undefined for all the extensions of \overline{n}. For this, we postulate the existence of a special ‘status variable’ in Var, and assume that its value at the final environment of f(\overline{n}) indicates whether \overline{n} is or is not a leaf of f. Thus if f(\overline{n}) = null then \overline{n} is in the source of f, and it is not a leaf and for every extension \overline{m} of \overline{n}, f(\overline{m}) = null as well. f(\overline{n}) = null convey lack of knowledge, which could change with further information; f(\overline{n}) = undefined is a definite knowledge that \overline{n} is not in the source of f and will never be. The equation for the domain of systems is

Sys = ω^{+} → State.

It is convenient to have also the following requirement on the domain Sys: For every f ∈ Sys and ν ∈ ω^{+}, let T_{0} be the pomset represented in f by the branch that ν determines. Suppose the pomset T_{1} is represented in f (perhaps by a branch that does not extend ν), and T_{1} extends T_{0}. Let S be a state such that the concatenation T_{0}; S is extended by T_{1}, then for some n ∈ ω, f(νˆ ⟨n⟩) = S.

Thus, if we let Y denote the system of all pomsets represented by f as well as their initial segments, then this condition says that any extension of the pomset represented by ν that is still in Y can be obtained by extending ν.

It follows that if fεSys then for any pomset, A, represented in f, all the decompositions of A into sequences of states appear in f. This is needed to ensure that the definition of the concurrent execution (p ∥ q) given below, results in all possible concurrent execution of p and q.

Now the domain of processes is defined by

Proc = Env → Sys.

In words, the domain of processes consists of the mappings from the environments into the systems, which are representing collections of pomsets. For f ∈ Proc, σ ∈ Env, and ⟨n⟩ ∈ ω^{+}, if f(σ)⟨n⟩ is not the null or the undefined state, then the initial environment of f(σ)⟨n⟩ is required to be σ. (Here, ⟨n⟩ is the sequence of length 1 containing n.)

We shall later need the undetermined (null) system s_{0} ∈ Sys which is such that s_{0}(⟨\overline{n}⟩) = null, for every \overline{n} ∈ ω^{+}. The undetermined process p_{0} ∈ Proc is such that p_{0}(σ) = s_{0} for every σ ∈ Env.

To sum up: The recursive set of domain equations is the following. There are initial domains given by the language and its intended semantics: These are ω^{+}, Var, Data and Moment. Then Val, Env, State, Sys and Proc are constructed to satisfy the following:

1. Val = Data + Proc.

2. Env = Var → Val.

3. State = Moment×Env×Env.

4. Sys = ω^{+} → State.

5. Proc = Env → Sys.

As indicated, these equations must be refined. For example the domain Sys should be so defined that its elements give rise to sequences of states that can be concatenated—the final pomset and environment of a state in a sequence must be equal to the initial pomset and environment of the succeeding state.

5.3 Serial and concurrent executions

For p and q in Proc, we are going to define (p; q) ∈ Proc and (p ∥ q) ∈ Proc to be the serial and concurrent processes (respectively) executing p and q.

First the serial concatenated execution r = (p; q) : Env → Sys is defined. For each σεEnv we must determine r(σ) = h ε (ω^{+} → State).

Given \overline{n} = ⟨n_{1}, …, n_{k}⟩ ε ω^{+}, h(\overline{n}) is defined by the following. Let p(σ) = f ε Sys. If \overline{n} is in the source of f (i.e., f(\overline{n}) ≠ undefined), then put h(\overline{n}) = f(\overline{n}). If \overline{n} is not in the source of f and it is not above a leaf of f, then h(\overline{n}) = undefined. Otherwise, \overline{n} is not in the source of f and is above a leaf of f. Let then 1 ≤ i < k be the last index so that l = ⟨n_{1}, … n_{i}⟩ is in the source of f. Decompose \overline{n} = \overline{l}\overline{m}, where \overline{l} of length i is a leaf in the source of f. Let μ be the final environment of the state f(\overline{l}), and suppose the final pomset of f(\overline{l}) equals the initial pomset of q(μ)⟨n_{i+1}⟩. Then h(\overline{n}) = q(μ)⟨n_{i+1}, …, n_{k}⟩. (Otherwise, h(\overline{n}) is undefined.)

In plain words, the process p; q gives to each environment σ the system obtained by concatenating all possible sequences of states S_{1} … S_{i}, S_{i+1} … S_{k} where the first part forms a complete pomset in p(σ) (i.e., not a proper initial segment) and the second part is obtained by looking at the environment obtained in the first part and applying q to it. Remark that a nonterminating execution in p (corresponding to an infinite branch of f) is also a nonterminating execution in p; q.

Let us turn now to the definition of parallel composition p ∥ q. The operator ∥: Proc×Proc → Proc depends on a restriction map, π, which is not explicitly shown for notational simplicity. A restriction is a map π : Moment → Moment (see Section 4.2). We will first define the parallel composition of two states, and then the composition of two systems (elements of Sys), and finally the parallel composition of two processes (in Proc).

For s_{1}, s_{2} ∈ State = Moment×Env×Env, where s_{i} = (m_{i}, a_{i}, b_{i}) (m_{i} is the pomset state of s_{i}, and a_{i}, b_{i} are the initial and final environments of s_{i}). Assume that πm_{1} = πm_{2} = p. Then m = (m_{1} ∥ m_{2}) is formed by unifying the two antichains of m_{1} and m_{2} into a single antichain. For simplicity, assume that the set of variables of s_{1} and s_{2} are disjoint (i.e., the sources of the functions a_{1}, b_{1} and a_{2}, b_{2} are disjoint). So a = a_{1} ∪ a_{2} and b = b_{1} ∪ b_{2} can be defined with no conflicts. Now define

s_{1} ∥ s_{2} = (m, a, b).

Put s_{1} ∥ s_{2} = undefined, in case m_{1} and m_{2} do not have the same projection. (Also, (undefined ∥ s_{2}) = (s_{1} ∥ undefined) = undefined.)

Suppose now S_{1}, S_{2} : ω^{+} → State are two elements of Sys. We are going to define the concurrent union S = S_{1} ∥ S_{2} ∈ Sys. For this, fix a bijection c : ω^{+} → ω^{+}×ω^{+} that is order and length preserving (the length of α, β and γ are all equal when c(α) = (β, γ)). Given a finite node ν ∈ ω^{+}, let c(ν) = (ν_{1}, ν_{2}). Naturally, we wish to define S(ν) to be S_{1}(ν_{1}) ∥ S_{2}(ν_{2}), and in case this cannot be done (if πS_{1}(ν_{1}) ≠ πS_{2}(ν_{2})) we set S(ν) to be undefined. Yet, we also want that if S(ν) is undefined then for every extension ν′ of ν, S(ν′) is undefined too. For this reason S(ν) is defined by induction on the length of ν:

If for some ν′ below ν, S(ν′) is undefined, then S(ν) is undefined. Otherwise, S(ν) is S_{1}(ν_{1}) ∥ S_{2}(ν_{2}) (which is possibly undefined).

Now we define r = (f ∥ g) for f, g ∈ Proc. r : Env → Sys. Given σ ∈ Env, let S_{1} = f(σ), S_{2} = g(σ); then S_{1}, S_{2} ∈ Sys and we put r(σ) = S_{1} ∥ S_{2}.

5.4 Denotations

For every construct, c, of the simple language, we will to define its denotation C^{|} (c) ∈ Proc. For that, C^{|} (c)(σ)ν ∈ State has to be defined for every σ ∈ Env and ν ∈ ω^{+}. It may be clearer to define the collectrion of pomsets that are to be represented by C^{|} (c)(σ) rather than to explicitly show the tree of states. We will outline the definition of C^{|} (c) for only five cases. We begin with the denotation of a concurrent program assuming its serial processes already have a denotation.

1. Let c be a concurrent program of the form a_{1} ∥ … ∥ a_{n}. The denotation C^{|} (c) depends on the semantics of the communication devices used by the processes. As an example, suppose a queue of capacity k, as specified in Section 3.4, is used by a_{1} (the producer) and by the two consumers a_{2} and a_{3}. So c = a_{1} ∥ a_{2} ∥ a_{3} is a program in which the three processes communicate through the queue. Given σ ∈ Env, set S_{i} = C^{|} (a_{i})σ for i = 1, 2, 3. Then S_{1} is the system describing all the possible executions of the producer’s program, and likewise S_{2} and S_{3} describe the consumer. But there is nothing in S_{1}, S_{2}, and S_{3} to indicate that a queue is used. So, for example, S_{1} may contain an execution that could never be normally observed in a concurrent execution of c. It is only by specifying the communication device that the denotation C^{|} (c) can be defined, and there should be enough freedom to enable any possible specification. So let Q : ω^{+} → State be the system that describes all the pomsets, S, that satisfy the queue specifications described in Section 3.4. Now define

C^{|} (c)σ = ((Q ∥ S_{1}) ∥ S_{2}) ∥ S_{3}

The definition of ∥ was given in Section 5.3. Intuitively, Q ∥ S_{1}, for example, is the system of all pomsets that can be obtained by running in parallel a pomset S in Q and a pomset S_{1} in S_{1} when the projections of S and S_{1} on the enqueue events are equal, and by identifying these common events. So the pomsets represented in C^{|} (c)σ describe the executions of the program c that use a queue as specified.

2. Take now, for example, a basic communication command such as c = ‘GET (Q, x)’ where Q is a name of a queue and x is a data variable.

To define C^{|} (c)(σ) for σ ∈ Env, we look at the set U of all states (m, e_{1}, e_{2}) ∈ State such that e_{1} = σ and e_{2} equals e_{1} except perhaps at the variable x, and m is a moment with a single event in E_{m} which is a dequeue event of value e_{2}(x). The system representing all the pomsets in U is defined to be C^{|} (c)(σ). Observe that there is nothing to indicate that a queue is used rather than any other device, and all possible outcomes of the GET are represented.

3. For a procedure call X, C^{|} (X) denotes the activation of the procedure named X. So, for any σ ∈ Env, C^{|} (X)σ = (σ(X))σ. In words, for a procedure variable X ∈ PVar, the denotation, C^{|} (X), of the activation of X is the element of Proc that assigns to every environment σ the system S defined as follows: Look at the value p = σ(X) of X in the environment σ, then p ∈ Proc = Env → Sys, and we define S = p(σ).

4. For sequential composition, (c_{1}; c_{2}),

C^{|} (c_{1}; c_{2}) = C^{|} (c_{1}); C^{|} (c_{2}).

Of course the symbol ‘;’ is used here in two distinct ways: as a syntactic symbol and as defined in Section 5.3.

5. The declaration, (procedure I; p), which binds procedure variable I to body p, is somewhat like an assignment command in that it only changes the environment, but it is complicated of course by the possibility of recursion (because p may use its own name I, directly or indirectly), and its denotation involves the use of fixed points. The function fix : (Proc → Proc) → Proc gives to every function f : Proc → Proc a ‘minimal fixed point’, p = fix(f), such that f(p) = p. To obtain p, start with the undetermined process p_{0}, iteratively apply f to it, get the increasing sequence f^{i}(p_{0}), i = 0, 1, …, and take its supremum to be fix(f).

We need the substitution function sub_{f}^{X} : Env → Env which changes the environment σ by assigning the value f ∈ Proc to the variable X ∈ PVar. So

sub_{f}^{X}(σ)(Y) = \{ \begin{matrix}f & if Y = X; \\ σ(Y) & otherwise. \end{matrix}

Now let I ∈ PVar be a fixed identifier, p a compound instruction. Define

t_{p}^{I} : Proc → Proc

by

t_{p}^{I}(f) = C^{|} (p) ∘ sub_{f}^{I}

(∘ is function composition). Intuitively, t_{p}^{I}(f) is the denotation of p when the variable I is interpreted as the name of procedure f. So fix(t_{p}^{I}) is ‘the denotation of I after the declaration that binds I with body p’.

The denotation of a procedure declaration can now be described in accordance with this intuition, define C^{|} (procedure I; p) = d as follows. d : Env → Sys, is the function that takes any σ ∈ Env to the system d(σ) = S ∈ Sys that has the following property. S comprises of all representations of the pomset (m, σ, sub_{fix(t_{p}^{I})}^{I}(σ)) which is a state where m ∈ Moment contains a single event, a ‘declaration’, which, intuitively, only changes the environment from σ to sub_{fix(t_{p}^{I})}^{I}(σ).

6 On domains

This section describes a modified version of Scott’s [1982] definition of ‘information system’. The modification consists in dropping the entailment relation, and showing that there always exists a definable (maximal) entailment relation which could be used instead.

Information systems were defined by Scott [1982] and used to provide domains for specifying the semantics of computer languages. An ‘information system’ is a structure A = (D_{A}, Δ_{A}, Con_{A}, ⊢) where D_{A} is a set; Δ_{A} ∈ D_{A} is the ‘null’ element; Con is a collection of finite subsets of D_{A} (the ‘consistent’ sets); and ⊢ is a relation on Con. Intuitively, an information system capture the idea that we often only have partial information on the objects with which we deal (the ‘elements’ of the system), but still want to be able to operate on these partially specified objects. The sets in Con are thought of as finite partial information, and ⊢ is an entailment relation. Accordingly, an ‘element’ of the information system is a subset x ⊆ D such that (1) every finite subset of x is in Con, and (2) if E ⊆ x and E ⊢ F, then F ⊂ x.

Scott also shows how information systems can be combined to form new information systems. The most interesting combination is the one by which the information system A → B (the ‘function space’) is formed. It seems to us that in some situations the entailment relation is not naturally defined (that is, it is not closely related with the objects studied). Especially in the definition of the function space there does not seem to be a natural explanation for the particular choice of the entailment relation (except for the fact that it leads to a smooth theory), and we try here to see how far the theory of information systems can be developed without the entailment relation— or, more precisely, with the entailment relation that is always present, namely A ⊢ B iff it is impossible for further information added to A to contradict B.

We continue to use the same term ‘information system’ for our systems which are devoid of ⊢, because we will refer here only to such systems. Definition 6.1 An ‘information system’ is a triple A = (D_{A}, Δ_{A}, Con_{A})

where D_{A} is a set (here finite or countable), Δ_{A} ∈ D_{A} is a distinguished element, and Con is a collection of finite subsets of D_{A} such that the following holds:

1. Con_{A} contains all singletons {a}, for a ∈ D_{A}, and is subset closed (i.e., if X ⊂ Y ∈ Con_{A}, then X ∈ Con_{A}).

2. If X ∈ Con_{A}, then X ∪ {Δ_{A}} ∈ Con_{A}.

Given an information system, A, let us define the ‘(maximal) entailment relation’, ⊢_{A}, on Con_{A}: For u, v ∈ Con_{A},

u ⊢_{A} v iff for every x, u ∪ x ∈ Con_{A} implies v ∪ x ∈ Con_{A}.

The following obvious properties of entailment hold:

1. If u ⊢_{A} v then u ∪ v ∈ Con_{A}, and for every x ⊇ u in Con_{A}, x ⊢_{A} v.

2. u ⊢_{A} {Δ_{A}}.

3. u ⊢_{A} v iff for every a ∈ v, u ⊢_{A} {a}.

4. u ⊢_{A} v for every v ⊆ u.

5. u ⊢_{A} v and v ⊢_{A} t imply u ⊢_{A} t.

It follows now that for any information system A as above, (A, ⊢_{A}) is an information system in the original sense of Scott’s definition. Thus our discussion may be viewed as a remark on a particular class of Scott’s information systems.

We shall say that e ⊂ D_{A} is ‘consistent’ if, for every finite E ⊆ e, E ∈ Con_{A}. Two (or more) subsets, E and F, of D_{A} are said to be consistent if E ∪ F is consistent.

The elements of an information system A are defined to be the consistent and entailment closed subsets of D_{A}. That is x ⊂ D_{A} is an ‘element’ of A iff every finite subset of x is in Con_{A}, and whenever E ⊂ x and E ⊢_{A} F, then F ⊂ x as well. The set of elements of A is denoted by | A |. A maximal element is one that is not included in any other element.

Given two information systems, A and B, the disjoint sum, A + B, the product, A × B, and the function space, A → B, are defined as in Scott [1982]—but now there is no need to define the entailment relation for each construct. We will restate the definition of the function space, in order to prove that the (modified) definition of ‘approximable mappings’ gives exactly the elements of the space. For that, let us first introduce some notations.

For any F ⊆ X × Y let us define left(F) = {x | ∃y (x, y) ∈ F }. Similarly, right(F) is defined, and, for any W, right_{W} (F) = {y | ∃x ⊆ W such that (x, y) ∈ F }. ∪left(F) is called the left projection of F. It is the set of all a such that a ∈ x for some (x, y) ∈ F. Similarly, ∪right(F) is called the right projection of F. For any W, ∪right_{W} (F) is denoted F_{W}.

For two information systems, A and B, define the function space C = A → B as the following information system:

1. D_{C} = Con_{A} × Con_{B} = {(u, v) | u ∈ Con_{A} & v ∈ Con_{B}}.

2. Δ_{C} = (∅, ∅).

3. For finite E ⊂ D_{C},

E ∈ Con_{C} iff for every X ∈ Con_{A}, E_{X} ∈ Con_{B}.

Equivalently,

E ∈ Con_{C} iff for every E_{0} ⊂ E, if the left projection of E_{0} is in

Con_{A}, then the right projection of E_{0} is in Con_{B}.

To define approximable mappings, we first need the following generalization of the entailment notation. Given an information system, A, define for u, u_{1}, …, u_{n} ∈ Con_{A} u ⊢_{A} (u_{1} ∨ … ∨ u_{n}) iff For every x ⊃ u in Con_{A} there is i ≤ n such that x ∪ u_{i} ∈ Con_{A}.

Definition 6.2 Let A and B be information systems. An approximable mapping, f : A → B, is a binary relation f ⊂ Con_{A} × Con_{B} such that

1. ∅ f ∅.

2. ufv & ufv′ ⇒ uf(v ∪ v′).

3. u′ ⊢_{A} u, ufv, v ⊢_{B} v′ ⇒ u′fv′.

4. u ⊢_{A} u_{1} ∨ … ∨ u_{n}, (∀i u_{i}fv) ⇒ ufv.

Remark: It follows that if F is a finite subset of an approximable mapping f : A → B then:

1. If X ∈ Con_{A}, then F_{X} ∈ Con_{B}. (Hence f is a consistent subset of A → B.)

2. If u ∈ Con_{A} is such that x ⊆ u whenever (x, y) ∈ F, then

(u, right(F)) ∈ f.

Theorem 6.3 The approximable mappings f : A → B are exactly the elements f ∈| A → B |.

Proof: Suppose first that f ∈| A → B |. Then f ⊂ D_{A→B} is consistent and entailment closed. So f ⊂ Con_{A} × Con_{B}. Since f is entailment closed, and as ∅ ⊢ {Δ} is always true, Δ_{A→B} ∈ f. That is, ∅f∅. Suppose now that (u, v), (u, v′) ∈ f; we are going to show that (u, v ∪ v′) ∈ f. Since f is consistent, {(u, v), (u, v′)} ∈ Con_{A→B}, and hence w = v ∪ v′ ∈ Con_{B}. To prove ufw, it suffices to observe that

{(u, v), (u, v′)} ⊢_{A→B} {(u, w)},

and then to use the fact that f is entailment closed. To prove items 3 and 4 in the definition of an approximable mapping, suppose that

u ⊢_{A} u_{1} ∨ … ∨ u_{n}, (∀i u_{i}fv), and v ⊢_{B} v′.

We have to prove that ufv′. For this, one proves that

{(u_{1}, v), …, (u_{n}, v)} ⊢_{A→B} {(u, v′)},

and uses the fact that f is entailment closed.

For the second direction of the proof we make some preliminary definitions and a lemma (which will also be used later). Let U be an information system and L ⊂ D_{U} (not necessarily consistent). T ∈ Con_{U} is said to be ‘maximal on L’ iff for every consistent T′ ⊃ T, T ∩ L = T′ ∩ L. In other words, T is maximal on L if T is consistent, but for every a ∈ L \ T, T ∪ {a} is inconsistent.

The collection of all T ∈ Con_{U} that are maximal on L is denoted M_{U}(L). The collection of all T ∈ Con_{U} that are maximal on L and such that L_{0} = T ∩ L is denoted M_{U}(L, L_{0}).

Observe that for finite L ⊂ D_{U}, and B ∈ Con_{U},

B ⊢_{U} ⋁{L ∩ T | T ∈ M_{U}(L)&B ⊆ T }.

(This disjunction is finite since L is finite.)

Lemma 6.4 Let A and B be information systems and M = (A → B). If F ∈ Con_{M} and (a, b) ∈ D_{M}, then the following are equivalent:

1. F ⊬_{M} {(a, b)}.

2. Put L = ⋃ left(F). There exists w ⊇ a in Con_{A}, maximal on L, such that F_{w} ⊬_{B} b. (Recall that F_{w} = ⋃ right_{w}(F).)

Proof: Assume first 1. So there is G ∈ Con_{M} such that F ⊆ G and E = G ∪ {(a, b)} is not consistent. Thus there is X ∈ Con_{A} such that E_{X} ∉ Con_{B}. Since G is consistent, it follows that a ⊆ X. Now extend X and find X ⊆ w that is maximal on L. Then E_{X} ⊆ E_{w} and so E_{w} ∉ Con_{B}. w is as required since F_{w} ⊬_{B} b because F_{w} ⊆ G_{w} ∈ Con_{B} and G_{w} ∪ b = E_{w}.

Assume 2 and let us check that 1 holds. Since F_{w} ⊬_{B} b, there is z ⊇ F_{w} in Con_{B} such that z ∪ b is not in Con_{B}. Hence {(w, z), (a, b)} is not in Con_{M}. But F′ = F ∪ {(w, z)} is consistent, and hence 1. To see that F′ is in Con_{M}, suppose that X ∈ Con_{A}, and let us check that F′_{X} ∈ Con_{B}. Since F is consistent we may assume that w ⊆ X, and then F′_{X} = F_{X} ∪ z. Since w is maximal on L, for every (x, y) ∈ F, if x is consistent with w then x ⊆ w, and in such a case y ⊆ F_{w} ⊆ z. Thus F_{X} ⊆ z and F′_{X} = z.

Returning to the proof of Theorem 6.3, assume f : A → B is an approximable mapping, and we will show that f ∈| A → B |. By Definition 6.2, f ⊂ D_{A→B}. We remarked that f is consistent (after Definition 6.2). To prove that f is entailment closed, suppose F ⊂ f is finite, and F ⊢_{A→B} {(u, v)}; we will show that (u, v) ∈ f.

Put L = ⋃ left(F). For every t, set L_{t} = t∩L. Then, since any consistent t can be extended to be maximal on L,

u ⊢_{A} ⋁{L_{t} | u ⊆ t and t is maximal on L}.

For any E ∈ Con_{A}, (E, F_{E}) ∈ f, because F ⊢_{A→B} {(E, F_{E})}. Thus (L_{t}, F_{L_{t}}) ∈ f. If we show that F_{L_{t}} ⊢_{B} v, for every such t, then by the closure property 4 of Definition 6.2, (u, v) ∈ f.

By Lemma 6.4, since F ⊢_{A→B} {(u, v)}, for every t ⊇ u maximal on L, F_{t} ⊢_{B} v. But F_{t} = F_{L_{t}}, and hence F_{L_{t}} ⊢_{B} v for each t ⊃ u maximal on L. Hence (u, v) ∈ f. This ends the proof of Theorem 6.3.

To solve a recursive system of information-system equations, one may proceed in defining better and better approximations to the solutions and then take their unions. (For more details read Larsen and G. Winskel [1984].) We shall define a relation U < V on information systems (which indicates that V is a better approximation than U), and then show how the diverse constructions are preserved, e.g., if U_{1} < U_{2} and V_{1} < V_{2}, then (U_{1} → V_{1}) < (U_{2} → V_{2}).

Say that X ∈ Con_{U} is full iff X ⊢_{U} Y for all consistent Y ⊃ X. Equivalently, for every two consistent sets, Y_{1} and Y_{2} extending X, Y_{1} ∪ Y_{2} is consistent.

Definition 6.5 Let U and V be information systems. U < V iff

1. D_{U} ⊆ D_{V}.

2. For every finite E ⊆ D_{U}, E ∈ Con_{U} iff E ∈ Con_{V}.

3. If A ∈ Con_{U}, then A is full in V if A is full in U.

4. For finite X, Y_{1}, …, Y_{n} ⊆ D_{U}, if X ⊢_{U} ⋁{Y_{i} | 1 ≤ i ≤ n}, then X ⊢_{V} ⋁{Y_{i} | 1 ≤ i ≤ n} as well.

Let us make the following remarks on this definition.

1. In applications, condition D_{U} ⊆ D_{V} is replaced by the existence of an appropriate embedding e : D_{U} → D_{V}. For example, if N is the discrete information system of the natural numbers, then N < (N → N) by the embedding taking k to ({Δ}, {k}).

2. Condition 3 is natural: Usually it is not the case that the closure under entailment (in V) of a maximal element of U is maximal in V, but if a finite set in U generates a maximal element (i.e., it is full) then the element it generates in V is maximal as well. The other direction in 3 is evident: If A ∈ Con_{U} is full in V then it is full in U.

3. Assuming the first two conditions, condition 4 is equivalent to the “reflection property” which is the following: For every finite A ⊆ D_{U} (not necessarily in Con_{U}), for every B ∈ Con_{V}, if B is maximal on A, then there exists B′ ∈ Con_{U} maximal on A and such that B ∩ A = B′ ∩ A. We say in this case that B′ reflects B on A.

(Let us check that 4 implies this reflection property. Assume 4. Since

B ∩ A ⊢_{U} ⋁{A ∩ T |T ∈ M_{U}(A) & B ∩ A ⊆ T },
B ∩ A ⊢_{V} ⋁{A ∩ T |T ∈ M_{U}(A) & B ∩ A ⊆ T }.

Hence B is consistent with some A ∩ T for T ∈ M_{U}(A) such that B ∩ A ⊆ T. By maximality, B ∩ A = T ∩ A.)

For A ⊆ D_{U} and A_{0} ∈ Con_{U}, such that A_{0} ⊆ A, define the width of the configuration (A, A_{0}) to be the supremum of the sizes of families A ⊆ M_{U}(A, A_{0}) consisting of pairwise inconsistent members (such a family is called an ‘antichain’ in M_{U}(A, A_{0})). The width of a configuration is ≥ 1 when M_{U}(A, A_{0}) ≠ ∅ and it can be ω.

We claim the following: For 0 < k < ∞, the width of (A, A_{0}) is k iff there is in M_{U}(A, A_{0}) a maximal antichain of size k consisting of full sets. Indeed, suppose that the width is k and let B_{1}, …, B_{k} be an antichain in M_{U}(A, A_{0}) (there are no antichains of size k + 1 there); then all the B_{i}’s are full or else k can be increased.

On the other hand, if B_{1}, …, B_{k} is a maximal antichain in M_{U}(A, A_{0}) (there are no antichains there extending this one) and each B_{i} is full, then M_{U}(A, A_{0}) contains no antichain of size k + 1. To see this, suppose that X_{1}, …, X_{k+1} is an antichain in M_{U}(A, A_{0}), and we will get a contradiction. If some X_{j} is inconsistent with each B_{i}, then the antichain of the B_{i}’s is not maximal. Hence every X_{j} is consistent with some B_{i}, and so there are two X_{j}’s consistent with the same B_{i} which is thence not full.

A similar argument shows that if the width of (A, A_{0}) is ω, then there is in M_{U}(A, A_{0}) an infinite antichain (the supremum is obtained). This is proved by contradiction. If all the antichains in M_{U}(A, A_{0}) are finite, construct by induction a tree in M_{U}(A, A_{0}) a follows. Suppose that the n-th level of the tree is a maximal antichain in M_{U}(A, A_{0}), extend each node to a maximal antichain of sets in M_{U}(A, A_{0}) that extend this node. Now the construction will not end at a finite stage or else the leaves form a maximal antichain of full sets and this implies a finite width. Hence the tree has an infinite branch and the infinite antichain is obtained by the splittings along this branch.

These considerations lead to the following lemma.

Lemma 6.6 If U < V, then the width of (A, A_{0}) in U (for A ⊆ D_{U}) is the same as its width in V. Hence for any finite A ⊂ D_{U}, and antichain X ⊂ M_{V} (A), there is a map ρ : X → M_{U}(A) such that ρ(v) reflects v on A, and, for distinct v_{1} and v_{2} in X, ρ(v_{1}) and ρ(v_{2}) are inconsistent.

Proof: For the first part of the lemma, suppose the width of (A, A_{0}) in U is k, and let B_{1}, …, B_{k} be a maximal antichain of full sets in M_{U}(A, A_{0}). By the reflection property, this family is maximal in V as well, and hence the width of (A, A_{0}) in V is k. If the width of (A, A_{0}) in U is ω, then it is obviously ω in V.

To prove the second part of the lemma, let M = {v ∩ A | v ∈ X}. For each A_{0} ∈ M there may be several (say k many, where k is finite or ω) v’s in X such that v ∩ A = A_{0}. However, since the width of (A, A_{0}) in V is not greater than its width in U, there is in M_{U}(A, A_{0}) an antichain of size k, and hence ρ can be defined. It is defined separately for each A_{0} ∈ M on {v ∈ X | v ∩ A = A_{0}} and the union of these functions is the desired ρ (observe that if X, Y ∈ M_{U}(A) and X ∩ A ≠ Y ∩ A then X and Y are inconsistent). Now comes the main Lemma, for which < was introduced.

Lemma 6.7 If U < V and S < T, then (U → S) < (V → T).

Proof: Set L = (U → S), M = (V → T). Let us check the four properties in Definition 6.5 needed to show that L < M.

The inclusion D_{L} ⊆ D_{M}, and the equality of Con_{L} with Con_{M} on subsets of D_{L} are clear.

Suppose that A ∈ Con_{L} is not full in M; we will show then that it is not full in L. So there is (v, t) ∈ D_{M} compatible with A (i.e., its singleton is consistent with A) and such that

A ⊬_{M} (v, t).

We will provide (v′, t′) ∈ D_{L} compatible with A such that A ⊬_{L} {(v′, t′)}.

Put E = ⋃ left(A). By Lemma 6.4 there is w ⊇ v in Con_{V}, maximal on E, such that for y = ⋃ right_{w}(A), y ⊬_{T} t. By reflection, there is w′ ∈ Con_{U} that reflects w on E. So, w′ is maximal on E, and w′ ∩ E = w ∩ E. Thus y = A_{w′}.

Now, y∪t ∈ Con_{T} since A and (v, t) are compatible. So y is not full in T. Hence y is not full in S, and there is t′ ∈ Con_{S} such that t′ is consistent with y but y ⊬_{S} t′. Hence A and {(w′, t′)} are consistent in L, but A ⊬ {(w′, t′)} (by Lemma 6.4).

Finally, we prove reflection of M in L. Let A ⊆ D_{L} be finite, and B ∈ Con_{M} be maximal on A. Put A_{0} = B ∩ A. We shall find B′ ∈ Con_{L} maximal on A such that A ∩ B′ = A_{0}.

Let E = ⋃ left(A), F = ⋃ left(A ∪ B). Let us define

K = {v | v ∈ Con_{V} is maximal such that v ⊆ F }.

Then K is an antichain in M_{V} (E). Fix a map ρ that assigns to every v ∈ K some ρ(v) ∈ Con_{U} that reflects v on E, and such that for distinct v’s the values of ρ are inconsistent (by Lemma 6.6).

For each v ∈ K let t = B_{v} and let \overline{t} ⊇ t be some extension in Con_{T} that is maximal on G = right(A). Then let γ(v) ∈ M_{S}(G, G ∩ \overline{t}) be some reflection of \overline{t}. Since A_{0} ⊆ B, (A_{0})_{v} ⊆ t. As (A_{0})_{v} ⊆ G,

(A_{0})_{v} ⊆ γ(v).

Define B_{1} ⊂ D_{L} by B_{1} = {(ρ(v), γ(v)) | v ∈ K}. Now set B′ = A_{0} ∪ B_{1}. We are going to prove that B′ ∈ Con_{L} and that for every (u, s) ∈ A \ A_{0}, {(u, s)} ∪ B′ is not consistent.

To prove that B′ ∈ Con_{L}, let X ∈ Con_{U} be given, and we shall see that B′_{X} ∈ Con_{S}. B′_{X} = (A_{0})_{X} ∪ (B_{1})_{X}. As A_{0} ∈ Con_{L} we may assume that (B_{1})_{X} ≠ ∅. But since {ρ(v) | v ∈ K} is an antichain, there is then exactly one v ∈ K with ρ(v) ⊆ X. So B′_{X} = (A_{0})_{X} ∪ γ(v). But (A_{0})_{X} = (A_{0})_{v}. (Because (A_{0})_{X} ⊃ (A_{0})_{v} follows from v ∩ E = ρ(v) ∩ E ⊆ X. For the second inclusion, take any (a, b) ∈ A_{0} such that a ⊆ X. Then a is consistent with ρ(v) and hence with v; by the maximality of v ∈ K, a ⊆ v.) We observed above that (A_{0})_{X} ⊆ γ(v), and thus B′_{X} = γ(v) ∈ Con_{S}.

We now prove the maximality of B′ on A. Take any (u, s) ∈ A \ A_{0}. By its maximality, B is not compatible with (u, s), and hence there is v ⊆ F such that u ⊆ v and s is not consistent with B_{v}. We may assume v ∈ K. To prove that B′ is not compatible with (u, s), take (ρ(v), γ(v)) ∈ B′ and prove that it is not compatible with (u, s). Indeed u ⊆ ρ(v), and s is not consistent with γ(v) because γ(v) reflects some \overline{t} ⊇ B_{v} on G.

7 Conclusion

The concept ‘pomset with functions’ presented here combines the system executions of Lamport [1986] and the pomsets of Gischer [1989] and Pratt [1986]. (It is unfortunate that divergent terminologies have evolved, since different aspects of the same concept were illuminated by these papers.

We are not the first to expand system executions. It is quite clear to any reader of Lamport [1986] that, at least informally, he enriches his structures by speaking about values obtained by reads etc. It is also clear that Gaifman [1989] was aware of the implications of adding the axioms of interval orders to pomsets. Ben-David [1988] has explicitly added unary predicates to the structures of Lamport, and thus combined the pomset notion with that of ‘pure’ system-executions.

The notion of a pomset is further extended by allowing functions (of bounded depth). One of the reasons for introducing these functions lies in the need to view systems in a hierarchical manner. An important benefit of the partial-ordering modeling approach—as opposed to the interleaving of atomic events—is the ability to consider higher-level views of system executions (for a definition see Lamport [1986]). In these higher-level views, some minute events are lumped together to form a single entity. In this passage from the concrete to the abstract, necessarily (and fortunately) some details are lost, and in order to preserve those lower-level properties that are important in the higher-level view, functions (or binary predicates) are used.

The notion of state was defined as a pomset that describes a moment (a pomset with no temporal relations). This was used to show the duality and equivalence of the state based and the event based approaches to concurrency.

A natural alternative approach is to define a state as an equivalence class of runs where two runs are equivalent iff they have exactly the same continuations. This idea is investigated in Probst and Li [1990] and it expresses the intuition that a state is the manifold of all future possibilities. We have chosen a different, more concrete, path in our definition, and one of our motives in this choice was the desire to show that states are finite objects. (However, our approach can be adapted to infinite domains as well; this is needed for denotational semantics, because then the realm of finite objects must be abandoned.)

We have outlined a possible approach to semantics of concurrency, which uses the notion of a pomset state. One advantage of our approach to semantics is the flexibility gained by having in one framework both the event approach and the state approach. Thus, the specifications for the communication devices are primarily given in terms of pomsets (this is an event approach), but the execution of sequential programs results (essentially) in a tree of states. When combined, the semantics of communicating processes can be clearly exposed—at least for the very simple language discussed here.

References

U. Abraham, S. Ben-David, and M. Magidor 1990 On Global-Time and Inter-process Communication. Semantics for

Concurrency, Proceedings of the International BCS-FACS Workshop, pp. 311-323.

F. Anger 1989 On Lamport’s interprocess communication. ACM Transactions on

Programming Languages and Systems, Vol. 11 No. 3, pp. 404-417.

S. Ben-David 1988 The global-time assumption and semantics for distributed systems.

7th ACM Symp. on Principles of Distributed Computing, pp. 223-232.

P. C. Fishburn 1986 Interval orders and interval graphs. Wiley, New-York (Wiley-Interscience

series in discrete mathematics).

H. Gaifman 1989 Modeling concurrency by partial orders and non-linear transition

systems. In Logic and Models for Concurrency, edited by J. de Bakker, W. de Roever, and G. Rozenberg. Lecture Notes in Computer Science 354. Springer-Verlag, Berlin, pp. 467-488.

J. Gischer 1989 The equational theory of pomsets. Theoretical Computer Science,

Vol. 61, pp. 199-224.

L. Lamport 1986 On Interprocess Communication, Part I: Basic formalism, Part II:

Algorithms. Distributed Computing, Vol. 1, pp. 77-101.

K. G. Larsen and G. Winskel 1984 Using information systems to solve recursive equations effectively.

Semantics of Data Types. Edited by G. Kahan et al. Lecture Notes in Computer Science 173. Springer-Verlag.

V. Pratt 1986 Modeling Concurrency with Partial Orders. International J. of Par-

allel Programming, Vol. 15, pp. 33-71.

D. K. Probst and H. F. Li 1990 Modelling Reactive Hardware Processes Using Partial Orders. Se-

mantics for Concurrency, Proceedings of the International BCS-FACS Workshop, pp. 324-343.

D. S. Scott 1982 Domains for Denotational Semantics. In Automata, Lang., and

Prog. Edited by M. Nielsen and E. M. Schmidt, Lecture Notes in Computer Science 140. Springer-Verlag, Berlin.

N. Wiener 1914 A contribution to the theory of relative position. Proc. Camb. Phi-

los. Soc. 17, pp. 441-449.