5

如何实现一个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.

在这个例子中，只有第一个答案应该出来，另外两个是多余的。

4

2 回答 2

5

这是library(reif)用于SICStus |的部分实现。斯威。这当然是正确的，因为当它无法继续时会产生错误。但它缺乏我们想要的普遍性。

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 !')).

答案是完全一样的......这里发生了什么，我想。这个版本是否较弱，一致性较差？

于 2017-11-24T17:21:59.720 回答
4

这是一种简单的方法，您可以做到这一点并保持！

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
   ).

让我们在 predicate 的定义中使用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 已成为确定性：现在更好！

底线：

  1. 用于library(reif)驯服过多的不确定性，同时保持逻辑纯度！
  2. 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).

上面的示例查询仍然给出相同的答案，所以我不会在这里展示这些。

于 2017-11-25T22:18:42.880 回答