追加/ 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。它應該結合「最佳」appendR/4和appendRR/4。

首先，我們定義了物化的非空列表測試謂詞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). 

---

讓我們來查詢並比較我們得到的答案！突出顯示不良結果（以加粗表示）。

1.  
   ?- 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\=[_|_]). 
   

2.  
   ?- 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]). 
   

3.  
   ?- 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. 
   

4.  
   ?- 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沒有。