Next: Remark
Up: Semantics
Previous: Global Choice Semantics
The global choice semantics is straightforward. However, contrary to the
situation 3.2.4, there is no correlation among individual choices this time
around, and thus there is no real need for a global choice function 
.
It may be more elegant to define
= NUpdates(R,S)
directly by induction
on R . We suppose again that S is appropriate to R and R is
S -conspicuous.
If R is an update instruction then
= {Updates(R,S)}.
If R is a
sequence of rules 
, ...,
, then
.
Notice that is empty if some
NUpdates(
, S)
is empty.
If R is a conditional rule with clauses
(
,
), ... ,
(
,).
,
we
have two cases as usual; if all k+1
guards fail in S then
,
and if 
is the first guard that holds in S then
=
NUpdates(, S).
(It would be a mistake to replace 
with 
above.
If NUpdates(, S) =
then
NUpdates((,
), S) =
for every rule
, which is not
desired.)
Finally, suppose that R is a choose rule with universe name U , main
existential variable v and body . For each
a 
U,
let 
be
the expansion of S of the auxiliary vocabulary
Fun(S) 
{v}
where
v is interpreted as a . Then
=
{NUpdates(,
) :
a U}.
Notice that is empty if U is empty.
It is easy to check that if R contains no choice subrules
then NUpdates(R, S) = {Updates(R, S)}.