The recursive definition of rules in 5.3 can be extended by import commands and/or (qualified) choice commands. The adjustment of the semantic definition is straightforward. For the sake of definiteness, consider the extension by means of the import constructor. The most important novelty, in comparison to 3.2.4, is that reserve elements have to be chosen for all combinations of the values of explicitly declared variables u such that the scope of the declaration of u properly includes the given import or choose subrule. For example, the rule
var u ranges over U
import v
Parent(v) := u
endimport
creates a new child for every element of U , and of course all these new children are different.
To reflect the novelty we redefine the domain of the global choice
function. Suppose that D is a variable declaration, R is a rule
covered by D , S is a state of an auxiliary vocabulary appropriate for
R , and R is (D,S) -perspicuous. For every bound variable v of R ,
list all explicitly declared variables u such that either u occurs in
D or u occurs in R and the scope of the declaration of u properly
includes the scope of the declaration of v : . (The
adverb properly is there to exclude v from the list.) Let
be the ranges of
in S respectively, and
be the
Cartesian product
. The
desired global function
assigns different reserve elements to every
pair
where
and
.
Here is a variant of the example from 3.2.5:
var u ranges over U extend Nodes with,
if Leaf(u) then FirstChild(u) :=