Search code examples
listprologreificationlogical-purity

Redundant answers of reified predicate variant of append/3


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!


Solution

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