Conditional Answers

Exercise 5.3.4   Consider the behavior of the win/1 predicate from Exercise 5.3.1.

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

when the when the move/2 relation is a cycle. Load the file $XSB_DIR/examplescycle1k.P into XSB and again type the query ?- win(1). Does the query succeed? Try tnot(win(1)).

Now query the table with the standard XSB predicate get_residual/2, e.g. ?- get_residual(win(1),X). Can you guess what is happening with this non-stratified program?

The predicate get_residual/2 (Section 6.12) unifies its first argument with a tabled subgoal and its second argument with the (possibly empty) delay list of that subgoal. The truth of the subgoal is taken to be conditional on the truth of the elements in the delay list. Thus win(1) is conditional on tnot(win(2)), win(2) in tnot(win(3)) and so on until win(1023) which is conditional on win(1).

From the perspective of the well-founded semantics, win(1) is undefined. Informally, true answers in the well-founded semantics are those that have a (tabled) derivation. False answers are those for which all possible derivations fail -- either finitely as in Prolog or by failing positive loops. win(1) fits in neither of these cases - there is no proof of win(1), yet it does not fail in the sense given above and is thus undefined.

However this explanation does not account for why undefined answers should be represented as conditional answers, or why a query with a conditional answer and its negation should both succeed. These features arise from the proof strategy of XSB, which we now examine in more detail.

Exercise 5.3.5   Consider the program

:- table simpl_p/1,simpl_r/0,simpl_s/0.
simpl_p(X):- tnot(simpl_s).

simpl_s:- tnot(simpl_r).
simpl_s:- simpl_p(X).

simpl_r:- tnot(simpl_s),simpl_r.

Is simpl_p(X) true for any X? Try the query ?- simpl_p(X) - be sure to backtrack through all possible answers. Now try the query again. What could possibly account for this behavior?

At this point, it is worthwhile to examine closely the evaluation of the program in Exercise 5.3.5. The query simpl_p(X) calls simpl_s and simpl_r and executes the portion of the program shown below in bold:

simpl_p(X):- tnot(simpl_s).

simpl_s:- tnot(simpl_r).

simpl_s:- simpl_p(X).

simpl_r:- tnot(simpl_s), simpl_r.

Based on evaluating only the bold literals, the three atoms are all undefined since they are neither proved true, nor fail. However if the evaluation could only look at the literal in italics, simpl_r, it would discover that simpl_r is involved in a positive loop and, since there is only one clause for simpl_r, the evaluation could conclude that the atom was false. This is exactly what XSB does, delays the evaluation of tnot(simpl_s) in the clause for simpl_r and looks ahead to the next literal in the body of that clause. This action of looking ahead of a negative literal is called delaying. A delayed literal is moved into the delay list of a current path of computation. Whenever an answer is derived, the delay list of the current path of computation is copied into the table. If the delay list is empty, the answer is unconditional; otherwise it is conditional. Of course, for definite programs any answers will be unconditional -- we therefore omited delay lists when discussing such programs.

In the above program, delaying occurs for the negative literals in clause for simpl_p(X), simpl_s, and simpl_r. In the first two cases, conditional answers can be derived, while in the third, simpl_r will fail as mentioned above. Delayed literals eventually become evaluated through simplification. Consider an answer of the form

simpl_p(X):- tnot(simpl_s)|

where the | is used to represent the end of the delay list. If, after the answer is copied into the table, simpl_s turns out to be false, (after being initially delayed), the answer can become unconditional. If simpl_s turns out to be true, the answer should be removed, it is false.

In fact, it is this last case that occurs in Exercise 5.3.5. The answer

simpl_p(X):- tnot(simpl_s)|

is derived, and returned to the user (XSB does not currently print out the delay list). The answr is then removed through simplification so that when the query is re-executed, the answer does not appear.

We will examine in detail how to alter the XSB interface so that evaluation of the well-founded semantics need not be confusing. It is worthwhile to note that the behavior just described is uncommon.

Version 2.2 of XSB handles dynamically stratified programs through delaying negative literals when it becomes necessary to look to their right in a clause, and then simplifying away the delayed literals when and if their truth value becomes known. However, to ensure efficiency, literals are never delayed unless the engine determines them to not to be stratified under the LRD-stratified evaluation method.