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

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

/* 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 prolog, так и с 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.

Что дает?


prolog prolog-dif logical-purity
person Alex028502    schedule 02.10.2016    source источник

Ответы (2)


arrow_upward
3
arrow_downward

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

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

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

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

Два игрока товарищи по команде?

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

?- team_mate(X, Y).

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

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

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

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

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

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

person Community    schedule 03.10.2016

arrow_upward
7
arrow_downward

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

?- teamMate(X, Y).
false.

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

Причина, по которой вы получаете это странное и логически неправильное поведение, заключается в том, что (\+)/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).
X = b.

Самый общий запрос конечно тоже работает корректно:

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

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

person mat    schedule 02.10.2016