list - append/3 的具体谓词变体的冗余答案

Question

我想为一些人提供一个逻辑上纯粹的解决方案 此论坛中的 other recent problem。

作为开始，我实现了 append/3 的具体化变体并将其命名为 appendR/4。它基于 Prolog union for A U B U C 中 @false 实现的谓词 if_/3 和 (=)/3 :

appendR([],Ys,Zs,T) :- 
    =(Ys,Zs,T).
appendR([X|Xs],Ys,ZZs,T) :-
    if_([X|Zs] = ZZs, appendR(Xs,Ys,Zs,T), T = false).

如以下查询所示，实现基本有效:

?- appendR([1,2],Ys,[2,3,4],T).
T = false ? ;
no

?- appendR([1,2],[3,4],Xs, T).
T = true,  Xs = [1,2,3,4],                       ? ;
T = false, Xs = [1,2|_A],  prolog:dif([3,4],_A)  ? ;
T = false, Xs = [1|_A],    prolog:dif([2|_B],_A) ? ;
T = false,                 prolog:dif([1|_A],Xs) ? ;
no

到目前为止，还不错……棘手的部分来了:

?- appendR([1,2],Ys,[1,2,3,4],T).
T = true,  Ys = [3,4]                   ? ;
T = false, prolog:dif(Ys,[3,4])         ? ;
T = false, prolog:dif([2|_A],[2,3,4])   ? ;
T = false, prolog:dif([1|_A],[1,2,3,4]) ? ;
no

我想得到前两个答案，但不想得到后两个答案。请帮忙!

Answer 1

我还编写了一个替代变体 appendRR/4:

appendRR([],Ys,Zs, T) :- 
    =(Ys,Zs,T).
appendRR([_|_],_,[], false).
appendRR([X|Xs],Ys,[Z|Zs], T) :-
    if_(X=Z, appendRR(Xs,Ys,Zs,T), T = false).

它不会给出多余的答案:

?- appendRR([1,2],Ys,[1,2,3,4],T).
T = true,  Ys = [3,4]           ? ;
T = false, prolog:dif(Ys,[3,4]) ? ;
no

但是，目标 appendRR([1,2],_,foo,T) 失败了。我更愿意得到答案 T = false。这有点让我烦恼。

如果 appendRR 的调用者可以保证非列表术语永远不会被用作 appendRR/4 的第三个参数，我仍然觉得可以容忍。