In this paper the author presents a formal definition of AMPL (applicative multi-programming language). The language allows expression of the four features mentioned in the title in the applicative (non-procedural) framework. A program consists of a sequence of possibly recursive function and stream definitions and an expression to be evaluated. Communication and concurrency are expressed via streams, and there are two operators to express nondetermin- ism: □ for erratic nondeterminism, and &bnabla; for angelic nondeterminism. Broy illustrates the intended difference between □ and &bnabla; thus
funct choose = &lgr; n : n &bnabla; choose ( n + 1 )
funct choose′ = &lgr; n : n □ choose′ ( n + 1 )
Here choose ( n ) may return any natural number ≥Cn but may not diverge while the meaning of choose′ ( n ) includes the diverging computation. The author explores a wide variety of topics in an almost tutorial style, indicating the richness of the language being discussed. Power domain denotational semantics and operational semantics via conditional rewriting systems with output are presented at a fairly relaxed pace, with several useful examples. In a long section on the relation between infinite streams and dataflow computation, many examples and few results are given to illustrate the essential similarity between these two models of computation. One wonders if Broy is not cheating however, since the semantics of dataflow graphs are defined to be those of the corresponding stream equations.
This is a good paper for someone starting to read about the semantics of concurrency and nondeterminism because the coverage is broad and the references are extensive. However, the specialist may be frustrated by the lack of detail at certain points. One example: Broy claims { x ∈ DOM | ⊥ ∈ f ( x ) } may be &Sgr;11 (implying it may not be arithmetical). Then, after saying that a function f : DOM n → 2DOM is definable in AMPL if and only if some AMPL program P , f ( x 1 ,..., x n ) is the set of y to which the expression P ( x 1 ,..., xn ) can be rewritten by some finitary, consistent, effective computation rule, he says, “This gives a clear hint at why our extended notion of definability (and ‘computability’) leads to &Sgr;11: we have to quantify over all finitary, consistent, effective computation rules.” But if the class of computation rules is RE, then the quantification may be expressed as a natural number quantification; and if not, this is a very peculiar operational semantics, and clarification would be in order.
