The Intuition behind Stratified Programs

Before considering the full well-founded semantics, we discuss how XSB can be used to evaluate programs with stratified negation. Intuitively, a program uses stratified negation whenever there is no recursion through negation. Indeed, most programmers, most of the time, use stratified negation.

Exercise 5.3.1   The program

         win(X):- move(X,Y),tnot(win(Y)).

is stratified when the move/2 relation is a binary tree. This can be seen by loading the file $XSB_DIR/examples/tree1k.P along with table_examples.P and typing the query

         ?- win(1).

win(1) calls win(2) through negation, win(2) calls win(4) through negation, and so on, but no subgoal ever calls itself recursively through negation.

The previous example of win/1 over a binary tree is a simple instance of a stratified program, but it does not even require tabling. A more complex example is presented below.

Exercise 5.3.2   Consider the query ?- lrd_s to the following program

lrd_p:- lrd_q,tnot(lrd_r),tnot(lrd_s).
lrd_q:- lrd_r,tnot(lrd_p).
lrd_r:- lrd_p,tnot(lrd_q).
lrd_s:- tnot(lrd_p),tnot(lrd_q),tnot(lrd_r).

Should lrd_s be true or false? Try it in XSB. Using the intuitive definition of ``stratified'' as not using recursion through negation, is this program stratified? Would the program still be stratified if the order of the literals in the body of clauses for lrd_p, lrd_q, or lrd_r were changed?

The rules for p, q and r are involved in a positive loop, and no answers are ever produced. Each of these atoms can be failed, thereby proving s. Exercise 5.3.2 thus illustrates an instance of how tabling differs from Prolog in executing stratified programs since Prolog would not fail finitely for this program.