logo标签列表

术语相等/不相等的具体化

prologprolog-dif
40
纯Prolog程序以清晰的方式区分术语的相等和不相等，即使所有相关术语都是ground，也会遭受执行效率低下的问题。最近在SO上的一个例子是这个答案。在这个定义中，所有答案和所有失败都是正确的。考虑：
?- Es = [E1,E2], occurrences(E, Es, Fs).
Es = Fs, Fs = [E, E],
E1 = E2, E2 = E ;
Es = [E, E2],
E1 = E,
Fs = [E],
dif(E, E2) ;
Es = [E1, E],
E2 = E,
Fs = [E],
dif(E, E1) ;
Es = [E1, E2],
Fs = [],
dif(E, E1),
dif(E, E2).

虽然从声明的角度来看，该程序是完美无缺的，但在当前系统（如B、SICStus、SWI、YAP）上直接执行却效率低下。对于以下目标，每个列表元素都会留下一个选择点。 
?- occurrences(a,[a,a,a,a,a],M).
M = [a, a, a, a, a] ;
false.
可以通过使用足够大的a列表来观察到这一点，例如： 
?- 24=I,N is 2^I,length(L,N), maplist(=(a),L).
ERROR: Out of global stack
必须调整I以便仍然可以表示列表；在SWI中，这意味着：

1mo 全局堆栈的I必须足够小，以避免出现类似以下的资源错误：

2do 当地的堆栈的I必须足够大才能引发资源错误：

?- 22=I,N是2的I次方,length(L,N), maplist(=(a),L), ( Length=ok ; occurrences(a,L,M) ).
I = 22,
N = 4194304,
L = [a, a, a, a, a, a, a, a, a|...],
Length = ok ;
ERROR: Out of local stack

为了克服这个问题并仍然保留良好的声明性质，需要一些比较谓词。

应该如何定义这个比较谓词？

以下是这样一个可能的定义:

equality_reified(X, X, true).
equality_reified(X, Y, false) :-
   dif(X, Y).

编辑：也许参数顺序应该与ISO内置compare/3类似（链接仅链接到草案）。

它的高效实现将首先处理快速确定的情况：

equality_reified(X, Y, R) ：- X == Y，！，R = true。
equality_reified(X, Y, R) ：- ?=(X, Y)，！，R = false。％语法不同
equality_reified(X, Y, R) ：- X \= Y，！，R = false。％语义不同
equality_reified(X, X, true)。
equality_reified(X, Y, false) ：
   dif（X，Y）。

编辑：我不确定在存在约束条件的情况下X \= Y是否是适当的保护条件。 没有约束条件，?=(X, Y)或X \= Y是相同的。

例子

正如@user1638891所建议的那样，这里是一个如何使用这种原始方法的示例。mats的原始代码如下：

occurrences_mats(_, [], []).
occurrences_mats(X, [X|Ls], [X|Rest]) :-
   occurrences_mats(X, Ls, Rest).
occurrences_mats(X, [L|Ls], Rest) :-
   dif(X, L),
   occurrences_mats(X, Ls, Rest).

这可以被重写为类似于：

occurrences(_, [], []).
occurrences(E, [X|Xs], Ys0) :-
   reified_equality(Bool, E, X),
   ( Bool == true -> Ys0 = [X|Ys] ; Ys0 = Ys ),
   % ( Bool = true, Ys0 = [X|Ys] ; Bool = true, Ys0 = Ys ),
   occurrences(E, Xs, Ys).

reified_equality(R, X, Y) :- X == Y, !, R = true.
reified_equality(R, X, Y) :- ?=(X, Y), !, R = false.
reified_equality(true, X, X).
reified_equality(false, X, Y) :-
   dif(X, Y).

请注意，SWI的第二参数索引仅在您输入类似于occurrences(_,[],_)的查询后才会被激活。此外，SWI需要本质上非单调的if-then-else，因为它不会对(;)/2 - 或者说是析取 - 进行索引。SICStus则会这样做，但只有第一个参数进行索引。因此，它会留下一个（1）选择点（在以[]结尾的位置）。
2
这确实是一个有趣的问题。您能否添加来自引用SO问题的代码，甚至更好地添加一个更明显的案例？ - NotAUser
1
@user1638891：搜索 [tag:prolog-dif] - 如果您找到我错过的其他示例，请重新标记。 - false
@false，@mat，@repeat。截至目前提交的所有occurrences/3实现，除了我昨天提交的，都会在查询中第1、2个参数自由且第3个参数是带有不同ground成员的列表时进入无限循环，正确的行为当然是失败。 - migfilg
1
@repeat 没关系。谢谢你把我的警告当作建设性的意见来接受。 - migfilg
6个回答
10

首先，名称应更具陈述性，例如equality_truth/2。

2
我的意思是，与其使用equality_reified/2，我们应该更加声明性地命名它，例如equality_truth/2或者甚至是equality_true/2（因为第二个参数的“false”很难称之为“truth”）。"Reified"这个词暗示着某人_做了_某些事情，这比声明性更加强制性。我们应该选择一个带有_保持_含义的名称。 - mat
9
以下代码基于 @false 在 Prolog union for A U B U C 中实现的 if_/3 和 (=)/3（又称为equal_truth/3）。
=(X, Y, R) :- X == Y,    !, R = true.
=(X, Y, R) :- ?=(X, Y),  !, R = false. % syntactically different
=(X, Y, R) :- X \= Y,    !, R = false. % semantically different
=(X, Y, R) :- R == true, !, X = Y.
=(X, X, true).
=(X, Y, false) :-
   dif(X, Y).

if_(C_1, Then_0, Else_0) :-
   call(C_1, Truth),
   functor(Truth,_,0),  % safety check
   ( Truth == true -> Then_0 ; Truth == false, Else_0 ).

与occurrences/3相比，辅助函数occurrences_aux/3采用不同的参数顺序，将列表Es作为第一个参数传递，这可以启用第一个参数索引：

occurrences_aux([], _, []).
occurrences_aux([X|Xs], E, Ys0) :-
   if_(E = X, Ys0 = [X|Ys], Ys0 = Ys),
   occurrences_aux(Xs, E, Ys).

正如 @migfilg 指出的那样，目标 Fs=[1,2], occurrences_aux(Es,E,Fs) 在逻辑上是错误的，因此应该失败。 occurrences_aux(_,E,Fs) 表示在 Fs 中所有元素都等于 E。 然而，在这种情况下，occurrences_aux/3 本身并不会中止。
我们可以使用一个辅助谓词 allEqual_to__lazy/2 来改进终止行为：
allEqual_to__lazy(Xs,E) :-
   freeze(Xs, allEqual_to__lazy_aux(Xs,E)).

allEqual_to__lazy_aux([],_).
allEqual_to__lazy_aux([E|Es],E) :-
   allEqual_to__lazy(Es,E).

在所有辅助谓语就位后，让我们定义occurrences/3：

occurrences(E,Es,Fs) :-
   allEqual_to__lazy(Fs,E),    % enforce redundant equality constraint lazily
   occurrences_aux(Es,E,Fs).   % flip args to enable first argument indexing

让我们来谈谈一些查询：

?- occurrences(E,Es,Fs).       % first, the most general query
Es = Fs, Fs = []        ;
Es = Fs, Fs = [E]       ;
Es = Fs, Fs = [E,E]     ;
Es = Fs, Fs = [E,E,E]   ;
Es = Fs, Fs = [E,E,E,E] ...    % will never terminate universally, but ...
                               % that's ok: solution set size is infinite

?- Fs = [1,2], occurrences(E,Es,Fs).
false.                         % terminates thanks to allEqual_to__lazy/2

?- occurrences(E,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1],     E=1                     ;
Fs = [2,2],                 E=2           ;
Fs = [3,3],                           E=3 ;
Fs = [],      dif(E,1), dif(E,2), dif(E,3).

?- occurrences(1,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1].                  % succeeds deterministically

?- Es = [E1,E2], occurrences(E,Es,Fs).
Es = [E,  E], Fs = [E,E],     E1=E ,     E2=E  ;
Es = [E, E2], Fs = [E],       E1=E , dif(E2,E) ;
Es = [E1, E], Fs = [E],   dif(E1,E),     E2=E  ;
Es = [E1,E2], Fs = [],    dif(E1,E), dif(E2,E).

?- occurrences(1,[E1,1,2,1,E2],Fs).
    E1=1 ,     E2=1 , Fs = [1,1,1,1] ;
    E1=1 , dif(E2,1), Fs = [1,1,1]   ;
dif(E1,1),     E2=1 , Fs = [1,1,1]   ;
dif(E1,1), dif(E2,1), Fs = [1,1].

编辑 2015-04-27

为了测试在某些情况下occurrences/3是否会普遍终止，以下是一些更多的查询：

?-           occurrences(1,L,[1,2]).
false. 
?- L = [_|_],occurrences(1,L,[1,2]).
false.
?- L = [X|X],occurrences(1,L,[1,2]).
false.
?- L = [L|L],occurrences(1,L,[1,2]).
false.
与 PO 所引用的代码相比，参数顺序发生了变化，这一点应在答案中明确说明。因此，本实现采用了我之前回答中使用原始谓词第二个参数的索引策略，以避免某些选择点。请问您能告诉我 if_/3 和 =/3 的定义在哪里吗？ - migfilg
1
抱歉，我错过了你的第二行；或许你应该为这个想法给予一些认可...谢谢提供链接。至于= / 3，我没有看到你在哪里使用它：是在你复制的if_ / 3内部使用吗？ - migfilg
2
我发现了=/3的用法。 - migfilg
5

最好使用相同的参数(=)/3来调用此谓词。这样，像if_/3这样的条件现在更易读了。而且使用后缀_t代替_truth：

memberd_t(_X, [], false).
memberd_t(X, [Y|Ys], Truth) :-
   if_( X = Y, Truth=true, memberd_t(X, Ys, Truth) ).

曾经是：

memberd_truth(_X, [], false).
memberd_truth(X, [Y|Ys], Truth) :-
   if_( equal_truth(X, Y), Truth=true, memberd_truth(X, Ys, Truth) ).
4
这是一个更短的逻辑纯粹的occurrences/3实现。
我们基于 tfilter/3、具体化的项相等谓词(=)/3和协程allEqual_to__lazy/2（在我对这个问题的先前回答中定义）构建它。
occurrences(E,Xs,Es) :-
   allEqual_to__lazy(Es,E),
   tfilter(=(E),Xs,Es).

完成！为了方便比较，我们重新运行了我在之前回答中使用的完全相同的查询：

?- Fs = [1,2], occurrences(E,Es,Fs).
false.

?- occurrences(E,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1],     E=1                     ;
Fs = [2,2],                 E=2           ;
Fs = [3,3],                           E=3 ;
Fs = [],      dif(E,1), dif(E,2), dif(E,3).

?- occurrences(1,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1].

?- Es = [E1,E2], occurrences(E,Es,Fs).
Es = [E, E ], Fs = [E,E],     E1=E ,     E2=E  ;
Es = [E, E2], Fs = [E],       E1=E , dif(E2,E) ;
Es = [E1,E ], Fs = [E],   dif(E1,E),     E2=E  ;
Es = [E1,E2], Fs = [],    dif(E1,E), dif(E2,E).

?- occurrences(1,[E1,1,2,1,E2],Fs).
    E1=1 ,     E2=1 , Fs = [1,1,1,1] ;
    E1=1 , dif(E2,1), Fs = [1,1,1]   ;
dif(E1,1),     E2=1 , Fs = [1,1,1]   ;
dif(E1,1), dif(E2,1), Fs = [1,1].

?- occurrences(1,L,[1,2]).
false.

?- L = [_|_],occurrences(1,L,[1,2]).
false.

?- L = [X|X],occurrences(1,L,[1,2]).
false.

?- L = [L|L],occurrences(1,L,[1,2]).
false.

最后，最常见的查询：
?- occurrences(E,Es,Fs).
Es = Fs, Fs = []      ;
Es = Fs, Fs = [E]     ;
Es = Fs, Fs = [E,E]   ;
Es = Fs, Fs = [E,E,E] % ... and so on ad infinitum ...

我们得到相同的答案。
4

更新：这个回答已经被我于4月18日的回答所取代。由于下面的评论，我并不建议删除该回答。

我的前一个回答是错误的。以下回答针对问题中的测试用例运行，并且实现具有避免多余选择点的期望功能。我假设顶层谓词模式为？,+，？虽然其他模式也可以轻松实现。

程序总共有4个子句：第二个参数中的列表被访问，并且对于每个成员，存在两种可能性：它要么与顶层谓词的第一个参数一致，要么与其不同，在后一种情况下应用 dif 约束：

occurrences(X, L, Os) :- occs(L, X, Os).

occs([],_,[]).
occs([X|R], X, [X|ROs]) :- occs(R, X, ROs).
occs([X|R], Y, ROs) :- dif(Y, X), occs(R, Y, ROs).

以下是使用YAP进行的示例运行：

?- occurrences(1,[E1,1,2,1,E2],Fs).
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
E1 = 1,
Fs = [1,1,1],
dif(1,E2) ? ;
E2 = 1,
Fs = [1,1,1],
dif(1,E1) ? ;
Fs = [1,1],
dif(1,E1),
dif(1,E2) ? ;
no  

?- occurrences(E,[E1,E2],Fs).
E = E1 = E2,
Fs = [E,E] ? ;
E = E1,
Fs = [E],
dif(E,E2) ? ;
E = E2,
Fs = [E],
dif(E,E1) ? ;
Fs = [],
dif(E,E1),
dif(E,E2) ? ;
no
3
下面的occurrences/3实现基于我的以前的答案，即通过利用第一个参数上的子句索引机制来避免一些选择点，并解决了所有提出的问题。
此外，它应对了迄今为止所有提交的实现中的一个问题，包括问题中提到的那个，即当查询具有2个自由参数和第3个参数是带有不同ground元素的列表时，它们都会进入无限循环。当然，正确的行为是失败。 使用比较谓词 我认为为了避免未使用的选择点并保持好的实现声明性，没有必要像问题中提出的那样使用比较谓词，但我同意这可能是一个品味或倾向的问题。 实现 按照以下顺序考虑三个互斥的情况：如果第二个参数是ground，则递归访问它；否则，如果第三个参数是ground，则检查它，然后递归访问；否则，为第二个和第三个参数生成合适的列表。
occurrences(X, L, Os) :-
  ( nonvar(L) -> occs(L, X, Os) ;
    ( nonvar(Os) -> check(Os, X), glist(Os, X, L) ; v_occs(L, X, Os) ) ).

访问ground 2（列表中的第二个参数）有三种情况，当列表不为空时：如果它的头部和上面的X是地面且可统一的，则X在结果出现列表的头部，没有其他选择；否则，有两个备选项，X与头部不同或与头部统一。
occs([],_,[]).
occs([X|R], Y, ROs) :-
  ( X==Y -> ROs=[X|Rr] ; foccs(X, Y, ROs, Rr) ), occs(R, Y, Rr).

foccs(X, Y, ROs, ROs) :- dif(X, Y).
foccs(X, X, [X|ROs], ROs).

检查第三个参数的基础是确保其所有成员与X统一。原则上，此检查可以由glist/3执行，但通过这种方式可以避免未使用的选择点。

check([], _).
check([X|R], X) :- check(R, X).

访问具有免费第二参数的地面3号参数必须通过向生成的列表添加与X不同的变量来终止。在每个递归步骤中，有两种选择：生成列表的当前头是访问列表的当前头，必须与X可统一，或者是与X不同的自由变量。这只是一个理论性描述，因为实际上存在无数解决方案，并且当列表头是变量时永远不会到达第三个子句。因此，下面的第三个子句被注释掉，以避免无用的选择点。
glist([], X, L) :- gdlist(L,X).
glist([X|R], X, [X|Rr]) :- glist(R, X, Rr).
%% glist([X|R], Y, [Y|Rr]) :- dif(X, Y), glist([X|R], Y, Rr).

gdlist([], _).
gdlist([Y|R], X) :- dif(X, Y), gdlist(R, X).

最后处理所有参数都为空的情况，方法类似于前面的情况，并且存在着一些解决方案模式无法生成的问题：

v_occs([], _, []).
v_occs([X|R], X, [X|ROs]) :- v_occs(R, X, ROs).
%% v_occs([X|R], Y, ROs) :- dif(Y, X), v_occs(R, Y, ROs). % never used

示例测试

?- occurrences(1,[E1,1,2,1,E2],Fs).
Fs = [1,1],
dif(E1,1),
dif(E2,1) ? ;
E2 = 1,
Fs = [1,1,1],
dif(E1,1) ? ;
E1 = 1,
Fs = [1,1,1],
dif(E2,1) ? ;
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
no

?- occurrences(1,L,[1,2]).
no

?- occurrences(1,L,[1,E,1]).
E = 1,
L = [1,1,1] ? ;
E = 1,
L = [1,1,1,_A],
dif(1,_A) ? ;
E = 1,
L = [1,1,1,_A,_B],
dif(1,_A),
dif(1,_B) ? ;
   ...
1
我赞赏occurrences(1,L,[1,2]).的终止（和正确失败），但是为什么专业化L = [_|_], occurrences(1,L,[1,2]).会循环？问题确实在于案例分析。还有一个风格方面：您混合了逻辑和过程方面。其他一些方法尝试将不纯的代码集中到一些通用的纯谓词(if_/3, (=)/3)中，以便实际代码保持纯净。 - false
我敢打赌（我没有时间测试）如果给定的列表参数不是自由或正确关闭的列表，那么所有实现都会循环，这是正确的，因为在Prolog中没有任何限定词的_list_表示一个封闭的列表。所以你提到的专业化将导致循环也就不足为奇了。至于风格方面，这是可以讨论的，特别是当你的问题涉及到实现层面的效率问题时。在我看来，“纯粹”并不意味着“声明式”，而且当效率成为关键时，我更喜欢编写基于Prolog的程序。 - migfilg
1
通常认为终止也是单调的，但在您的情况下并非如此。也就是说，通常认为如果 Q 终止，则 L = [_|_], Q 也将终止。 - false
非常有趣。也许你想尝试一下这里出现的其他实现，使用查询L=[X|X], Q，除了我的实现，似乎你期望它们都会终止。由于这个讨论没有任何进展，我就在这里退出了：祝你有美好的一天。 - migfilg
我不理解你的评论。对于所有其他实现来说，以下是正确的：如果 Q 终止，则 L = [_|_]，Q 终止。 - false
我认为你会理解我的观点：如果参数可以是任何东西，那么谓词的描述就有误了，因为它说最后两个是列表（= properly closed lists）。我可以向你保证，在我的程序中，我会避免你提到的情况。但是，如果可以使用任何术语，那么我建议你尝试使用一个循环术语进行测试，也许你会明白，在其他实现中需要更多不纯的代码来摆脱它。至于我，这就是我要说的全部。 - migfilg
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接