Почему это правило Пролога не входит в бесконечный цикл?

Question

У меня есть следующие факты и правила:

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

Для запроса two(Y,X). Я получаю такой результат:

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

Я не понимаю, почему результаты Y=s и X=t.Почему Пролог не входит бесконечно много раз в \+two(Y,X)?Помнит ли Пролог, какие предикаты уже были обработаны?

Answer 1

У вас определены следующие предикаты:

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

Предикат two(X,Y) эквивалентен

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).

, и это то, что вы получаете.

Answer 2

Это успешно, потому что Пролог использует отрицание как конечный сбой .

Если мы оценим предикат Пролога, мы увидим, что:

[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 .

Итак, во-первых "path ", который терпит неудачу X и Y, оба установлены в s:

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

Но затем мы возвращаемся назад по вызову one(Y), и мы получаем:

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).

Теперь \+ p(X, Y) считается true, учитывая, что p(X, Y) не может быть удовлетворено, и застревает в бесконечном цикле.Таким образом, мы называем two(t, s), и это терпит неудачу, так как:

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

Таким образом, three(t) терпит неудачу, и, поскольку здесь нет возможностей для возврата, two(t, s), таким образом, заканчивается.Таким образом, это означает, что two(t, s) имеет конечный сбой, следовательно, \+ two(t, s) успешно, и, таким образом, two(X, Y) успешно с X = s, Y = t.