What minimal change to my code would make it preserve logical purity?

Question

I posted the code below as an answer to this question and user "repeat" answered and commented that it's not logically pure and "if you are interested in a minimal change to your code that makes it preserve logical-purity, I suggest posting a new question about that. I'd be glad to answer it :)".

% minset_one(1 in D1, 1 in D2, D1, D2, D1Len, D2Len, T).
minset_one_(true,  false, D1, _,  _,     _,     D1).
minset_one_(false, true,  _,  D2, _,     _,     D2).
minset_one_(true,  true,  _,  D2, D1Len, D2Len, D2) :- D1Len >= D2Len.
minset_one_(true,  true,  D1, _,  D1Len, D2Len, D1) :- D1Len < D2Len.

minset_one(D1, D2, T) :-
    (member(1, D1) -> D1check = true ; D1check = false),
    (member(1, D2) -> D2check = true ; D2check = false),
    length(D1, D1Len),
    length(D2, D2Len),
    
    minset_one_(D1check, D2check, D1, D2, D1Len, D2Len, T).

e.g.

?- D1 = [X,Y,Z], D2 = [U,V], minset_one(D1,D2,T).

D1 = [1, Y, Z],
D2 = T, T = [1, V],
U = X, X = 1 ;

false

there are more solutions possible. member(1, D1) is not backtracking through [1, Y, Z], then [X, 1, Z] then [X, Y, 1].

Answer 1

The Problem with (->)/2 (and friends)

Consider the following goal:

(member(1,D1) -> D1check = true ; D1check = false)

(->)/2 commits to the first answer of member(1,D1)—other answers are disregarded.

Can alternatives to (->)/2—like (*->)/2 (SWI, GNU) or if/3 (SICStus)—help us here?

No. These do not ignore alternative answers to make member(1,D1) succeed, but they do not consider that the logical negation of member(1,D1) could also have succeeded.

Back to basics: "If P then Q else R" ≡ "(P ∧ Q) ∨ (¬P ∧ R)"

So let's rewrite (If -> Then ; Else) as (If, Then ; Not_If, Else):

(member(1,D1), D1check = true ; non_member(1,D1), D1check = false)

How should we implement non_member(X,Xs)—can we simply write \+ member(X,Xs)?

No! To preserve logical purity we better not build upon "negation as finite failure".

Luckily, combining maplist/2 and dif/2 does the job here:

non_member(X,Xs) :-
   maplist(dif(X),Xs).

Putting it all together

So here's the minimum change I propose:

minset_one_(true,  false, D1, _,  _,     _,     D1).
minset_one_(false, true,  _,  D2, _,     _,     D2).
minset_one_(true,  true,  _,  D2, D1Len, D2Len, D2) :- D1Len >= D2Len.
minset_one_(true,  true,  D1, _,  D1Len, D2Len, D1) :- D1Len < D2Len.

non_member(X,Xs) :- 
   maplist(dif(X),Xs).

minset_one(D1, D2, T) :-
   (member(1,D1), D1check = true ; non_member(1,D1), D1check = false),
   (member(1,D2), D2check = true ; non_member(1,D2), D2check = false),
   length(D1, D1Len),
   length(D2, D2Len),
   minset_one_(D1check, D2check, D1, D2, D1Len, D2Len, T).

Running the sample query we now get:

?- D1 = [X,Y,Z], D2 = [U,V], minset_one(D1,D2,T).
   D1 = [1,Y,Z], X = U, U = 1, D2 = T, T = [1,V]
;  D1 = [1,Y,Z], X = V, V = 1, D2 = T, T = [U,1]
;  D1 = T, T = [1,Y,Z], X = 1, D2 = [U,V], dif(U,1), dif(V,1)
;  D1 = [X,1,Z], Y = U, U = 1, D2 = T, T = [1,V]
;  D1 = [X,1,Z], Y = V, V = 1, D2 = T, T = [U,1]
;  D1 = T, T = [X,1,Z], Y = 1, D2 = [U,V], dif(U,1), dif(V,1)
;  D1 = [X,Y,1], Z = U, U = 1, D2 = T, T = [1,V]
;  D1 = [X,Y,1], Z = V, V = 1, D2 = T, T = [U,1]
;  D1 = T, T = [X,Y,1], Z = 1, D2 = [U,V], dif(U,1), dif(V,1)
;  D1 = [X,Y,Z], D2 = T, T = [1,V], U = 1, dif(X,1), dif(Y,1), dif(Z,1)
;  D1 = [X,Y,Z], D2 = T, T = [U,1], V = 1, dif(X,1), dif(Y,1), dif(Z,1)
;  false.

Better. Sure looks to me like there's nothing missing.

Answer 2

I think it would be:

add:

:- use_module(library(reif)).

... and replace:

    %(member(1, D1) -> D1check = true ; D1check = false),
    %(member(1, D2) -> D2check = true ; D2check = false),
    memberd_t(1, D1, D1check),
    memberd_t(1, D2, D2check),

Example of the difference between member and memberd_t:

?- member(X, [A, B, C]).
X = A ;
X = B ;
X = C.

?- memberd_t(X, [A, B, C], IsMember).
X = A,
IsMember = true ;
X = B,
IsMember = true,
dif(A,B) ;
X = C,
IsMember = true,
dif(A,C),
dif(B,C) ;
IsMember = false,
dif(A,X),
dif(B,X),
dif(C,X).

?- memberd_t(X, [A, B, C], IsMember), X = 5, A = 5, C = 5.
X = A, A = C, C = 5,
IsMember = true ;
false.

So, memberd_t is itself adding the dif/2 constraints. To aid performance slightly, it loops through the list only once.

The definition of memberd_t is at e.g. https://github.com/meditans/reif/blob/master/prolog/reif.pl#L194 and https://www.swi-prolog.org/pack/file_details/reif/prolog/reif.pl?show=src