Избыточные ответы варианта уточненного предиката append/3

Question

Я хотел предложить логически чистое решение некоторых других недавних проблем на этом форуме.

Для начала я внедрил усовершенствованный вариант append/3 и назвал это appendR/4, Он основан на предикатах if_/3 а также (=)/3 реализовано @false в объединении Prolog для AUBUC:

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 = ложь, Cs = [] 
    ; T = ложь, 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], стоп-кадр (_X,_X\=[_|_]); T = false, Cs = [_X|_], dif(_X,1); T = false, заморозить (Cs, Cs \ = [_ | _]).
   

2. ? - appendR ([1,2], Bs, [1,2,3,4], T). Т = верно, Bs = [3,4]; T = false, dif (Bs, [3,4]); Т = ложь; Т = ложь.? - appendRR ([1,2], Bs, [1,2,3,4], T). Т = верно,     Bs=[3,4]; T = false, dif(Bs,[3,4]).?- append_t([1,2],Bs,[1,2,3,4],T). Т = верно, Bs = [3,4]; T = false, dif (Bs, [3,4]). 

3. ? - appendR ([1,2], _, [2,3,4], T).
   Т = ложь.?- appendRR([1,2],_,[2,3,4],T).
   Т = ложь.?- append_t([1,2],_,[2,3,4],T).
   Т = ложь.
   

4. ? - appendR ([1,2], _, non_list, T).
   Т = ложь.
   
   ? - appendRR ([1,2], _, non_list, T). 
    ложный.? - append_t ([1,2], _, non_list, T).
   Т = ложь.
   

Резюме: appendR/4 а также appendRR/4 потерпеть неудачу с некоторыми тестами, append_t/4 не.