prologlogical-purity

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

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

Solution

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