Describing algorithms on higher abstraction levels, one often comes across the phenomenon of nondeterminism. Nevertheless, the built-in nondeterminism of ealgebras has been rarely used. It is often more appropriate to use external functions to reflect nondeterministic behavior. (In the distributed case, nondeterminism may be often eliminated by introducing additional agents.) Consider for instance the assignment statement of the C programming language. Should one evaluate the left side or the right side first? According to the ANSI standard (ANSI is the American National Standards Institute), the choice of the evaluation order is implementation-dependent. Moreover, an implementation does not have to be consistent; the evaluation order may change when the same assignment statement is executed next time around (say, in a loop). This is an obvious case of nondeterminism and first we, the authors of [GH], were tempted to use a nondeterministic rule to reflect the nondeterminism. But then we realized that C is perfectly deterministic. It is just that execution may depend on information provided by implementation. Thus it is more faithful to the standard (and more convenient) to use an external function that decides the evaluation order.
Still, nondeterministic commands may be desired and we provide such commands in this section. For example, it may be convenient to formalize the environment in a distributed situation, so that an external function of one agent is nondeterministically computed by another agent.
For simplicity, we ignore the import constructor in this section. It is easy to extend the language of this section with the import constructor. Moreover, the choice constructor defined below and the import constructor can be combined into one constructor.