Пролог не дает мне решения, когда он существует

Question

Я работаю через Семь языков за семь недель, но есть кое-что, чего я не понимаю в прологе. У меня есть следующая программа (в зависимости от их программы Wallace и Grommit):

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

и загрузить это так

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

но это не дает мне никаких решений для следующего

?- teamMate(a, X).
false.

это может решить более простые вещи (что показано в книге):

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

и есть решения:

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

Что мне не хватает? Я пробовал как с GNU пролог и Swipl.

... И ЕЩЕ БОЛЬШЕ...

когда вы перемещаете ограничение "не может быть вашим собственным товарищем по команде", то оно заканчивается:

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

это дает мне решения, которые я ожидал:

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

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

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

Что дает?

Answer 1

Ответ от mat дает вам некоторые соображения высокого уровня и решение. Мой ответ больше о причинах, которые могут или не могут быть вам интересны.

(Кстати, изучая Пролог, я задал почти тот же вопрос и получил очень похожий ответ от того же пользователя. Отлично.)

Дерево доказательства

У вас есть вопрос:

Товарищи по команде двух игроков?

Чтобы получить ответ от Пролога, вы сформулируете запрос:

?- team_mate(X, Y).

где X и Y могут быть свободными переменными или связанными.

Основываясь на вашей базе данных о предикатах (фактах и ​​правилах), Пролог пытается найти доказательства и предлагает вам решения. Пролог ищет доказательства, выполняя обход дерева доказательств в глубину.

В вашей первой реализации, \+ (X = Y) предшествует чему-либо еще, поэтому он находится в корневом узле дерева и будет оцениваться до достижения следующих целей. И если либо X или же Y свободная переменная, X = Y должен преуспеть, что означает, что \+ (X = Y) должен потерпеть неудачу. Таким образом, запрос должен потерпеть неудачу.

С другой стороны, если либо X или же Y свободная переменная, dif(X, Y) будет успешным, но более поздняя попытка объединить их друг с другом не удастся. В этот момент Прологу придется искать доказательство в другой ветви дерева доказательств, если они еще остались.

(Имея в виду дерево доказательств, попробуйте найти способ реализации dif/2 Вы думаете, что это возможно без а) добавления какого-либо состояния к аргументам dif/2 или б) изменение стратегии разрешения?)

И, наконец, если вы положите \+ (X = Y) в самом конце, и позаботьтесь о том, чтобы оба X а также Y к моменту его оценки, тогда объединение становится больше похожим на простое сравнение, и оно может потерпеть неудачу, так что отрицание может быть успешным.

Answer 2

Вы сделали очень хорошее наблюдение! На самом деле ситуация еще хуже, потому что даже самый общий запрос не выполняется:

? - teamMate (X, Y).
ложь

Декларативно, это означает, что "решений вообще не существует", что, очевидно, неверно, а не то, как мы ожидаем, что отношения будут вести себя: если есть решения, то более общие запросы не должны завершаться неудачей.

Причина, по которой вы получаете это странное и логически некорректное поведение, заключается в том, что (\+)/1 Это только звук, если его аргументы достаточно созданы.

Чтобы выразить неравенство терминов в более общем виде, который работает правильно, независимо от того, созданы ли аргументы или нет, используйте dif/2 или, если ваша система Prolog не обеспечивает этого, безопасное приближение iso_dif/2 который вы можете найти в теге prolog-dif.

Например, в вашем случае (note_that_I_am_using_underscores_for_readability вместо tuckingTheNamesTogetherWhichMakesThemHarderToRead):

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

Ваш запрос теперь работает точно так, как ожидалось:

? - team_mate (a, X).
Х = б.

Конечно, самый общий запрос также работает правильно:

? - team_mate (X, Y).
Х = а,
Y = b;
X = b,
Y = а;
X = b,
Y = с;
и т.п.

Таким образом, используя dif/2 выражать неравенство сохраняет логическую чистоту ваших отношений: система больше не просто говорит false хотя есть решения. Вместо этого вы получите ожидаемый ответ! Обратите внимание, что, в отличие от ранее, это также работает независимо от того, где вы звоните!