Converting if-then in Prolog to multiple clauses with reification

Question

I want to design a top-level interface for Prolog that is not buggy (where ! successfully cuts choicepoints, not if-then causing choicepoints to be buggily cut). I thought that I could convert if-then to clauses where the truth of the antecedent is reified and its truth is tested to be true or false at the start of each clause.

For example, test1 below shows the original if-then clause.

test1:-(a1(1)->b1;c1).
a1(1).
b1.
c1.

Answer 1

With the help of library(reif) also more complex conditions can be reified. In particular, conjunctions and disjunctions of any reified condition. So facts can be encoded as a disjunction (one alternative per fact) of a conjunction (one = per argument). Of course, neither direct cuts nor a soft cut like *-> can solve this problem alone. See char_class/2 for such an example.

To better illustrate the use of library(reif), here is a correct implementation of @brebs' member_other/3. It is just as determinate as brebs expects it to be, in addition it is correct for the cases where brebs' implementation is was broken. Some benchmarks at the end show that this solution is sometimes the fastest and most space efficient.

member_other(E, Lst, Elem) :-
   if_(memberd_t(E, Lst), E = Elem, other(E) = Elem).

?- member_other(E, [a,b], O).
   E = a, O = a
;  E = b, O = b
;  O = other(E), dif(a,E), dif(b,E).
?- member_other(b, [a,b], O).
   O = b.
?- member_other(c, [a,b], O).
   O = other(c).
?- member_other(a, [a], other(a)).
   false.
?- freeze(E,(E=a;E=b)), member_other(E,[c],R).
   R = other(E),
   freeze(E, (E=a;E=b)).  % brebs has a redundant dif(E, c).
?- freeze(E,E < 0), numlist(1,400000,L), time(member_other(E,L,R)).
%  3,600,003 inferences, 0.280 CPU in 0.280 seconds (100% CPU, 12836803 Lips)
% vs. brebs' and newbrebs:
% 13,200,005 inferences, 1.382 CPU in 1.382 seconds (100% CPU,  9554032 Lips)
%  3,600,004 inferences, 0.263 CPU in 0.263 seconds (100% CPU, 13688070 Lips)
?- numlist(1,400000,L), time(member_other_if(-1,L,R)).
%    800,003 inferences, 0.042 CPU in 0.042 seconds (100% CPU, 18944780 Lips)
% vs. brebs' and newbrebs:
%  2,000,004 inferences, 0.203 CPU in 0.203 seconds (100% CPU,  9834699 Lips)
%    800,004 inferences, 0.043 CPU in 0.043 seconds (100% CPU, 18709716 Lips)
?- numlist(1, 4000, L), time(member_other_if(E, L, other(M))).
% 288,115,984 inferences, 14.393 CPU in 14.396 seconds (100% CPU, 20018259 Lips)
% vs. brebs' and newbrebs which is much faster in this case:
%     104,005 inferences,  0.019 CPU in  0.019 seconds (100% CPU,  5563599 Lips)
%     112,005 inferences,  0.037 CPU in  0.037 seconds (100% CPU, 3011414 Lips)

The major difference between both versions can best be seen with the following query:

?- member_other(E,[A,B,C],R).
   E = A, R = E
;  E = B, R = E, dif:dif(A,E)
;  E = C, R = E, dif:dif(A,E), dif:dif(B,E)
;  R = other(E), dif:dif(A,E), dif:dif(B,E), dif:dif(C,E).
?- member_other_brebs(E,[A,B,C],R).
   E = A, R = E
;  E = B, R = E, partially_redundant
;  E = C, R = E, partially_redundant
;  R = other(E), dif:dif(E,A), dif:dif(E,C), dif:dif(E,B).

So brebs' version admits the same redundancies that also member/2 does. The deeper problem behind is that it seems difficult to ensure that brebs' version is indeed pure and monotonic, as was shown by this lengthy development process.

And here is its expansion for SICStus with module prefixes removed such that it can be used also with systems whose differing goal expansion mechanisms do not produce the optimal result like (currently) SWI and Scryer.

member_other(A,B,C) :-
   memberd_t(A,B,D),
   (  D==true ->
      A=C
   ;  D==false ->
      other(A)=C
   ;  nonvar(D) ->
      throw(error(type_error(boolean,D),type_error(call(user:memberd_t(A,B),D),2,boolean,D)))
   ;  throw(error(instantiation_error,instantiation_error(call(user:memberd_t(A,B),D),2)))
   ).

memberd_t(A, B, C) :-
   i_memberd_t(B, A, C).

i_memberd_t([], _, false).
i_memberd_t([A|B], C, D) :-
   (  A\=C ->
      i_memberd_t(B, C, D)
   ;  A==C ->
      D=true
   ;  A=C,
      D=true
   ;  dif(A, C),
      i_memberd_t(B, C, D)
   ).

Answer 2

Here, test2 shows how if-then has been converted into separate clauses. So, test1. does the same thing as test2., but test2's choicepoints are available to cut, as against the if-then clause in test1 possibly causing choicepoints to be buggily cut.

test2:-a2(1,R),d2(R). 

a2(1,true).
a2(_,false).
d2(true):-b2,!. 
d2(false):-c2.
b2.
c2.

Answer 3

As an example of determinism:

member_other(Elem, Lst, Member) :-
    member_other_(Lst, Elem, [], Member).
    
% Can be other
member_other_([], Elem, DL, other(Elem)) :-
    % Have delayed adding attributes to Elem, for performance
    maplist(dif(Elem), DL).
member_other_([H|T], E, DL, M) :-
    (   H \= E
    % Fast failure, no need for dif
    ->  member_other_(T, E, DL, M)
    ;   (   H == E
        % Certain match, can ignore DL
        ->  Eq = true
        % Unsure, add to DL list
        ;   DL1 = [H|DL]
        ),
        member_other_eq_(Eq, T, H, E, DL1, M)
    ).

member_other_eq_(true, _, E, E, _, member(E)).
member_other_eq_(false, T, _, E, DL, M) :-
    member_other_(T, E, DL, M).

Results in swi-prolog:

?- member_other(a, [a], M).
M = member(a).

?- member_other(E, [a,b], M).
E = a,
M = member(a) ;
E = b,
M = member(b) ;
M = other(E), % Loops through all choices
dif(E, a),
dif(E, b).

?- member_other(b, [a,b,c], M).
M = member(b). % Nice determinism

?- member_other(c, [a,b], M).
M = other(c). % Nice determinism

?- freeze(L, (L=[a] ; L=[b])), member_other(a, L, other(a)).
L = [b].

dif is being used, to segregate the other (final) alternative from the list members - applied only to the necessary variables, and applied as late as possible (for performance, because adding attributes to variables slows down comparisons).

The list is treated as a set.

Performance comparison:

?- numlist(1, 4000, L), time(member_other(E, L, other(M))), sleep(3).
% 112,004 inferences, 0.022 CPU in 0.022 seconds (100% CPU, 5032910 Lips)

Versus using if_:

?- numlist(1, 4000, L), time(member_other_if(E, L, other(M))), sleep(3).
% 288,115,984 inferences, 6.124 CPU in 6.139 seconds (100% CPU, 47043287 Lips)

... defined as:

member_other_if(E, Lst, Elem) :-
   if_(memberd_t(E, Lst), member(E) = Elem, other(E) = Elem).

Answer 4

In order to find the pure building blocks of @brebs' approach:

member_other_ifc(E, Lst, Elem) :-
   if_(memberc_t(E, Lst), member(E) = Elem, other(E) = Elem).

memberc_t(E, Xs, T) :-
   i_memberc_t(Xs, E, [], T).

i_memberc_t([], E, Ds, false) :-
   maplist(dif(E), Ds).
i_memberc_t([X|Xs], E, Ds, T) :-
   (  X \= E -> i_memberc_t(Xs, E, Ds, T)
   ;  X == E -> T = true
   ;  X = E, T = true
   ;  i_memberc_t(Xs, E, [X|Ds], T)
   ).

memberc(X, Xs) :-
   memberc_t(X, Xs, true).

?- memberc(B,[A,B|Xs]).
   B = A, redundant
;  true.
?- memberc(B,Xs).
   Xs = [B|_A]
;  Xs = [_A,B|_B], partially_redundant
;  Xs = [_A,_B,B|_C], partially_redundant
;  Xs = [_A,_B,_C,B|_D], partially_redundant
;  ... .
?- memberc(B,"aaa").
   B = a
;  B = a, redundant
;  B = a, redundant
;  false.

So this version has quite favorable termination conditions, quite similar to memberd/2 and at the same time has less dif/2-bulk to maintain. That, at the price of redundancies.

memberc/2 can be specialized to:

memberc(E, [X|Xs]) :-
   (  E == X -> true
   ;  E = X
   ;  memberc(E, Xs)
   ).