different(Xs, Ys) :-
member(X, Xs),
non_member(X, Ys).
different(Xs, Ys) :-
member(Y, Ys),
non_member(Y, Xs).
虽然从声明的角度来看，这个定义使用member/2andnon_member/2几乎是1完美的，但它为某些查询产生了冗余的解决方案，并在周围留下了选择点。
什么是在此基础上改进的定义（以纯粹的方式可能使用if_/3and (=)/3）使得完全相同的一组解决方案被描述different/2但至少对于地面查询是确定的（因此不会留下任何无用的选择点）并省略（如果可能）任何多余的答案？
1
其实，different([a|nonlist],[]), different([],[b|nonlist])成功了。它同样可能失败。因此，两者都失败的解决方案很好（甚至更好）。
第一次尝试！
以下代码基于元谓词tfilter/3and tpartition/4、单调 if-then-else 控制结构if_/3、具体化一元逻辑连接词not_t/3和具体化术语相等谓词(=)/3：
different([],[_|_]).
different([X|Xs0],Ys0) :-
tpartition(=(X),Ys0,Es,Ys1),
if_(Es=[], true, (tfilter(not_t(=(X)),Xs0,Xs1),different(Xs1,Ys1))).
示例查询：
?- different([A,B],[X,Y]).
A=Y , dif(B,Y), X=Y
; A=X , B=X , dif(X,Y)
; A=X , dif(B,X), dif(B,Y), dif(X,Y)
; A=Y , B=Y , dif(X,Y)
; A=Y , dif(B,X), dif(B,Y), dif(X,Y)
; dif(A,X), dif(A,Y).
让我们在处理地面数据时观察确定性：
?- different([5,4],[1,2]).
true.
上述方法感觉像是朝着正确方向迈出的一步......但是，就目前而言，我不会称其为完美。
这是另一个尝试！我们利用单调 if-then-else 控制结构if_/3，结合具体化列表成员谓词memberd_t/3和第一个参数索引来避免创建无用的选择点。
different(Xs,Ys) :-
different_aux(Xs,Ys,Xs,Ys).
different_aux([],[_|_],Xs0,Ys0) :-
different_aux(Ys0,[],Ys0,Xs0). % swap Xs/Ys pair
different_aux([X|Xs],Ys,Xs0,Ys0) :-
if_(memberd_t(X,Ys0),
different_aux(Ys,Xs,Ys0,Xs0), % variant: different_aux(Xs,Ys,Xs0,Ys0)
true).
首先，我们运行一个预期会失败的查询：
?- different([1,2,3],[2,3,1]).
false.
以下查询类似于上面给出的失败查询；每个人都有一个“不同”的项目x放置在第一个[1,2,3]或第二个列表中的不同索引处[2,3,1]：
?- 不同的([ 4 ,2,3],[2,3,1]), 不同的([1,2,3],[ 4 ,3,1]), 不同的（[1, 4 ,3],[2,3,1]），不同的（[1,2,3]，[2, 4 ,1]）， 不同的（[1,2, 4 ],[2,3,1]），不同的（[1,2,3],[2,3, 4 ]）。 真的。%所有子目标确定性地成功
好的！ 让我们运行我在 上一个答案中使用的另一个（非常一般的）查询：
?- different([A,B],[X,Y]).
A=X , B=X , dif(Y,X)
; A=X , dif(B,X), dif(Y,B)
; A=Y , dif(B,X), dif(Y,X)
; dif(A,X), dif(A,Y).
袖珍的！与我 之前介绍的相比有了很大的改进！
（受@repeat最后一个答案的启发，名字还是太笨拙了）
different(Xs, Ys) :-
if_(tnotexists_inlist_t(list_memberd_t(Ys), Xs),
true,
tnotexists_inlist_t(list_memberd_t(Xs), Ys)).
tnotexists_inlist_t(_P_2, [], false).
tnotexists_inlist_t(P_2, [E|Es], T) :-
if_(call(P_2, E),
tnotexists_inlist_t(P_2, Es, T),
T = true).
回归本源！此变体非常接近问题中 OP 给出的代码。
以下是基于if_/3和memberd_t/3。
different(Xs,Ys) :-
if_(some_absent_t(Xs,Ys),
true,
some_absent_t(Ys,Xs,true)).
some_absent_t([] ,_ ,false).
some_absent_t([X|Xs],Ys,Truth) :-
if_(memberd_t(X,Ys), some_absent_t(Xs,Ys,Truth), Truth=true).
这是一个地面查询：
?- 不同的([ 4 ,2,3],[2,3,1]), 不同的([1,2,3],[ 4 ,3,1]), 不同的（[1, 4 ,3],[2,3,1]），不同的（[1,2,3]，[2, 4 ,1]）， 不同的（[1,2, 4 ],[2,3,1]），不同的（[1,2,3],[2,3, 4 ]）。 真的。%所有子目标确定性地成功
这是我在以前的答案中使用的（更一般的）查询：
?- different([A,B],[X,Y]).
A=X , B=X , dif(Y,X)
; A=X , dif(B,X), dif(B,Y)
; A=Y , B=Y , dif(Y,X), dif(Y,X)
; A=Y , dif(B,X), dif(B,Y), dif(Y,X)
; dif(A,X), dif(A,Y).
代码选美比赛的下一位参赛者！-)
此答案显示了 先前答案中显示的代码的重构变体。它使用具体化的连词和析取：
and_(P_1,Q_1) :-
and_t(P_1,Q_1,true).
or_(P_1,Q_1) :-
or_t(P_1,Q_1,true).
and_t(P_1,Q_1,Truth) :-
if_(P_1, call(Q_1,Truth), Truth=false).
or_t(P_1,Q_1,Truth) :-
if_(P_1, Truth=true, call(Q_1,Truth)).
注意“and”和“or”的两个版本；有后缀的_t有一个额外的真值论证，没有后缀的没有并假设Truth=true应该成立。
基于and_t/3具体化的术语不等式谓词dif/3，我们定义nonmember_t/3：
nonmember_t(X,Ys,Truth) :-
list_nonmember_t(Ys,X,Truth).
list_nonmember_t([] ,_, true).
list_nonmember_t([Y|Ys],X,Truth) :-
and_t(dif(X,Y), list_nonmember_t(Ys,X), Truth).
现在，让我们定义和some_absent_t/3，如下所示：different_t/3different/2
some_absent_t([] ,_ ,false)。
some_absent_t([X|Xs],Ys,Truth) :-
or_t(nonmember_t(X,Ys), some_absent_t(Xs,Ys), Truth)。
different_t (Xs,Ys, Truth ) :-
or_t(some_absent_t(Xs,Ys),
some_absent_t(Ys,Xs),
真相）。
不同（Xs，Ys）：-
不同的_t（Xs，Ys，真）。
它还运行吗？
?-不同（[A，B]，[X，Y]）。
A=X , B=X , 差异(Y,X)
; A=X , 差异(B,X), 差异(B,Y)
; A=Y , B=Y , 差异(Y,X), 差异(Y,X)
; A=Y，差异（B，X），差异（B，Y），差异（Y，X）
; 差异（A，X），差异（A，Y）。% 与之前相同的结果
?- 不同的([ 4 ,2,3],[2,3,1]), 不同的([1,2,3],[ 4 ,3,1]),
不同的（[1, 4 ,3],[2,3,1]），不同的（[1,2,3]，[2, 4 ,1]），
不同的（[1,2, 4 ],[2,3,1]），不同的（[1,2,3],[2,3, 4 ]）。
真的。% 与之前相同的结果
看起来不错！
总而言之，对现有答案并没有太大的改进，但 IMO 的代码更具可读性，并且different/2作为额外奖励的具体版本！
让我们把它发挥到极致——借助list_nonmember_t/3,exists_in_t/3和
or_/2!
some_absent_t(Xs,Ys,Truth) :-
exists_in_t(list_nonmember_t(Ys),Xs,Truth).
different(Xs,Ys) :-
or_(some_absent_t(Xs,Ys),
some_absent_t(Ys,Xs)).
不久前提供了以下大胆的赏金（+500） ：
这里仍然缺少一个惯用的答案。例如，or_t/3 应该是 (;)/3。还有更多。
接受挑战！这个答案是对这个先前答案的后续。
我们使用具体化的逻辑连接词，可以这样定义：(;)/3
';'(P_1,Q_1,T) :- if_(P_1, T=true, call(Q_1,T))。
接下来，我们定义元谓词 call_/1。对于此答案中使用的具体谓词，它很有用。以其名称和语义，call_/1跟随if_/3, and_/2, 和or_/2!
call_(P_1) :-调用(P_1, true )。
使用(;)/3, call_/1,some_absent_t/3我们实现different/2：
不同（As，Bs）：- call_（（some_absent_t（As，Bs）； some_absent_t（Bs，As）））。
完毕！就是这样。
让我们重新运行我们在之前的答案中使用的查询！
?- 不同（[ 5 , 4 ],[ 1 , 2 ]）。 真的。 ?-不同（[1,2,3]，[2,3,1]）。 错误的。 ?- 不同（[ 4 ,2,3],[2,3,1]），不同（[1, 4 ,3],[2,3,1]），不同（[1,2, 4 ]， [2,3,1]), 不同（[1,2,3],[ 4 ,3,1]），不同（[1,2,3]，[2, 4 ,1]），不同（[1,2,3],[2 ,3, 4 ])。 真的。
相同的查询，相同的答案……对我来说没问题！
关于使用if_的解决方案，我想说另一种方法是从一开始就使用建设性否定。建设性否定早在80年代就有研究，先驱者是David Chan，至今仍不时出现。
假设我们有一个具有建设性否定的 Prolog 解释器(~)/2。这种建设性的否定(~)/2可以用来定义一个声明性的 if-then-else，如下所示，让我们调用这个操作符(~->)/2：
(A ~-> B; C) :- (A, B); (~A, C).
如果 Prolog 解释器除了建设性否定之外还嵌入了含义(=>)/2，则可以另外定义一个声明性 if-then-else，如下所示，让我们调用此运算符(~=>)/2：
(A ~=> B; C) :- (A => B), (~A => C).
注意从析取(;)/2到合取的转换(,)/2。询问二元决策图 (BDD) 人员为什么他们在逻辑上是等价的。在程序上存在细微差别，但通过对某个 A 的嵌入式暗示的后门，第二个 if-then-else 变体也将引入非确定性。
但是我们将如何在 Prolog 解释器中进行并引入例如建设性否定。一种直接的方法是将建设性否定委托给约束求解器。如果约束求解器已具体化否定，则可以按如下方式完成：
~ A :- #\ A.
但是周围没有那么多约束求解器，这将允许对诸如member/2etc 之类的示例进行合理使用。因为它们通常只为有限整数、有理数等域提供具体化否定。但是对于诸如member/2我们需要的谓词对赫布兰德宇宙的具体化否定。
另请注意，建设性否定的常用方法还假设普通规则含义得到另一种解读。这意味着通常在建设性否定下，我们可以选择普通member/2定义，并得到查询结果，例如：
?- ~ member(X, [a,b,c]).
dif(X, a),
dif(X, b),
dif(X, c).
但是再一次，具体化的否定很难与已定义的谓词一起使用，因此以下查询可能无法正常工作：
?- #\ member(X, [a,b,c]).
/* typically won't work */
如果上述方法比任何声明性 if-then-else 成功，例如(~->)/2or(~=>)/2将使用较少，因为普通谓词定义已经由 Prolog 解释器提供声明性解释。但是为什么建设性的否定没有广泛传播呢？一个原因可能是这种 Prolog 解释器的设计空间很大。我注意到我们会有以下选择：
反向链接：我们基本上会将原版解释器solve/1分成两个谓词solvep/1和solven/1. solvep/1负责解决积极的目标，solven/1负责解决消极的目标。当我们尝试这个时，我们迟早会发现我们需要对量词进行更仔细的处理，并且最终可能会使用 Herbrand 域的量词消除方法。
前向链接：我们还将注意到，在后向链接中，我们将遇到对带有析取或存在量词的子句进行建模的问题。这与适用于 Prolog 的后续演算在右侧只有一个公式有关。因此，要么我们在右手边使用多重公式并且会失去平行一致性，要么我们使用前向链接。
Magic Sets：但是前向链接会以不受控制的方式污染解空间。所以我们可能需要某种形式的正向和反向链接组合。我的意思不仅仅在于，我们应该能够在求解过程中在两者之间动态切换，而是我的意思是我们还需要一种方法来生成引导前向链接过程的集合。
此处的此答案还指出了更多问题。这并不意味着迟早会找到一个公式，将所有这些问题和解决方案组合在一起，但这可能需要更多时间。
再见