different/2 - does a pure, determinate definition

Question

different(Xs, Ys) :-
   member(X, Xs),
   non_member(X, Ys).
different(Xs, Ys) :-
   member(Y, Ys),
   non_member(Y, Xs).

While this definition using member/2 and non_member/2 is almost¹ perfect from a declarative viewpoint, it produces redundant solutions for certain queries and leaves choice points all around.

What is a definition that improves upon this (in a pure manner probably using if_/3 and (=)/3) such that exactly the same set of solutions is described by different/2 but is determinate at least for ground queries (thus does not leave any useless choice points open) and omits (if possible) any redundant answer?

---

¹ _{Actually, different([a|nonlist],[]), different([],[b|nonlist]) succeeds. It could equally fail. So a solution that fails for both is fine (maybe even finer).}

Answer 1

Next contestant to the code beauty pageant!-)

This answer shows a refactored variation of code shown in a previous answer. It uses reified conjunction and disjunction:

and_(P_1,Q_1) :-
   and_t(P_1,Q_1,true).

or_(P_1,Q_1) :-
   or_t(P_1,Q_1,true).

and_t(P_1,Q_1,Truth) :-
   if_(P_1, call(Q_1,Truth), Truth=false).

or_t(P_1,Q_1,Truth) :-
   if_(P_1, Truth=true, call(Q_1,Truth)).

Note the two versions for both "and" and "or"; the ones with suffix _t have an extra argument for the truth value, the ones without the suffix do not and assume that Truth=true should hold.

Based on and_t/3 and on reified term inequality predicate dif/3, we define nonmember_t/3:

nonmember_t(X,Ys,Truth) :-
   list_nonmember_t(Ys,X,Truth).

list_nonmember_t([]    ,_, true).
list_nonmember_t([Y|Ys],X,Truth) :-
   and_t(dif(X,Y), list_nonmember_t(Ys,X), Truth).

Now, let's define some_absent_t/3, different_t/3 and different/2, like so:

some_absent_t([]    ,_ ,false).
some_absent_t([X|Xs],Ys,Truth) :-
   or_t(nonmember_t(X,Ys), some_absent_t(Xs,Ys), Truth).

different_t(Xs,Ys,Truth) :-
   or_t(some_absent_t(Xs,Ys),
        some_absent_t(Ys,Xs),
        Truth).

different(Xs,Ys) :-
   different_t(Xs,Ys,true).

Does it still run?

?- different([A,B],[X,Y]).
      A=X ,               B=X ,           dif(Y,X)
;     A=X ,           dif(B,X), dif(B,Y)
;               A=Y ,               B=Y , dif(Y,X), dif(Y,X)
;               A=Y , dif(B,X), dif(B,Y), dif(Y,X)
; dif(A,X), dif(A,Y).                     % same result as before

?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]),
   different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]),
   different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]).
true.                                    % same result as before

Looks alright!

All in all, not a huge improvement over existing answers, but IMO somewhat more readable code, and a reified version of different/2 as an added bonus!

Answer 2

The following bold bounty (+500) was offered not too long ago:

^{An idiomatic answer is still missing here. For example, or_t/3 should rather be (;)/3. There is more to it.}

Challenge accepted! This answer is a follow-up to this previous answer.

1. We use the reified logical connective (;)/3, which can be defined like this:

   ';'(P_1,Q_1,T) :- if_(P_1, T=true, call(Q_1,T)).
   

2. Next, we define the meta-predicate call_/1. It is useful with reified predicates used in this answer. With its name and semantics, call_/1 follows if_/3, and_/2, and or_/2!

   call_(P_1) :- call(P_1,true).
   

3. Using (;)/3, call_/1, and some_absent_t/3 we implement different/2:

   different(As,Bs) :- call_((some_absent_t(As,Bs) ; some_absent_t(Bs,As))).
   

Done! That's it.

---

Let's re-run the queries we used in previous answers!

?- different([5,4],[1,2]).
true.

?- different([1,2,3],[2,3,1]).
false.

?- different([4,2,3],[2,3,1]), different([1,4,3],[2,3,1]), different([1,2,4],[2,3,1]),
   different([1,2,3],[4,3,1]), different([1,2,3],[2,4,1]), different([1,2,3],[2,3,4]).
true.

Same queries, same answers... Looks alright to me!

Answer 3

First try!

The following code is based on the meta-predicates tfilter/3 and tpartition/4, the monotone if-then-else control construct if_/3, the reified unary logical connective not_t/3, and the reified term equality predicate (=)/3:

different([],[_|_]).
different([X|Xs0],Ys0) :-
   tpartition(=(X),Ys0,Es,Ys1),
   if_(Es=[], true, (tfilter(not_t(=(X)),Xs0,Xs1),different(Xs1,Ys1))).

Sample query:

?- different([A,B],[X,Y]).
                A=Y ,           dif(B,Y),     X=Y
;     A=X           ,     B=X           , dif(X,Y)
;     A=X           , dif(B,X), dif(B,Y), dif(X,Y)
;               A=Y ,               B=Y , dif(X,Y)
;               A=Y , dif(B,X), dif(B,Y), dif(X,Y)
; dif(A,X), dif(A,Y).

Let's observe determinism when working with ground data:

?- different([5,4],[1,2]).
true.

The above approach feels like a step in the right direction... But, as-is, I wouldn't call it perfect.

Answer 4

Conerning solutions that use if_, I would say an alternative approach would be to use constructive negation from the beginning. Constructive negation was researched already in the 80's, a pioneer was David Chan, and still pops up from time to time.

Assume we have a Prolog interpreter which has a constructive negation (~)/2. This constructive negation (~)/2 can be used to define a declarative if-then-else as follows, lets call this operator (~->)/2:

  (A ~-> B; C) :- (A, B); (~A, C).

If the Prolog interpreter has also embedded implication (=>)/2 besides constructive negation, one could alternatively define a declarative if-then-else as follows, lets call this operator (~=>)/2:

  (A ~=> B; C) :- (A => B), (~A => C).

Note the switch from disjunction (;)/2 to conjunction (,)/2. Ask the Binary Decision Diagram (BDD) people why they are logically equivalent. Procedurally there are nuances, but through the backdoor of embedded implication for certain A, the second if-then-else variant will also introduce non-determinancy.

But how would we go about and introduce for example constructive negation in a Prolog interpreter. A straight forward way would be to delegate constructive negation to a constraint solver. If the constraint solver has reified negation this can be done as follows:

 ~ A :- #\ A.

But there not so many constraint solvers around, that would permit a sensible use for examples such as member/2 etc.. Since often they provide reified negation only for domains such as finite integers, rationals, etc.. But for a predicate such as member/2 we would need reified negation for the Herbrand universe.

Also note that the usual approaches for constructive negation also assume that the ordinary rule implication gets another reading. This means that usually under constructive negation, we could pick the ordinary member/2 definition, and get query results such as:

?- ~ member(X, [a,b,c]).
dif(X, a),
dif(X, b),
dif(X, c).

But again the reified negation will hardly easily work with defined predicates, so that the following query will probably not work:

?- #\ member(X, [a,b,c]).
/* typically won't work */

If the above succeeds than any of the declarative if-then-else such as (~->)/2 or (~=>)/2 will have less frequent use, since ordinary predicate definitions will already deliver declarative interpretation by the Prolog interpreter. But why is constructive negation not wide spread? One reason might be the large design space of such a Prolog interpreter. I noticed that we would have the following options:

Backward Chaining: We would basically spit the vanilla interpreter solve/1 into two predicates solvep/1 and solven/1. solvep/1 is responsible for solving positive goals and solven/1 is responsible for solving negative goals. When we try this we will sooner or later see that we need more careful treatment of quantifiers and probably end up with a quantifier elimination method for the Herbrand domain.

Forward Chaining: We will also notice that in backward chaining we will run into problems for the modelling of clauses with disjunction or existential quantifier in the head. This has to do with the fact that the sequent calculus suitable for Prolog has only one formula on the right hand side. So either we go multi formula on the right hand side and will loose paraconsistency, or we use forward chaining.

Magic Sets: But forward chaining will polute the solution spaces in an uncontrolled way. So we might need some form of combination of forward and backward chaining. I don't mean by that only, that we should be able dynamically switch between the two during the solution process, but I mean that we nead also a means to generate sets that direct the forward chaining process.

More problems are also noted in this answer here. This doesn't mean that sooner or later a formula will be found, to fit all this problem and solution pairs together, but it might take some more time.

Bye

Answer 5

Let's take it to the limit---by the help of list_nonmember_t/3, exists_in_t/3, and or_/2!

some_absent_t(Xs,Ys,Truth) :-
   exists_in_t(list_nonmember_t(Ys),Xs,Truth).

different(Xs,Ys) :-
   or_(some_absent_t(Xs,Ys),
       some_absent_t(Ys,Xs)).

Answer 6

Here's another try! We utilize the monotone if-then-else control construct if_/3, in combination with the reified list membership predicate memberd_t/3, and first argument indexing to avoid the creation of useless choice-points.

different(Xs,Ys) :-
   different_aux(Xs,Ys,Xs,Ys).

different_aux([],[_|_],Xs0,Ys0) :-
   different_aux(Ys0,[],Ys0,Xs0).     % swap Xs/Ys pair
different_aux([X|Xs],Ys,Xs0,Ys0) :-
   if_(memberd_t(X,Ys0),
       different_aux(Ys,Xs,Ys0,Xs0),  % variant: different_aux(Xs,Ys,Xs0,Ys0)
       true).

First, we run a query that we expect to fail:

?- different([1,2,3],[2,3,1]).
false.

The following queries are similar to the failing query given above; each one has a single "different" item x placed at different indices in the first [1,2,3] or the second list [2,3,1]:

?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]),
   different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]),
   different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]).
true.                                 % all subgoals succeed deterministically

OK! Let's run another (quite general) query that I used in my previous answer:

?- different([A,B],[X,Y]).
      A=X ,               B=X , dif(Y,X)
;     A=X ,           dif(B,X), dif(Y,B)
;               A=Y , dif(B,X), dif(Y,X)
; dif(A,X), dif(A,Y).

Compact! A big improvement over what I presented earlier!