关于对称关系的 Prolog 重复解

Question

考虑这个小程序：

married(bill, hillary).
spouse(X, Y) :- married(X, Y); married(Y, X).
likes(X, Y) :- spouse(X, Y).

现在我想评估一个目标

?- likes(X, Y).
X = bill
Y = hillary ?;
X = hillary
Y = bill
yes 

有没有办法防止在回溯时重复这种对称关系，并且仍然保持目标的对称性?- likes(hillary, X).？

Answer 1

这是一种定义方法spouse/2：

married(bill, hillary).
married(tom, mary).
married(sam, linda).

spouse(X, Y) :-
     \+ married(X, Y) -> married(Y, X) ; married(X, Y).

否则，。married(X, Y)married(Y, X)married(X, Y)

| ?- spouse(X, Y).

X = bill
Y = hillary ? ;

X = tom
Y = mary ? ;

X = sam
Y = linda

(1 ms) yes
| ?- spouse(tom, Y).

X = tom
Y = mary

yes
| ?- spouse(X, tom).

X = mary
Y = tom

yes

从表面上看，以下稍微简单的谓词可能是等效的，但它不会找到所有的解决方案：

spouse(X, Y) :-
     married(X, Y) -> true ; married(Y, X).

| ?- spouse(X, Y).

X = bill
Y = hillary ? ;

(1 ms) yes
| ?-

附录

根据谢尔盖的观察：

| ?- Y = bill, spouse(X, Y).

X = hillary
Y = bill

yes

但：

| ?- spouse(X, Y), Y = bill.

no

这个结果是不一致的，因为通过限制spouse/2认为对称解冗余的唯一解，谓词本质上是说在任何给定时间只有 和 之一spouse(bill, hillary)可以spouse(hillary, bill)为真。如果第一个参数预定义为bill，则意味着第二个参数必须为hillary。如果两个参数都未实例化并spouse(X, Y)指示解X = bill和Y = hillary，则后续查询 会Y = bill失败。

因此，正如@Sergey 在他的评论中指出的那样，必须谨慎使用这种谓词，并理解其逻辑含义在某些情况下是有限的，甚至是自相矛盾的。