How come this Prolog rule doesn't go into a infinity loop?

2
votes

I have following facts and rules:

one(s).
one(t).
two(X,Y) :- one(X), one(Y), three(X), \+three(Y), \+two(Y,X).
three(s).

For the query two(Y,X). I get this result:

?- two(Y,X).
Y = s,
X = t ;
false.

I don't understand why the results are Y=s and X=t. Why does Prolog don't go infinitely many times into \+two(Y,X)? Does Prolog remember which predicates have already been processed?

2
prolog
There is only one way for one(X), one(Y), three(X) to succeed, which is X = s and Y = t. Then \+ three(Y) succeeds since three(t) fails, and \+ two(Y,X) succeeds because two(t,s) fails. In short, two(Y,X) has only one solution, which is the one your query shows. Prolog doesn't call \+ two(Y,X) infinitely many times because there aren't infinitely many choices for a possible solution. - lurker
Exactly what @lurker says. Note that something like two(X, Y) :- \+ two(Y, X), ... would produce an infinite loop. But because you have constrained what X and Y can be prior to the recursion, it won’t. - Daniel Lyons
You can use trace. to see how Prolog obtains a certain result. - Willem Van Onsem
I think I got it now. Thanks for the help @ all. - JumbleGee

2 Answers

1
votes

This succeeds because Prolog uses negation as finite failure.

If we evaluate the Prolog predicate, we see that:

[trace]  ?- two(X, Y).
   Call: (8) two(_660, _662) ? creep
   Call: (9) one(_660) ? creep
   Exit: (9) one(s) ? creep
   Call: (9) one(_662) ? creep
   Exit: (9) one(s) ? creep
   Call: (9) three(s) ? creep
   Exit: (9) three(s) ? creep
   Call: (9) three(s) ? creep
   Exit: (9) three(s) ? creep
   Redo: (9) one(_662) ? creep
   Exit: (9) one(t) ? creep
   Call: (9) three(s) ? creep
   Exit: (9) three(s) ? creep
   Call: (9) three(t) ? creep
   Fail: (9) three(t) ? creep
   Redo: (8) two(s, t) ? creep
   Call: (9) two(t, s) ? creep
   Call: (10) one(t) ? creep
   Exit: (10) one(t) ? creep
   Call: (10) one(s) ? creep
   Exit: (10) one(s) ? creep
   Call: (10) three(t) ? creep
   Fail: (10) three(t) ? creep
   Fail: (9) two(t, s) ? creep
   Redo: (8) two(s, t) ? creep
   Exit: (8) two(s, t) ? creep
X = s,
Y = t .

So in a first "path" that fails X and Y are both set to s:

two(X,Y) :-
    one(X),     %% X = s
    one(Y),     %% Y = s
    three(X),   %% X = s
    \+three(Y), %% Y = s, fail
    \+two(Y,X).

But then we backtrack over the one(Y) call, and we obtain:

two(X,Y) :-
    one(X),     %% X = s
    one(Y),     %% Y = t
    three(X),   %% X = s
    \+three(Y), %% Y = t
    \+two(Y,X)  %% call two(t, s).

Now \+ p(X, Y) is considered true, given p(X, Y) can not be satisfied, and gets stuck in an infinite loop. We thus call two(t, s), and this fails, since:

two(t,s) :-
    one(t),     %% succeeds
    one(s),     %% succeeds
    three(t),   %% fails
    \+three(s), %% 
    \+two(s,t)  %%

So three(t) fails, and since there are no backtracking opportunities here, two(t, s) thus ends. So that means that two(t, s) has finite failure, hence \+ two(t, s) succeeds, and thus two(X, Y) succeeds with X = s, Y = t.

1
votes

You have the following predicates defined:

one(s).
one(t).
two(X,Y) :- one(X), one(Y), three(X), \+three(Y), \+two(Y,X).
three(s).

The predicate two(X,Y) is equivalent to

two(X,Y) :- (X=s ; X=t), (Y=s ; Y=t), (X=s), \+(Y=s), \+two(Y,X).
=
two(X,Y) :- (X=s, (Y=s ; Y=t), X=s ; X=t, (Y=s ; Y=t), X=s), \+(Y=s), \+two(Y,X).
=
two(X,Y) :- (X=s, (Y=s ; Y=t), s=s ; X=t, (Y=s ; Y=t), t=s), \+(Y=s), \+two(Y,X).
=
two(X,Y) :- (X=s, (Y=s ; Y=t) ; false), \+(Y=s), \+two(Y,X).
=
two(X,Y) :- ((X=s, Y=s ; false), \+(Y=s) ; (X=s, Y=t ; false), \+(Y=s)), \+two(Y,X).
=
two(X,Y) :- ((X=s, Y=s ; false), \+(s=s) ; (X=s, Y=t ; false), \+(t=s)), \+two(Y,X).
=
two(X,Y) :- (X=s, Y=t ; false), true, \+two(Y,X).
=
two(X,Y) :- (X=s, Y=t, \+two(Y,X) ; false).
=
two(s,t) :- (true, \+two(t,s) ; false).
=
two(s,t) :- (true ; false).

and that's what you're getting.