Fat*_*ize 5 predicate list prolog prolog-dif logical-purity
如何实现not_all_equal/1谓词,如果给定列表包含至少2个不同的元素,则谓词成功,否则失败？
这是我的尝试(不是很纯粹):
not_all_equal(L) :-
( member(H1, L), member(H2, L), H1 \= H2 -> true
; list_to_set(L, S),
not_all_equal_(S)
).
not_all_equal_([H|T]) :-
( member(H1, T), dif(H, H1)
; not_all_equal_(T)
).
然而,这并不总是具有最佳行为:
?- not_all_equal([A,B,C]), A = a, B = b.
A = a,
B = b ;
A = a,
B = b,
dif(a, C) ;
A = a,
B = b,
dif(b, C) ;
false.
在这个例子中,只有第一个答案应该出来,另外两个答案是多余的.
以下是library(reif)用于SICStus | 的部分实现 SWI.这当然是正确的,因为当它无法继续时会产生错误.但它缺乏我们想要的普遍性.
not_all_equalp([A,B]) :-
dif(A,B).
not_all_equalp([A,B,C]) :-
if_(( dif(A,B) ; dif(A,C) ; dif(B,C) ), true, false ).
not_all_equalp([A,B,C,D]) :-
if_(( dif(A,B) ; dif(A,C) ; dif(A,D) ; dif(B,C) ; dif(B,D) ), true, false ).
not_all_equalp([_,_,_,_,_|_]) :-
throw(error(representation_error(reified_disjunction),'C\'est trop !')).
?- not_all_equalp(L).
L = [_A,_B], dif(_A,_B)
; L = [_A,_A,_B], dif(_A,_B)
; L = [_A,_B,_C], dif(_A,_B)
; L = [_A,_A,_A,_B], dif(_A,_B)
; L = [_A,_A,_B,_C], dif(_A,_B)
; L = [_A,_B,_C,_D], dif(_A,_B)
;
! error(representation_error(reified_disjunction),'C\'est trop !')
?- not_all_equalp([A,B,C]), A = a, B = b.
A = a,
B = b
; false.
编辑:现在我意识到我根本不需要添加那么多dif/2目标!一个变量与第一个变量不同就足够了!不需要互相排斥!我仍然觉得有点不安全去除dif(B,C)目标......
not_all_equalp([A,B]) :-
dif(A,B).
not_all_equalp([A,B,C]) :-
if_(( dif(A,B) ; dif(A,C) ), true, false ).
not_all_equalp([A,B,C,D]) :-
if_(( dif(A,B) ; dif(A,C) ; dif(A,D) ), true, false ).
not_all_equalp([_,_,_,_,_|_]) :-
throw(error(representation_error(reified_disjunction),'C\'est trop !')).
答案完全相同......我想,这里发生了什么.这个版本是否较弱,那不太一致？
这是一种简单的方法，您可以做到这一点并保持逻辑纯度！
not_all_equal([E|Es]) :-
some_dif(Es, E).
some_dif([X|Xs], E) :-
( dif(X, E)
; X = E, some_dif(Xs, E)
).
以下是使用 SWI-Prolog 7.7.2 的一些示例查询。
首先，最常见的查询：
?- not_all_equal(Es).
dif(_A,_B), Es = [_A,_B|_C]
; dif(_A,_B), Es = [_A,_A,_B|_C]
; dif(_A,_B), Es = [_A,_A,_A,_B|_C]
; dif(_A,_B), Es = [_A,_A,_A,_A,_B|_C]
; dif(_A,_B), Es = [_A,_A,_A,_A,_A,_B|_C]
...
接下来，OP 在问题中给出的查询：
?- not_all_equal([A,B,C]), A=a, B=b.
A = a, B = b
; false. % <- the toplevel hints at non-determinism
最后，让我们把子目标放在A=a, B=b前面：
?- A=a, B=b, not_all_equal([A,B,C]).
A = a, B = b
; false. % <- (non-deterministic, like above)
很好，但理想情况下最后一个查询应该确定性地成功！
library(reif)第一个参数索引 考虑第一个谓词参数的主函子（加上一些简单的内置测试），以提高充分实例化目标的确定性。
这本身并不能令人满意地涵盖dif/2。
我们可以做什么？使用
具体化术语平等/不平等——有效索引dif/2！
some_dif([X|Xs], E) :- % some_dif([X|Xs], E) :-
if_(dif(X,E), true, % ( dif(X,E), true
(X = E, some_dif(Xs,E)) % ; X = E, some_dif(Xs,E)
). % ).
请注意新旧实现的相似之处！
上图中，球门X = E在左侧是多余的。让我们删除它吧！
some_dif([X|Xs], E) :-
if_(dif(X,E), true, some_dif(Xs,E)).
甜的！但是，唉，我们还没有完成！
？- not_all_equal(Xs)。 不终止
这是怎么回事？
事实证明， 的实现dif/3阻止我们为最一般的查询获得一个好的答案序列。为此，在不使用强制公平枚举的额外目标的情况下，我们需要对 的实现进行调整dif/3，我将其称为diffirst/3：
diffirst(X, Y, T) :-
( X == Y -> T = false
; X \= Y -> T = true
; T = true, dif(X, Y)
; T = false, X = Y
).
让我们在谓词的定义中使用diffirst/3代替：dif/3some_dif/2
some_dif([X|Xs], E) :-
if_(diffirst(X,E), true, some_dif(Xs,E)).
所以，最后，这里是上面的新查询some_dif/2：
?- not_all_equal(Es). % query #1
dif(_A,_B), Es = [_A,_B|_C]
; dif(_A,_B), Es = [_A,_A,_B|_C]
; dif(_A,_B), Es = [_A,_A,_A,_B|_C]
...
?- not_all_equal([A,B,C]), A=a, B=b. % query #2
A = a, B = b
; false.
?- A=a, B=b, not_all_equal([A,B,C]). % query #3
A = a, B = b.
查询 #1 不会终止，但具有相同的紧凑答案序列。好的！
查询 #2 仍然不确定。好的。对我来说，这已经是最好的了。
查询 #3 已变得确定性：现在更好！
底线：
library(reif)驯服过多的非决定论，同时保持逻辑纯度！diffirst/3应该找到它的方式library(reif):)编辑：更一般地使用元谓词（由评论建议；谢谢！）
让我们some_dif/2这样概括：
:- meta_predicate some(2,?).
some(P_2, [X|Xs]) :-
if_(call(P_2,X), true, some(P_2,Xs)).
some/2可以与除 之外的具体化谓词一起使用diffirst/3。
这里的更新not_all_equal/1现在使用some/2而不是some_dif/2：
not_all_equal([X|Xs]) :-
some(diffirst(X), Xs).
上面的示例查询仍然给出相同的答案，因此我不会在这里显示这些答案。