A Simple Generalization of Kahn’s Principle to Indeterminate Dataflow Networks

Eugene W. Stark^{∗}

Department of Computer Science

State University of New York at Stony Brook

Stony Brook, NY 11794 USA

July 31, 1990

Abstract

Kahn’s principle states that if each process in a dataflow network computes a continuous input/output function, then so does the entire network. Moreover, in that case the function computed by the network is the least fixed point of a continuous functional determined by the structure of the network and the functions computed by the individual processes. Previous attempts to generalize this principle in a straightforward way to “indeterminate” networks, in which processes need not compute functions, have been either too complex or have failed to give results consistent with operational semantics. In this paper, we give a simple, direct generalization of Kahn’s fixed-point principle to a large class of indeterminate dataflow networks, and we prove that results obtained by the generalized principle are in agreement with a natural operational semantics.

1 Introduction

Dataflow networks are a parallel programming paradigm in which a collection of concurrently and asynchronously executing sequential processes communicate by transmitting sequences or “streams” of “tokens” containing data values over unidirectional FIFO communication channels. Kahn [14, 15] envisioned a simple programming language built on this paradigm, in which the communication primitives available to processes are sufficiently restrictive that only functional processes can be programmed. That is, each process may be viewed as computing a function from the complete history of values received on its input channels to the complete history of values emitted on its output channels. Kahn argued that such processes compute functions that are in fact continuous with respect to a suitable complete partial order (cpo) structure on the sets of input and output histories. Moreover, a network of such processes also computes a continuous function, which can be characterized as the least fixed point of a continuous functional associated with the network. This elegant idea has been called “the Kahn principle,” and it has been shown [9, 21, 36] to give results in agreement with a natural “token-pushing” operational semantics.

∗Research supported in part by NSF Grants CCR-8702247 and CCR-8902215.

In practical programming applications of the dataflow idea, the restriction to functional processes is somewhat limiting, because there are useful programs one wants to write that do not describe processes with functional input/output behavior. An example of a class of such processes are the merge processes, which shuffle together values arriving on two input channels onto a single output channel. A variety of such processes can be defined, corresponding to various conditions under which arriving inputs are guaranteed to be eventually transmitted to the output [24, 39]. They do not have functional behaviors, because in general there are many possible output interleavings for a single pair of input sequences. We use the term indeterminate to refer to dataflow networks in which processes need not have functional behaviors.

There have been many attempts to generalize Kahn’s theory to a class of indeterminate networks. The obvious idea of generalizing functions to relations fails to give results consistent with token-pushing semantics. This fact was first noticed by Keller [16], and subsequently became known as the “Brock/Ackerman anomaly,” after Brock and Ackerman [7] demonstrated convincingly by some clever examples that no denotational semantics based on set-theoretic input/output relations can give results consistent with token-pushing semantics. Subsequently, a rather large literature has developed on this subject. A variety of sophisticated approaches, such as powerdomains [1, 8], categories [3], “scenarios” [6, 7], sets of “linear traces” [4, 11, 12, 17, 23], “pomsets” [10, 26, 27], multilinear algebra [22], and other ideas [18, 19, 25, 28, 29, 30, 34, 37, 35] have been tried, but up until now none of these approaches has resulted in a truly simple and natural generalization of Kahn’s principle that also maintains a clear connection with operational semantics.

In the remainder of this paper, we present a very simple and straightforward generalization of Kahn’s principle, and prove that it gives results in agreement with operational semantics.

2 Kahn’s Fixed-Point Principle

To give a precise statement of the Kahn principle, we must first formalize the notion of the input/output relation of a dataflow network. We begin by postulating a countably infinite set V, whose elements represent the possible data values that can be communicated between processes. Let V^{∞} be the set of all finite and infinite sequences of elements of V, partially ordered by the prefix relation ⊑. We use ϵ to denote the empty sequence, which is the least element of V^{∞}. If X is a finite or countably infinite set (of channels), then an X-history is a function from X to V^{∞}. We think of such a function as representing the complete history of values communicated on the channels in X during some computation of a dataflow network. Let HX denote the set of all X-histories, then HX is also partially ordered, with x ⊑ x′ iff x(c) ⊑ x′(c) for all c ∈ X. The poset HX has the structure of a Scott domain (an ωalgebraic, consistently complete cpo [32]). The least element ⊥ is the identically ϵ function. The finite elements (or compact elements, or isolated elements) of HX are exactly those histories x with x(c) finite for all channels c ∈ X, and with x(c) = ϵ for all but finitely many c ∈ X. It is also important for us that HX is finitary, which means that each finite element can have at most a finite set of elements below it.

Functions on channel sets induce corresponding functions on channel histories. Formally, if X and Y are sets of channels, then a function ϕ : Y → X induces a function Hϕ : HX → HY satisfying Hϕ(x)(c) = x(ϕ(c)) for all c ∈ Y. The function Hϕ is obviously continuous; in fact the mapping H is a contravariant functor from the category of at most countable sets and functions to the category of Scott domains and continuous maps. Moreover, this functor maps the empty set to the one-point domain, and maps coproducts of sets (disjoint union) to products of domains; that is, we have a natural isomorphism H(X + Y) ≃ HX × HY.

In Section 5, we shall continue with this formal development, defining an operational model for dataflow networks in which both a network and its constituent processes are represented as a certain kind of automata having fixed sets of input and output channels. Computation of a dataflow network may be regarded as a token-pushing game played on a graph whose nodes are automata, and whose arcs indicate when an output channel c of one automaton A is connected to an input channel d of another automaton B (we admit the possibility that A = B). As execution progresses, the automata change state and tokens containing data values move around on the graph. Communication between automata occurs when a token containing a data value is simultaneously output on channel c by process A and input on channel d by process B. This synchronized communication model looks at first glance to be different from the usual formulations of operational semantics for dataflow networks, in which communication channels are regarded as FIFO buffers distinct from processes. Instead of following the usual approach, we find it more convenient and economical to imagine each process as having, for each of its input channels, a component of its internal state that serves as an input buffer for that channel. We do not actually impose any direct structural requirements on the states of an automaton, but instead merely axiomatize the essential properties of the transition relation that are consequences of this structure. Among other things, the axioms imply that an automaton is always prepared to accept arbitrary input on an input channel (the buffer is never full), and the production of output in a step can depend only on input received in a previous step. In this way, we obtain the effect of a buffered communication model without the notational inconvenience.

Once a formal definition of “token-pushing semantics” has been given, it becomes possible to define the input/output relation of a network. In particular, the input/output relation of a network with input channels X and output channels Y is a subset of HX × HY, whose elements are pairs ⟨x, y⟩ representing the history of input and output that could occur in one particular network computation. We are not interested in including in the input/output relation pairs ⟨x, y⟩ corresponding to all possible computations, but rather only in those pairs obtained from completed computations. Intuitively, a computation of a network is completed if each component process that is capable of performing some non-input step eventually does so. We need this condition to rule out uninteresting computations in which a process fails to

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

Figure 1: An Open-Loop Network and one with Feedback

process data in its input buffer simply because that process is never scheduled to execute a step. Having defined the input/output relation of a network, we may then classify networks as determinate or indeterminate according to whether or not their input/output relations are functional (i.e. are graphs of functions from HX to HY) or nonfunctional. In [21] it is shown that, for a formal operational model of dataflow networks defined along these lines, if the input/output relation of a network is functional, then in fact it is the graph of a continuous function from HX to HY.

Kahn’s principle concerns determinate networks. In its simplest form, the principle gives a relationship between the function computed by a determinate network with a feedback loop and the corresponding “open-loop” network. The principle may be stated as follows:

The Kahn Principle

Suppose a network computes the continuous function f : HX × HZ → HY. Let ϕ : Z → Y be an injective function, which we regard as designating, for each channel in Z, a corresponding channel in Y to which it is to be connected in a feedback loop (see Figure 1). Define the feedback functional

Φ : [HX → HY] → [HX → HY]

by

Φ(g)(x) = f(x, Hϕ(g(x))).

Then Φ is continuous, and the function computed by the closed-loop network is the least fixed-point μΦ of Φ.

3 A Generalization of Kahn’s Principle

To motivate the generalized version of Kahn’s principle, we reconsider the original version stated above, with a few changes in notation. First of all, instead of representing the behavior of a network with input channels X and output channels Y by a continuous function f :

HX → HY, let us use instead the function p : HX → [HY → HY] defined by p(x)(y) = f(x) ⊓ y. Here f(x) ⊓ y denotes the greatest lower bound of f(x) and y, which always exists due to the fact that HY is a consistently complete cpo, and is continuous because HX and HY are algebraic. Observe that no information is lost in replacing f by p, because f(x) = ⨆{y : y = p(x)(y)}. Note also that for each x ∈ X the function p(x) : HY → HY has the following properties:

1. p(x) ∘ p(x) = p(x).

2. p(x) ⊑ id_{HY}.

That is, p(x) is a projection on the domain HY [13]. In the sequel, we use P(D) to denote the set of all projections on the finitary domain D. It can be shown that P(D), partially ordered by ⊑, is a domain; in fact it is a complete lattice.

Now, let us redefine the feedback functional to be compatible with the new notation. If p : HX × HZ → P(HY) represents the open-loop behavior of a network, and ϕ : Z → Y is an injective function, then the corresponding feedback functional

Ψ : [HX → [HY → HY]] → [HX → [HY → HY]]

is defined by

Ψqxy = p⟨x, Hϕ(qxy)⟩y.

Here, and in the rest of the paper, we omit unnecessary parentheses under the convention that application associates to the left, and we use angle brackets to indicate tupling of arguments. It is immediate from the above definition that Ψ is continuous. Moreover, the least fixed point μΨ of Ψ determines the least fixed point μΦ of Φ in the same way as p determines f.

Lemma 3.1 μΦx = ⨆{y : y = μΨxy}.

Proof – Recall that the fundamental fixed-point theorem (see, e.g. [32]) in the theory of complete partial orders states that if a functional Γ : D → D is continuous, then μΓ = ⨆_{i} Γ^{i}0, where 0 denotes the least element of D, and the iterates Γ^{i} of Γ are defined inductively by: Γ^{0} = id, Γ^{i+1} = Γ ∘ Γ^{i}.

Let y = μΦx = ⨆_{i} Φ^{i}0x. We first claim that Φ^{i}0x ⊑ Ψ^{i}0xy for all i ≥ 0. This is established by induction on i. The basis case is immediate. For the induction step, observe:

Φ^{i+1}0x = Φ^{i+1}0x ⊓ y
= f⟨x, Hϕ(Φ^{i}0x)⟩ ⊓ y
= p⟨x, Hϕ(Φ^{i}0x)⟩y
⊑ p⟨x, Hϕ(Ψ^{i}0xy)⟩y
= Ψ^{i+1}0xy,

where the induction hypothesis was used to obtain the inequality. This completes the induction. Since Φ^{i}0x ⊑ Ψ^{i}0xy for all i ≥ 0, and since Ψ^{i}0xy ⊑ y = μΦx for all i, it follows that μΦx = μΨx(μΦx).

To complete the proof, we now show that if y is any element of HY with y = μΨxy, then y ⊑ μΦx. By induction on i we first show that Ψ^{i}0xy ⊑ Φ^{i}0x for all x, y and all i ≥ 0. The basis case is obvious. For the induction step, observe:

Ψ^{i+1}0xy = p⟨x, Hϕ(Ψ^{i}0xy)⟩y
= f⟨x, Hϕ(Ψ^{i}0xy)⟩ ⊓ y
⊑ f⟨x, Hϕ(Ψ^{i}0xy)⟩
⊑ f⟨x, Hϕ(Φ^{i}0x)⟩
= Φ^{i+1}0xy,

completing the induction. Now, if y = μΨxy, then y = ⨆_{i} Ψ^{i}0xy ⊑ ⨆_{i} Φ^{i}0x = μΦx.

We thus see that Kahn’s principle generalizes in a straightforward way to the new representation of network behaviors. However, the new representation has an important advantage over the old one: it is general enough to permit the specification of some nonfunctional behaviors. We observed above that if f : HX → HY is continuous, and p : HX → P(HY) is defined by pxy = fx⊓y, then fx = ⨆{y : y = pxy}; that is to say, fx is the maximal fixed point of the projection px ∈ P(HY). Instead of just considering functions p : HX → P(HY) of the form fx⊓y, we may consider the whole class of continuous functions p : HX → P(HY). For an arbitrary such function p, the set of fixed points of px need not be directed, hence it may contain many maximal elements. Given x ∈ HX, we regard each maximal fixed point y of px as a possible output on input x, and in this way we may think of the function p as describing an indeterminate network whose input/output relation is the set of all ⟨x, y⟩ such that y is a maximal fixed point of px.

As a simple example of an indeterminate behavior, consider a network with no input channels (X = ∅, hence HX ≃ {⊥}) and one output channel (Y = {∗}, hence HY ≃ V^{∞}), which simply emits an arbitrary infinite sequence of values on its output channel. Such a network is described by the function p : HX → P(HY) satisfying pxy = y. It is clear that any maximal element y of HY is a maximal fixed point of p⊥, hence determines a pair ⟨⊥, y⟩ in the input/output relation of the network. This kind of “oracle” network can be used in the construction of a variety of other indeterminate behaviors. For example, it can be shown that a network that implements a kind of merging operation called infinity-fair merge [24, 39] can be constructed using functional components and an oracle that outputs an infinite sequence of natural numbers.

Although the generalizations we have made so far permit us to describe some indeterminate networks, the class of networks that can be represented as functions p : HX → P(HY) is not yet large enough to admit “hiding” operations (see Section 5.6), by which some output channels of a network are made invisible to its environment. However, we can describe a larger and more interesting class of networks, which does admit hiding, by making one further generalization. The additional generalization is to replace the single map p : HX → P(HY) by two maps: p : HX → P(D) and l : D → HY, where D is an arbitrary finitary domain. We therefore arrive at the following general definition of an indeterminate behavior:

An (X, Y)-behavior is a triple (D, p, l), where D is a finitary domain, and p :

HX → P(D) and l : D → HY are continuous functions.

The input/output relation corresponding to an (X, Y)-behavior (D, p, l) is the set of all ⟨x, ld⟩ ∈ HX × HY such that d is a maximal fixed point of the projection px.

As an example of the kind of indeterminate networks that can be described as behaviors (D, p, l), we consider angelic merge. A network that performs angelic merge has two input channels (X = {a, b}) and one output channel (Y = {c}), and operates by merging together the sequences of data values on its two input channels into a single output sequence. It is required to satisfy the following liveness condition: In any completed computation, if only a finite number of values arrive on one of the inputs, then eventually all the values from the other input will be transmitted to the output.

To describe angelic merge as an (X, Y)-behavior, we first define σ : {a, b}^{∞} ×HY → HX to be the continuous function that on argument ⟨w, y⟩, splits the sequence of values y into two result sequences, where the ith value in y goes to the result sequence for channel a, if a is the ith value in the sequence w, otherwise to the result sequence for channel b. Angelic merge may then be defined to be the behavior ({a, b}^{∞} × HY, p, l), where

• l : {a, b}^{∞} × HY → HY is defined by l⟨w, y⟩ = y.

• p : HX → P({a, b}^{∞} × HY) satisfies the following condition: for each x ∈ HX, w ∈ {a, b}^{∞}, and y ∈ HY, px⟨w, y⟩ is the greatest ⟨w′, y′⟩ ⊑ ⟨w, y⟩ such that σ⟨w′, y′⟩ ⊑ x.

Many interesting indeterminate networks can be constructed using angelic merge and functional components. However, it should be pointed out that there is yet a more powerful kind of merging operation that cannot be described as a behavior (D, p, l). This is the fair merge, which shuffles two input sequences together onto a single output sequence in such a way that every value in both input channels eventually appears in the output channel. The results of this paper do not apply to indeterminate networks having this powerful merging capability.

We now state our generalized version of Kahn’s principle.

The Generalized Kahn Principle

Suppose (D, p, l) is an (X ×Z, Y)-behavior that corresponds to the open-loop network shown in Figure 1. Let ϕ : Z → Y be an injective function that assigns to each input channel in Z a corresponding output channel in Y. Define the feedback functional corresponding to (D, p, l) and ϕ to be the map:

Φ : [HX → [D → D]] → [HX → [D → D]]

defined by:

Φqxd = p⟨x, Hϕ(l(qxd))⟩d.

Then Φ is continuous, and (D, μΦ, l) is the behavior corresponding to the closedloop network.

In the remainder of the paper, we justify this principle by showing that it gives results in agreement with token-pushing semantics.

4 Resolution of the Anomalies

In this section, we briefly examine the way in which Keller/Brock/Ackerman-type “anomalies” are avoided by our semantics for networks. We consider a particularly simple example of such an anomaly, due to J. Russell [31]. Suppose P is a process, having one input channel and one output channel, that obeys the following intuitive algorithm: Nondeterministically choose either: (1) read an input value, then output 0 followed by 1, or (2) output 0, read an input value, then output 0. Let Q be a similar process that has the additional possibility:

(3) output 0, read an input value, then output 1. The input/output relation of P consists of all pairs of histories of the form ⟨⊥, 0⟩, ⟨vx, 01⟩, or ⟨vx, 00⟩, where v is an arbitrary value in V, and x an arbitrary sequence of elements of V. The input/output relation of Q is identical to that of P.

Even though P and Q have identical input/output relations, a difference between the two processes can be detected by placing them in a feedback loop. If P_{ϕ} denotes the network consisting of P with its output fed back to its input, and similarly for Q_{ϕ} , then under token-pushing semantics the set of possible outputs of P_{ϕ} is {⊥, 00}, whereas the set of possible outputs of Q_{ϕ} is {⊥, 00, 01}. This demonstrates that no semantics for indeterminate networks, in which processes and networks are represented by their input/output relations, can support a definition of the feedback operation that gives results in agreement with token-pushing semantics.

Let us now see how the difficulty is resolved using our definition of behavior. Let X = {a} and Y = {b}, and let {1, 2}_{⊥} denote the flat domain generated by {1, 2}. Then the process P can be represented as the (X, Y)-behavior ({1, 2}_{⊥} × HY, p, l), where l⟨w, y⟩ = y and

p : HX → [{1, 2}_{⊥} × HY → {1, 2}_{⊥} × HY]

is defined as follows:

px⟨⊥, y⟩ = ⟨⊥, ⊥⟩
px⟨1, y⟩ = \{ \begin{matrix}⟨1, ⊥⟩, & if x = ⊥ \\ ⟨1, 01 ⊓ y⟩, & otherwise. \end{matrix}
px⟨2, y⟩ = \{ \begin{matrix}⟨2, 0 ⊓ y⟩, & if x = ⊥ \\ ⟨2, 00 ⊓ y⟩, & otherwise. \end{matrix}

Similarly, the process Q can be represented by the (X, Y)-behavior ({1, 2, 3}_{⊥} × HY, q, l), where

q : HX → [{1, 2, 3}_{⊥} × HY → {1, 2, 3}_{⊥} × HY]

is defined by:

qx⟨⊥, y⟩ = ⟨⊥, ⊥⟩

qx⟨1, y⟩ = px⟨1, y⟩
qx⟨2, y⟩ = px⟨2, y⟩
qx⟨3, y⟩ = \{ \begin{matrix}⟨3, 0 ⊓ y⟩, & if x = ⊥ \\ ⟨3, 01 ⊓ y⟩, & otherwise. \end{matrix}

Let ϕ : X → Y be the map taking a to b. Applying the generalized Kahn principle, the behavior of P_{ϕ} is the (∅, Y)-behavior ({1, 2}_{⊥} × HY, p_{ϕ} , l), where

p_{ϕ} : {⊥} → [{1, 2}_{⊥} × HY → {1, 2}_{⊥} × HY]

is defined by:

p⊥⟨w, y⟩ = \{ \begin{matrix}⟨⊥, ⊥⟩, & if w = ⊥ \\ ⟨1, ⊥⟩, & if w = 1 \\ ⟨2, 00 ⊓ y⟩, & if w = 2. \end{matrix}

The maximal fixed points of p_{ϕ} are {⟨1, ⊥⟩, ⟨2, 00⟩}, hence the input/output relation of P_{ϕ} is {⟨⊥, ⊥⟩, ⟨⊥, 00⟩}.

The behavior of Q_{ϕ} is the (∅, Y)-behavior ({1, 2, 3}_{⊥} × HY, q_{ϕ} , l), where

q_{ϕ} : {⊥} → [{1, 2, 3}_{⊥} × HY → {1, 2, 3}_{⊥} × HY]

is defined by:

q⊥⟨w, y⟩ = \{ \begin{matrix}⟨⊥, ⊥⟩, & if w = ⊥ \\ ⟨1, ⊥⟩, & if w = 1 \\ ⟨2, 00 ⊓ y⟩, & if w = 2 \\ ⟨3, 01 ⊓ y⟩, & if w = 3. \end{matrix}

The maximal fixed points of q_{ϕ} are {⟨1, ⊥⟩, ⟨2, 00⟩, ⟨3, 01⟩}, hence the input/output relation of Q_{ϕ} is {⟨⊥, ⊥⟩, ⟨⊥, 00⟩, ⟨⊥, 01⟩}.

Evidently, the input/output relations of P_{ϕ} and Q_{ϕ} , obtained by the generalized Kahn principle, are in agreement with token-pushing semantics.

5 Operational Semantics

In this section, we define an operational semantics for indeterminate dataflow networks. In this semantics a network is represented as a certain kind of automaton, called a monotone automaton [24, 39]. The construction of larger networks from component automata is modeled by certain operations on automata. In fact, assuming the existence of sufficiently many “basic” determinate automata (in particular, the existence of an automaton that computes function Hϕ : HX → HY for each function ϕ : Y → X), then any finite network can be constructed using basic automata and just three network-building operations: parallel composition, hiding, and feedback. Parallel composition corresponds to simply placing two

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

Figure 2: Parallel Composition

automata side-by-side in a network, without any communication (see Figure 2). Hiding makes some of the output channels of an automaton into “internal” channels, which are not available for external communication. Feedback is the operation depicted in Figure 1. Hiding and parallel composition pose no particular semantic difficulties in the framework we have set up here, and we shall discuss them here only briefly.

5.1 Monotone Automata

A monotone automaton (henceforth simply “automaton”) is a tuple

A = (X, W, Y, Q, i, T)

where

• X, W, and Y are pairwise disjoint sets of channels, which we assume are at most countable. The elements of X, Y, and W are called input channels, output channels, and internal channels, respectively. Let E = (X + Y + W) × V, then the elements of E are called actions of A. If e = ⟨c, v⟩ is an action of A, then we write chan(e) for the channel component c and val(e) for the value component v, of e. An action e is an input action or a non-input action, according to whether chan(e) ∈ X or chan(e) ∉ X.

• Q is a set of states, and i ∈ Q is a distinguished initial state.

• T : Q × E → Q is a partial transition function.

These data are required to satisfy the following conditions:

(Commutativity) For all states q and actions e, e′, if chan(e) ≠ chan(e′), r = T (q, e), and r′ = T (q, e′), then there exists a state s such that s = T (r′, e) = T (r, e′).

(Receptivity) For all states q and input actions e, there exists a state r such that r = T (q, e).

These automata are closely related to the input/output automata defined by Lynch and Tuttle [21], and also to the automata that have been studied by Bednarczyk [5], Kwiatkowska [20], and Shields [33].

A transition of A is a triple q⟶^{e}r, where r = T (q, e). We write t : q⟶^{e}r, or just q⟶^{e}r, to assert the existence of a transition t = q⟶^{e}r of A. Intuitively, a transition q⟶^{e}r represents a potential computation step of A in which action e occurs and the state changes from q to r. We say that action e ∈ E is enabled in state q if there exists a transition q⟶^{e}r in T. 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.

The receptivity condition in the definition of an automaton can be viewed as an abstract statement of the unboundedness of the buffers associated with input channels. The commutativity property can be thought of as saying that actions for different ports are concurrent, hence affect different components of the state. Together, the commutativity and receptivity imply the following monotonicity property: If non-input action e is enabled in state q, and e′ is an arbitrary input action with r = T (q, e′), then e is enabled in state r as well. One can think of this condition as saying that it is possible to test for the presence of inputs in an input buffer, but not for their absence.

As an example of how we can model a dataflow process as an automaton, consider the case of the angelic merge process aleady discussed. Recall that X = {a, b} and Y = {c}. Let W = {d}. We then represent the merge process as an automaton

A = ({a, b}, {d}, {c}, V^{∗} × V^{∗} × V^{∗}, ⟨ϵ, ϵ, ϵ⟩, T),

where 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 = ⟨a, v⟩, x′_{1} = x_{1}v, x′_{2} = x_{2}, and y′ = y.

2. e = ⟨b, v⟩, x′_{1} = x_{1}, x′_{2} = x_{2}v, and y′ = y.

3. e = ⟨d, 1⟩, vx′_{1} = x_{1}, x′_{2} = x_{2}, and y′ = yv.

4. e = ⟨d, 2⟩, x′_{1} = x_{1}, vx′_{2} = x_{2}, and y′ = yv.

5. e = ⟨c, v⟩, x′_{1} = x_{1}, x′_{2} = x_{2}, and vy′ = y.

It is straightforward to check that A satisfies the conditions for an automaton. In cases (3) and (4), the actions ⟨d, 1⟩ and ⟨d, 2⟩ are in E by our assumption that V contains all the natural numbers. (It is actually not important that the numbers 1 and 2 be used here; they could be replaced by any two distinct elements of V.)

Intuitively, the state of A contains two “input buffers” and one “output buffer.” Transitions of type (1) and (2) correspond to arriving input values being placed at the end of the appropriate input buffer. Transitions of type (3) and (4) 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 (5) correspond to the transmission of output from the output buffer. Similar constructions can be used to model many other kinds of dataflow processes.

5.2 Computations of Automata

Suppose A = (X, W, Y, Q, i, T) is an automaton. A finite computation sequence for A is a finite sequence γ of transitions of A of the form:

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

An infinite computation sequence is an infinite sequence of transitions:

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

The state q_{0} is called the domain dom(γ) of γ. If γ is finite, then the state q_{n} is called the codomain cod(γ) of γ, and the number n is called the length |γ| of γ. We call the computation sequence of length 0 from state q the identity computation sequence. A computation sequence γ is initial if dom(γ) is the distinguished initial state i. Finite computation sequences γ and δ are called composable if dom(δ) = cod(γ) and in that case we define their composition γδ to be the computation sequence obtained by concatenating them in the obvious way.

Each computation sequence γ of A determines a corresponding channel history H(γ) ∈ H(X + W + Y), where for each channel c ∈ X + W + Y, the sequence H(γ)(c) is the subsequence of all val(e_{i}) for those actions e_{i} with chan(e_{i}) = c. In view of the natural isomorphism H(X + W + Y) ≃ HX × HW × HY, we may think of the history H(γ) of a computation sequence γ as a triple ⟨x, w, y⟩ ∈ HX × HW × HY, and it will generally be convenient to do so. Let H(A) ⊆ HX × HW × HY denote the set of all histories of initial computation sequences γ of A.

Lemma 5.1 Suppose A = (X, W, Y, Q, i, T) is an automaton. Then

1. ⟨⊥, ⊥, ⊥⟩ ∈ H(A).

2. If ⟨x, w, y⟩ ∈ HX × HW × HY is finite, ⟨x, w, y⟩ ∈ H(A), and x′ is a finite element of HX with x ⊑ x′, then ⟨x′, w, y⟩ ∈ H(A).

Proof – (1) The identity initial computation sequence has history ⟨⊥, ⊥, ⊥⟩.

(2) Given a finite ⟨x, w, y⟩ ∈ HX ×HW ×HY such that ⟨x, w, y⟩ ∈ H(A), we may obtain a finite initial computation sequence γ whose history is ⟨x, w, y⟩. Given a finite x′ ∈ HX with x ⊑ x′, we may then use the receptivity property of A to construct a finite pure-input extension γ′ of γ, such that γ′ has ⟨x′, w, y⟩ as its history.

To state properly the next results, we need some concepts from domain theory. If D is a domain, then a subdomain of D is a subset U of D, which is a domain under the restriction of the ordering on D, such that the inclusion of U in D is continuous. A subdomain U is normal if for all d ∈ D, the set {u ∈ U : u ⊑ d} is directed. The following easily proved characterization of normal subdomains will be convenient:

Proposition 5.2 Suppose U is a subdomain of a domain D. Then U is normal iff the following conditions hold:

1. ⊥ ∈ U.

2. If u, u′ ∈ U are consistent (i.e. have an upper bound) in D, then u ⊔ u′ ∈ U.

Suppose U is a subdomain of D, and let m : U → D be the inclusion map. If U is a normal subdomain of D, then we may define a map e : D → U by: ed = ⨆{u ∈ U : u ⊑ d}. It is then easy to see that e ∘ m = id_{U} and m ∘ e ⊑ id_{D}. Then (m ∘ e) ∘ (m ∘ e) = m ∘ (e ∘ m) ∘ e = m ∘ e, so the map m ∘ e : D → D is a projection, and U = {d ∈ D : d = m(ed)}. Thus, normal subdomains determine projections. Conversely, if p : D → D is a projection on a finitary domain D, then U = p(D) = {d ∈ D : d = pd} is a normal subdomain of D. Hence there is a correspondence between projections on D and normal subdomains of D. In fact, the following is easily shown:

Proposition 5.3 For any finitary^{1} domain D, the set of all normal subdomains of D, partially ordered by inclusion, is a complete lattice that is isomorphic to the set of projections on D, partially ordered by ⊑. Moreover, if {D_{i} : i ∈ I} is a collection of normal subdomains of D which is directed under inclusion order, then its supremum in the lattice of normal subdomains is given by:

(⋃{D_{i} : i ∈ I})^{c},

where ( )^{c} denotes closure under directed suprema.

Lemma 5.4 Suppose U is a normal subdomain of a finitary domain D. Let U^{o} denote the set of elements of U that are finite in D. Then U = (U^{o})^{c}.

Proof – Since D is algebraic, and U ⊆ D, every u ∈ U is the supremum of the set of finite elements d ∈ D with d ⊑ u. Let p denote the projection on D corresponding to the normal subdomain U, then by the continuity of p it follows that u is also the supremum of the set of all pd such that d ∈ D is finite and d ⊑ u. But if d ∈ D is finite in D, then so is pd, because projections are decreasing and in a finitary domain no infinite element can be below a finite element. Since U ⊆ D, an element of u is finite in U if it is finite in D. It follows that u is the supremum of the directed subset {pd : d ∈ D, d ⊑ u, d finite} of U^{o}.

An interval in a domain D is a pair [d, d′] of elements of D such that d ⊑ d′. An interval [d, d′] is prime if there exists no d′′ ∈ D such that d d′′ ⊑ d′. The result below, proved in [35, 38], gives a great deal of information about the structure of the set H(A).

1The author thanks Carl Gunter for pointing out that for a projection p on an arbitrary domain D, it is not necessarily the case that p(D) is algebraic. However, in case D is finitary, then p(d) is a finite element of p(D) whenever d is a finite element of D, and this is sufficient for algebraicity.

Proposition 5.5 Suppose A = (X, W, Y, Q, i, T) is an automaton. Then the set H(A), partially ordered by ⊑, is a normal subdomain of HX × HW × HY. Moreover, the inclusion of H(A) in HX × HW × HY preserves prime intervals.

To give the proof of this proposition would require a fairly substantial digression to develop the necessary techniques. Instead, we merely comment on the method used. We begin by defining two computation sequences γ and γ′ to be equivalent if dom(γ) = dom(γ′) and H(γ) = H(γ′). We call equivalence classes of computation sequences computations. We then observe that the partial ordering on histories induces a corresponding partial ordering on computations, making the map, taking each computation to the corresponding history, injective and order-preserving. It then remains to show that the partially ordered set of initial computations is a domain, and that the map from computations to histories is an embedding of a normal subdomain that preserves prime intervals. To accomplish this, we introduce the auxiliary notion of the residual of one computation sequence “after” another, and obtain a characterization in terms of residuals of the ordering on computations.

More precisely, suppose γ and γ′ are finite computation sequences, such that dom(γ) = dom(γ′) and such that the histories H(γ) and H(γ′) are consistent. Then there exists a pair of finite computation sequences γ \ γ′ and γ′ \ γ (read “γ after γ′ and γ′ after γ), such that the computation sequences γ(γ′ \ γ) and γ′(γ \ γ′) are equivalent, and such that if δ and δ′ are any finite computation sequences with γδ′ and γ′δ equivalent, then there exists a finite computation sequence ξ, unique up to equivalence, such that (γ \ γ′)ξ is equivalent to δ and (γ′ \ γ)ξ is equivalent to δ′.

Thus \ is a partial binary operation on pairs of computation sequences, where γ \ δ is defined exactly when dom(γ) = dom(δ) and H(γ) and H(δ) are consistent. We then think of γ and δ as potentially being part of the “same concurrent computation,” and the computation sequence γ \ δ as that obtained by “cancelling” from γ the greatest common prefix of γ and δ, up to equivalence. If dom(γ) = dom(δ), but H(γ) and H(δ) are not consistent, then γ \ δ and δ \ γ are undefined. In this case, γ and δ “conflict” in the sense that γ contains some indeterminate choice that is incompatible with a choice made in δ. Observe that we distinguish between two types of choice that may be represented in an automaton: concurrent choice, in which actions e, e′ for distinct channels are both enabled in the same state q, and indeterminate choice, in which actions e and e′ for the same channel are both enabled in state q. A formal definition of γ \ δ is given by induction on the length of γ and δ, and can be found in [35, 38].

A residual operation can also be defined on finite histories. Formally, if x and x′ are consistent histories, then the residual of x after x′ is the unique history x\x′ with the property that x′(x \ x′) = x ⊔ x′. From this definition, one can easily see that x ⊑ x′ iff x \ x′ = ⊥. A similar relation holds for computations: [γ] ⊑ [δ] iff γ \ δ is an identity computation sequence. Thus, the partial ordering on computations has an equivalent characterization in terms of residuals. Proposition 5.5 may then be proved by first using residuals to perform an inductive construction of suprema for directed collections of computations, and also for consistent pairs of computations, and then to show that the map taking each computation to its history preserves residuals (hence is additive and continuous), and reflects consistency.

A map between domains that is strict, additive, continuous, and reflects consistency is an embedding of a normal subdomain.

The same techniques also establish the following result:

Proposition 5.6 Suppose A = (X, W, Y, Q, i, T) is an automaton. Let γ be a finite initial computation sequence of A having history ⟨x, w, y⟩, and suppose ⟨x′, w′, y′⟩ is a finite element of HX × HW × HY with ⟨x, w, y⟩ ⊑ ⟨x′, w′, y′⟩. If ⟨x′, w′, y′⟩ ∈ H(A), then there exists a finite initial computation sequence δ of A with history ⟨x′, w′, y′⟩, such that γ is a prefix of δ.

The proof of Proposition 5.6 is accomplished by letting γ′ be an arbitrary initial computation sequence of A having history ⟨x′, w′, y′⟩, observing that H(γ) and H(γ′) are consistent, hence the residual γ′ \ γ is defined, and then taking δ = γ(γ′ \ γ).

Lemma 5.7 Suppose A = (X, W, Y, Q, i, T) is an automaton. Then the map taking x to the set

U(x) = {⟨w, y⟩ : ⟨x, w, y⟩ ∈ H(A)},

is a continuous function from HX to the lattice of normal subdomains of HW × HY.

Proof – We first use Proposition 5.2 to show that for each x ∈ HX, the set U(x) is a normal subdomain of HW × HY. Note that ⟨⊥, ⊥⟩ ∈ U(x) for all x ∈ HX by Lemma 5.1. Also, if ⟨w, y⟩ ∈ U(x) and ⟨w′, y′⟩ ∈ U(x), where ⟨w, y⟩ and ⟨w′, y′⟩ are consistent, then ⟨x, w, y⟩ ∈ H(A) and ⟨x, w′, y′⟩ ∈ H(A), hence ⟨x, w ⊔ w′, y ⊔ y′⟩ ∈ H(A) and ⟨w ⊔ w′, y ⊔ y′⟩ ∈ U(x) by the normality of H(A). To show that U(x) is a subdomain of HW × HY, we show that if V ⊆ U(x) is directed, then ⨆ V ∈ U(x). Now, if V ⊆ U(x) is directed, then ⟨x, w, y⟩ ∈ H(A) whenever ⟨w, y⟩ ∈ V, hence if ⟨w, y⟩ = ⨆ V, then ⟨x, w, y⟩ ∈ H(A) because H(A) is a subdomain of HX × HW × HY. It follows that ⟨w, y⟩ ∈ U(x).

To prove that the map taking x to U(x) is continuous, we show that for all x ∈ HX,

U(x) = (⋃{U(x′) : x′ ⊑ x, x′ finite})^{c},

where ( )^{c} denotes closure under directed suprema. By Lemma 5.4, it suffices to show that if ⟨w, y⟩ ∈ HW × HY is finite, then ⟨w, y⟩ ∈ U(x) iff ⟨w, y⟩ ∈ U(x′) for some finite x′ ⊑ x. So, suppose ⟨w, y⟩ ∈ HW × HY is finite. If ⟨w, y⟩ ∈ U(x), then ⟨x, w, y⟩ ∈ H(A), hence there exists an initial computation sequence γ of A such that the history of γ is ⟨x, w, y⟩. Moreover, since ⟨w, y⟩ is finite, there must be some finite x′ ∈ HX and some finite prefix γ′ of γ whose history is ⟨x′, w, y⟩. This shows that ⟨w, y⟩ ∈ U(x′) for some finite x′ ⊑ x. Conversely, if ⟨w, y⟩ ∈ U(x′) for some finite x′ ⊑ x, then there exists a finite initial computation sequence γ of A whose history is ⟨x′, w, y⟩. Then ⟨x, w, y⟩ ∈ H(A) by Lemma 5.1 and the fact that H(A) is closed under directed suprema.

5.3 Behaviors of Automata

There is a simple way to obtain an (X, Y)-behavior from an automaton A = (X, W, Y, Q, i, T). Specifically, let D = HW × HY, and define functions

p : HX → [D → D] l : D → HY

as follows:

px⟨w, y⟩ = ⨆{⟨w′, y′⟩ ⊑ ⟨w, y⟩ : ⟨x, w′, y′⟩ ∈ H(A)}.
l⟨w, y⟩ = y.

The definition of p makes sense because by Lemma 5.7, the set on the right-hand side is directed.

Lemma 5.8 Suppose A = (X, W, Y, Q, i, T) is an automaton and D, p, l are defined as above. Then (D, p, l) is an (X, Y)-behavior.

Proof – Obviously D is a domain, and l is continuous. Moreover, from Lemma 5.7 we know that the map taking x to the set

U(x) = {⟨w, y⟩ : ⟨x, w, y⟩ ∈ H(A)},

is a continuous function from HX to the lattice of normal subdomains of HW × HY. But px is just the projection corresponding to U(x) under the isomorphism, given by Proposition 5.3, between the lattice of normal subdomains of HW × HY and the lattice of projections on HW × HY. Hence p is a continuous function from HX to P(HW × HY).

Recall that we defined the input/output relation of an (X, Y)-behavior (D, p, l) to be the set of all ⟨x, ld⟩ such that d is a maximal fixed point of px. A few words are in order here about why this makes sense if (D, p, l) is the behavior of an automaton A = (X, W, Y, Q, i, T). For such a behavior, a history d ∈ D is a maximal fixed point of the projection px iff the history ⟨x, d⟩ is maximal among all histories of the form ⟨x, d′⟩ ∈ H(A). In [24], it was shown that for monotone automata that are obtained by composing a collection of “sequential” component automata into networks, a history ⟨x, d⟩ is maximal among all histories of the form ⟨x, d′⟩ ∈ H(A) iff ⟨x, d⟩ is the history of a “completed” or “fair” computation sequence. Since we wish all and only the completed computation sequences to contribute pairs to the input/output relation, we regard the coincidence of completedness and maximality as the justification for our definition of the input/output relation associated with a behavior. Of course, it might be that there are automata that are not representable as a network of sequential components, and whose input/output relations thus do not necessarily have any relationship to any concrete, intuitive notion of completed or fair computation sequences. However, we do not regard this potential extra generality of our model as any cause for alarm.

5.4 Automata from Behaviors

For certain (X, Y)-behaviors (D, p, l), it is possible to construct an automaton having (D, p, l) as its behavior up to isomorphism of the domain D. In particular, suppose (D, p, l) is an (X, Y)-behavior that satisfies the following assumptions:

1. D ≃ HW × HY for some set W.

2. For all x ∈ HX, the inclusion of the normal subdomain

{⟨w, y⟩ ∈ HW × HY : ⟨w, y⟩ = px⟨w, y⟩}

in HW × HY preserves prime intervals.

Then, define Q to be the set of all finite elements of HX ×HW ×HY, and let i = ⟨⊥, ⊥, ⊥⟩. If q ∈ Q and e = ⟨c, v⟩ ∈ (X + W + Y) × V, then let q; e ∈ Q denote the history such that (q; e)c = (qc)v and (q; e)c′ = qc′ for c′ ≠ c. Let r = T (q, e) iff r = q; e and one of the following holds:

1. chan(e) ∈ X.

2. chan(e) ∈ Y + W, and if r = ⟨x, w, y⟩ then ⟨w, y⟩ = px⟨w, y⟩.

It is straightforward to check that A = (X, W, Y, Q, i, T) is an automaton, and that (D, p, l) is its behavior up to isomorphism. Assumption (2) above implies that for all x ∈ HX, every maximal fixed point ⟨w, y⟩ of px is reachable from ⟨⊥, ⊥⟩ by a sequence of prime intervals. This fact is used to prove that for each state q = ⟨x, w, y⟩, if ⟨w, y⟩ is not a maximal fixed point of px, then there exists some non-input action e that is enabled in state q.

In the above construction, the condition that D ≃ HW × HY for some W is a strong restriction that can be weakened substantially if we are willing to generalize the definition of automata by relaxing the requirement that internal actions be port/value pairs. In particular, if we merely require that internal actions be elements of a “concurrent alphabet,” then we can weaken condition (1) above to the condition that D ≃ E × HY for some “conflict event domain” E [38]. Further generalizations are possible if we consider automata for which more than one action can appear in a single transition. In this paper, we eschew the extra generality because it makes it more difficult to see the connection with the intuitive token-pushing semantics for dataflow networks.

5.5 The Parallel Composition Operation

The parallel composition operation builds a network from two component automata by placing them next to each other without establishing any communication. Formally, suppose

A = (X, W, Y, Q, i, T), A′ = (X′, W′, Y′, Q′, i′, T′)

are automata, where X +W +Y and X′ +W′ +Y′ are disjoint. Then the parallel composition of A and A′ is the automaton

A∥A′ = (X + X′, W + W′, Y + Y′, Q × Q′, ⟨i, i′⟩, T′′),

where ⟨r, r′⟩ = T′′(⟨q, q′⟩, e) iff one of the following conditions holds:

1. e is an action of A, r = T (q, e), and r′ = q′.

2. e is an action of A′, r′ = T′(q′, e) and r = q.

There are no particular theoretical difficulties associated with the parallel composition operation. All we shall have to say about it is to state the following result:

Proposition 5.9 Suppose A has behavior (D, p, l) and A′ has behavior (D′, p′, l′). Then A∥A′ has behavior (D × D′, p′′, l × l′), where p′′⟨x, x′⟩⟨d, d′⟩ = ⟨pxd, p′x′d′⟩.

5.6 The Hiding Operation

The hiding operation on automata takes some of the output ports and makes them into internal ports. Formally, suppose

A = (X, W, V + Y, Q, i, T)

is an automaton. Then the hiding of V in A is the automaton

A \ V = (X, W + V, Y, Q, i, T).

The map from automata to their behaviors also respects hiding operations, as the following result states:

Proposition 5.10 Suppose the (X, V + Y)-automaton A has behavior (D, p, l). Then the (X, Y)-automaton A \ V has behavior (D, p, ρ ∘ l), where ρ : H(V + Y) → HY is the evident restriction map.

5.7 The Feedback Operation

We now formalize the feedback operation depicted schematically in Figure 1 as a construction on automata. Suppose

A = (X + Z, W, Y, Q, i, T)

is an automaton, and let ϕ : Z → Y be an injection. Then the feedback of A by ϕ is the automaton

A_{ϕ} = (X, W, Y, Q, i, T_{ϕ} )

where r = T_{ϕ} (q, e) iff one of the following conditions holds:

1. chan(e) ∉ ϕ(Z) and r = T (q, e).

2. e = ⟨ϕ(c), v⟩ for some c ∈ Z (which is then unique by the injectiveness of ϕ) and if e′ = ⟨c, v⟩, then there exists a state s with s = T (q, e) and r = T (s, e′).

It is easy to check that A_{ϕ} satisfies the conditions for an automaton.

The intuition behind this construction is as follows: The automaton A_{ϕ} behaves exactly as A does in the case of actions e with chan(e) ∉ ϕ(Z). Such actions correspond either to inputs on channels in X or outputs on channels in Y that are not to be fed back to channels in Z. However, if e = ⟨ϕ(c), v⟩ for some c ∈ Z, then e corresponds to the production of an output value v that is immediately reapplied as feedback input on channel c.

Lemma 5.11 Suppose γ is a finite initial computation sequence of A_{ϕ} having history ⟨x, w, y⟩. Then there exists a finite initial computation sequence δ of A having history ⟨x, Hϕy, w, y⟩, such that γ and δ end in the same state.

Proof – Straightforward induction on the length of a finite computation sequence.

Lemma 5.12 Suppose ⟨x, w, y⟩ and ⟨x, w′, y′⟩ are finite elements of HX ×HW ×HY, such that ⟨w, y⟩ ⊑ ⟨w′, y′⟩. If ⟨x, w, y⟩ ∈ H(A_{ϕ} ), and ⟨x, Hϕy, w′, y′⟩ ∈ H(A), then ⟨x, w′, y′⟩ ∈ H(A_{ϕ} ).

Proof – Since ⟨x, w, y⟩ ∈ H(A_{ϕ} ), we may obtain a finite initial computation sequence γ of A_{ϕ} with history ⟨x, w, y⟩. By Lemma 5.11, there exists a finite initial computation sequence δ of A having history ⟨x, Hϕy, w, y⟩, such that γ and δ end in the same state q. Since ⟨x, Hϕy, w′, y′⟩ ∈ H(A) by hypothesis, it follows by Proposition 5.6 that there exists a finite computation sequence δ′ for A having history ⟨x, Hϕy, w′, y′⟩, such that δ is a prefix of δ′. Then δ′ = δτ, where the history of τ is of the form ⟨⊥, ⊥, w′′, y′′⟩, hence τ contains no actions on ports in Z. A straightforward induction on the length of τ shows that there exists a finite computation sequence σ of A_{ϕ} from state q, such that exactly the same sequence of actions occurs in σ as in τ. Since σ starts in state q, the computation sequences γ and σ are composable, and the computation sequence γσ has history ⟨x, w′, y′⟩, as required.

6 Correctness of the Generalized Kahn Principle

Suppose A = (X + Z, W, Y, Q, i, T) is an automaton, and ϕ : Z → Y is an injection. Let A_{ϕ} be the feedback of A by ϕ. Let (D, p, l) be the behavior of A, and let (D_{ϕ} , p_{ϕ} , l_{ϕ} ) be the behavior of A_{ϕ} . Note that D = D_{ϕ} = HW × HY, and both l and l_{ϕ} take ⟨w, y⟩ to y.

The feedback functional corresponding to (D, p, l) and ϕ is the map:

Φ : [HX → [D → D]] → [HX → [D → D]]

defined by:

Φqxd = p⟨x, Hϕ(l(qxd))⟩d.

It is obvious from the definition that Φ is continuous. The generalized Kahn principle then states that p_{ϕ} = μΦ.

For all x ∈ HX, z ∈ HZ, and i ≥ 0, define

p_{i} = Φ^{i}0
D(x, z) = {⟨w, y⟩ : ⟨w, y⟩ = p⟨x, z⟩⟨w, y⟩} = {⟨w, y⟩ : ⟨x, z, w, y⟩ ∈ H(A)}
D_{ϕ} (x) = {⟨w, y⟩ : ⟨w, y⟩ = p_{ϕ} x⟨w, y⟩} = {⟨w, y⟩ : ⟨x, w, y⟩ ∈ H(A_{ϕ} )}.
D_{i}(x) = {⟨w, y⟩ : ⟨w, y⟩ = p_{i}x⟨w, y⟩}.

Intuitively, D(x, z) is the set of non-input portions of histories of initial computation sequences of A on input ⟨x, z⟩, and D_{ϕ} (x) is the set of non-input portions of histories of initial computation sequences of A_{ϕ} on input x. The sets D_{i}(x) may be thought of as approximations to D_{ϕ} (x) in which feedback of output to input is limited to at most i cycles.

Lemma 6.1

1. For all x ∈ HX and all i ≥ 0, the map p_{i}x : D → D is a projection, hence D_{i}(x) is a normal subdomain of D.

2. For all x ∈ HX, the map μΦx : D → D is a projection.

Proof – The second statement follows immediately from the first by the continuity of composition. To show the first statement, fix an arbitrary x ∈ HX. Clearly, p_{i}x ⊑ id_{D}. To complete the proof, we show by induction on i that (p_{i}x) ∘ (p_{i}x) = p_{i}x for all i ≥ 0, hence p_{i}x is a projection on D. The basis case is obvious. For the induction step, suppose we have shown that p_{i}x is a projection. Fix an arbitrary d ∈ D, and let d_{i} = p_{i}xd and d_{i+1} = p_{i+1}xd.

We first claim that p_{i}xd_{i+1} = d_{i}. To see this, observe that since p_{i}x is a projection we have

p_{i}xd_{i+1} = ⨆{d′ : d′ ⊑ d_{i+1}, d′ = p_{i}xd′}
= ⨆{d′ : d′ ⊑ d_{i}, d′ = p_{i}xd′}
= d_{i},

because d_{i+1} ⊑ d and d_{i} = p_{i}xd is the maximal d′ ⊑ d with d′ = p_{i}xd′.

It now follows that

p_{i+1}xd_{i+1} = p⟨x, Hϕ(l(p_{i}xd_{i+1}))⟩d_{i+1}
= p⟨x, Hϕ(ld_{i})⟩d_{i+1}
= p⟨x, Hϕ(ld_{i})⟩(p⟨x, Hϕ(ld_{i})⟩d)
= p⟨x, Hϕ(ld_{i})⟩d
= p_{i+1}xd
= d_{i+1},

where we have used the idempotence of p⟨x, Hϕ(ld_{i})⟩. Thus p_{i+1}x(p_{i+1}xd) = p_{i+1}xd, completing the induction.

Lemma 6.2 Given ⟨x, w, y⟩ ∈ HX × HW × HY, and i ≥ 0, let ⟨w′, y′⟩ = p_{i}x⟨w, y⟩. Then ⟨w, y⟩ ∈ D_{i+1}(x) iff ⟨w, y⟩ ∈ D(x, Hϕy′).

Proof – Simply note that ⟨w, y⟩ ∈ D_{i+1}(x) iff ⟨w, y⟩ = p_{i+1}x⟨w, y⟩ = p⟨x, Hϕy′⟩⟨w, y⟩ iff ⟨w, y⟩ ∈ D(x, Hϕy′).

The next result establishes the basic approximation relationship between the domains D_{i}(x) and the domain D_{ϕ} (x). Its proof requires an analysis of the relationship between the set of finite initial computation sequences of A and those of A_{ϕ} .

Lemma 6.3 Suppose ⟨x, w, y⟩ ∈ HX × HW × HY is finite. Then ⟨w, y⟩ ∈ D_{ϕ} (x) iff ⟨w, y⟩ ∈ D_{n}(x) for some n.

Proof – Suppose ⟨x, w, y⟩ is finite. If ⟨w, y⟩ ∈ D_{ϕ} (x), then there exists a finite initial computation sequence γ of A_{ϕ} with ⟨x, w, y⟩ as its history. Suppose γ is of length n, and for 0 ≤ i ≤ n let γ_{i} be the prefix of γ of length i. We claim that for all i with 0 ≤ i ≤ n, if ⟨x_{i}, w_{i}, y_{i}⟩ is the history of γ_{i}, then ⟨w_{i}, y_{i}⟩ ∈ D_{i}(x_{i}). Since ⟨x, w, y⟩ = ⟨x_{n}, w_{n}, y_{n}⟩, it then follows that ⟨w, y⟩ ∈ D_{n}(x). The claim is proved by induction on i. The basis case is obvious. For the induction step, suppose we have proved the claim for i, and consider the case of i+1. Since γ_{i+1} is exactly one transition longer than γ_{i}, the history ⟨x_{i+1}, w_{i+1}, y_{i+1}⟩ differs from ⟨x_{i}, w_{i}, y_{i}⟩ in exactly one of the three components. We consider each case separately.

1. In case x_{i} x_{i+1}, then ⟨w_{i+1}, y_{i+1}⟩ = ⟨w_{i}, y_{i}⟩. Since ⟨w_{i}, y_{i}⟩ ∈ D_{i}(x_{i}), D_{i}(x_{i}) ⊆ D_{i}(x_{i+1}) by Proposition 5.3 and the monotonicity of p_{i}, and D_{i}(x_{i+1}) ⊆ D_{i+1}(x_{i+1}) by Proposition 5.3 and the fact that p_{i}x_{i+1} ⊑ p_{i+1}x_{i+1}, it follows that ⟨w_{i+1}, y_{i+1}⟩ = ⟨w_{i}, y_{i}⟩ ∈ D_{i}(x_{i}) ⊆ D_{i}(x_{i+1}) ⊆ D_{i+1}(x_{i+1}).

2. Suppose w_{i} w_{i+1}, so that x_{i+1} = x_{i} and y_{i+1} = y_{i}. Then, ⟨x_{i+1}, w_{i+1}, y_{i+1}⟩ = ⟨x_{i}, w_{i+1}, y_{i}⟩ ∈ H(A_{ϕ} ), so ⟨x_{i}, Hϕ(y_{i}), w_{i+1}, y_{i+1}⟩ ∈ H(A) by Lemma 5.11, and thus ⟨w_{i+1}, y_{i+1}⟩ ∈ D(x_{i}, Hϕ(y_{i})). Applying Lemma 6.2 and the induction hypothesis, we conclude ⟨w_{i+1}, y_{i+1}⟩ ∈ D_{i+1}(x_{i}) = D_{i+1}(x_{i+1}).

3. If y_{i} y_{i+1}, then the argument is similar to the previous case.

Conversely, suppose ⟨w, y⟩ ∈ D_{n}(x) for some n. For 0 ≤ i ≤ n, let ⟨w_{i}, y_{i}⟩ = p_{i}x⟨w, y⟩. We show, by induction on i, that ⟨w_{i}, y_{i}⟩ ∈ D_{ϕ} (x) for all i with 0 ≤ i ≤ n. Since ⟨w, y⟩ = ⟨w_{n}, y_{n}⟩, it then follows that ⟨w, y⟩ ∈ D_{ϕ} (x). The basis case is immediate from Lemma 5.1. For the induction step, suppose we have shown that ⟨w_{i}, y_{i}⟩ ∈ D_{ϕ} (x). Since ⟨w_{i+1}, y_{i+1}⟩ ∈ D_{i+1}(x), and ⟨w_{i}, y_{i}⟩ = p_{i}x⟨w_{i+1}, y_{i+1}⟩, it follows that ⟨w_{i+1}, y_{i+1}⟩ = p⟨x, Hϕy_{i}⟩⟨w_{i+1}, y_{i+1}⟩, hence ⟨w_{i+1}, y_{i+1}⟩ ∈ D(x, Hϕy_{i}). Then ⟨x, w_{i}, y_{i}⟩ ∈ H(A_{ϕ} ) and ⟨x, Hϕy_{i}, w_{i+1}, y_{i+1}⟩ ∈ H(A), so ⟨x, w_{i+1}, y_{i+1}⟩ ∈ H(A_{ϕ} ) by Lemma 5.12. But this means that ⟨w_{i+1}, y_{i+1}⟩ ∈ D_{ϕ} (x), completing the induction step.

Lemma 6.4 D_{ϕ} (x) = (⋃_{i} D_{i}(x))^{c}.

Proof – For finite x, the result is a direct consequence of Lemma 6.3, Lemma 5.4, and the fact that D_{ϕ} (x) is a normal subdomain of HW × HY. To extend to all x, we use the algebraicity of HX and Lemma 5.7 to obtain:

D_{ϕ} (x) = (⋃{D_{ϕ} (x′) : x′ ⊑ x, x′ finite})^{c}.

Using Lemma 6.1, we obtain a similar characterization of D_{i}(x):

D_{i}(x) = (⋃{D_{i}(x′) : x′ ⊑ x, x′ finite})^{c}.

The result is now immediate.

Theorem 1 p_{ϕ} = μΦ, hence the generalized Kahn principle is correct.

Proof – First note that for all x ∈ HX we have μΦx = ⨆_{i} p_{i}x. Also, for all x ∈ HX, the projection p_{ϕ} x is the projection corresponding to the normal subdomain D_{ϕ} (x) of HW × HY, under the isomorphism between the lattice of normal subdomains of HW × HY and the lattice of projections on HW × HY. Similarly, p_{i}x is the projection corresponding to the normal subdomain D_{i}(x). By the previous lemma, D_{ϕ} (x) = (⋃_{i} D_{i}(x))^{c}. But (⋃_{i} D_{i}(x))^{c} is the least normal subdomain containing all the D_{i}(x), hence is the normal subdomain corresponding to the projection ⨆_{i} p_{i}x = μΦ.

7 Discussion

We have stated a generalized version of Kahn’s fixed-point principle for a class of indeterminate networks, and we have proved that it gives results in accordance with token-pushing operational semantics. Our generalized Kahn principle is simple to state, and parallels Kahn’s original fixed-point principle in a pleasant way. The class of dataflow networks to which it applies includes at least all networks that can be constructed from functional processes and angelic merge, but not to networks built using fair merge or an equivalent primitive such as “poll” [24]. Although our generalized Kahn principle is easily stated, the proof that it agrees with token-pushing semantics seems to require a rather detailed analysis of a particular operational model, using results the author has been accumulating over the past several years. It remains to be seen whether a simpler proof can be given. Other interesting possibilities for future work are to extend the result to recursively defined networks, and to look at possibilities for treating fair merge.

Abramsky [2] has recently proposed a generalized Kahn Principle that can be viewed as a “pointwise” extension of Kahn’s result to those networks whose behaviors can be represented as sets of continuous functions. In Abramsky’s work, a network with input channels X and output channels Y would be represented as a set of functions from HX to HY. A precise relationship can be drawn between the generalized Kahn Principle of the present paper and a pointwise version like that of Abramsky. Suppose B = (D, p, l) is an (X + Z, Y)-behavior with the following special form: D ≃ (HX × HZ) × D′, and up to this isomorphism we have p⟨x, z⟩⟨⟨x′, z′⟩, d′⟩ = ⟨⟨x ⊓ x′, z ⊓ z′⟩, d′⟩. Such a behavior models a network in which all indeterminacy arises from the choices made by an “oracle” (represented by D′) that operates independently of the network input. These behaviors were called “semi-determinate” in [39]. We may associate with such a semi-determinate behavior the set F (B) of all functions f_{d′} : HX × HZ → HY satisfying f_{d′}⟨x, z⟩ = l(p⟨x, z⟩⟨⟨x, z⟩, d′⟩) = l(⟨⟨x, z⟩, d′⟩), where d′ is a maximal element of D′. Notice that the special form of B ensures that the set F (B) contains enough information to recover the input/output relation R(B) of B, because R(B) = {⟨⟨x, z⟩, f⟨x, z⟩⟩ : f ∈ F (B)}. Now, if B_{ϕ} is the (X, Y)-behavior obtained by applying our generalized Kahn Principle to B, and if f_{ϕ} : HX → HY denotes the result of applying the original Kahn Principle to a function f : HX × HZ → HY, then F (B_{ϕ} ) = {f_{ϕ} : f ∈ F (B)}.

The comments of the previous paragraph apply only to semi-determinate behaviors. All networks built using functional processes and infinity-fair merge are semi-determinate, however it can be shown [39] that angelic merge is not semi-determinate. Thus, when viewed in this way, it would appear that our generalized Kahn principle applies to a larger class of networks than does the pointwise version of Abramsky. However, B. A. Trakhtenbrot and A. Rabinovich [private communication] have recently reminded the author that there is another way to associate a set of functions with a behavior, and that is to assign to each (X × Z, Y)-behavior B = (D, p, l) the set G(B) of all functions g_{d} : HX × HZ → D × HY satisfying g_{d}⟨x, z⟩ = ⟨p⟨x, z⟩d, l(p⟨x, z⟩d)⟩, where d is an arbitrary element of D. If B is not semi-determinate, then we cannot discard the D component of the codomains of the functions g_{d}, since to do so would mean that the set G(B) would no longer contain sufficient information to recover the input/output relation of B.^{2} As in the previous paragraph, we have that G(B_{ϕ} ) = {g_{ϕ} : g ∈ G(B)} (this is an easy corollary of Theorem 1), so from this standpoint it appears that the “set of functions” model and the “pointwise lifted Kahn Principle” is just about as good as the behavior model and generalized Kahn Principle presented here. Our generalized Kahn Principle serves to reduce the problem of reasoning about indeterminate networks to that of reasoning about continuous functions, whereas the pointwise version requires reasoning about sets of continuous functions. However, in favor of the behavior model over the set of functions model we advance the argument that the former shows more clearly the underlying mathematical structure, because it makes evident the way in which all the functions in a set must relate to each other, if that set is to represent the behavior of an indeterminate network. It should also be noted that, because of the presence of the domain D, neither of the two models is sufficiently abstract, and therefore further investigation is required to reach the goal of a highly structured, fully abstract model of indeterminate dataflow networks.

2If however, as in the work of Trakhtenbrot and Rabinovich to date [29], one does not insist that only “completed” computation sequences contribute to the input/output relation, then it is no problem to throw away the domain D.

References

[1] S. Abramsky. Experiments, powerdomains, and fully abstract models for applicative multiprogramming. In Foundations of Computation Theory, pages 1–13, Springer-Verlag. Volume 158 of Lecture Notes in Computer Science, 1983.

[2] S. Abramsky. A generalized Kahn principle for abstract asynchronous networks. In Mathematical Foundations of Program Semantics, Springer Verlag. Lecture Notes in Computer Science, 1990. (to appear).

[3] S. Abramsky. On the semantic foundations for applicative multiprogramming. In ICALP 83, Springer Verlag. Lecture Notes in Computer Science, 1983.

[4] R. J. Back and N. Mannila. A refinement of Kahn’s semantics to handle nondeterminism and communication. In Proc. ACM Symposium on Principles of Distributed Computing, pages 111–120, 1982.

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

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

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

[8] M. Broy. Fixed point theory for communication and concurrency. In D. Bjørner, editor, Formal Description of Programming Concepts II, pages 125–148, North-Holland. 1983.

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

[10] H. Gaifman and V. Pratt. Partial order models of concurrency and the computation of functions. In Symposium on Logic in Computer Science, pages 72–85, Ithaca, NY, June 1987.

[11] B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Uppsala University, Uppsala, Sweden, 1987.

[12] B. Jonsson. A fully abstract trace model for dataflow networks. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, pages 155–165, January 1989.

[13] A. Jung. Cartesian Closed Categories of Domains. PhD thesis, University of Darmstadt, 1988.

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

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

[16] R. M. Keller. Denotational models for parallel programs with indeterminate operators. In E. J. Neuhold, editor, Formal Description of Programming Concepts, pages 337–366, North-Holland. 1978.

[17] R. M. Keller and P. Panangaden. Semantics of networks containing indeterminate operators. In S. D. Brookes, A. W. Roscoe, and G. Winskel, editors, Seminar on Concurrency, pages 479–496, Springer-Verlag. Volume 197 of Lecture Notes in Computer Science, 1984.

[18] J. N. Kok. Denotational semantics of nets with nondeterminism. In ESOP 86, pages 237– 249, Springer-Verlag. Volume 213 of Lecture Notes in Computer Science, March 1986.

[19] J. N. Kok. A fully abstract semantics for data flow nets. pages 351–368, Springer-Verlag. Volume 259 of Lecture Notes in Computer Science, 1987.

[20] M. Kwiatkowska. Fairness for Non-Interleaving Concurrency. PhD thesis, University of Leicester, May 1989.

[21] N. A. Lynch and E. W. Stark. A proof of the Kahn principle for input/output automata. Information and Computation, 82(1):81–92, July 1989.

[22] M. G. Main and D. B. Benson. Functional behavior of nondeterministic and concurrent programs. Information and Control, 62:144–189, 1984.

[23] J. Misra. Equational reasoning about nondeterministic processes (preliminary version). In ACM Symposium on Principles of Distributed Computing, pages 29–44, 1989.

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

[25] D. M. R. Park. The “fairness problem” and nondeterministic computing networks. In Proceedings, 4th Advanced Course on Theoretical Computer Science, pages 133–161, Mathematisch Centrum, 1982.

[26] V. R. Pratt. On the composition of processes. In Ninth Annual ACM Symposium on Principles of Programming Languages, pages 213–223, January 1982.

[27] V. R. Pratt. The pomset model of parallel processes: unifying the temporal and the spatial. In S. D. Brookes, A. W. Roscoe, and G. Winskel, editors, Seminar on Concurrency, pages 180–196, Springer-Verlag. Volume 197 of Lecture Notes in Computer Science, July 1984.

[28] A. Rabinovich. Pomset semantics is consistent with data flow semantics. EATCS Bulletin, 107–117, June 1987.

[29] A. Rabinovich and B. A. Trakhtenbrot. Communication among relations. In Automata, Languages, and Programming: 17th International Colloquium, pages 294–307, Springer Verlag. Volume 443 of Lecture Notes in Computer Science, 1990.

[30] A. Rabinovich and B. A. Trakhtenbrot. Nets and data flow interpreters. In Logic in Computer Science, IEEE, 1989.

[31] J. Russell. Full abstraction for nondeterministic dataflow networks. June 1989. Unpublished manuscript, Cornell University.

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

[33] M. W. Shields. Deterministic asynchronous automata. In E. J. Neuhold and G. Chroust, editors, Formal Methods in Programming, pages 317–345, North-Holland. 1985.

[34] J. Staples and V. L. Nguyen. A fixpoint semantics for nondeterministic data flow. Journal of the ACM, 32(2):411–444, April 1985.

[35] E. W. Stark. Compositional relational semantics for indeterminate dataflow networks. In Category Theory and Computer Science, pages 52–74, Springer-Verlag. Volume 389 of Lecture Notes in Computer Science, Manchester, U. K., 1989.

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

[37] E. W. Stark. Concurrent transition systems. Theoretical Computer Science, 64:221–269, 1989.

[38] 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, 1990. (to appear).

[39] E. W. Stark. On the relations computed by a class of concurrent automata. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 329– 340, January 1990.