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

Question

纯粹的Prolog程序以清晰的方式区分术语的平等和不平等,导致执行效率低下; 即使所有相关术语都是基础的.

关于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.

这可以通过使用足够大的as 列表来观察如下.您可能需要调整,I以便仍然可以表示列表; 在SWI,这意味着

1mo I必须小到足以防止全局堆栈的资源错误,如下所示:

?- 24=I,N is 2^I,length(L,N), maplist(=(a),L).
ERROR: Out of global stack

2 I必须足够大才能引发本地堆栈的资源错误:

?- 22=I,N is 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. % syntactically different
equality_reified(X, Y, R) :- X \= Y, !, R = false. % semantically different
equality_reified(X, X, true).
equality_reified(X, Y, false) :-
   dif(X, Y).

编辑:我不清楚X \= Y在存在约束的情况下是否是合适的防守.没有约束,?=(X, Y)或者X \= Y是相同的.

---

例

正如@ user1638891所建议的,这是一个如何使用这种原语的例子.垫子的原始代码是:

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)个选择点(最后一个[]).

Answer 1

好吧,有一点,名称应该更具说明性,比如equality_truth/2.

Answer 2

以下代码基于if_/3和(=)/3(又名equal_truth/3),由Prolog union for AUBUC中的@false实现:

=(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.

Answer 3

似乎最好用相同的参数调用这个谓词(=)/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) ).