Compositional Relational Semantics for Indeterminate Dataflow Networks

Eugene W. Stark^{∗}

Department of Computer Science

State University of New York at Stony Brook

Stony Brook, NY 11794 USA

Abstract

Given suitable categories T, C and functor F : T → C, if X, Y are objects of T, then we define an (X, Y)-relation in C to be a triple (R, \underline{r}, r̄), where R is an object of C and \underline{r} : R → F X and r̄ : R → F Y are morphisms of C. We define an algebra of relations in C, including operations of “relabeling,” “sequential composition,” “parallel composition,” and “feedback,” which correspond intuitively to ways in which processes can be composed into networks. Each of these operations is defined in terms of composition and limits in C, and we observe that any operations defined in this way are preserved under the mapping from relations in C to relations in C′ induced by a continuous functor G : C → C′.

To apply the theory, we define a category Auto of concurrent automata, and we give an operational semantics of dataflow-like networks of processes with indeterminate behaviors, in which a network is modeled as a relation in Auto. We then define a category EvDom of “event domains,” a (non-full) subcategory of the category of Scott domains and continuous maps, and we obtain a coreflection between Auto and EvDom. It follows, by the limit-preserving properties of coreflectors, that the denotational semantics in which dataflow networks are represented by relations in EvDom, is “compositional” in the sense that the mapping from operational to denotational semantics preserves the operations on relations. Our results are in contrast to examples of Brock and Ackerman, which imply that no compositional semantics is possible in terms of set-theoretic relations.

1 Introduction

Dataflow networks (see, e.g. [4, 3, 5, 7, 9, 10]) consist of a collection of concurrently and asynchronously executing sequential processes that communicate by transmitting sequences or “streams” of “value tokens” over FIFO communication channels. Typically, a network is described as a directed graph, whose nodes are processes and whose arcs are communication channels. Each channel serves to connect an “output port” of one process to an “input port” of another process. “Determinate” (or functional) networks were first studied by Kahn [9], who gave an elegant fixed-point principle for determining the function computed by a network from the functions computed by the components.

∗Research supported in part by NSF Grant CCR-8702247.

“Indeterminate” (or non-functional) networks remain less well understood, despite extensive study. An interesting class of indeterminate processes are the “merge” processes, which shuffle together sequences of values from two input channels onto a single output channel. Brock and Ackerman have shown [3, 4] that no naive generalization of Kahn’s theory to indeterminate networks, obtained by replacing input/output functions with input/output relations, can be “compositional” in the sense that the mapping from operational to denotational semantics preserves the operations by which networks are built from component processes. Their examples use only functional processes and a weak form of merge process; thus, their results apply to essentially any interesting class of indeterminate networks.

The title of this paper advertises “compositional relational semantics for indeterminate dataflow networks.” This reason this is not a contradiction with Brock and Ackerman’s results is that their results apply only to the usual set-theoretic notion of a relation, whereas here we use instead a category-theoretic generalization. Our notion of relation involves two suitably complete categories T and C, and a suitable functor F : T → C. If X and Y are objects of T, then by an “(X, Y)-relation in C” we mean a triple (R, \underline{r}, r̄) where R is an object of C, and \underline{r} : R → F X and r̄ : R → F Y are morphisms of C. We think of the objects of T as “types,” and in our semantics of dataflow networks the types X and Y are simply the sets of input ports and output ports over which a process may communicate. An algebra of relations in C can be defined, including operations of “relabeling,” “sequential composition,” “parallel composition,” and “feedback” that correspond intuitively to ways in which networks can be built from component processes. These operations have categorical definitions in terms of composition and limits in C. It is a simple observation (Theorem 1) that any operations definable in this way are preserved by the mapping from relations in C to relations in C′ induced by a continuous functor G : C → C′.

To obtain a correct semantics of process networks, we must choose properly the category C, and this is a bit tricky. In this paper, we give two examples for C: (1) a category Auto of concurrent automata, and (2) a certain (non-full) subcategory EvDom of the category of Scott domains and continuous maps. The semantics based on Auto is “operational,” because it involves automata and computation sequences, and it is not difficult to become convinced that it can serve as accurate model of the usual informal “token-pushing” operational semantics usually given for dataflow networks (see, e.g. [3]). The semantics based on EvDom is more “denotational,” because it is defined using order-theoretic notions that do not necessarily have to do with computation. The objects of EvDom are the “event domains,” which have been studied previously [6, 20], but the morphisms we use are apparently new, and are crucial to our results. We obtain a coreflection between Auto and EvDom, and from the limit-preserving properties of coreflectors it follows immediately that the denotational semantics based on EvDom is “compositional” in the sense that the map from operational to denotational semantics preserves the operations of our relational algebra. Moreover, the denotational semantics is not “too abstract,” in the sense that networks having distinct input/output relations in the ordinary set-theoretic sense, also determine distinct relations in EvDom. The semantics is not fully abstract, though.

In this paper, F X or F (X) denotes the application of functor (or function) F to argument X. If F : X → Y and G : Y → Z, then GF or G ∘ F denotes the composition of F and G. We use parentheses freely to increase readability. For basic definitions and terminology of category theory, we refer the reader to [8, 11]. The text [15] and the unpublished [14] contain material on domain theory.

2 An Algebra of Relations

We begin by defining a category-theoretic generalization of the notion of a relation, and we show how to obtain various operations on relations that correspond intuitively to ways in which processes can be composed into networks.

2.1 Relations

Let T be a category equipped with a specified terminal object and binary products, and let C be a category with a specified terminal object, binary products, and equalizers of parallel pairs of arrows. Let F : T → C be a functor that preserves the specified terminal object and products. Intuitively, we think of T as a category whose objects are “types” and whose morphisms are “relabeling maps.” Pairs of objects of T will be used to index classes of relations, which are built in the category C.

Formally, if X and Y are objects of T, then an (X, Y)-relation in C (with respect to the functor F) is a triple (R, \underline{r}, r̄), where R is an object of C and \underline{r} : R → F X, r̄: R → F Y are morphisms of C:

[figure: F Y; R; F X; r̄; \underline{r}]

When there can be no confusion, we usually say “let R be an (X, Y)-relation in C,” and use corresponding lower-case letters \underline{r}, r̄ to denote the morphisms.

If R and S are (X, Y)-relations in C, then a morphism from R to S is a morphism f : R → S in C such that the obvious diagram commutes:

[figure: F Y; R; F X; r̄; \underline{r}; S; s̄; \underline{s}; f]

Let Reln_{C}(X, Y) denote the category of (X, Y)-relations in C and their morphisms.

For example, if T = C = Set, the category of sets and functions, and F : T → C is the identity functor, then an ordinary set-theoretic relation R ⊆ X × Y may be represented as an (X, Y)-relation in C by taking \underline{r} : R → X and r̄ : R → Y to be the projections on the first and second components, respectively.

2.2 Operations on Relations

We may define various operations on relations.

2.2.1 Relabeling

Suppose R is an (X, Y)-relation in C. If ϕ : Y → Y′ is a morphism in T, then the output relabeling of R by ϕ is the (X, Y′)-relation R; ϕ = (R, \underline{r}, (F ϕ)r̄). Similarly, if ψ : X → X′ is a morphism in T, then the input relabeling of R by ψ is the (X′, Y)-relation ψ; R = (R, (F ψ)\underline{r}, r̄). Output relabeling by ϕ extends to a functor

( - ); ϕ : Reln_{C}(X, Y) → Reln_{C}(X, Y′).

and input relabeling by ψ extends to a functor

ψ; ( - ) : Reln_{C}(X, Y) → Reln_{C}(X′, Y).

2.2.2 Sequential Composition

Relations may be composed in sequence as suggested by the picture:

[figure: X; Y; Z; R; S]

Formally, if R is an (X, Y)-relation in C and S is a (Y, Z)-relation in C, then their sequential composition is the (X, Z)-relation R; S = (R; S, \underline{r}s′, s̄r′), where r′ and s′ are defined to make the square in the following diagram a pullback:

[figure: S; R; S; R; r′; s′; F Y; \underline{s}; r̄; F Z; F X; \underline{r}; s̄]

It should be noted that in the case T = C = Set, with F : T → C the identity functor, the above definition of sequential composition of relations does not agree exactly with the standard set-theoretic definition. Specifically, if R ⊆ X × Y and S ⊆ Y × Z, then

R; S ≃ {(x, y, z) : (x, y) ∈ R, (y, z) ∈ S}.

2.2.3 Parallel Composition

Relations may also be composed in parallel, as suggested by the picture:

[figure: X′; Y′; X; Y; S; R]

Formally, suppose R is an (X, Y)-relation in C and S is an (X′, Y′)-relation in C. Then their parallel composition is the (X × X′, Y × Y′)-relation R∥S = (R × S, \underline{r} × \underline{s}, r̄× s̄), where we have used the assumption that F (X × X′) = F X × F X′ and F (Y × Y′) = F Y × F Y′.

The mapping that takes the pair (R, S) to R∥S extends to a functor

∥ : Reln_{C}(X, Y) × Reln_{C}(X′, Y′) → Reln_{C}(X × X′, Y × Y′).

2.2.4 Feedback

We can also define an operation of “feedback,” corresponding to the picture:

[figure: R; X; Z; Y; ϕ]

Formally, suppose R is an (X × Z, Y)-relation in C, and ϕ : Y → Z is a morphism in T. The feedback of R by ϕ is the (X, Y)-relation (R_{ϕ} , π_{F X} \underline{r}e, r̄e), where e is the equalizer of π_{F Z} \underline{r} and (F ϕ)r̄ in C:

[figure: R_{ϕ}; R; F Y; F (X × Z); F Z; F X; F Y; e; \underline{r}; r̄; π_{F Z}; F ϕ; π_{F X}; id_{F Y}]

The map ( - )_{ϕ} extends to a functor

( - )_{ϕ} : Reln_{C}(X × Z, Y) → Reln_{C}(X, Y).

The operations we have defined are not independent: in particular, sequential composition is definable (up to isomorphism) in terms of parallel composition, output relabeling, and feedback. Formally, suppose R is an (X, Y)-relation in C and S is a (Y, Z)-relation in C. Let π_{Y} : Y × Z → Y and π_{Z} : Y × Z → Z be the projections associated with the product Y × Z in T. Then

R; S ≃ ((R∥S)_{π_{Y}} ); π_{Z}.

2.3 Preservation of Operations by Functors

Suppose now we have two categories, C and C′, equipped with specified terminal object, binary products, and equalizers, and two functors F : T → C and F′ : T → C′ that preserve the specified terminal object and products. If G : C → C′ is a functor such that GF = F′, then each (X, Y)-relation R = (R, \underline{r}, r̄) in C determines an (X, Y)-relation GR = (GR, G\underline{r}, Gr̄) in C′. The map taking R to GR extends, for each (X, Y), to a functor

G_{X,Y} : Reln_{C}(X, Y) → Reln_{C′}(X, Y).

Moreover, if G preserves the specified limits, then the ensemble of functors {G_{X,Y} : X, Y ∈ T} preserves the operations of relabeling, sequential composition, parallel composition, and feedback on relations in a way made precise by the following result:

Theorem 1 Suppose C, C′, F, F′ and G are as above. Then

1. If R ∈ Reln_{C}(X, Y), ϕ : Y → Y′, and ψ : X → X′, then

G_{X,Y′}(R; ϕ) = G_{X,Y} (R); ϕ, G_{X′,Y} (ψ; S) = ψ; G_{X,Y} (S).

2. If R ∈ Reln_{C}(X, Y) and S ∈ Reln_{C}(Y, Z), then G_{X,Z}(R; S) = G_{X,Y} (R); G_{Y,Z}(S).

3. If R ∈ Reln_{C}(X, Y) and R′ ∈ Reln_{C}(X′, Y′), then

G_{X×X′,Y ×Y′}(R∥R′) = G_{X,Y} (R)∥G_{X′,Y′}(R′).

4. If R ∈ Reln_{C}(X × Z, Y) and ϕ : Y → Z, then G_{X,Z}(R_{ϕ} ) = G_{X×Z,Y} (R)_{ϕ} .

Proof – All of these operations have categorical definitions in terms of composition and limits, and these are preserved by the functor G.

Obviously, the same reasoning applies to show that the functors G_{X,Y} preserve any other operations on relations in C we might wish to consider, provided those operations can be defined in terms of composition and limits in C.

3 Concurrent Automata

In this section, we define a category Auto of concurrent automata. This category serves as our operational semantics for dataflow networks, in that we shall model networks as relations in Auto. The kind of automata we consider incorporate concurrency in the form of a binary concurrency relation ∥ on a set E of events. The pair (E, ∥) is called a “concurrent alphabet.” Intuitively, events represent primitive occurrences during computation. If events e and e′ are both possible occurrences when in state q, and if e and e′ are related by the concurrency relation, then e and e′ can be executed in either order, with equivalent effect. Similar automata have been studied by Bednarczyk [2], and by the author [18, 19].

3.1 Concurrent Alphabets

A concurrent alphabet is a set E, equipped with a symmetric, irreflexive binary relation ∥_{E}, called the concurrency relation. Elements e, e′ ∈ E are said to commute if e∥_{E}e′, and a subset U of E is called commuting if every pair of its elements commutes. Let Com(E) denote the set of all finite commuting subsets of E. Suppose U, V ∈ Com(E). Then U and V are called orthogonal, and we write U ⊥_{E} V, if U ∪ V ∈ Com(E) and U ∩ V = ∅.

A morphism from a concurrent alphabet E to a concurrent alphabet F is a function μ : Com(E) → Com(F) such that

1. μ(∅) = ∅.

2. If U ∪ V ∈ Com(E), then μ(U) ∪ μ(V) ∈ Com(F), and μ(U \ V) = μ(U) \ μ(V).

Here the symbol \ denotes set difference. Let Alph denote the category of concurrent alphabets and their morphisms.

Concurrent alphabets constitute the starting point for “trace theory” [1, 12]. The above definition of morphism of concurrent alphabets was motivated by the author’s study of “concurrent transition systems” [16, 17, 18]. The category Alph has a number of pleasant properties, although the author is not aware of it having been studied previously.

Lemma 3.1 Suppose μ : E → F is a morphism of concurrent alphabets. If U∪V ∈ Com(E), then (1) μ(U ∪ V) = μ(U) ∪ μ(V) and (2) μ(U ∩ V) = μ(U) ∩ μ(V).

Proof – (1) Observe that for arbitrary sets A, B, C, we have C = A∪B iff A\C = ∅ = B\C, C\A = B\A, and C\B = A\B. Clearly, ∅ = μ(U \(U ∪V)) = μ(U)\μ(U ∪V), and similarly μ(V) \ μ(U ∪ V) = ∅. Since μ(U ∪ V) \ μ(V) = μ((U ∪ V) \ V) = μ(U \ V) = μ(U) \ μ(V), and similarly, μ(V ∪ U) \ μ(U) = μ(V) \ μ(U), it follows that μ(U ∪ V) = μ(U) ∪ μ(V).

(2) μ(U ∩ V) = μ(U \ (U \ V)) = μ(U) \ (μ(U) \ μ(V)) = μ(U) ∩ μ(V).

Lemma 3.2 Suppose μ : E → F is a morphism of concurrent alphabets. Then μ(e) ⊥_{F} μ(e′) whenever e∥_{E}e′. Conversely, any function μ : E → Com(F) having this property extends uniquely to a morphism μ : E → F.

Proof – If μ : E → F is a morphism, and e∥_{E}e′, then μ({e}) = μ({e} \ {e′}) = μ({e}) \ μ({e′}), and similarly, μ({e′}) = μ({e′}) \ μ({e}), so μ({e}) ∩ μ({e′}) = ∅.

Conversely, if μ : E → Com(F) has the stated property, then it extends to a morphism by defining μ(U) = ⋃{e ∈ U : μ(e)}. Moreover, by Lemma 3.1, any extension of μ to a morphism must satisfy this relation, so the extension of μ is uniquely determined.

Theorem 2 Alph has finite limits.

Proof – We show that Alph has: (1) a terminal object, (2) binary products, and (3) equalizers of parallel pairs.

(1) The empty concurrent alphabet is easily seen to be a terminal object (in fact a zero object) in Alph.

(2) Suppose E and F are concurrent alphabets. Let E⊗F denote the concurrent alphabet with elements E + F (disjoint union), and with ∥_{E⊗F} = ∥_{E} ∪ ∥_{F} ∪ (E × F) ∪ (F × E). Note that the sets in Com(E ⊗ F) are precisely those of the form U + V with U ∈ Com(E) and V ∈ Com(F). Define projections π_{E} : E ⊗ F → E and π_{F} : E ⊗ F → F by π_{E}(U) = U ∩ E and π_{F} (U) = U ∩ F. It is easy to check that π_{E} and π_{F} are morphisms, and that E ⊗ F, equipped with π_{E} and π_{F}, has the universal property required of a categorical product.

(3) Suppose σ, τ : E → F are morphisms in Alph. Define a nonempty set U ∈ Com(E) to be equalizing if σ(U) = τ(U). Call U minimal equalizing if it is equalizing and it has no proper equalizing subsets. We observe the following fact: if U and V are distinct minimal equalizing subsets of E, and U ∪ V ∈ Com(E), then U and V are disjoint. For, if U ∩ V = W ≠ ∅, then σ(W) = σ(U) ∩ σ(V) = τ(U) ∩ τ(V) = τ(W), so W is equalizing, a contradiction with the assumed minimality of U, V. It follows from this observation that every equalizing U ∈ Com(E) can be written uniquely as a finite union of minimal equalizing subsets.

Now, let D be the set of all minimal equalizing subsets of E, and define U∥_{D}V iff U ∪V ∈ Com(E). Define μ : D → E to be the morphism that satisfies μ({U_{1},…, U_{n}}) = ⋃_{k} U_{k} whenever {U_{1},…, U_{n}} ∈ Com(D). One may now check that μ is an equalizer of σ and τ.

3.2 Automata

An automaton is a tuple A = (E, Q, q^{o}, T), where

• E is a concurrent alphabet of events, not containing the special symbol ϵ, called the identity event.

• Q is a set of states.

• q^{o} ∈ Q is a distinguished start state.

• T ⊆ Q × (E ∪ {ϵ}) × Q is a set of transitions. We write t : q⟶^{e}r, or just q⟶^{e}r, to denote a transition t = (q, e, r) ∈ T or to assert the existence of such a transition in T.

These data are required to satisfy the following conditions:

(Identity) q⟶^{ϵ}r iff q = r.

(Disambiguation) If q⟶^{e}r and q⟶^{e}r′, then r = r′.

(Commutativity) For all states q and events e, e′ ∈ E, if e∥_{E}e′, q⟶^{e}r, and q⟶^{e′}r′, then for some state s there exist transitions r⟶^{e′}s and r′⟶^{e}s.

If t : q⟶^{e}r, then q is called the domain dom(t) of t and r is called the codomain cod(t) of t. Transitions t and u are called coinitial if dom(t) = dom(u). We say that event e ∈ E is enabled in state q if there exists a transition q⟶^{e}r in T.

Intuitively, if e ∈ E, then a transition q⟶^{e}r represents a potential computation step of A in which event e occurs and the state changes from q to r. Identity transitions q⟶^{ϵ}q do not represent computation steps of A; they serve merely to “pad” computations. The (Identity) condition ensures that this is all they can do. The (Disambiguation) condition ensures that the new state r in a transition q⟶^{e}r is uniquely determined by q and e. The (Commutativity) condition says that if two commuting events are enabled in the same state, then they can occur in either order with the same effect.

A finite computation sequence for an automaton A is a finite sequence γ of transitions of the form:

q_{0}⟶^{e_{1}}q_{1}⟶^{e_{2}} … ⟶^{e_{n}}q_{n}.

The number n is called the length |γ| of F. (By convention, if n = 0 then the computation sequence consists of the single state q_{0}, and no transitions.) Similarly, an infinite computation sequence for A is an infinite sequence of transitions:

q_{0}⟶^{e_{1}}q_{1}⟶^{e_{2}} ….

We extend notation and terminology for transitions to computation sequences, so that if γ is a computation sequence, then the domain dom(γ) of γ is the state q_{0}, and if γ is finite, then the codomain cod(γ) of γ is the state q_{n}. We write γ : q → r to assert that γ is a finite computation sequence with domain q and codomain r. A computation sequence γ is initial if dom(γ) is the distinguished start state q^{o}. If γ : q → r and δ : q′ → r′ are finite computation sequences, then γ and δ are called composable if q′ = r, in which case we define their composition to be the finite computation sequence γδ : q → r′, obtained by concatenating γ and δ and identifying cod(γ) with dom(δ).

If A = (E, Q, q^{o}, T) and A′ = (E′, Q′, (q^{o})′, T′) are automata, then a morphism from A to A′ is a pair ρ = (ρ_{e}, ρ_{s}), where ρ_{e} : E → E′ is a morphism of concurrent alphabets, and ρ_{s} : Q → Q′ is a function, such that

1. ρ_{s}(q^{o}) = (q^{o})′.

2. Suppose q⟶^{e}r ∈ T, with e ≠ ϵ. Then for every enumeration {e′_{1},…, e′_{n}} of ρ_{e}({e}), there exists a (necessarily unique) finite computation sequence

ρ_{s}(q) = r′_{0}⟶^{e′_{1}}r′_{1}⟶^{e′_{2}} … ⟶^{e′_{n}}r′_{n} = ρ_{s}(r)

of A′.

We usually drop the subscripts on ρ_{e} and ρ_{s}, writing ρ for both.

Let Auto denote the category of automata and their morphisms. There is an obvious forgetful functor AuAl : Auto → Alph, which takes each automaton A = (E, Q, q^{o}, T) to the concurrent alphabet E, and each morphism (ρ_{e}, ρ_{s}) of automata to the morphism ρ_{e} of concurrent alphabets.

Theorem 3 The forgetful functor AuAl : Auto → Alph has a right adjoint AlAu : Alph → Auto.

Proof – Given a concurrent alphabet E, let AlAu(E) be the one-state automaton (E, {∗}, ∗, T), where T = {∗} × (E ∪ {ϵ}) × {∗}. We claim that this construction defines the object map of a functor AlAu : Alph → Auto, which is right-adjoint to the forgetful functor AuAl : Auto → Alph. To prove this, it suffices to show that for each E ∈ Alph, there exists an “evaluation map” ε_{E} : AuAl(AlAu(E)) → E, universal from AuAl to E. We may simply take ε_{E} = id_{E}.

Theorem 4 Auto has finite limits.

Proof – We show that Auto has (1) a terminal object, (2) binary products, and (3) equalizers.

(1) It is easy to see that the one-state, one-transition automaton with the empty alphabet of events is a terminal object (in fact a zero object) in Auto.

(2) Suppose A_{1} = (E_{1}, Q_{1}, q_{1}^{o}, T_{1}) and A_{2} = (E_{1}, Q_{2}, q_{2}^{o}, T_{2}) are automata. Let A_{1} × A_{2} be the automaton

A_{1} × A_{2} = (E_{1} ⊗ E_{2}, Q_{1} × Q_{2}, (q_{1}^{o}, q_{2}^{o}), T),

where T is the set of all ((q_{1}, q_{2}), e, (r_{1}, r_{2})) such that one of the following conditions holds:

1. e = ϵ, q_{1} = r_{1}, and q_{2} = r_{2}.

2. e ∈ E_{1}, (q_{1}, e, r_{1}) ∈ T_{1}, and q_{2} = r_{2}.

3. e ∈ E_{2}, (q_{2}, e, r_{2}) ∈ T_{2}, and q_{1} = r_{1}.

Define projections π_{i} : A_{1} × A_{2} → A_{i} (i ∈ {1, 2}) by letting (π_{i})_{e} : E_{1} ⊗ E_{2} → E_{i} be the projection in Alph and (π_{i})_{s} : Q_{1} × Q_{2} → Q_{i} be the projection in Set. It is straightforward to verify that A_{1} × A_{2}, equipped with projections π_{1} and π_{2}, is a product in Auto.

(3) Suppose σ, τ : A → A′ are morphisms in Auto, where A = (E, Q, q^{o}, T) and A′ = (E′, Q′, (q^{o})′, T′). Let μ_{e} : D → E be an equalizer of σ_{e} and τ_{e} in Alph, let μ_{s} : R → Q be an equalizer of σ_{s} and τ_{s} in Set. Recall that D is the set of all minimal equalizing sets U ∈ Com(E). Define B = (D, R, q^{o}, T), where T consists of all triples (q, U, r) such that to each enumeration {e_{1},…, e_{n}} of U there corresponds a computation sequence

q = q_{0}⟶^{e_{1}}q_{1}⟶^{e_{2}} … ⟶^{e_{n}}q_{n} = r

of A. Let μ = (μ_{e}, μ_{s}), then it is straightforward to verify that μ is an equalizer of σ and τ in Auto.

4 Operational Semantics of Dataflow Networks

In this section, we give a formal operational semantics for dataflow networks as relations in Auto.

4.1 Port Sets

Let Port be the category whose objects are finite or countably infinite sets (of ports), and whose morphisms are the opposites of functions; thus, a morphism f : P P′ is a function from P′ to P. The empty set ∅ is clearly a terminal object in Port, and if + denotes disjoint union, then the set P + P′ is obviously a product of P and P′ in Port. Let V be a fixed universe of data values, which we assume contains the set of natural numbers as a subset. If P is an object of Port, then define a P -event to be an element of the concurrent alphabet Events(P) = P × V, where (p, v)∥(p′, v′) iff p ≠ p′. Intuitively, we think of a P -event e = (p, v) as representing the transmission of data value v over port p. We write port(e) to denote the port component p and value(e) to denote the value component v, of e.

Define the functor PoAl : Port → Alph to take each object P of Port to the concurrent alphabet Events(P), and each morphism f : P P′ of Port to the morphism ϕ : PoAl(P) → PoAl(P′), defined by

ϕ(U) = {e ∈ PoAl(P′) : (f(port(e)), value(e)) ∈ U}

for all U ∈ Com(Events(P)). Intuitively, we think of a morphism f : P P′ in Port as a relabeling map that labels each port in P′ by a port in P. The corresponding morphism ϕ : PoAl(P) → PoAl(P′) in Alph has the dual effects: (1) of deleting events for ports in P that are not the labels of ports in P′, and (2) of duplicating events for ports in P that happen to be the labels of more than one port in P′.

Lemma 4.1 The functor PoAl preserves finite products.

Proof – Straightforward.

Let PoAu : Port → Auto be the composite functor AlAu ∘ PoAl. Then since PoAl preserves finite products and AlAu is a right adjoint, hence preserves limits, it follows that PoAu also preserves finite products.

4.2 Port Automata

Define a port signature to be a pair (X, Y) of objects of Port. The elements of X are called input ports and those of Y, output ports. If (X, Y) is a port signature, then an (X, Y)- port automaton is an automaton A = (E, Q, q^{o}, T), such that E = Events(X + Y + Z) = Events(X) ⊗ Events(Y) ⊗ Events(Z) and the following condition holds:

(Receptivity) For all q ∈ Q and all a ∈ Events(X), there exists a transition q⟶^{a}r in T.

Elements of Events(X), Events(Y), and Events(Z) are called input events, output events, and internal events, respectively. Intuitively, the receptivity condition states that a port automaton is always prepared to receive arbitrary input.

A port automaton is determinate if the following additional condition holds:

(Determinacy) For all q ∈ Q and all b, b′ ∈ Events(Y + Z), if both b and b′ are enabled in state q, then b∥b′.

Intuitively, determinate port automata make no internal choices between conflicting events.

As an example of how we can model a dataflow process as a port automaton, consider the case of a “merge” process, whose function is to shuffle together sequences of values arriving on two input ports into a single output sequence. Let i_{1} and i_{2} denote the two input ports and let o denote the single output port. We may represent the merge process as a port automaton

A_{mrg} = (Events({i_{1}, i_{2}} + {o} + {n}), V^{∗} × V^{∗} × V^{∗}, (⊥, ⊥, ⊥), T),

where ⊥ denotes the empty string, and the set of transitions T contains a transition

((x_{1}, x_{2}, y), e, (x′_{1}, x′_{2}, y′))

iff one of the following conditions holds:

1. e = ϵ, x′_{1} = x_{1}, x′_{2} = x_{2}, and y′ = y.

2. e = (i_{1}, v), x′_{1} = x_{1}v, x′_{2} = x_{2}, and y′ = y.

3. e = (i_{2}, v), x′_{1} = x_{1}, x′_{2} = x_{2}v, and y′ = y.

4. e = (n, 1), vx′_{1} = x_{1}, x′_{2} = x_{2}, and y′ = yv.

5. e = (n, 2), x′_{1} = x_{1}, vx′_{2} = x_{2}, and y′ = yv.

6. e = (o, v), x′_{1} = x_{1}, x′_{2} = x_{2}, and vy′ = y.

It is straightforward to check that A_{mrg} satisfies the conditions for a port automaton, and that it is not determinate.

Intuitively, the state of A_{mrg} contains two “input buffers” and one “output buffer.” Transitions of type (2) and (3) correspond to arriving input values being placed at the end of the appropriate input buffer. Transitions of type (4) and (5) are internal transitions that correspond to the indeterminate selection of input in one input buffer or the other to be moved to the output buffer. Transitions of type (6) correspond to the transmission of output from the output buffer. Similar constructions can be used to model many other kinds of dataflow processes.

4.3 Port Automata as Relations

An (X, Y)-port automaton A = (E, Q, q^{o}, T) may be identified with the (X, Y)-relation (A, λ_{X}, λ_{Y}) in Auto (with respect to the functor AlAu ∘ PoAl : Port → Auto), where

λ_{X} : A → AlAu(PoAl(X)), λ_{Y} : A → AlAu(PoAl(Y))

are the adjoint transforms of the projections

π_{X} : AuAl(A) → PoAl(X), π_{Y} : AuAl(A) → PoAl(Y).

(Recall that AuAl(A) = E = PoAl(X) ⊗ PoAl(Y) ⊗ PoAl(Z).)

By making the above identification of port automata as relations in Auto, the definitions of Section 2.2 immediately become applicable, yielding operations of relabeling, sequential composition, parallel composition, and feedback on port automata. However, since not every (X, Y)-relation in Auto is an (X, Y)-port automaton, we do not know a priori that the class of port automata is closed under these operations.

Theorem 5 The classes of port automata and of determinate port automata are closed under the following operations:

1. Input relabeling by bijections, and output relabeling by injections.

2. Sequential composition.

3. Parallel composition.

4. Feedback by injections.

Proof – The proof simply requires substituting the characterizations of Theorem 4 into the definitions of the operations on relations, and checking that the conditions for port automata are satisfied in each case. We omit the details.

By working through the details of the previous proof, one may convince oneself that the port automaton model is a reasonable operational semantics for dataflow networks. For example, suppose A = (E, Q, q^{o}, T) is an (X × Z, Y)-port automaton, and let ϕ be an injection from Z to Y, viewed as a morphism ϕ : Y Z in Port. Intuitively, we think of ϕ as specifying, for each input port in Z, a corresponding port in Y to which it is to be “connected” by a “feedback loop.” Applying the feedback operation _{ϕ} to A results (up to isomorphism) in an (X, Y)-port automaton A′ = (E \ Events(Z), Q, q^{o}, T′). Each input transition q⟶^{e}r of A with port(e) ∈ X is also a transition of A′, and if q⟶^{e}r is an output transition of A with port(e) ∈ Y \ ϕ(Z), then A′ has that same output transition. However, if q⟶^{e}r is an output transition of A with e = (ϕ(z), v) for some z ∈ Z, then A′ has instead a transition q⟶^{e}r′, where r′ is the unique state such that r⟶^{(z,v)}r′ is a transition of A. Intuitively, A′ behaves like A, except that in A′ outputs of values on ports in ϕ(Z) occur simultaneously with inputs of the same values on the corresponding ports in Z.

4.4 Set-Theoretic Input/Output Relations

We now complete our operational semantics of dataflow networks by showing how the usual set-theoretic input/output relation between domains of “port histories” can be extracted from port automata.

Formally, if P is a set of ports, then a P -history is a mapping from P to the CPO V^{∞} of all finite and infinite sequences of values in V, equipped with the prefix ordering ⊑. If H is a P -history, and P′ ⊆ P, then we write H|P′ to denote the P′-history H′ such that H′(p) = H(p) for all p ∈ P′.

Suppose A = (Events(P), Q, q^{o}, T) is an (X, Y)-port automaton, where P = X + Y + Z. Then each finite or infinite computation sequence

γ = q_{0}⟶^{e_{1}}q_{1}⟶^{e_{2}} …

of A determines a P -history H_{γ} as follows: for each p ∈ P, the sequence H_{γ}(p) is the sequence of values value(e′_{1}), value(e′_{2}),…, where e′_{1}, e′_{2},…, is the subsequence of e_{1}, e_{2},… consisting of precisely those e_{k} ≠ ϵ with port(e_{k}) = p.

A computation sequence γ of A is called completed if there exists no computation sequence δ, such that dom(γ) = dom(δ), H_{γ}|X = H_{δ}|X, and H_{γ} H_{δ}. That is, completed computation sequences are those whose histories are maximal among all computation sequences having the same domain and input port history. This is actually a kind of “fairness” property (see [13]), which intuitively is true when “every enabled output or internal event, not in conflict with some other enabled output or internal event, eventually occurs.” The set-theoretic input/output relation Rel(A) of A is the set of all pairs (H_{γ}|X, H_{γ}|Y) such that γ is a completed initial computation sequence of A.

For example, the input/output relation of the automaton A_{mrg} defined in the previous section is the set of all (H^{in}, H^{out}), with H^{in} an {i_{1}, i_{2}}-history and H^{out} an {o}-history, such that H^{out}(o) is a shuffle of a prefix x_{1} of H^{in}(i_{1}) and a prefix x_{2} of H^{in}(i_{2}), subject to the following conditions:

1. If H^{in}(i_{1}) is finite, then x_{2} = H^{in}(i_{2}).

2. If H^{in}(i_{2}) is finite, then x_{1} = H^{in}(i_{1}).

3. If both H^{in}(i_{1}) and H^{in}(i_{2}) are infinite, then either x_{1} = H^{in}(i_{1}) or else x_{2} = H^{in}(i_{2}).

Thus, the input/output relation of A_{mrg} is the angelic merge relation [13]. It is also possible to construct a port automaton having a slightly different merging relation, called infinity-fair merge, as its input/output relation. However, it is shown in [13] that no port automaton can have as its input/output relation the fair merge relation, which is the set of all (H^{in}, H^{out}) such that H^{out}(o) is a shuffle of all of H^{in}(i_{1}) and all of H^{out}(i_{2}).

We may regard the set-theoretic input/output relation Rel(A) of an (X, Y)-port automaton A as an (X, Y)-relation in the category Set of sets and functions. To do this, let F be the functor Hist : Port → Set that takes a set P of ports to the set Hist(P) of all port histories over P, and that takes a morphism f : P → P′ to the corresponding duplication/restriction map Hist(f) : Hist(P) → Hist(P′), given by Hist(f)(H)(p) = H(f(p)) for all p ∈ P′. This functor is easily seen to preserve finite products. The set-theoretic input/output relation Rel(A) of an (X, Y)-port automaton A may now be regarded as the (X, Y)-relation (Rel(A), π_{X}, π_{Y}) in Set, where π_{X} : Rel(A) → Hist(X) and π_{Y} : Rel(A) → Hist(Y) are the obvious projections.

It is important to observe that, although we may regard the set-theoretic input/output relation of an (X, Y)-port automaton as an (X, Y)-relation in Set, and thereby obtain formal operations of relabeling, composition, product, and feedback on such relations, these operations are incompatible with the corresponding operations on port automata. Specifically, the feedback operation is not preserved by the mapping from port automata to input/output relations. Brock and Ackerman have given specific examples of this failure of commutativity, and it has come to be called the “Brock-Ackerman anomaly.” The situation may be described succinctly as the failure of the set-theoretic relational semantics to be “compositional.”

5 Denotational Semantics of Dataflow Networks

The goal of this section of the paper is to replace the category Set, which does not yield a compositional denotational semantics for dataflow networks, with a more highly structured category EvDom, for which a compositional semantics is obtained. We do this in two steps: first we define a category TrDom of “trace domains,” which are domains that are embedded as certain normal subdomains of the domains of “traces” generated by a concurrent alphabet, then we throw away the embedding domains and obtain a category EvDom, whose objects are “event domains” and whose morphisms are certain continuous maps. We construct coreflections between Auto and TrDom and between TrDom and EvDom, with the right adjoints (coreflectors) going from Auto to TrDom and from TrDom to EvDom. It follows by Theorem 1 and the fact that right adjoints preserve limits, that the induced ensemble of functors, from (X, Y)-relations in Auto to (X, Y)-relations in EvDom, preserves the operations of relabeling, sequential and parallel composition, and feedback.

5.1 Domains

A (Scott) domain is an ω-algebraic, consistently complete CPO. A domain D is finitary if for all finite (=isolated=compact) elements d ∈ D the set {d′ ∈ D : d′ ⊑ d} is finite. If D and E are domains, then a monotone map f : D → E is continuous if it preserves directed lubs, strict if f(⊥_{D}) = ⊥_{E}, and additive if whenever d, d′ are consistent elements of d, then f(d), f(d′) are consistent elements of E, and f(e ⊔ e′) = f(e) ⊔ f(e′). Let Dom denote the category of domains and continuous maps.

A subdomain of D is a subset U of D, which is a domain under the restriction of the ordering on D, and is such that the inclusion of U in D is strict and continuous. A subdomain U of D is normal if for all d ∈ D, the set {e ∈ U : e ⊑ d} is directed.

Lemma 5.1 A subdomain U of D is normal iff the inclusion of U in D is additive and reflects consistent pairs.

Proof – Suppose U is a normal subdomain of D. If e, e′ ∈ U are consistent in D, then the set V = {e′′ ∈ U : e′′ ⊑ e ⊔_{D} e′} is directed and contains e, e′, so e and e′ are consistent in U. Let v = ⨆_{D} V, then v ∈ U because V ⊆ U and U is a subdomain of D. Clearly, v ⊑ e ⊔_{D} e′.

Also, e ⊔_{D} e′ ⊑ v, because v is an upper bound of e and e′. Hence v = e ⊔_{D} e′ = e ⊔_{U} e′ is an upper bound for e and e′ in U.

Conversely, suppose that whenever e and e′ are consistent in D, then e, e′ are consistent in U, and e ⊔_{U} e′ = e ⊔_{D} e′. We claim that for each d ∈ D, the set U_{d} = {e ∈ U : e ⊑ d} is directed. If e, e′ ∈ U_{d}, then e ⊑ d and e′ ⊑ d, so e, e′ are consistent in D, hence e, e′ are consistent in U, and e ⊔_{U} e′ = e ⊔_{D} e′ ⊑ d. Thus e ⊔_{U} e′ ∈ U_{d}.

An interval of a domain D is a pair I = (dom(I), cod(I)) ∈ D×D, with dom(I) ⊑ cod(I). Intervals I and J are coinitial if dom(I) = dom(J). The interval I is an identity if dom(I) = cod(I), and a nonidentity interval I is prime if there exists no d ∈ D with dom(I) d cod(I). It is ⊔-prime if there exists a finite, nonempty set U of prime and identity intervals, such that dom(J) = dom(I) for all J ∈ U, and cod(I) = ⨆{cod(J) : J ∈ U}. Coinitial intervals I and J are consistent if cod(I) and cod(J) are consistent elements of D. If I and J are consistent, then the residual of I after J is the interval I\J = (cod(J), cod(I)⊔cod(J)).

In the sequel, we shall use the term “interval” exclusively to mean “interval with finite endpoints.”

5.2 Trace Domains

Concurrent alphabets generate domains. Formally, suppose E is a concurrent alphabet. Let E^{∗} denote the free monoid generated by E, then there is a least congruence ∼ on E^{∗} such that e∥_{E}e′ implies ee′ ∼ e′e for all e, e′ ∈ E. The quotient E^{∗} /∼ is the free partially commutative monoid generated by E, and its elements are called traces. Define the relation ⊑ on E^{∗} /∼ by [x] ⊑ [y] iff there exists z ∈ E^{∗} with [xz] = [y]. This relation is a partial order with respect to which every consistent pair of elements has a least upper bound (this is not completely trivial to prove). We call ⊑ the prefix relation. By forming the ideal completion of the poset (E^{∗} /∼, ⊑), we obtain a domain Ê. The map taking E to Ê extends to a functor (ˆ -) : Alph → Dom.

We may think of the elements of Ê as equivalence classes of finite and infinite strings. The finite elements of E are the equivalence classes of finite strings. All the finite strings that are representatives of a given finite element of Ê are permutations of each other, hence have the same length and the same number of occurrences of each element of E. The prime intervals of Ê are those of the form ([x], [xe]), where x ∈ E^{∗} and e ∈ E, and the ⊔-prime intervals are those of the form ([x], [xe_{1} … e_{n}]), where x ∈ E^{∗} and {e_{1},…, e_{n}} ∈ Com(E). Distinct coinitial prime intervals I = ([x], [xe]) and I′ = ([x], [xe′]) are consistent iff e∥_{E}e′, in which case I \ I′ = ([xe′], [xe′e]).

Lemma 5.2 If E is a concurrent alphabet, then the domain Ê is finitary.

Proof – The finite elements of E are permutation equivalence classes of finite strings, and for finite [x], [y] we have [y] ⊑ [x] iff there exists z with [yz] = [x]. Thus, the cardinality of {[y] : [y] ⊑ [x]} is bounded by the number of prefixes of permutations of x, which is finite.

A trace domain is a pair (E, D), where E is a concurrent alphabet and D is a normal subdomain of Ê, such that every prime interval of D is also a prime interval of Ê. If (E, D) and (E′, D′) are trace domains, then a morphism from (E, D) to (E′, D′) is a morphism μ : E → E′ of concurrent alphabets such that the following two conditions hold:

1. μ̂(D) ⊆ D′.

2. Whenever (d, d′) is a prime interval of D, then (μ̂(d), μ̂(d′)) is a ⊔-prime interval of D′.

Let TrDom denote the category of trace domains and their morphisms.

We say that an element d of a domain D is secured if there exists a finite chain

⊥ = d_{0} ⊑ d_{1} ⊑ … ⊑ d_{n} = d,

such that each interval (d_{k}, d_{k+1}) is prime. We call such a chain a securing chain for d. We say that a domain D is secured if each of its finite elements is secured. It is easy to see that finitary domains are secured. We say that a subdomain U of D is secured in D if each finite element of U is secured as an element of D.

Lemma 5.3 Suppose (E, D) is a trace domain. Then D is finitary and secured in Ê.

Proof – Since D is a normal subdomain of Ê, every finite element of D is also a finite element of Ê. Since Ê is finitary, so is D. Now, since D is finitary we know that D is secured (in itself). Since every prime interval in D is also a prime interval of E, it follows that every securing chain for d ∈ D is also a securing chain for d ∈ Ê. Thus D is secured in E.

Automata “unwind” to trace domains, and the unwinding map gives a coreflection between Auto and TrDom. Formally, suppose A = (E, Q, q^{o}, T) is an automaton. Each finite or infinite computation sequence

γ = q_{0}⟶^{e_{1}}q_{1}⟶^{e_{2}} …

of A, determines an element tr(γ) of the domain Ê, according to the definition

tr(γ) = ⨆_{k} e_{1}e_{2} … e_{k},

where concatenation denotes multiplication in the monoid of finite traces E^{∗} /∼, and we identify the identity event ϵ with the monoid identity, so that ϵ does not appear in the trace e_{1} … e_{k}. We call tr(γ) the trace of the computation sequence γ. Let Traces(A) denote the set of all traces of initial computation sequences of A.

Theorem 6 Suppose A = (E, Q, q^{o}, T) is an automaton. Then (E, Traces(A)) is a trace domain. Moreover, the map taking A to (E, Traces(A)) is the object map of a functor AuTr : Auto → TrDom, which is right-adjoint to a full embedding TrAu : TrDom → Auto.

Proof – See the Appendix.

Corollary 5.1 TrDom has finite limits.

Proof – This follows immediately from the previous result, but as an aid to intuition we give the explicit constructions.

(Terminal Object) The trace domain (∅, {⊥}) is a terminal object (in fact a zero object) in TrDom.

(Products) Suppose (E_{1}, D_{1}), (E_{2}, D_{2}), are trace domains. Let E = E_{1} ⊗ E_{2} be the product of E_{1} and E_{2} in Alph, and let π_{i} : E_{1} ⊗ E_{2} → E_{i} (i ∈ {1, 2}) be the associated projections. Let D be the set of all x ∈ Ê such that π̂_{1}(x) ∈ D_{1} and π̂_{2}(x) ∈ D_{2}. Then (E, D), equipped with the morphisms π_{1} and π_{2}, is a product of (E_{1}, D_{1}) and (E_{2}, D_{2}) in TrDom.

(Equalizers) Suppose σ, τ : (E_{1}, D_{1}) → (E_{2}, D_{2}) is a parallel pair of morphisms in TrDom. Let μ : E → E_{1} be an equalizer of σ and τ in Alph. Define an element d ∈ Ê to be reachable if there exists a chain

⊥ = d_{0} ⊑ d_{1} ⊑ …

of finite elements of Ê, such that d = ⨆_{k} d_{k}, μ̂(d_{k}) ∈ D_{1} for all k ≥ 0, and for all k ≥ 0 the interval (μ̂(d_{k}), μ̂(d_{k+1})) is ⊔-prime. Let D be the set of all reachable elements of E. Then μ : (E, D) → (E_{1}, D_{1}) is an equalizer of σ and τ in TrDom.

5.3 Event Domains

We now wish to view a trace domain (E, D) as a domain in its own right, rather than as a normal subdomain of the domain Ê of traces. In fact, this can be done. By discarding the concurrent alphabet component of trace domains we obtain a class of domains called “event domains,” which have been studied previously. It is known that event domains are exactly those domains that are isomorphic to the “domains of configurations” of a certain kind of “event structure” [6, 20]. A byproduct of our investigation is the following representation theorem, which the author has not seen explicitly stated before.

• Event domains are precisely those domains D for which there exists a concurrent alphabet E and an embedding f : D → Ê of D as a normal subdomain of Ê, such that if (d, d′) is a prime interval of D, then (f(d), f(d′)) is a prime interval of Ê.

The formal definition of event domains requires a few preliminaries. Suppose D is a domain with the following property:

1. I \ J is a prime interval whenever I and J are distinct, consistent prime intervals.

Then it is not difficult to see that the same property holds if “prime” is replaced by “⊔- prime.”

If I = (d, d′) is a ⊔-prime interval of D, then define

pr(I) = {(d, d′′) : d d′′ ⊑ d′ and (d, d′′) is prime}.

Call coinitial ⊔-prime intervals I and J orthogonal if they are consistent and pr(I)∩pr(J) = ∅. Note that coinitial prime intervals are orthogonal iff they are distinct and consistent. Let ≡ be the least equivalence relation on ⊔-prime intervals of D such that I ≡ I \ J whenever I and J are orthogonal ⊔-prime intervals. A straightforward induction using property (1) shows that if I is prime and I ≡ I′, then I′ is also prime.

An event domain is a finitary domain D that satisfies property (1) above, and in addition satisfies:

2. I ≡ J implies I = J, whenever I, J are coinitial prime intervals.

3. If I, I′, J, J′ are prime intervals such that I ≡ I′, J ≡ J′, I and J are coinitial, and I′ and J′ are coinitial, then I and I′ are consistent iff J and J′ are consistent.

A morphism from an event domain D to an event domain D′ is a strict, additive, continuous function f : D → D′ with the following two additional properties:

1. Whenever I is a prime interval of D, then f(I) is a ⊔-prime interval of D′.

2. Whenever I, J are distinct consistent prime intervals of D, then f(I) and f(J) are orthogonal.

Let EvDom denote the category of event domains and their morphisms, then EvDom is a (non-full) subcategory of Dom.

Lemma 5.4 If (E, D) is a trace domain, then D is an event domain. Moreover, the map taking (E, D) to D extends to a (forgetful) functor TrEv : TrDom → EvDom.

Proof – We first show that if E is a concurrent alphabet, then Ê is an event domain. We have already seen (Lemma 5.2) that Ê is finitary. It remains to verify axioms (1)-(3) for event domains.

(1) An interval I of Ê is prime iff it is of the form ([x], [xe]), with x ∈ E^{∗} and e ∈ E. Distinct, coinitial prime intervals I = ([x], [xe]) and I′ = ([x], [xe′]) are consistent iff e∥_{E}e′, in which case I \ I′ is the interval ([xe], [xee′]), which is prime.

(2) A straightforward induction shows that if I ≡ I′, where I = ([x], [xe]) and I′ = ([x′], [x′e′]) are prime intervals, then e = e′. Hence if I ≡ I′ and I, I′ are coinitial, then I = I′.

(3) If distinct prime intervals I = ([x], [xe]) and J = ([x], [xe′]) are consistent, then e∥_{E}e′. If I′ = ([x′], [x′e]) ≡ I and J′ = ([x′], [x′e′]) ≡ J, then clearly I′ and J′ must also be consistent.

Next, we show that if D is is a normal subdomain of Ê, such that an interval of D is prime in D iff it is also prime in Ê, then D is also an event domain. Suppose D is such a domain. Clearly, D has property (1) of an event domain. By an induction we see that if I and J are prime intervals of D, then I ≡ J in D iff I ≡ J in Ê. Properties (2)-(3) of an event domain follow easily from this fact.

Finally, to see that TrEv is a functor, note that given a morphism μ : (E, D) → (E′, D′) in TrDom, the map μ̂ : Ê → Ê′ restricts to a map TrEv(μ) : D → D′. The prime intervals of D are those of the form I = ([x], [xe]) where x ∈ E^{∗} and e ∈ E. Then μ̂(I) = (μ̂([x]), μ̂([x])μ̂(e)), which is a ⊔-prime interval of D′. Also, if I and J are distinct, consistent prime intervals of D, then I = ([x], [xe]) and J = ([x], [xe′]), where e∥_{E}e′. Since μ(e)∩μ(e′) = ∅, it follows that μ̂(I) and μ̂(J) are orthogonal. Hence TrEv(μ) is a morphism of event domains.

Theorem 7 The forgetful functor TrEv : TrDom → EvDom has a left adjoint EvTr, such that TrEv ∘ EvTr ≃ 1.

Proof – See the Appendix.

Corollary 5.2 EvDom has finite limits.

5.4 Summary

We have now reached our goal. Dataflow networks have an operational semantics as port automata, which we identify with the corresponding relations in Auto. The functor G = TrEv ∘ AuTr : Auto → EvDom preserves limits, hence induces an ensemble of functors

G_{X,Y} : Reln_{Auto}(X, Y) → Reln_{EvDom}(X, Y)

which preserve not only the operations of relabeling, sequential composition, parallel composition, and feedback, but any operations that have categorical definitions in terms of composition and limits in Auto. Thus, the denotational semantics, in which a dataflow network denotes an (X, Y)-relation in EvDom, agrees with the operational semantics given by port automata. Moreover, the semantics is not “too abstract,” in the sense that networks with distinct set-theoretic input/output relations receive distinct denotations. This can be verified by observing that the set-theoretic input/output relation of a port automaton can still be extracted from the corresponding relation in EvDom.

6 Port Automata and Causal Relations

Not every (X, Y)-relation in EvDom is the relation corresponding to an (X, Y)-port automaton. There are a number of reasons why this is so, but the easiest to see is that although the receptivity condition in the definition of port automata introduces an asymmetry between input and output, there is no such asymmetry in the definition of relations in EvDom. We would like to have a theorem that characterizes exactly, in terms of categorical properties of EvDom, those (X, Y)-relations that are the relations corresponding to (X, Y)-port automata and those that are the relations corresponding to determinate (X, Y)-automata.

Note that the category EvDom has a substantial amount of structure with which to express such properties; for example, its hom-sets are partially ordered by virtue of its being a subcategory of the category Dom. At the moment, we have no exact characterization theorem, but we do have some partial results. In particular, we can show that the relation in EvDom corresponding to an (X, Y)-port automaton is causal, in a sense to be defined formally below, and that the class of causal relations in EvDom is closed under those relational operations that make sense for port automata. The notion of causality captures some of the input/output asymmetry exhibited by port automata.

Formally, let categories T and C, and functor F : T → C be as in Section 2. Suppose further that the category C is pointed; that is, it has a unique zero morphism 0_{A,B} : A → B for every pair of objects A, B. Then an (X, Y)-relation R in C is causal if there exists a morphism m : F X → R such that \underline{r}m = id_{F X} and r̄m = 0. Then \underline{r} is a retraction and m is a section.

Theorem 8 The class of causal relations in C is closed under the following operations:

1. Output relabeling by arbitrary morphisms and input relabeling by retractions.

2. Sequential composition on the output with arbitrary relations (hence also sequential composition on the input with causal relations).

3. Parallel composition.

4. Feedback.

Proof – Omitted.

Lemma 6.1 The category EvDom is pointed.

Proof – The one-point domain is a zero object.

Theorem 9 If R is the (X, Y)-relation in EvDom corresponding to an (X, Y)-port automaton, then R is causal.

Proof – The receptivity property of an (X, Y)-port automaton A implies that for each input history H ∈ Hist(X), there is a corresponding initial computation sequence γ such that γ consists entirely of input or identity transitions, and H_{γ}|X = H. The map m_{0} : Hist(X) → R that takes each such H to the trace tr(γ) ∈ R is the m required to show R causal.

It appears that we can go quite a bit further than this. By taking into account the order relation ≤ on the hom-sets of EvDom, one can see that if R is an (X, Y)-relation in EvDom corresponding to an (X, Y)-port automaton, then the section m_{0} : Hist(X) → R produced by the construction in the proof of the previous theorem is characterized by the properties \underline{r}m_{0} = id_{Hist(X)} and m_{0}\underline{r} ≤ id_{R}. That is, (m_{0}, \underline{r}) is an embedding-projection pair. One may also observe that for relations R corresponding to determinate automata, the class of all sections m, such that \underline{r}m = id_{Hist(X)}, is directed by ≤ and has m_{0} as a least element. By taking the least upper bound of this collection (working now in the full subcategory of Dom whose objects are the event domains), we obtain a continuous map μ : Hist(X) → R. By composing with r̄, we obtain a continuous map r̄μ : Hist(X) → Hist(Y). Thus we see that determinate automata determine continuous maps from input to output. We expect that this observation can form the basis for a nice connection between the category-theoretic semantics of feedback we gave here in terms of equalizers, and the order-theoretic version given by Kahn in terms of least fixed points. We are currently attempting to work out the details of this connection.

7 Conclusion

By showing that the algebra of causal relations in EvDom constitutes a correct semantics for dataflow networks, we obtain a substantial amount of algebraic machinery for reasoning about such networks. Further clarification of the structure of those relations in EvDom that correspond to port automata should yield even more machinery. The study of relations in EvDom may also yield useful characterizations of “observational equivalence” of networks, and information about the structure of the fully abstract semantics with respect to this equivalence.

A Appendix: Proofs of Theorems 6 and 7

Theorem 6 Suppose A = (E, Q, q^{o}, T) is an automaton. Then (E, Traces(A)) is a trace domain. Moreover, the map taking A to (E, Traces(A)) is the object map of a functor AuTr : Auto → TrDom, which is right-adjoint to a full embedding TrAu : TrDom → Auto.

Proof – We first show that Traces(A) is a normal subdomain of Ê. To do this requires a detailed analysis of the structure of the set of initial computation sequences of A, and we perform this analysis using the notion of the “residual” γ \ δ of one finite computation sequence γ “after” another finite computation sequence δ. Intuitively, γ \ δ is obtained from γ by cancelling out transitions that, “up to permutation equivalence,” also appear in δ.

Formally, the residual operation is a partial binary operation on coinitial pairs of computation sequences. We first define \ for single transitions, and then extend to arbitrary finite computation sequences by induction on their length. For single transitions, suppose t : q⟶^{a}r and u : q⟶^{b}s. If a = ϵ, then t \ u = (s⟶^{ϵ}s) and u \ t = u. If a = b ≠ ϵ, then we define t \ u = (s⟶^{ϵ}s) = (r⟶^{ϵ}r) = u \ t. If ϵ ≠ a ≠ b ≠ ϵ, then t \ u is defined iff a∥_{E}b, in which case the commutativity property of A implies there must exist (necessarily unique) transitions s⟶^{a}p and r⟶^{b}p, which we take as t \ u and u \ t, respectively.

Next, we extend to arbitrary finite computation sequences. Suppose γ : q → r and δ : q → s are coinitial finite computation sequences. Then 1. If |γ| = 0 then γ \ δ = id_{s}, where id_{s} denotes the length-0 computation sequence from

state s.

2. If |γ| > 0 and |δ| = 0, then γ \ δ = γ.

3. If γ = tγ′, δ is the single transition u, t \ u is defined, and γ′ \ (u \ t) is defined, then

γ \ δ = (t \ u)(γ′ \ (u \ t)).

4. If |γ| > 0, δ = uδ′ with |δ′| > 0, γ \ u is defined, and (γ \ u) \ δ′ is defined, then

γ \ δ = (γ \ u) \ δ′.

For a more detailed explanation of this operation and its properties, the reader is referred to [13, 18].

We now use \ to define a relation ∼ on initial computation sequences as follows: For finite sequences γ and δ, define γ ∼ δ to hold precisely when γ \ δ is a sequence of identity transitions. Extend this definition to infinite sequences by defining γ′ ∼ δ′ iff for every finite prefix γ of γ′, there exists a finite prefix δ of δ′, such that γ ∼ δ.

We observe the following facts about ∼:

1. The relation ∼ is a preorder, and the set of ∼-equivalence classes, equipped with the induced partial ordering, is a domain whose finite elements are precisely the equivalence classes of finite initial computation sequences.

2. The map taking each ∼-equivalence class to its trace is strict, additive, and continuous.

3. Initial computation sequences γ and δ have a ∼-upper bound (given by γ(δ \ γ) or δ(γ \ δ), which are ∼-equivalent) iff the traces tr(γ) and tr(δ) are consistent.

4. γ ∼ δ iff tr(γ) ⊑ tr(δ).

Facts (1) and (2) are shown in [13] using the properties of the residual operation developed there. Facts (3) and (4) can be verified by straightforward inductive arguments from the definition of the residual operation. It follows from these facts and Lemma 5.1 that the map taking each ∼-equivalence class to its trace is an isomorphism of the domain of equivalence classes of initial computation sequences of A to a normal subdomain of Ê. Since this subdomain is Traces(A), we conclude that Traces(A) is a normal subdomain of Ê.

To complete the proof that (E, Traces(A)) is a trace domain, we observe that the prime intervals ([γ], [δ]) in the domain of equivalence classes of initial computation sequences of A are those for which δ \ γ contains precisely one nonidentity transition. Since this implies that tr(δ) is longer than tr(γ) by one symbol, it follows that prime intervals in Traces(A) are also prime intervals in Ê.

It remains to be shown the map AuTr, taking A to (E, Traces(A)), is the object map of a functor that is right-adjoint to a full embedding TrAu : TrDom → Auto. Given a trace domain (E, D), define the automaton TrAu(E, D) = (E, Q, q^{o}, T) as follows:

• Let Q be the set of finite elements of D, with q^{o} = ⊥. Then Q is a set of equivalence classes of finite strings.

• Let T contain all transitions [x]⟶^{ϵ}[x] with [x] ∈ Q and all transitions [x]⟶^{e}[xe] with both [x] and [xe] in Q.

It is straightforward to verify that TrAu(E, D) is an automaton. Moreover, each morphism ϕ : (E, D) → (E′, D′) in TrDom determines a morphism TrAu(ϕ) : TrAu(E, D) → TrAu(E′, D′), where TrAu(ϕ)_{e} = ϕ, and TrAu(ϕ)_{s} is the restriction of ϕ̂ to a map from finite elements of D to finite elements of D′. To see that TrAu(ϕ) is in fact a morphism of automata, note that the nonidentity transitions t of TrAu(E, D) correspond bijectively to the prime intervals ([x], [xe]) in D. For each such interval, (ϕ̂([x]), ϕ̂([xe])) is a ⊔-prime interval of D′. hence is of the form

([x′], [x′e′_{1}] ⊔… ⊔ [x′e′_{n}]),

where {e′_{1},…, e′_{n}} is an arbitrary enumeration of ϕ({e}), and [x′e′_{1}],…, [x′e′_{n}] are all in D′. It follows from this that to each enumeration {e′_{1},…, e′_{n}} of ϕ({e}) there corresponds a computation sequence

TrAu(ϕ)_{s}([x]) = [x′]⟶^{e′_{1}}[x′e′_{1}]⟶^{e′_{2}}([x′e′_{1}]⊔[x′e′_{2}])⟶^{e′_{3}} … ⟶^{e′_{n}}([x′e′_{1}]⊔…⊔[x′e′_{n}]) = TrAu(ϕ)_{s}([xe])

of TrAu(E′, D′).

Clearly, the functor TrAu is faithful and injective on objects. It is also full, because if (ψ_{e}, ψ_{s}) : TrAu(E, D) → TrAu(E′, D′), then (1) an induction on the length of securing chains shows that ψ_{s}([x]) = ψ̂_{e}([x]) for each finite trace [x] ∈ D, and (2) it follows from the defining properties of automata that if ([x], [xe]) is a prime interval of Traces(TrAu(E, D)), then (ψ̂_{e}([x]), ψ̂_{e}([xe])) is a ⊔-prime interval of Traces(TrAu(E′, D′)). Hence if ϕ : (E, D) → (E′, D′) is the morphism in TrDom with ϕ and ψ_{e} the same morphism of concurrent alphabets, then TrAu(ϕ) = ψ.

Given an automaton A, define the “evaluation map” ε_{A} : TrAu(AuTr(A)) → A to be the identity on events and to take each state [x] of TrAu(AuTr(A)) to the state cod(γ) of A, where γ is an initial computation sequence of A having trace [x]. Since all such computation sequences γ determine the same state cod(γ) by commutativity, we know that ε_{A} is welldefined. To see that ε_{A} is in fact a morphism of automata, suppose that [x]⟶^{e}[xe] is a transition of TrAu(AuTr(A)). Then there exist initial computation sequences γ and δ of A, such that γ has trace [x] and δ has trace [xe]. Then δ \ γ : cod(γ) → cod(δ) is a computation sequence of A that contains precisely one nonidentity transition t : cod(γ) → cod(δ). Hence, to every enumeration of {e} of ε_{A}({e}) there corresponds a computation sequence cod(γ)⟶^{e}cod(δ) of A, as required to show that ε_{A} is a morphism.

We claim that ε_{A} is universal from TrAu to A. Suppose ψ : TrAu(E′, D′) → A is a morphism in Auto. We claim that there is a unique morphism ϕ : (E′, D′) → AuTr(A) in TrDom such that ε_{A} ∘ TrAu(ϕ) = ψ. Since ε_{A} is the identity on events, ϕ and ψ must be the same morphism of concurrent alphabets, thus there is only one possible definition for ϕ. To show that this definition actually yields a morphism ϕ : (E′, D′) → AuTr(A) of trace domains, we must show: (1) that ϕ̂(D′) ⊆ Traces(A), and (2) if ([x′], [x′e′]) is a prime interval in D′, then (ϕ̂([x′]), ϕ̂([x′e′])) is a ⊔-prime interval in Traces(A).

To show (1), observe that ϕ̂(D′) = ψ̂(D′). An induction on the length of securing chains in D′ shows that each finite [x′] ∈ D′ determines an initial computation sequence γ of A with tr(γ) = ψ̂([x′]) and cod(γ) = ψ_{s}([x′]). Thus, ψ̂([x′]) ∈ Traces(A) for all finite [x′] ∈ D′. By continuity, ψ̂(D′) ⊆ Traces(A).

To show (2), it suffices to show that if [x] = ϕ̂([x′]) then [xe] ∈ Traces(A) for each e ∈ ϕ({e′}). Given [x′], obtain an initial computation sequence γ′ of TrAu(E′, D′) with cod(γ′) = [x′], and a transition t′ : [x′]⟶^{e′}[x′e′] of TrAu(E′, D′). Using the fact that ψ is a morphism of automata, we may construct an initial computation sequence γ of A, with tr(γ) = [x] and cod(γ) = ψ_{s}([x′]). Now, e′ is enabled in state [x′] of A′, so each element e of ϕ({e′}) is enabled in state cod(γ) = ψ_{s}([x′]) of A. It follows that [xe] ∈ Traces(A) for each e ∈ ϕ({e′}).

Theorem 7 The forgetful functor TrEv : TrDom → EvDom has a left adjoint EvTr, such that TrEv ∘ EvTr ≃ 1.

Proof – We first define a mapping from event domains to trace domains. Given an event domain D, define the events of D to be the ≡-classes of prime intervals of D. Let E_{D} be the set of all events of D. Say that events e, e′ ∈ E_{D} commute, and write e∥e′, when e ≠ e′ and there exist representatives I ∈ e and I′ ∈ e′, such that I and I′ are consistent. (By the properties of event domains, this implies that whenever I ∈ e and I′ ∈ e′ are coinitial, then they are consistent.) Then E_{D}, equipped with the relation ∥, is a concurrent alphabet. Let A be the automaton (E_{D}, Q, ⊥, T), where Q is the set of finite elements of D and T contains all transitions q⟶^{ϵ}q and all transitions q⟶^{[I]}r such that I = (q, r) is a prime interval of D. Let U_{D} = Traces(A) ⊆ Ê_{D}. It follows from Theorem 6 that (E_{D}, U_{D}) is a trace domain.

Next, we claim that D and U_{D} are isomorphic. To see this, note that the finite initial computation sequences γ of A are in bijective correspondence with the securing chains for finite elements d of D. Moreover, by definition of the commutativity relation ∥ on E_{D}, any two securing chains for the same element d correspond to computation sequences having the same trace [x] ∈ Ê_{D}. Thus the mapping that takes d to the trace [x] determined by a securing chain for d is a bijection between the finite elements of D and the finite elements of U_{D} = Traces(A). It can be shown that this mapping is monotone, hence by continuous extension we obtain an isomorphism μ_{D} : D → U_{D}.

Finally, we show that the forgetful functor TrEv has a left adjoint whose object map takes D to (E_{D}, U_{D}). Given D, let the “inclusion of generators” be the isomorphism μ_{D} : D → U_{D} constructed above. We claim that μ_{D} is universal from D to TrEv. Suppose (E′, D′) ∈ TrDom and ϕ : D → D′ in EvDom are given. Note that each prime interval I of D determines a ⊔-prime interval ϕ(I) of D′, which in turn determines a set V_{I} ∈ Com(E′). If I and J are distinct consistent intervals, then ϕ(I) and ϕ(J) are orthogonal by the properties of the EvDom-morphism ϕ, hence V_{I} ∩ V_{J} = ∅. Then an induction using the definition of ≡ shows that if I ≡ I′, then ϕ(I) ≡ ϕ(I′), hence V_{I} = V_{I′}. Thus, the map taking each equivalence class [I] to the corresponding V_{I} determines an Alph-morphism ρ : E_{D} → E′.

Now, an induction on the length of securing chains in U_{D} shows that ρ̂([x]) = ϕ(μ_{D}^{−1}([x])) for all finite [x] ∈ U_{D}, so ρ̂(μ_{D}(d)) = ϕ(d) ∈ D′ for all finite d ∈ D, hence for all d ∈ D by continuity. Also, if I = ([x], [xe]) is a prime interval of U_{D}, then e = [(d, d′)], where d = μ_{D}^{−1}([x]) and d′ = μ_{D}^{−1}([xe]). Since then ρ̂(I) = (ϕ(d), ϕ(d′)), which is a ⊔-prime interval of D′, it follows that ρ̂ maps prime intervals of U_{D} to ⊔-prime intervals of D′. Thus, we have shown that ρ : (E_{D}, U_{D}) → (E′, D′) is a TrDom-morphism, and TrEv(ρ) ∘ μ_{D} = ϕ.

Finally, we note that any TrDom-morphism ρ : (E_{D}, U_{D}) → (E′, D′) satisfying TrEv(ρ)∘ μ_{D} = ϕ must satisfy ρ̂([xe]) = ϕ(μ_{D}^{−1}([xe])) for all finite prime intervals I = ([x], [xe]) ∈ U_{D}. Let d = μ_{D}^{−1}([x]) and d′ = μ_{D}^{−1}([xe]), then since ρ̂([xe]) = ρ̂([x])ρ̂(e) = ϕ(d)ρ̂(e) and ϕ(d′) = ϕ(d)[e′_{1} … e′_{n}] for some {e′_{1},…, e′_{n}} ∈ Com(E′), it must be the case that ρ̂(e) = [e′_{1} … e′_{n}] and ρ({e}) = {e′_{1},…, e′_{n}}. Since every e ∈ E_{D} is [(d, d′)] for some prime interval (d, d′) ∈ D, for each e ∈ E_{D} we can find a corresponding prime interval ([x], [xe]) in U_{D} by taking [x] = μ_{D}(d) and [xe] = μ_{D}(d′). It follows that the condition TrEv(ρ) ∘ μ_{D} = ϕ uniquely determines ρ.

References

[1] I. J. Aalbersberg and G. Rozenberg. Theory of traces. Theoretical Computer Science, 60(1):1–82, 1988.

[2] M. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, October 1987.

[3] J. D. Brock. A Formal Model of Non-Determinate Dataflow Computation. PhD thesis, Massachusetts Institute of Technology, 1983. Available as MIT/LCS/TR-309.

[4] J. D. Brock and W. B. Ackerman. Scenarios: a model of non-determinate computation. In Formalization of Programming Concepts, pages 252–259, Springer-Verlag. Volume 107 of Lecture Notes in Computer Science, 1981.

[5] M. Broy. Nondeterministic data-flow programs: how to avoid the merge anomaly. Science of Computer Programming, 10:65–85, 1988.

[6] P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Research Notes in Theoretical Computer Science, Pitman, London, 1986.

[7] A. A. Faustini. An operational semantics for pure dataflow. In Automata, Languages, and Programming, 9th Colloquium, pages 212–224, Springer-Verlag. Volume 140 of Lecture Notes in Computer Science, 1982.

[8] H. Herrlich and G. E. Strecker. Category Theory. Sigma Series in Pure Mathematics, Heldermann Verlag, 1979.

[9] G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information Processing 74, pages 471–475, North-Holland, 1974.

[10] G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Information Processing 77, pages 993–998, North-Holland, 1977.

[11] S. Mac Lane. Categories for the Working Mathematician. Volume 5 of Graduate Texts in Mathematics, Springer Verlag, 1971.

[12] A. Mazurkiewicz. Trace theory. In Advanced Course on Petri Nets, GMD, Bad Honnef, September 1986.

[13] P. Panangaden and E. W. Stark. Computations, residuals, and the power of indeterminacy. In Automata, Languages, and Programming, pages 439–454, Springer-Verlag. Volume 317 of Lecture Notes in Computer Science, 1988.

[14] G. D. Plotkin. Domains: lecture notes. 1979. (unpublished manuscript).

[15] D. A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986.

[16] E. W. Stark. Concurrent transition system semantics of process networks. In Fourteenth ACM Symposium on Principles of Programming Languages, pages 199–210, January 1987.

[17] E. W. Stark. Concurrent transition systems. Theoretical Computer Science, 1989. (to appear).

[18] E. W. Stark. Connections between a concrete and abstract model of concurrent systems. In Fifth Conference on the Mathematical Foundations of Programming Semantics, Springer-Verlag. Lecture Notes in Computer Science, New Orleans, LA, 1989 (to appear).

[19] E. W. Stark. On the Relations Computed by a Class of Concurrent Automata. Technical Report 88-09, SUNY at Stony Brook Computer Science Dept., 1988.

[20] G. Winskel. Events in Computation. PhD thesis, University of Edinburgh, 1980.