Redundant answers of reified predicate variant of append/3

Question

I wanted to offer a logically pure solution to some other recent problem in this forum.

As a start, I implemented a reified variant of append/3 and named it appendR/4. It is based on the predicates if_/3 and (=)/3 implemented by @false in Prolog union for A U B U C:

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

The implementation basically works, as shown by the following queries:

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

So far, so good... Here comes the tricky part:

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

I want to get the first two answers, but not the last two. Help, please!

Answer 1

I have also coded an alternative variant 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).

It does not give redundant answers:

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

However, the goal appendRR([1,2],_,foo,T) fails. I'd prefer getting the answer T = false. This is bugging me somewhat.

I still feel it can be tolerated if the caller of appendRR can guarantee that non-list terms will never be used as the 3rd argument of appendRR/4.

Answer 2

Next try: append_t/4. It should combine the "best" of appendR/4 and appendRR/4.

First, we define the reified non-empty-list testing predicate 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
   ).

Building on cons_t/2, (=)/3, and if_/3 we define append_t/4 like so:

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).

---

Let's queries and compare the answers we get! Bad results are highlighted (written in bold-face).

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.
   

Summary: appendR/4 and appendRR/4 fail with some test cases, append_t/4 does not.