期限平等/不平等的具体化
用纯净的方式区分术语的平等和不平等的Pure Prolog程序遭受执行效率低下的影响; 即使所有相关条款都是基础的。
最近的例子就是这个答案 。 所有的答案和所有的失败在这个定义是正确的。 考虑：
?- 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). 虽然从声明的angular度来看，程序是完美无瑕的，但是它在B，SICStus，SWI，YAP等当前系统上的直接执行却是不必要的低效。 为了以下目标，列表中的每个元素都保留一个select点。
发生（a，[a，a，a，a，a]，M）。 M = [a，a，a，a，a] ; 假的 。
这可以通过使用足够大a s列表来观察，如下所示。 你可能需要修改I ，使得列表仍然可以被表示。 在SWI这将意味着
1mo I必须小到足以防止全局堆栈的资源错误，如下所示：
？= 24 = 1，N是2 ^ I，长度（L，N），maplist（=（a），L）。 错误：超出全局堆栈
2 I必须足够大，以激发本地堆栈的资源错误：
？= 22 = I，N是2 ^ I，长度（L，N），maplist（=（a），L），（长度= ok;出现次数（a，L，M））。 我= 22， N = 4194304， L = [a，a，a，a，a，a，a，a，a | ...] 长度=好; 错误：超出本地堆栈
为了克服这个问题，仍然保留好的声明性属性，需要一些比较谓词。
这个比较谓词应该如何定义？
这是一个可能的定义：
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。
equal_reified（X，Y，R）： - ？=（X，Y），！，R = false。 ％在语法上不同
equal_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所build议的，这是一个例子，可以使用这样一个原语。 垫子的原始代码是：
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的第二个参数索引只有在您input查询（如occurrences(_,[],_) 之后才会被激活。 而且，SWI需要本质上非单调的if-then-else，因为它不在(;)/2 – 析取索引。 SICStus这样做，但只有第一个参数索引。 所以它留下一个（1）select点打开（最后是[] ）。
那么一方面，这个名字应该更具说明性，比如equality_truth/2 。
下面的代码是基于if_/3和(=)/3 （又名equal_truth/3 ），由Prolog union中的@false为AUBUC实现 ：
=(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
在某些情况下，一些更多的查询用于testingoccurrences/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.
似乎最好用相同的参数(=)/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月18日的矿取代。 我不build议因为下面的评论而被删除。
我以前的回答是错误的。 下面的一个针对问题中的testing用例运行，实现具有避免多余select点的期望特征。 我假设顶级谓词模式是？，+，？ 尽pipe其他模式可以很容易地实现。
该程序共有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
这是一个甚至更短的occurrences/3逻辑纯实现。
我们根据元谓词 tfilter/3 ，被定义的等式谓词(=)/3 ，以及协程allEqual_to__lazy/2 （在我之前对这个问题的回答中定义的）进行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 ...
我们得到相同的答案。
下面的occurrences/3的实现基于我以前的答案，即通过从第一个参数的子句索引机制中获益，以避免一些select点，并解决所有提出的问题。
此外，它应对所有潜在实现中的问题，包括问题中提到的一个问题，即当查询有2个第一个参数时，它们全部进入无限循环，第三个是具有不同地面元素的列表。 当然，正确的行为是失败的。
使用比较谓词
我认为，为了避免不必要的select点，并保持良好的执行声明程度，不需要在问题中提出一个比较谓词，但是我同意这可能是一个味道或倾向的问题。
履行
按照这个顺序考虑三个独占的情况：如果第二个参数是地面的，那么它被recursion地访问; 否则，如果第三个参数被磨削，它将被检查并recursion访问; 否则为第二和第三个参数生成合适的列表。
occurrences(X, L, Os) :- ( nonvar(L) -> occs(L, X, Os) ; ( nonvar(Os) -> check(Os, X), glist(Os, X, L) ; v_occs(L, X, Os) ) ).
第二个参数的访问有三种情况，当列表不为空时：如果它的头部和上面的X都是一致的并且是可以统一的，则X在结果列表的头部，并且没有别的select; 否则有两种select， 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来执行，但是这样可以避免不使用的select点。
check([], _). check([X|R], X) :- check(R, X).
使用空闲的第二个参数访问第三个参数必须通过向生成的列表中添加与X不同的variables来终止。 在每个recursion步骤中，有两种select：生成列表的当前头部是访问列表的当前头部，必须可以用X来统一，或者是与X不同的自由variables。 这只是一个理论上的描述，因为实际上有无数的解决scheme，当列表头是一个variables时，第三个子句将不会被达到。 因此，下面的第三个条款被注释掉，以避免不可用的select点。
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).
最后，所有参数都是自由的情况与前面的情况类似，并且有一些解决scheme模式没有被实际生成的类似问题：
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
示例testing
?- 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) ? ; ...
