swi-prolog 在第一个 true 与析取（或）后不会停止

Question

我（Prolog 绝对初学者）尝试从 prolog 中理解。这是swi-prolog 中的圣诞老人示例：

gives(santa,leonard,book).
gives(santa,adrian,game).
gives(santa,adrian,smartmax).

likes(leonard,lego).
likes(adrian,lego).
likes(adrian,book).

age(leonard,6).
age(adrian,4).

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

jealous(C1,C2) :- findall(G, 
    (owns(C2,G), 
     likes(C1,G), 
     not(owns(C1,G))
    ), 
    Gifts),
  length(Gifts,NGifts),
  NGifts > 0,
  true.

这按预期工作：

?- jealous(adrian,leonard).
true.

但是，当我颠倒代码中两个jealous-predicates 的顺序时：

?- jealous(adrian,leonard).
true ;
false.

这很奇怪：我认为jealous-clauses 会表现为“或”：只要其中一个结果为真，就不应该进行任何进一步的处理。 所以我想知道：如何制作它以使其真正表现为“或”：如果jealous-规则中的任何一个为真，它应该返回true，在所有其他情况下，它是false .我不想要“下一个结果”。我只需要 1 个结果：true 或 false。

我做错了什么？ （可能有几件事，所以请赐教:)）。

谢谢。

Answer 1

按照顺序排列的子句，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

该子句认为 adrian 有 2 个礼物和 leonard 1，因此 N1

?- jealous(adrian,leonard).
true.

此时已尝试所有子句，没有其他替代路径可以尝试解析查询，因此到此结束。

如果子句颠倒，则先尝试成功的，给出的解决方法：

?- jealous(adrian,leonard).
true

但存在第二个子句，但尚未尝试过，因此搜索算法为您提供了返回以耗尽第二个选项的选项。你做什么：

;
false.

尝试第二个子句并像以前一样失败，但它在第一个子句已经解决了查询之后才这样做。

行为上的差异还取决于算法如何优化其选择点记录。回溯是资源密集型的，Prolog 算法通过从选择点堆栈中丢弃确定性解决方案来优化这一点。也就是说，如果某处有语句

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.

这使得本例中两个程序的行为相同。我将“小心削减”的讨论留给 cmets 和其他问题。