Singular and Plural Nondeterministic Parameters.
The article defines algebraic semantics of singular (call-time-choice) and plural (run-time-choice) nondeterministic parameter passing and presents a specification language in which operations with both kinds of parameters can be defined simultaneously. Sound and complete calculi for both semantics are introduced. We study the relations between the two semantics and point out that axioms for operations with plural arguments may be considered as axiom schemata for operations with singular arguments.
Introduction
The notion of nondeterminism arises naturally in describing concurrent systems. Various
approaches to the theory and specification of such systems, for instance, CCS [16], CSP [9],
process algebras [1], event structures [26], include the phenomenon of nondeterminism.
But nondeterminism is also a natural concept in describing sequential programs, either as a
means of indicating a "don't care'' attitude as to which among a number of computational
paths will actually be utilized in a particular computation (e.g., [3]) or as a means of
increasing the level of abstraction [14,25]. The present work proceeds from the theory of
algebraic specifications [4, 27] and generalizes it so that it can be applied to describing
nondeterministic operations.
In deterministic programming the distinction between call-by-value and call-by-name
semantics of parameter passing is well known. The former corresponds to the situation
where the actual parameters to function calls are evaluated and passed as values. The latter
allows parameters which are function expressions, passed by a kind of Algol copy rule [21],
and which are evaluated whenever a need for their value arises. Thus call-by-name will
terminate in many cases when the value of a function may be determined without looking at
(some of) the actual parameters, i.e., even if these parameters are undefined. Call-by-value
will, in such cases, always lead to undefined result of the call. Nevertheless, the call-by-value
semantics is usually preferred in the actual programming languages since it leads to clearer
and more tractable programs.
*) This work has been partially supported by the Architectural Abstraction project under NFR
(Norway), by CEC under ESPRIT-II Basic Reearch Working Group No. 6112 COMPASS, by the
US DARPA under ONR contract N00014-92-J-1928, N00014-93-1-1335 and by the US Air Force
Office of Scientific Research under Grant AFOSR-91-0354.
Following [20], we call the nondeterministic counterparts of these two notions singular
(call-by-value) and plural (call-by-name) parameter passing. Other names applied to this, or
closely related distinction, are call-time-choice vs. run-time-choice [2, 8], or inside-out (IO) vs .
outside-in (OI) which reflect the substitution order corresponding to the respective
semantics [5, 6]. In the context where one allows nondeterministic parameters the difference
between the two semantics becomes quite apparent even without looking at their
termination properties. Let us suppose that we have defined operation g(x) as "if x=0 then a
else (if x=0 then b else c)", and that we have a nondeterministic choice operation #.
returning an arbitrary element from the argument set. The singular interpretation will
satisfy the formula f: then a else c), while the plural interpretation need not
satisfy this formula. For instance, under the singular interpretation g(#.{0,1}) will yield
either a or c, while the set of possible results of g(#.{0,1}) under the plural interpretation will
be {a,b,c}. (Notice that in a deterministic environment both semantics would yield the same
results.) The fact that the difference between the two semantics occurs already in very trivial
examples of terminating nondeterministic operations motivates our investigation.
We discuss the distinction between the singular and plural passing of nondeterministic
parameters in the context of algebraic semantics focusing on the associated reasoning
systems. The singular semantics is given by multialgebras, that is, algebras where functions
are set-valued and where these values correspond to the sets of possibile results returned by
nondeterministic operations. Thus, if f is a nondeterministic operation, f(t) will denote the set
of possible results returned by f when applied to t. We introduce the calculus NEQ which is
sound and complete with respect to this semantics.
Although terms may denote sets the variables in the language range only over
individuals. This is motivated by the interest in describing unique results returned by each
particular application of an operation (execution of the program). It gives us the possibility
of writing, instead of a formula F(f(t)) which expresses something about the whole set of
possible results of f(t), the formula corresponding to x# f(t) # F(x) which express something
about each particular result x returned by f(t). Unfortunately, this poses the main problem
of reasoning in the context of nondeterminism - the lack of general substitutivity. From the
fact that h(x) is deterministic (for each x, has a unique value) we cannot conclude that so is
h(t) for an arbitrary term t. If t is nondeteministic, h(t) may have several possible results. The
calculus NEQ is designed so that it appropriately restricts the substitution of terms for
singular variables.
Although operations in multialgebras are set-valued their carriers are usual sets. Thus
operations map individuals to sets. This is not sufficient to model plural arguments. Such
arguments can be understood as sets being passed to the operation. The fact that, under
plural interpretation, g(x) as defined above need not satisfy f results from the two
occurrences of x in the body of g. Each of these occurrences corresponds to a repeated
application of choice from the argument set x, that is, potentially, to a different value. I n
order to model such operations we take as the carrier of the algebra a (subset of the) power
set - operations map sets to sets. In this way we obtain power algebra semantics. The
extension of the semantics is reflected at the syntactic level by introduction of plural
variables ranging over sets rather than over individuals. The sound and complete extension
of NEQ is obtained by adding one new rule which allows for usual substitution of arbitrary
terms for plural variables.
The structure of the paper is as follows. In sections 2-3 we introduce the language for
specifying nondeterministic operations and explain the intuition behind its main features. I n
section 4 we define multialgebraic semantics for singular specifications and introduce a sound
and complete calculus for such specifications. In section 5 the semantics is generalized to
power algebras capable of modeling plural parameters, and the sound and complete extension
of the calculus is obtained by introducing one additional rule. A comparison of both
semantics in section 6 is guided by the similarity of the respective calculi. We identify the
subclasses of multimodels and power models which may serve as equivalent semantics of one
specification. We also highlight the increased complexity of the power algebra semantics
reflecting the problems with intuitive understanding of plural arguments.
Proofs of the theorems are merely indicated in this presentation. It reports some of the
results from [24] where the full proofs and other details can be found.
2. The specification language
A specification is a pair ((,P) where the signature ( is a pair (S,F) of sorts S and operation
(with argument and result sorts in S). The set of terms over a signature ( and
variable set X is denoted by W (,X . We always assume that, for every sort S, the set of ground
words of sort S, S W ( , is not empty. 1
P is a set of sequents of atomic formulae written as a 1 ,.,a n a e 1 ,.,e m . The left hand side
(LHS) of a is called the antecedent and the right hand side (RHS) the consequent, and both are
to be understood as sets of atomic formulae (i.e., the ordering and multiplicity of the atomic
formulae do not matter). In general, we allow either antecedent or consequent to be empty,
though - is usually dropped in the notation. A sequent with exactly one formula in the
consequent (m=1) is called a Horn formula, and a Horn formula with empty antecedent (n=0)
is a simple formula (or a simple sequent).
This restriction is motivated by the fact (pointed out in [7]) that admitting empty carriers requires
additional mechanisms (explicit quantification) in order to obtain sound logic. We conjecture that s i m i l ar
solution can be applied in our case.
Singular and Plural Nondeterministic ParametersAll variables occurring in a sequent are implicitly universally quantified over the whole
sequent. A sequent is satisfied if, for every assignment to the variables, one of the
antecedents is false or one of the consequents is true (it is valid iff the formula a 1 #a n #
For any term (formula, set of formulae) j, V[j] will denote the set of variables in j. If
the variable set is not mentioned explicitly, we may also write x#V to indicate that x is a
variable.
An atomic formula in the consequent is either an equation, t=s, or an inclusion, t#s, of
terms t, s#W (,X . An atomic formula in the antecedent, written tas, will be interpreted as non-empty
intersection of the (result) sets corresponding to t and s. For a given specification
SP=((,P), L(SP) will denote the above language over the signature (.
The above conventions will be used throughout the paper. The distinction between the
singular and plural parameters (introduced in the section 5) will be reflected in the notation
by the superscript * : a plural variable will be denoted by x * , the set of plural variables in a
term t by V * [t], a specification with plural arguments SP * , the corresponding extension of
the language L by L * etc.
3. A note on the intuitive interpretation
Multialgebraic semantics [10, 13] interprets specifications in some form of power structures
where the (nondeterministic) operations correspond to set-valued functions. This means that
a (ground) term is interpreted as a set of possibilities - it denotes the set of possible results of
the corresponding operation. We, on the other hand, want our formulae to express necessary
i.e., facts which have to hold in every evaluation of a program (specification). This is
achieved by interpreting terms as applications of the respective operations. Every two
syntactic occurrences of a term t will refer to possibly distinct applications of t. For
nondeterministic terms this means that they may denote two distinct values.
Typically, equality is interpreted in a multialgebra as set equality [13, 23, 12]. For
instance, the formula a t=s means that the sets corresponding to all possible results of the
operations t and s are equal. This gives a model which is mathematically plausible, but which
does not correspond to our operational intuition. The (set) equality a t=s does not guarantee
that the result returned by some particular application of t will actually be equal to the result
returned by an application of s. It merely tells us that in principle (in all possible executions)
any result produced by t can also be produced by s and vice versa.
Equality in our view should be a necessary equality which must hold in every evaluation
of a program (specification). It does not correspond to set equality, but to identity of 1-element
sets. Thus the simple formula a t=s will hold in a multistructure M iff both t and s are
interpreted in M as one and the same set which, in addition, has only one element. Equality is
then a partial equivalence relation and terms t for which a t=t holds are exactly the
deterministic terms, denoted by D SP ,X . This last equality indicates that arbitrary two
applications of t have to return the same result.
If it is possible to produce a computation where t and s return different results - and this
is possible when they are nondeterministic - then the terms are not equal but, at best,
equivalent. They are equivalent if they are capable of returning the same results, i.e., if they
are interpreted as the same set. This may be expressed using the inclusion relation: s#t holds
iff the set of possible results of s is included in the set of possible results of t, and s#t if each
is included in the other.
Having introduced inclusion one might expect that a nondeterministic operation can be
specified by a series of inclusions - each defining one of its possible results. However, such a
specification gives only a "lower bound" on the admitted nondeterminism. Consider the
following example:
Example 3.1
S: { Nat },
F: 0: # Nat (zero)
_#_: Nat-Nat # Nat (binary nondeterministic choice)
P: 1. a 0=0
2. a s(x)=s(x)
3. 1a0 a (As usual, we abbreviate s n (0) as n.)
4. a 0 # 0#1 a 1 # 0#1
The first two axioms make zero and successor deterministic. A limited form of negation is
present in L in the form of sequents with empty consequent. Axiom 3. makes 0 distinct from
Axioms 4. make then # a nondeterministic choice with 0 and 1 among its possible results.
This, however, ensures only that in every model both 0 and 1 can be returned by 0#1. I n
most models all other kinds of elements may be among its possible results as well, since no
extension of the result set of 0#1 will violate the inclusions of 4. If we are satisfied with this
degree of precision, we may stop here and use only Horn formula. All the results in the rest
of the paper apply to this special case. But to specify an "upper bound" of nondeterministic
operations we need disjunction - the multiple formulae in the consequents. Now, if we write
the axiom:
5. a 0#1=0, 0#1=1
the two occurrences of 0#1 refer to two arbitrary applications and, consequently, we obtain
Singular and Plural Nondeterministic Parametersthat either any application of 0#1 equals 0 or else it equals 1, i.e., that # is not really
nondeterministic, but merely underspecified. Since axioms 4. require that both 0 and 1 be
among the results of t, the addition of 5. will actually make the specification inconsistent.
What we are trying to say with the disjunction of 5. is that every application of 0#1
returns either 0 or 1, i.e., we need a means of identifying two occurrences of a
nondeterministic term as referring to one and the same application. This can be done b y
binding both occurrences to a variable.The appropriate axiom will be:
59. xa0#1 a x=0, x=1
The axiom says: whenever 0#1 returns x, then x equals 0 or x equals 1. Notice that such an
interpretation presupposes that the variable x refers to a unique, individual value. Thus
bindings have the intended function only if they involve singular variables. (Plural variables,
on the other hand, will refer to sets and not individuals, and so the axiom
599. x * a0#1 a x * =0, x * =1
would have a completely different meaning.) The singular semantics is the most common in
the literature on algebraic semantics of nondeterministic specification languages [2, 8, 11], in
spite of the fact that it prohibits unrestricted substitution of terms for variables. Any
substitution must now be guarded by the check that the substituted term yields a unique
value, i.e., is deterministic. We return to this point in the subsection on reasoning where we
introduce a calculus which does not allow one, for instance, to conclude 0#1=0#1 a 0#1=0,
0#1=1 from the axiom 59 (though it could be obtained from 599).
4. The singular case: semantics and calculus
This section defines the multialgebraic semantics of specifications with singular arguments
and introduces a sound and complete calculus.
4.1. Multistructures and multimodels.
Definition 4.2 (Multistructures). Let ( be a signature. M is a (-multistructure if
(1) its carrier _M_ is an S-sorted set and
(2) for every f: S 1 -S n #S in F, there is a corresponding fuction
A function F: A#B (i.e., a family of functions
for every S#S) is a
multihomomorphism from a (-multistructure A to B if
for each constant symbol c#F, F(c A
(H2) for every f: S 1 -S n #S in F and a 1 .a n #S 1
A
F(f A (a 1 .a n
If all inclusions in H1 and H2 are (set) equalities the homomorphism is tight,
otherwise it is strictly loose (or just loose).
denotes the set of non-empty subsets of the set S. Operations applied to sets refer to
their unique pointwise extensions. Notice that for a constant c: #S, 2. indicates that c M can
be a set of several elements of sort S.
Since multihomomorphisms are defined on individuals and not sets they preserve
singletons and are #-monotonic. We denote the class of (-multistructures by MStr((). It has
the distinguished word structure MW ( defined in the obvious way, where each ground term
is interpreted as a singleton set. We will treat such singleton sets as terms rather than 1-
element sets (i.e., we do not take special pains to distinguish MW ( and W ( ). MW ( is not an
initial (-structure since it is deterministic and there can exist several homomorphisms from
it to a given multistructure. We do not focus on the aspect of initiality and merely register
the useful fact from [11]:
4.3. M is a (-multistructure iff, for every set of variables X and assignment b:
X#_M_, there exists a unique function b[_]: W (,X #P + (_M_) such that:
1.
2.
3. b[f(t
In particular, for X=-, there is a unique interpretation function (not a multihomomorphism)
satisfying the last two points of this definition.
As a consequence of the definition of multistructures, all operations are #-monotonic,
i.e., b[s]#b[t] # b[f(s)]#b[f(t)]. Notice also that assignment in the lemma (and in general,
whenever it is an assignment of elements from a multistructure) means assignment of
individuals, not sets.
Next we define the class of multimodels of a specification.
Definition 4.4 (Satisfiability). A (-multistructure M satisfies an L(() sequent p
for every b: X#M we have
where A#B iff A and B are the same 1-element set.
An SP-multimodel is a (-multistructure which satisfies all the axioms of SP. We
denote the class of multimodels of SP by MMod(SP).
The reason for using nonempty intersection (and not set equality) as the interpretation of a
in the antecedents is the same as using "elementwise" equality # in the consequents. Since we
Singular and Plural Nondeterministic Parametersavoid set equality in the positive sense (in the consequents), the most natural negative form
seems to be the one we have chosen. For deterministic terms this is the same as equality, i.e.,
deterministic antecedents correspond exactly to the usual (deterministic) conditions. For
nondeterministic terms this reflects our interest in binding such terms: the sequent
".sat.a." is equivalent to ".xas, xat.a. A binding ".xat.a." is also equivalent to
the more familiar ".x#t.a.", so the notation sat may be read as an abbreviation for the
more elaborate formula with two # and a new variable x not occurring in the rest of the
sequent.
For a justification of this, as well as other choices we have made here, the reader is
referred to [24].
4.2. The calculus for singular semantics
In [24] we have introduced the calculus NEQ which is sound and complete with respect to
the class MMod(SP). Its rules are:
R1: a x=x x#V
R2:
G D G D
G G D D
x
x
x
x
a a
a
R3:
G D G D
G G D D
x
x
x
x
a a
a
- x not in a RHS of #
R4: a) xay a x=y b) xat a x#t x,y#V
R5:
G D G D
G G D D
a a
a
a (CUT) (# stands for either = or #)
a)

G D
G D
a
a , e
G D
a
a
R7: G D
G D
x
x
a a
a
x#V-V[t], at most one x in G a D (ELIM)
a denotes G with b substituted for a. Short comments on each of the rules may be in order.
The fact that '=' is a partial equivalence relation is expressed in R1. It applies only to
variables and is sound because all assignments assign individual values to the (singular)
variables.
is a paramodulation rule allowing replacement of terms which may be deterministic
(in the case when t 1 =t 2 holds in the second assumption). In particular, it allows derivation of
the standard substitution rule when the substituted terms are deterministic, and prevents
substitution of nondeterministic terms for variables.
R3 allows "specialization" of a sequent by substituting for a term t 2 another term t 1 which
is included in t 2 . The restriction that the occurrences of t 2 which are substituted for don't
occur in the RHS of # is needed to prevent, for instance, the unsound conclusion a t 3 #t 1
from the premises a t 3 #t 2 and a t 1 #t 2 .
R4 and R5 express the relation between a in the antecedent and the equality and
inclusion in the consequent. The axiom of standard sequent calculus, e a e, (i.e., sat a s#t)
does not hold in general here because the antecedent corresponds to non-empty intersection
of the result sets while the consequent to the inclusion (#) or identity of 1-element (=) result
sets. Only for deterministic terms s, t, do we have that sa t a s=t holds.
R5 allows us to cut both a s=t and a s#t with sa t a D.
R7 eliminates redundant bindings, namely those that bind an application of a term
occurring at most once in the rest of the sequent.
We will write P # CAL p to indicate that p is provable from P with the calculus CAL.
When we need to write the sequent p explicitly this notation becomes sometimes awkward,
and so we will optionally write it as P
The counterpart of soundness/completeness of the equational calculus is [24]:
Theorem 4.5. NEQ is sound and complete wrt. MMod(SP):
Proof idea:
Soundness is proved by induction on the length of the proof P # NEQ p. The proof of
the completeness part is a standard, albeit rather involved, Henkin-style argument.
The axiom set P of SP is extended by adding all L(SP) formulae p which are
consistent with P (and the previously added formulae). If the addition of p leads to
inconsistency, one adds the negation of p. Since empty consequents provide only a
restricted form of negation, the general negation operation is defined as a set of
formulae over the original signature extended with new constants. One shows then
that the construction yields a consistent specification with a deterministic basis from
which a model can be constructed.
We also register an easy lemma that the set-equivalent terms, t#s satisfy the same formulae:
Lemma 4.6. t#s iff, for any sequent p, P# NEQ p t
z iff P# NEQ p s
z .
Singular and Plural Nondeterministic Parameters5. The plural case: semantics and calculus
The singular semantics for passing nondeterminate arguments is the most common notion to
be found in the literature. Nevertheless, the plural semantics has also received some
attention. In the denotational tradition most approaches considered both possibilities [18,
19, 20, 22]. Engelfriet and Schmidt gave a detailed study of both - in their language, IO and
OI - semantics based on tree languages [5], and continuous algebras of relations and power
sets [6]. The unified algebras of Mosses and the rewriting logic of Meseguer [15] represent
other algebraic approaches distinguishing these aspects.
We will define the semantics for specifications where operations may have both singular
and plural arguments. The next subsection gives the necessary extension of the calculus
NEQ to handle this generalized situation.
5.1. Power structures and power models
Singular arguments (such as the variables in L) have the usual algebraic property that they
refer to a unique value. This reflects the fact that they are evaluated at the moment of
substitution and the result is passed to the following computation. Plural arguments, on the
other hand, are best understood as textual parameters. They are not passed as a single value,
but every occurrence of the formal parameter denotes a distinct application of the operation.
We will allow both singular and plural parameter passing in one specification. The
corresponding semantic distinction is between power set functions which are merely #-
monotonic and those which also are #-additive.
In the language we merely introduce a notational device for distinguishing the singular
and plural arguments. We allow annotating the sorts in the profiles of the operation by a
superscript, like S * , to indicate that an argument is plural.
Furthermore, we partition the set of variables into two disjoint subsets of singular, X,
and plural, X * , variables. x and x * are to be understood as distinct symbols. We will say that
an operation f is singular in the i-th argument iff the i-th argument (in its signature) is
singular. The specification language extended with such annotations of the signatures will be
referred to as L * .
These are the only extensions of the language we need. We may, optionally, use
superscripts t * at any (sub)term to indicate that it is passed as a plural argument. The
outermost applications, e.g. f in f(.), are always to be understood plurally, and no
superscripting will be used at such places.
Definition 5.7. Let ( be a L * -signature. A is a (-power structure, A#PStr((), iff A is a
(deterministic) structure such that:
1. for every sort S, the carrier S A is a (subset of the) power set P
of some basis
set S -
2. for every f: S 1 -S n #S in (, f A is a # -monotonic function S 1
A
A
#S A such
that, if the i-th argument is S i (singular) then f A is singular in the i-th argument.
The singularity in the i-th argument in this definition refers not to the syntactic notion but
to its semantic counterpart:
Definition 5.8. A function f A
A
A
#S A in a power structure A is singular in the
i-th argument iff if it is #-additive in the i-th argument, i.e., iff for all x i #S i
A and all
A (for k-i), f A (.x 1 .x i .x n
Thus, the definition of power structures requires that syntactic singularity be modeled b y
the semantic one.
Note the unorthodox point in the definition - we do not require the carrier to be the
whole power set, but allow it to be a subset of some power set. Usually one assumes a
primitive nondeterministic operation with the predefined semantics as set union. Then all
finite subsets are needed for the interpretation of this primitive operator. Also, the join
operation (under the set inclusion as partial order) corresponds exactly to set union only if
all sets are present (see example 6.18). None of these assumptions seem necessary.
Consequently, we do not assume any predefined (choice) operation but, instead, give the
user means of specifying any nondeterministic operation (including choice) directly.
Let ( be a signature, A a (-power structure, X a set of singular and X * a set of plural
variables, and b an assignment X#X *
# _A_ such that for all x#X (Saying
"assignment" we will from now on mean only assignments satisfying this last condition.)
Then, every term t(x,x * )#W (,X,X * has a unique set interpretation b[t(x,x * )] in A defined as
t A (b(x),b(x * )).
Definition 5.9 (Satisfiability). Let A be a (-power structure and p: t i as i a
be a sequent over L * ((,X,X * ). A satisfies p, A-p, iff for every assignment b:
# _A_, we have that:
A is a power model of the specification SP=((,P), A#PMod(SP), iff A#PStr(() and A
satisfies all axioms from P.
Except for the change in the notion of an assignment, this is identical to the definition 4.4,
which is the reason for retaining the same notation for the satisfiability relation.
Singular and Plural Nondeterministic Parameters5.2. The calculus for plural parameters
The calculus NEQ is extended with one additional rule:
R8: G D
G D
a
a
x
x

Rules R1-R7 remain unchanged, but now all terms t i belong to W (,X,X * . In particular, any t i
may be a plural variable. We let NEQ * denote the calculus NEQ+R8.
The new rule R8 expresses the semantics of plural variables. It allows us to substitute an
arbitrary term t for a plural variable x * . Taking t to be a singular variable x, we can thus
exchange plural variables in a provable sequent p with singular ones. The opposite is, in
general, not possible because rule applies only to singular variables. For instance, a
plural variable x * will satisfy a x *
#x * but this is not sufficient for performing a general
substitution for a singular variable. The main result concerning PMod and NEQ * is:
Theorem 5.10. For any L * -specification SP and L * (SP) sequent p:
Proof idea:
The proof is a straightforward extension of the proof of theorem 4.5.
6. Comparison
Since plural and singular semantics are certainly not one and the same thing, it may seem
surprising that essentially the same calculus can be used for reasoning about both. One
would perhaps expect that PMod, being a richer class than MMod, will satisfy fewer formulae
than the latter, and that some additional restrictions of the calculus would be needed to
reflect the increased generality of the model class. In this section we describe precisely the
relation between the L and L * specifications (6.1) and emphasize some points of difference
(6.2).
6.1. The "equivalence" of both semantics
The following example illustrates a strong sense of equivalence of L and L * .
Example 6.11
Consider the following plural definition:
a
It is "equivalent" to the collection of definitions
a f(t) # if t=t then 0 else 1
for all terms t.
In the rest of this section we will clarify the meaning of this "equivalence".
Since the partial order of functions from a set A to the power set of a set B is isomorphic
to the partial order of additive (and strict, if we take P (all subsets) instead of
from the power set of A to the power set of B, [A#P(B)] # [P(A) # P(B)], we may consider
every multistructure A to be a power structure A * by taking _A * extending all
operations in A pointwise. We then have the obvious
Lemma 6.12. Let SP be a singular specification (i.e., all operations are singular in all
arguments), let A#MStr(SP), and p be a sequent in L(SP). Then A-p iff A * -p, and so
#PMod(SP).
Call an L * sequent p p-ground (for plurally ground) if it does not contain any plural
variables.
Theorem 6.13. Let SP * ,P * ) be an L * specification. There exists a (usually infinite)
specification SP=((,P) such that
1.
2. for any p-ground p#L * (SP * ) . PMod(SP * )-p iff MMod(SP)-p.
Proof:
Let ( be ( * with all " * " symbols removed. This makes 1. true. Any p-ground p as in 2.
is then a p over the language L((,X).
The axioms P are obtained from P * as in the example 6.11. For every p *
#P * with
plural variables x 1

Obviously, for any p#L(SP) if P# NEQ p then P *
then the proof
can be simulated in NEQ. Let p9(x * ) be the last sequent used in the NEQ * -proof which
contains plural variables x * , and the sequent p9 be the next one obtained by R8.
Build the analogous NEQ-proof tree with all plural variables replaced by the terms
which occupy their place in p9. The leaves of this tree will be instances of the P *
axioms with plural variables replaced by the appropriate terms, and all such axioms
are in P.
Then soundness and completness of NEQ and NEQ * imply the conclusion of the
theorem.
Singular and Plural Nondeterministic ParametersWe now ask whether, or under which conditions, the classes PMod and MMod are
interchangeable as the models of a specification. Let SP * , SP be as in the theorem. The one
way transition is trivial. Axioms of SP are p-ground so PMod(SP * ) will satisfy all these axioms
by the theorem. The subclass #PMod(SP * )#PMod(SP * ) where, for every P#PMod(SP * ), all
operations are singular, will yield a subclass of MMod(SP).
For the other direction, we have to observe that the restriction to p-ground sequents in
the theorem is crucial because plural variables range over arbitrary - also undenotable -
sets. Let MMod * (SP) denote the class of power structures obtained as in lemma 6.12. It is not
necessarily the case that MMod * (SP)-P * as the following argument illustrates.
Example 6.14
Let M *
#MMod * (SP) have infinite carrier, p *
#P * be t i as i a
and let b: X#X *
# _M * _ be an assignment such that b(x * )={m 1 .m l .} is a set which is
not denoted by any term in W (,X . Let b l be an assignment equal to b except that
b l (x * )={m l }, i.e., b=U
l
b l . Then
(a) M * - U
l
l
b l [s l
l
l
l
l
since operations in M * are defined by pointwise extension. M *
#MMod * (SP) implies
that, for all l
But (b) does not necessarily imply (a). In particular, even if for all l, all intersections
in the antecedent of (b) are empty, those in (a) may be non-empty. So we are not
guaranteed that M *
#PMod(SP * ).
Thus, the intuition that the multimodels are contained in the power models is not quite
correct. To ensure that no undenotable sets from M * can be assigned to the plural variables
we redefine the lifting operator * : MMod(SP)# PMod(SP) from 6.12.
Definition 6.15. Given a singular specification SP, and M#MMod(SP), we denote b y
-M the following power structure
is such that
a) for every n#_M_: {n}#_-M_,
b) for every m#_-M_ there exist a t#W (,X , n#_M_, such
2) the operations in -M can be then defined by: f(m)
Then, for any assignment b: X *
#_-M_ there exists an assignment u: X *
(1b), and an
assignment a: X#_M_ (1a) such that b(x * i.e., such that the following diagram
commutes:
x * -M
a
x
Since M#MMod(SP) it satisfies all the axioms P obtained from P * and the commutativity of
the diagram gives us the second part of:
Corollary 6.16. Let SP * and SP be as in the theorem 6.13. Then
The corollary makes precise the claim that the class of power models of a plural specification
SP * may be seen as a class of multimodels of some singular specification SP, and vice versa.
The reasoning about both semantics is essentially the same because the only difference
concerns the (arbitrary) undenotable sets which can be referred to by plural variables.
6.2. Plural specification of choice
Plural variables provide access to arbitrary sets. In the following example we attempt to
utilize this fact to give a more concise form to the specification of choice.
Example 6.17
The specification
S: { S }
F: { #._ : S *
P: { a#.x *
#x * }
defines #. as the choice operator - for any argument t, #.t is capable of returning
any element belonging to the set interpreting t.
The specification may seem plausible but there are several difficulties. Obviously, such a
Singular and Plural Nondeterministic Parameterschoice operation would be redundant in any specification since the axiom makes #.t
observationally equivalent to t, and lemma 4.6 allows us to remove any occurrences of #.
from the (derivable) formulae. Furthermore, observe how such a specification confuses the
issue of nondeterministic choice. Choice is supposed to take a set as an argument and return
one element from the set, or, perhaps, to convert an argument of type "set" to a result of type
"individual". This is the intention of writing the specification above. But power algebras
model all operations as functions between power sets and such a "conversion" simply does
not make sense. The only points where conversion of a set to an individual takes place is
when a term is passed as a singular argument to another operation. If we have an operation
with a singular argument f: S#S, then f(t) will make (implicitly) the choice from t.
This might be particularly confusing because one tends to think of plural arguments as
sets and mix up the semantic sets (i.e., the elements of the carrier of a power algebra) and the
syntactic ones (as expressed by the profiles of the operations in the signature). As a matter
of fact, the above specification does not at all express the intention of choosing an element
from the set. In order to do that it would have to give choice the signature Set(S)#S.
Semantically, this would be then a function from P + (Set(S)) to P Assuming that
semantics of Set(S) will somehow correspond to the power set construction, this makes
things rather complicated, forcing us to work with a power set of a power set. Furthermore,
since Set(S) and S are different sorts we cannot let the same variable range over both as was
done in the example above.
The above example and remarks illustrate some of the problems with the intuitive
understanding of plural parameters. Power algebras - needed for modelling such parameters
significantly complicate the model of nondeterminism as compared to multialgebras.
On the other hand, plural variables allow us to specify the "upper bound" of
nondeterministic choice without using disjunction. The choice operation can be specified as
the join which under the partial ordering # interpreted as set inclusion will correspond to
set union (cf. [17]).
Example 6.18
The following specification makes binary choice the join operation wrt. # :
S: { S }
F: { _#_ : S-S # S }
P: { 1. a x *
#y * a y *
#y *
2. xaz * , yaz * a x#y # z * }
Axiom 2, although using singular variables x, y, does specify the minimality of # with
respect to all terms. (Notice that the axiom x * az * , y * az * a x *
#y *
# z * would have a different,
and in this context unintended, meaning.) We can show that whenever a t#p and a s#p
hold (for arbitrary terms) then so does a t#s#p.
x z z z
x
a a
a a
a

a
a
a
a
a
a a
a
a
a
Violating our formalism a bit, we may say that the above proof shows the validity of the
formula stating the expected minimality of join: t#p, s#p a t#s#p.
Thus, in any model of the specification from 6.18 # will be a join. It is then natural to
consider # as the basic (primitive) operation used for defining other nondeterministic
operations. Observe also that in order to ensure that join is the same as set union, we have
to require the presence of all (finite) subsets in the carrier of the model. For instance, the
power structure A with the carrier
{ {1},{2},{3},{1,2,3} } and
# A defined as x A
will be a model of the specification although # A is not the same as set union.
7. Conclusion
We have defined the algebraic semantics for singular (call-time-choice) and plural (run-time-
choice) passing of nondeterministic parameters. One of the central results reported in the
paper is soundness and completeness of two new reasoning systems, NEQ and NEQ * ,
respectively, for singular and plural semantics. The plural calculus NEQ * is a minimal
extension of NEQ which merely allows unrestricted substitution for plural variables. This
indicated a close relationship between the two semantics. We have shown that plural
specifications have equivalent (modulo undenotable sets) singular formulations if one
considers the plural axioms as singular axiom schemata.

Acknowledgments

We are grateful to Manfred Broy for pointing out the inadequacy of our original notation and
to Peter D. Mosses for the observation that in the presence of plural variables choice may be
specified as join with Horn formulae.



--R

"Algebra of communicating processes"
"Nondeterministic call by need is neither lazy nor by name"
A Discipline of Programming
Fundamentals of Algebraic Specification
"IO and OI. 1"
"IO and OI. 2"
"Completeness of Many-Sorted Equational Logic"
"The semantics of call-by-value and call-by-name in a nondeterministic environment"


Nondeterminism in Algebraic Specifications and Algebraic Programs
"Rewriting with a Nondeterministic Choice Operator"
Towards a theory of abstract data types
"An Abstract Axiomatization of Pointer Types"
"Conditional rewriting logic as a unified model of concurrency"
Calculi for Communicating Systems
"Unified Algebras and Institutions"
Introducing Girard's quantitative domains
"Domains"

"An axiomatic treatment of ALGOL 68 routines"
"Power domains"
"Nondeterminism in Abstract Data Types"
Algebraic Specifications of Nondeterminism

"An introduction to event structures"
"Algebraic Specification"
--TR
many-sorted algebra;sequent calculus;nondeterminism;algebraic specification