swi-prolog doesn't stop after first true with disjunction (or)

Question

I (Prolog absolute beginner) try to make sense out of prolog. Here's a Santa example in swi-prolog:

gives(santa,leonard,book).
gives(santa,adrian,game).
gives(santa,adrian,smartmax).

likes(leonard,lego).
likes(adrian,lego).
likes(adrian,book).

age(leonard,6).
age(adrian,4).

jealous(C1,C2) :- aggregate_all(count, gives(santa,C1,X), N1), 
  aggregate_all(count, gives(santa,C2,X), N2),
  N1 < N2,
  true.

jealous(C1,C2) :- findall(G, 
    (owns(C2,G), 
     likes(C1,G), 
     not(owns(C1,G))
    ), 
    Gifts),
  length(Gifts,NGifts),
  NGifts > 0,
  true.

This works as expected:

?- jealous(adrian,leonard).
true.

However, when I reverse the order of the two jealous-predicates in the code:

?- jealous(adrian,leonard).
true ;
false.

That's pretty weird: I thought the jealous-clauses would behave as an 'or': whenever one of the results is true, there shouldn't be any further processing. So I'm wondering: how to I make this so that it really behaves as an 'or': if any of the jealous-rules is true, it should return true, in all other cases, it's false. I don't want 'the next results'. I need only 1 result: true or false.

What am I doing wrong? (Probably a few things, so please, enlighten me :) ).

Thx.

Answer 1

With the clauses as ordered, Prolog's search attempts first to match the first clause:

jealous(C1,C2) :- aggregate_all(count, gives(santa,C1,X), N1), 
  aggregate_all(count, gives(santa,C2,X), N2),
  N1 < N2.
  % the final true is unnecessary

that clause counts that adrian has 2 gifts and leonard 1, therefore N1 < N2, it fails here. Prolog backtracks, the whole clause fails and the algorithm attempts the second one, which succeeds:

?- jealous(adrian,leonard).
true.

At this point all clauses have been attempted, there is no other alternative path to try to resolve the query and so it ends here.

If the clauses are reversed, the successful one is tried first, and the resolution given:

?- jealous(adrian,leonard).
true

But a second clause exists which hasn't been tried yet, and so the search algorithm offers you the option of returning to exhaust this second option. Which you do:

;
false.

The second clause is attempted and fails as before, but it does so after the first has already resolved the query.

The difference in behaviour is also due to how the algorithm optimises its record of choice points. Backtracking is resource intensive, and Prolog algorithms optimise this by discarding deterministic solutions from the stack of choice points. That is, if there is a statement somewhere

NGifts > 0

clearly if NGifts is known there's only one possible solution (doesn't matter which), and backtracking at this point will not return with an alternative proof. So this statement is discarded from the choice stack as it is deterministic - its only solution has been explored.

When the clauses are ordered as in your questions, by the time both have been investigated and the solution is given, there is no choice point in the stack and the theorem prover exits. But if you swap them, a solution is found in the first clause before the second is attempted, therefore the existence of a second jealous clause leaves a choice point to explore, which is proposed to you.

If you need to control this behaviour, and do not need to identify cases where little boys are doubly jealous of each other, you can force Prolog to 'cut' out choice points:

jealous(C1,C2) :-
  findall(G, 
    (owns(C2,G), 
     likes(C1,G), 
     not(owns(C1,G))
    ), 
    Gifts),
  length(Gifts,NGifts),
  NGifts > 0,
  !. % cut: if this clause gets so far, later clauses do not need to be explored

jealous(C1,C2) :-
  aggregate_all(count, gives(santa,C1,X), N1), 
  aggregate_all(count, gives(santa,C2,X), N2),
  N1 < N2.

Which makes the behaviour of both programs identical in this example. I leave the 'be careful with cuts' discussion to comments and other questions.