prolog doesn't give me a solution when one exists

Question

I am working through Seven Languages in Seven Weeks, but there is something I don't understand about prolog. I have the following program (based on their wallace and grommit program):

/* teams.pl */

onTeam(a, aTeam).
onTeam(b, aTeam).
onTeam(b, superTeam).
onTeam(c, superTeam).

teamMate(X, Y) :- \+(X = Y), onTeam(X, Z), onTeam(Y, Z).

and load it like this

?- ['teams.pl'].
true.

but it doesn't give me any solutions to the following

?- teamMate(a, X).
false.

it can solve simpler stuff (which is shown in the book):

?- onTeam(b, X).
X = aTeam ;
X = superTeam.

and there are solutions:

?- teamMate(a, b).
true ;
false.

What am I missing? I have tried with both gnu prolog and swipl.

...AND THERE IS MORE...

when you move the "can't be your own teammate" restriction to then end:

/* teams.pl */

onTeam(a, aTeam).
onTeam(b, aTeam).
onTeam(b, superTeam).
onTeam(c, superTeam).

teamMate(X, Y) :- onTeam(X, Z), onTeam(Y, Z), \+(X = Y).

it gives me the solutions I would expect:

?- ['teams.pl'].
true.

?- teamMate(a, X).
X = b.

?- teamMate(b, X).
X = a ;
X = c.

What gives?

Answer 1

The answer by mat gives you some high-level considerations and a solution. My answer is a more about the underlying reasons, which might or might not be interesting to you.

(By the way, while learning Prolog, I asked pretty much the same question and got a very similar answer by the same user. Great.)

The proof tree

You have a question:

Are two players team mates?

To get an answer from Prolog, you formulate a query:

?- team_mate(X, Y).

where both X and Y can be free variables or bound.

Based on your database of predicates (facts and rules), Prolog tries to find a proof and gives you solutions. Prolog searches for a proof by doing a depth-first traversal of a proof tree.

In your first implementation, \+ (X = Y) comes before anything else, so it at the root node of the tree, and will be evaluated before the following goals. And if either X or Y is a free variable, X = Y must succeed, which means that \+ (X = Y) must fail. So the query must fail.

On the other hand, if either X or Y is a free variable, dif(X, Y) will succeed, but a later attempt to unify them with each other must fail. At that point, Prolog will have to look for a proof down another branch of the proof tree, if there are any left.

(With the proof tree in mind, try to figure out a way of implementing dif/2: do you think it is possible without either a) adding some kind of state to the arguments of dif/2 or b) changing the resolution strategy?)

And finally, if you put \+ (X = Y) at the very end, and take care that both X and Y are ground by the time it is evaluated, then the unification becomes more like a simple comparison, and it can fail, so that the negation can succeed.

Answer 2

You have made a very good observation! In fact, the situation is even worse, because even the most general query fails:

?- teamMate(X, Y).
false.

Declaratively, this means "there are no solutions whatsoever", which is obviously wrong and not how we expect relations to behave: If there are solutions, then more general queries must not fail.

The reason you get this strange and logically incorrect behaviour is that (\+)/1 is only sound if its arguments are sufficiently instantiated.

To express disequality of terms in a more general way, which works correctly no matter if the arguments are instantiated or not, use dif/2, or, if your Prolog system does not provide it, the safe approximation iso_dif/2 which you can find in the prolog-dif tag.

For example, in your case (note_that_I_am_using_underscores_for_readability instead of tuckingTheNamesTogetherWhichMakesThemHarderToRead):

team_mate(X, Y) :- dif(X, Y), on_team(X, Z), on_team(Y, Z).

Your query now works exactly as expected:

?- team_mate(a, X).
X = b.

The most general query of course also works correctly:

?- team_mate(X, Y).
X = a,
Y = b ;
X = b,
Y = a ;
X = b,
Y = c ;
etc.

Thus, using dif/2 to express disequality preserves logical-purity of your relations: The system now no longer simply says false even though there are solutions. Instead, you get the answer you expect! Note that, in contrast to before, this also works no matter where you place the call!