Query evaluation strategies

 

ConceptBase employs an SLDNF-style query evaluation method, i.e. query literals are evaluated top-down much like in standard Prolog. This is known to cause infinite loops for certain recursive rule sets. To overcome this, the SLDNF evaluator is augmented by a em caching sub-system which detects recursive predicate calls and answers them from the cached results of a query rather than entering an infinite loop. This cache-based evaluation computes the fixpoint (=answer) of a query provided that the overall rule set is stratified. Even more: also dynamically stratified rule sets are supported. Other than with the static stratification test, a violation is detected at run time of a query rather than at compile time.

For a precise definition of stratification, we refer you to the literature on deductive databases. For the purposes of this manual, consider the following rule:

forall p/Position (exists p1/Position (p moveTo p1) and not (p1 in Win)) 
  ==> (p in Win)

ConceptBase internally compiles such rules into a representation where Position, moveTo, and Win are predicate symbols:

forall p 
   (exists p1 Position(p) and Position(p1) and 
   moveTo(p,p1) and not Win(p1)) 
  ==> Win(p)

Static stratification requires that one can consistently assign stratification levels (=numbers) to the set of predicate symbols such that

1. If there is a rule with conclusion predicate A and positive condiction predicate B (=not negated), then the level of A must be greater or equal the level of B.
2. If there is a rule with conclusion predicate A and negated condiction predicate B , then the level of A must be strictly greater the level of B.

In the example above, the conclusion predicate Win depends on the condition predicate not Win. Since we only can assign one level to Win, we cannot find a static stratification for the above rule. The same argument also works in case of multiple inter-dependent rules. Static stratification can be tested at compile-time of a rule.

Dynamic stratification is an extension of static stratification, i.e. any statically stratified rule set is also dynamically stratified. It is not only considering predicate symbols but also the arguments with which a predicate is called at run-time. Obviously, this depends on the database state at a certain point of time. The global rule of dynamic stratification is that the answer to a predicate call A(x) may not depend on its negation not A(x). Such a clash can be detected by maintaining a stack of active predicate calls.

ConceptBase reports a violation of dynamic stratification in the log window of the CB client with a message ``STRATIFICATION VIOLATION`` indicating the predicate that participated in the violation. Three flavors of error messages can occur:

• STRATIFICATION_VIOLATION1 The evaluation of a predicate P leads to a cycle in which a negated predicate Q occurs. Hence, P depends on and Q depends on P. Consequently, P indirectly depends on its negation.
• STRATIFICATION_VIOLATION2 A predicate P (or ) is called while its negation (or P) is still being evaluated. Consequently, P ( , resp.) depends on its negation.
• STRATIFICATION_VIOLATION3 While evaluation a predicate the system derives that P would be true, i.e. the fact P is in the extension of the variable free predicate call P. This evaluation occurs in the context of a matching positive call P' where the system cannot prove that P would be in the extension. The matching call P' has the same arguments as P except for certain variable positions.

In practice, most rule sets are already statically stratified, i.e. no violation can occur regardless of the data in the database. Counter examples are in the CB-Forum (see http://conceptbase.cc) in the models Russel.sml and Win.sml. These examples are neither statically nor dynamically stratified. Note also the example WinNim.sml which uses the same query as Win.sml but is dynamically stratified. Even in the case of stratification violations, ConceptBase will display an answer to a query. The user can then decide which parts of the answer are usable. In principle, this decision can also be automated which is subject of future ConceptBase releases.

There is a second (legacy) query evaluation method, the magic set method. It is realized in ConceptBase but used only for internal purposes . The user may override the SLDNF query evaluation method for certain queries/rules by magic set method as follows:

QueryClass Q in Magic ...

Similar deductive rules can also be represented in the magic format. This is done by using the mrule instead of the rule category:

   ...
   mrule,rule
      myrule: $ forall ... $
        ...

Both representations can be mixed but one should notice that query classes and rules in SLDNF format don't have access to the magic set format of other queries and rules. Hence, this feature should only be used by experts who want to experiment with the (now outdated) magic set evaluation method of ConceptBase.