swi-prolog не останавливается после первого истины с дизъюнкцией (или)

При таком порядке предложений поиск Prolog пытается сначала сопоставить первое предложение:

jealous(C1,C2) :- aggregate_all(count, gives(santa,C1,X), N1), 
  aggregate_all(count, gives(santa,C2,X), N2),
  N1 < N2.
  % the final true is unnecessary

в этом предложении считается, что у Адриана 2 дара, а у Леонарда 1, поэтому N1 ‹N2, здесь он не работает. Prolog выполняет возврат, все предложение не выполняется, и алгоритм пытается выполнить второе, которое завершается успешно:

?- jealous(adrian,leonard).
true.

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

Если пункты поменяны местами, сначала проверяется успешный вариант, и дается разрешение:

?- jealous(adrian,leonard).
true

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

;
false.

Второе предложение выполняется и терпит неудачу, как и раньше, но делает это после того, как первое уже разрешило запрос.

Различие в поведении также связано с тем, как алгоритм оптимизирует запись точек выбора. Отслеживание с возвратом требует значительных ресурсов, и алгоритмы Пролога оптимизируют его, отбрасывая детерминированные решения из стека точек выбора. То есть, если где-то есть утверждение

NGifts > 0

ясно, что если известно о NGifts, существует только одно возможное решение (неважно какое), и возврат в этот момент не вернется с альтернативным доказательством. Таким образом, этот оператор исключен из стека выбора, поскольку он детерминирован - его единственное решение было изучено.

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

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

jealous(C1,C2) :-
  findall(G, 
    (owns(C2,G), 
     likes(C1,G), 
     not(owns(C1,G))
    ), 
    Gifts),
  length(Gifts,NGifts),
  NGifts > 0,
  !. % cut: if this clause gets so far, later clauses do not need to be explored

jealous(C1,C2) :-
  aggregate_all(count, gives(santa,C1,X), N1), 
  aggregate_all(count, gives(santa,C2,X), N2),
  N1 < N2.

Это делает поведение обеих программ идентичным в этом примере. Я оставляю обсуждение «будьте осторожны с сокращениями» для комментариев и других вопросов.