If v is a variable and is a rule, then the following expression is
a rule with main existential variable v and body
:
import v
endimport
In the usual and obvious way define which occurrences of variables are free and which are bound. Call a rule perspicuous if no variable has both bound and free occurrences, and no bound variable is declared more than once. (The latter means here that different occurrences of the import command have different main existential variables.)
Let Free(R) be the set of free variables of a rule R.
In other words, Free(R)
is the set of variables v such that v occurs freely in rule
R. Define Bound(R)
similarly. If R is an import rule with main
existential variable v and body , we have:
Free(R) = Free(
) - {v},
and
Bound(R) = Bound(
)
{v}.