different/2 - does a pure, determinate definition exist?

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).}

Contemptuous

Are we talking about lists or sets, because this can have some implications (especially with respect to efficiency). – Londalondon

@CommuSoft: I avoided to mention these closely related notions completely to better focus on the actual definition. Of course the intention would be to represent sets, but this knowledge should not change anything. In any case, it is possible to have duplicates! – Contemptuous

Furthermore this predicate seems to do a bit too much work: when querying with different([a,b],Y)., it gives: Y = [_G122], dif(_G122, a) ;, but the dif(_G122,a); is not necessary: even if it is equal to a, that's not a problem. Of course if one queries for different([a,b],[Y]), one gets dif(Y,a), dif(Y,b) and dif(Y,b),dif(Y,a), but still that's not necessary. – Londalondon

@CommuSoft: So far, I have not thought about redundancies on that level at all. I was completely absorbed by the inefficiency for ground queries. So if you succeed to find a pure definition that takes this into account - that would be even better! There are plenty of bounties :-) – Contemptuous

Answer 1

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

Pacheco

Answer 2

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.

Pacheco

You mean not_t/2, don't you? – Contemptuous

Is it determinate for the ground case? – Contemptuous

@false. I meant not_t(Goal,Param,Truth1) :- call(Goal,Param,Truth0), truth_negated(Truth0,Truth1). with truth_negated(true,false). truth_negated(false,true). IMO a third parameter is required for threading thru the item to be tested. – Pacheco

@false. Any hints/tips on how to systematically test for determinism? (possibly using the setup_call_cleanup/3 interface...) – Pacheco

det(G_0) :- setup_call_cleanup(true,G_0, Det=true), ( Det\==true -> throw(...) ; true). But the best would be to use a nice, catchy prefix op that fits into these debugging ops – Contemptuous

Answer 3

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!

Pacheco

Conjecture: different/2 (as given by the OP) is to different/2 (shown above) as CNF is to DNF. (Well, actually not exactly the definition given above, but the variant that doesn't swap Xs and Ys with every step---like the infamous split/3 does---but does so only once when the first argument is the empty list.) – Pacheco

Ultra-nit: The toplevel of SWI distinguished between last determinate answer and an aborted query by adding a single space. Consider the query true;false. which produces true . as response if you abort the query. Thus: adding spaces prior to the . - the end toke (* 6.4.8 *) insinuates that the answer was not determinate. – Contemptuous

Better. But is it intention revealing? – Contemptuous

@false. In some sense, the variation different_aux(Xs,Ys,Xs0,Ys0) is. I see it like this: the two clauses different/2 (given by the OP) are linked with "logical or" and may cause redundant solutions. different_aux OTOH links with "logical and". This makes it necessary to preserve Xs and Ys (as Prolog's backtracking doesn't do it anymore). – Pacheco

Answer 4

(Much inspired by @repeat's last answer, the names are still too clumsy)

different(Xs, Ys) :-
   if_(tnotexists_inlist_t(list_memberd_t(Ys), Xs),
      true,
      tnotexists_inlist_t(list_memberd_t(Xs), Ys)).

tnotexists_inlist_t(_P_2, [], false).
tnotexists_inlist_t(P_2, [E|Es], T) :-
   if_(call(P_2, E),
      tnotexists_inlist_t(P_2, Es, T),
      T = true).

Contemptuous

I wonder if the predicate name should include list (like maplist does) or if that information is actually made redundant by structuring the code in modules. – Pacheco

Answer 5

Back to the roots! This variant is very close to the code given by the OP in the question.

The following is based on if_/3 and memberd_t/3.

different(Xs,Ys) :-
   if_(some_absent_t(Xs,Ys),
       true,
       some_absent_t(Ys,Xs,true)).

some_absent_t([]    ,_ ,false).
some_absent_t([X|Xs],Ys,Truth) :-
   if_(memberd_t(X,Ys), some_absent_t(Xs,Ys,Truth), Truth=true).

Here is a ground query:

?- 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

And here's the (more general) query I used in previous answers:

?- 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).

Pacheco

The name _aux is not very revealing. Don't have a better name? – Contemptuous

different_aux_t(Xs, Ys, T): There exists an X in Xs such that : X notin Ys. – Contemptuous

Answer 6

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!

Pacheco

@false. So far, I have used both or_t/3 and or_/2. I get that or_t/3 should better become (;)/3 (same for and_t/3 and ','/3). But what about or_/2 and and_/2? They are specialisations of if_/3, but simply cannot be renamed to (;)/2 and ','/2. – Pacheco

@false. I see if_/3 as if it was defined by if_(Cond,Then,Else) :- if_t(Cond,Then,Else,true)., even though said if_t/4 has not been used (yet). Still, we should have an easy-to-follow clear scheme so that if_/3 users can offer two versions of the predicate without much pain, IMO. – Pacheco

Answer 7

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!

Pacheco

Answer 8

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

Vulgus

The difference here is the overhead: if_/3 is one rule added. Nothing more. And for many cases, performance is comparable to impure and efficient code. It is certainly possible to add constructive negation like so: cn_t(G_0, true) :- G_0. cn_t(G_0, false) :- ~ G_0. But similar to your definition of (~->)/2 there is no direct way to avoid useless choicepoints. – Contemptuous

Assume you can do the best, then you still have the (;)/2! which creates a useless choicepoint. However, if_/3 can be trivially expanded. (Actually, to be 100% ISO, it is not that trivial, but close). – Contemptuous