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

Question

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

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

中实现的谓词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的第三个参数永远不会使用非列表项，我觉得还是可以容忍的。

Answer 2

下次尝试：append_t/4。它应该结合 and .

的 "best"

首先，我们定义具体化的非空列表测试谓词cons_t/2:

cons_t(V,T) :- 
   (  nonvar(V)                         % we can decide right now!
   -> (  V = [_|_]
      -> T = true
      ;  T = false
      )
   ;  V = [_|_],          T = true      % go nondet!
   ;  freeze(V,V\=[_|_]), T = false
   ).

在 cons_t/2、(=)/3 和 if_/3 的基础上，我们定义 append_t/4 如下：

append_t([],Bs,Cs,T) :-
   =(Bs,Cs,T).
append_t([A|As],Bs,Cs0,T) :-
   if_(cons_t(Cs0),
       (Cs0=[C|Cs], if_(A=C, append_t(As,Bs,Cs,T), T=false)),
       T=false).

让我们查询并比较我们得到的答案！错误的结果会突出显示（以粗体书写）。

?- appendR([1,2],[3,4],Cs,T).
  T = true ,     Cs=[1,2,3,4]
; T = false,     Cs=[1,2|_X] , dif(_X,[3,4])
; T = false,     Cs=[1|_X]   , dif(_X,[2|_])
; T = false, dif(Cs,[1|_]).

?- appendRR([1,2],[3,4],Cs,T).
  T = false, Cs = []
; T = false, Cs = [1]
; T = true , Cs = [1,2,3,4]
; T = false, Cs = [1,2|_X] , dif(_X,[3,4])
; T = false, Cs = [1,_X|_] , dif(_X,2)
; T = false, Cs = [_X|_]   , dif(_X,1).

?- append_t([1,2],[3,4],Cs,T).
  T = true , Cs = [1,2,3,4]
; T = false, Cs = [1,2|_X] , dif(_X,[3,4])
; T = false, Cs = [1,_X|_] , dif(_X,2)
; T = false, Cs = [1|_X]   , freeze(_X,_X\=[_|_])
; T = false, Cs = [_X|_]   , dif(_X,1)
; T = false, freeze(Cs,Cs\=[_|_]).

?- appendR([1,2],Bs,[1,2,3,4],T).
  T = true ,     Bs=[3,4]
; T = false, dif(Bs,[3,4])
; T = false
; T = false.

?- appendRR([1,2],Bs,[1,2,3,4],T).
  T = true ,     Bs=[3,4]
; T = false, dif(Bs,[3,4]).

?- append_t([1,2],Bs,[1,2,3,4],T).
  T = true ,     Bs=[3,4]
; T = false, dif(Bs,[3,4]).

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

?- appendRR([1,2],_,[2,3,4],T).
T = false.

?- append_t([1,2],_,[2,3,4],T).
T = false.

?- appendR([1,2],_,non_list,T).
T = false.

?- appendRR([1,2],_,non_list,T).
false.

?- append_t([1,2],_,non_list,T).
T = false.

总结： appendR/4 和 appendRR/4 一些测试用例失败，append_t/4 没有。

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

Redundant answers of reified predicate variant of append/3

list

prolog

reification

logical-purity