Next: Transition Rules: Semantics
Up: Importing New Elements
Previous: The Import Constructor
The names of variables are different from function names of course, but it
is convenient to treat free variables of rules as auxiliary nullary
functions (which cannot be subjects of update instructions). An
auxiliary vocabulary has the form
V,
where is a
genuine vocabulary and V is a finite set of variables.
If S is a state of an auxiliary vocabulary
' =
V, then
Fun(S) = '.
S is appropriate for a rule R if contains all function names of R and V contains all free variables of
R . R is S -perspicuous if it is perspicuous and its bound
variables do not occur in V .