different/2 - 是否存在纯粹的、确定的定义？答案

【问题标题】：different/2 - does a pure, determinate definition exist?different/2 - 是否存在纯粹的、确定的定义？
【发布时间】：2015-09-01 01:08:26
【问题描述】：

different(Xs, Ys) :-
   member(X, Xs),
   non_member(X, Ys).
different(Xs, Ys) :-
   member(Y, Ys),
   non_member(Y, Xs).

虽然使用member/2 和non_member/2 的定义从声明的角度来看几乎¹完美，但它为某些查询产生了冗余解决方案并留下了选择点。

什么是对此进行改进的定义（以纯粹的方式可能使用if_/3 和(=)/3），使得different/2 描述了完全相同的一组解决方案，但至少对于地面查询是确定的（因此不会留下任何无用的选择点）并省略（如果可能）任何多余的答案？

¹_{实际上，different([a|nonlist],[]), different([],[b|nonlist]) 成功了。它同样可能失败。因此，两者都失败的解决方案很好（甚至更好）。}

【问题讨论】：

我们是在谈论 lists 还是 sets，因为这可能会产生一些影响（尤其是在效率方面）。
@CommuSoft：我完全避免提及这些密切相关的概念，以便更好地关注实际定义。当然，目的是表示集合，但这种知识不应该改变任何东西。无论如何，是可能有重复的！
此外，这个谓词似乎做了太多工作：使用different([a,b],Y). 查询时，它给出：Y = [_G122], dif(_G122, a) ;，但dif(_G122,a); 不是必需的：即使它等于@ 987654335@，这不是问题。当然，如果查询different([a,b],[Y])，则会得到dif(Y,a)、dif(Y,b) 和dif(Y,b),dif(Y,a)，但这仍然没有必要。
@CommuSoft：到目前为止，我还没有考虑过那种级别的冗余。我完全被地面查询的低效率所吸引。因此，如果你成功地找到了一个考虑到这一点的纯粹定义——那就更好了！有很多赏金:-)

标签： prolog prolog-dif logical-purity

【解决方案1】：

不久前提供了以下大胆的赏金 (+500)：

^{这里仍然缺少一个惯用的答案。例如，or_t/3 应该是 (;)/3。还有更多。}

接受挑战！此答案是this previous answer 的后续。

我们使用具体化的逻辑连接词(;)/<b>3</b>，可以这样定义：
';'(P_1,Q_1,T) :- if_(P_1, T=true, call(Q_1,T))。
接下来，我们定义meta-predicate call_/1。对于此答案中使用的具体谓词，它很有用。 call_/1 以其名称和语义跟在 if_/3、and_/2 和 or_/2 之后！
call_(P_1) :- call(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])。
真的。}

相同的查询，相同的答案...在我看来还可以！

【讨论】：

【解决方案2】：

使用if_ 的Conerning 解决方案，我想说另一种方法是从一开始就使用建设性否定。 Constructive negation早在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/2 等示例进行合理使用。因为它们通常只为有限整数、有理数等域提供具体的否定。但是对于诸如 member/2 这样的谓词，我们需要对 Herbrand 宇宙进行具体化否定。

还要注意，建设性否定的常用方法也假设普通规则含义得到另一种解读。这意味着通常在建设性否定的情况下，我们可以选择普通的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（例如 (~->)/2 或 (~=>)/2）使用频率较低，因为普通谓词定义已经由 Prolog 解释器提供声明性解释。但是为什么建设性的否定没有广泛传播呢？一个原因可能是这种 Prolog 解释器的设计空间很大。我注意到我们会有以下选择：

反向链接：我们基本上会将原版解释器solve/1 分成两个谓词solvep/1 和solven/1。 solvep/1 负责解决积极目标，solven/1 负责解决消极目标。当我们尝试这样做时，我们迟早会发现我们需要对量词进行更仔细的处理，并且最终可能会使用 Herbrand 域的量词消除方法。

前向链接：我们还会注意到，在后向链接中，我们会遇到对带有析取或存在量词的子句进行建模的问题。这与适用于 Prolog 的后续演算在右侧只有一个公式有关。因此，要么我们在右手边使用多重公式并且会失去副一致性，要么我们使用前向链接。

Magic Sets：但是前向链接会以不受控制的方式污染解空间。所以我们可能需要某种形式的正向和反向链接组合。我的意思不仅仅在于，我们应该能够在求解过程中在两者之间动态切换，而是我的意思是我们还需要一种方法来生成引导正向链接过程的集合。

这个答案here 中还指出了更多问题。这并不意味着迟早会找到一个公式，将所有这些问题和解决方案组合在一起，但这可能需要更多时间。

再见

【讨论】：

这里的区别在于开销：if_/3 是添加的一条规则。而已。在许多情况下，性能与不纯且高效的代码相当。当然可以像这样添加建设性否定：cn_t(G_0, true) :- G_0. cn_t(G_0, false) :- ~ G_0. 但类似于您对(~->)/2 的定义，没有直接的方法可以避免无用的选择点。
假设你能做到最好，那么你还有(;)/2！这会创建一个无用的选择点。但是，if_/3 可以轻松扩展。（实际上，要 100% ISO，并不是那么简单，而是接近）。

【解决方案3】：

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

【讨论】：

【解决方案4】：

这是另一个尝试！我们利用单调 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] ）。真的。 % all 子目标确定性地成功

好的！ 让我们运行另一个我在我的 previous answer:

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

紧凑！比我介绍的内容有了很大改进 earlier!

【讨论】：

猜想：different/2（由 OP 给出）对应于different/2（如上所示），就像 CNF 对应于 DNF。（嗯，实际上不完全是上面给出的定义，但不会在每一步都交换 Xs 和 Ys 的变体——就像臭名昭著的 split/3 那样——但只交换一次当第一个参数是空列表时。）
Ultra-nit：SWI 的顶层通过添加一个空格来区分最后确定的答案和中止的查询。考虑查询true;false.，如果您中止查询，它将产生true . 作为响应。因此：在 . 之前添加空格 - 结束标记 (* 6.4.8 *) 暗示答案不确定。
更好。但它是意图暴露吗？
@false。从某种意义上说，different_aux(Xs,Ys,Xs0,Ys0) 的变体是。我是这样看的：different/2 两个子句（由 OP 给出）与“逻辑或”相关联，可能会导致冗余解决方案。 different_aux OTOH 与“逻辑与”链接。这使得有必要保留Xs 和Ys（因为Prolog 的回溯不再这样做了）。

【解决方案5】：

回归本源！此变体非常接近问题中 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] ）。真的。 % all 子目标确定性地成功

这是我在之前的答案中使用的（更一般的）查询：

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

【讨论】：

_aux 这个名字不是很暴露。没有更好的名字吗？
different_aux_t(Xs, Ys, T)：在Xs 中存在一个X，这样：X notin Ys。

【解决方案6】：

代码选美的下一位选手！-)

这个答案显示了代码的重构变体 a previous answer。它使用具体化的连词和析取：

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/3 和different/2，如下所示：

some_absent_t([] ,_ ,false)。 some_absent_t([X|Xs],Ys,Truth) :- or_t(nonmember_t(X,Ys), some_absent_t(Xs,Ys), Truth)。 不同的_t(Xs,Ys,真相) :- 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 的具体版本是额外的奖励！

【讨论】：

@false。到目前为止，我已经使用了or_t/3 和or_/2。我知道or_t/3 最好变成(;)/3（and_t/3 和','/3 相同）。但是or_/2 和and_/2 呢？它们是if_/3 的特化，但根本不能重命名为(;)/2 和','/2。
@false。我看到if_/3 好像它是由if_(Cond,Then,Else) :- if_t(Cond,Then,Else,true). 定义的，即使说if_t/4 尚未使用（还）。尽管如此，我们应该有一个易于遵循的清晰方案，以便if_/3 用户可以提供两个版本的谓词而不会带来太多痛苦，IMO。

【解决方案7】：

第一次尝试！

以下代码基于元谓词tfilter/3和tpartition/4、单调if-then-else控制结构if_/3、具体化一元逻辑连接词not_t/3和具体化术语相等谓词@ 987654325@:

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.

上述方法感觉像是朝着正确方向迈出的一步......但是，就目前而言，我不会称其为完美。

【讨论】：

你的意思是not_t/2，不是吗？
地面案例是否确定？
@false。我的意思是not_t(Goal,Param,Truth1) :- call(Goal,Param,Truth0), truth_negated(Truth0,Truth1). 和truth_negated(true,false). truth_negated(false,true). IMO 需要第三个参数才能穿过要测试的项目。
@false。关于如何系统地测试确定性的任何提示/技巧？（可能使用setup_call_cleanup/3接口...）
det(G_0) :- setup_call_cleanup(true,G_0, Det=true), ( Det\==true -> throw(...) ; true). 但最好是使用适合these debugging ops的漂亮、醒目的前缀操作

【解决方案8】：

（受@repeat 的last answer 启发很大，名字还是太笨拙了）

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

【讨论】：

我想知道谓词名称是否应该包含list（就像maplist 一样），或者是否通过在模块中构建代码实际上使该信息变得多余。