Next: Duplication
Up: Qualified Choose Construct
Previous: Qualified Choose Construct
If U is a universe name different from Reserve, v is
a variable, g(v)
is a Boolean term and 
is a rule, then the following expression is a
rule with main existential variable v that ranges over U and
body :
choose v in U satisfying g(v)
endchoose
Replacing the choose constructor with the qualified choose constructor
requires only a small and obvious change in the semantical definition of
4.1.2. We restrict attention to the global choice approach. Consider the
case in the inductive definition of
Updates(R', S', 
)
where
R' is a
choose rule and the range U of the main existential variable
v of R in S' is not empty. If
g((v))
fails in
S, set
Updates(R', S', ) =
.
It is easy to construct a rule to choose several elements
, ...,
subject
to a condition g(, ...,
)
.
The qualified choose constructor may be too powerful. The decision problem
whether there is any tuple 
in the universe U satisfying the condition g may be hard. If U is the set of natural
numbers and g a polynomial, the decision problem may even be undecidable
[Mt]. But the logical clarity of the constructor is attractive. It may be
used in particular to reflect environmental forces that are not necessarily
algorithmic.