Previous topic  Top  Next topic  Print this Topic
 

Quantifier Scoping

 

The quantifiers FORALL and EXISTS introduce variables in rules and queries. Syntactically, variables like ?X or ?Y do not differ from constant symbols in ObjectLogic, hence the requirement for explicit declaration with quantifiers. In the unusual situation where there is a conflict between a used variable and an existing constant, it is important to know the scope, i.e. the lifetime of variables. To illustrate the notion of variable scopes we present an example formula where all variables are underlined and all constants are not.

p(?X,?Y) :- r(?X,?Y) AND (EXIST ?U q(?U,?Y)).

p(?X,?Y) :- (EXIST ?U q(?U,?Y) AND r(?U,?Y)).

p(?X,?Y) :- (EXIST ?U q(?U,?Y)) AND r(?U,?Y).

 

The rule-of-thumb is that each quantifiers binds variables till the end of the complete formula. You can overwrite this pattern only by introducing parenthesis and, thus, explicitly introducing a new scope for the quantifier. Note: the semantics of the first and third formula above is equivalent (the ?U in the r predicate is a constant), whereas formula two is different (here, the ?U in the r predicate is bound by the EXIST quantifier).