What am I missing about equality and unification in Prolog?

Question

I'm working through Clocksin and Mellish to try and finally go beyond just dabbling in Prolog. FWIW, I'm running SWI-Prolog:

SWI-Prolog version 7.2.3 for x86_64-linux

Anyway, I implemented a diff/2 predicate as part of exercise 1.4. The predicate is very simple:

diff(X,Y) :- X \== Y.

And it works when used in the sister_of predicate, like this:

sister_of(X,Y) :- 
    female(X),
    diff(X,Y),
    parents(X, Mum, Dad ),
    parents(Y, Mum, Dad ).

in that, assuming the necessary additional facts, doing this:

?- sister_of(alice,alice).

returns false as expected. But here's the rub. If I do this instead:

?- sister_of(alice, Who).

(again, given the additional facts necessary) I get

Who = edward ;

Who = alice;

false

Even though, as already shown, the sister_of predicate does not treat alice as her own sister.

On the other hand, if I use the SWI provided dif/2 predicate, then everything works the way I would naively expect.

Can anyone explain why this is happening this way, and why my diff implementation doesn't work the way I'm expecting, in the case where I ask for additional unifications from that query?

The entire source file I'm working with can be found here

Any help is much appreciated.

Answer 1

As you note, the problem stems from the interplay between equality (or rather, inequality) and unification. Observe that in your definition of sister_of, you first find a candidate value for X, then try to constrain Y to be different, but Y is still an uninstantiated logic variable and the check is always going to succeed, like diff(alice, Y) will. The following constraints, including the last one that gives a concrete value to Y, come too late.

In general, what you need to do is ensure that by the time you get to the inequality check all variables are instantiated. Negation is a non-logical feature of Prolog and therefore potentially dangerous, but checking whether two ground terms are not equal is safe.