Monotonic equivalent of findall(X, (member(X, [a(1), b(2), c(3)]), X \= a(_)), Xs).

[jjtolton]

?- findall(X, (member(X, [a(1), b(2), c(3)]), X \= a(_)), Xs).
%@    Xs = [b(2),c(3)].

This works as expected.

To my surprise, this did not:

?- findall(X, (member(X, [a(1), b(2), c(3)]), dif(X, a(_))), Xs).
%@    Xs = [a(1),b(2),c(3)].

tfilter/3 did not work as I had hoped:

?- findall(X, member(X,[a(1), b(2), c(3)]), Qs),
   tfilter(dif(a(_)), Qs, Xs).
%@    Qs = [a(1),b(2),c(3)], Xs = [b(2),c(3)]
%@ ;  Qs = [a(1),b(2),c(3)], Xs = [a(1),b(2),c(3)], dif:dif(a(_A),a(1)).

I tried this also and I'm starting to see a pattern:

:- use_module(library(reif)).

awith_awithout(Awith, Awithout) :-
        phrase(awith_awithout(Awith), Awithout).
awith_awithout([]) --> [].
awith_awithout([A|Awith]) -->
        { if_(=(A,a(_)), false, true) },
        [A],
        awith_awithout(Awith).

?- awith_awithout([a(1), b(2), c(3)], Awithout).
%@    Awithout = [a(1),b(2),c(3)], dif:dif(a(1),a(_A)).

I realize that this is correct per se, as dif(a(1), a(_)) holds, but that's not helping me to get these a functors outta here!!

[jjtolton]

/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   xs_ys_setdiff(Xs, Ys, Diff): Diff is the set difference of Xs and Ys.
   https://github.com/mthom/scryer-prolog/discussions/2507#discussioncomment-10471435
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
xs_ys_setdiff([], _, []).
xs_ys_setdiff([X|Xs], Ys, Diff0) :-
        if_(memberd_t(X, Ys),
            Diff0=Diff,
            Diff0=[X|Diff]
            ),
        xs_ys_setdiff(Xs, Ys, Diff).

/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   xs_ys_setunion(Xs, Ys, Union): Union is the set union of Xs and Ys.
   Courtesy of Rayh https://github.com/librarianmage
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
xs_ys_setunion(Xs, Ys, Union) :- 
  xs_ys_setdiff(Xs, Ys, UniqXs),
  append(UniqXs, Ys, Union).


awith_awithout(Awith, Awithout) :-
        findall(A, (member(A, Awith), A = a(_)), As),
        xs_ys_setdiff(Awith, As, Awithout).

?- awith_awithout([a(1), b(2), c(3)], Awithout).
%@    Awithout = [b(2),c(3)].

This is an answer, but it feels very indirect!

[bakaq]

findall/3 itself is not monotonic:

?- findall(X, (X = 1;  X = 2), Xs), Xs = [_].
   false.
?- X = 1, findall(X, (X = 1;  X = 2), Xs), Xs = [_].
   % Adding a constraint gives more solutions!
   X = 1, Xs = [1].

Anything that depends on the number of results is in general not monotonic.

[bakaq]

What you would need here is a predicate pattern_match_t/3 to be used with tfilter/3, but I don't think general pattern matching is monotonic.

This is the best I could come up, and maybe it's enough for your uses:

?- [user].
:- use_module(library(reif)).

% T = true if either the functor indicator or arity are different
different_functor_t(A, B, T) :-
    functor(A, AFunctor, AArity),
    functor(B, BFunctor, BArity),
    ';'(dif(AFunctor, BFunctor), dif(AArity, BArity), T).

?- tfilter(different_functor_t(a(_)), [a(1), b(2), c(3)], Xs).
   Xs = [b(2),c(3)].

[jjtolton]

Ahh perfect, thanks this is exactly what I was looking for!

[UWN]

Just a minor stylistic remark. It is often more readable (though currently less efficient) to write

call((dif(AFunctor, BFunctor) ; dif(AArity, BArity)), T).

And if at it, expressing a disjunction of inequalities can be done more compactly.

[triska]

One small comment regarding "as dif(a(1), a(_)) holds":

In the example, dif(a(1), a(_)) is a residual constraint that appears in an answer: It does not mean that "this holds", but rather: If this constraint can be satisfied, then this is a solution! We therefore say this is a conditional solution. In this concrete example, it is easy to see that the constraint can be satisfied, and all terms that satisfy this constraint are solutions. There are infinitely many solutions. For instance, X = 2 is a solution satisfying dif(a(1), a(X)). But in general, it can be hard to see whether the residual constraints can be satisfied, in fact this may not even be decidable.

Seeing this concrete residual goal, I have filed #2540, because the residual goal can be simplified to dif(1, _) in this case.

Note also that we can use operator notation to write =(A,a(_)) as A=a(_).

[jjtolton]

Interesting, I have some questions about that

One small comment regarding "as dif(a(1), a(_)) holds":

In the example, dif(a(1), a(_)) is a residual constraint that appears in an answer: It does not mean that "this holds", but rather: If this constraint can be satisfied, then this is a solution! We therefore say this is a conditional solution. In this concrete example, it is easy to see that the constraint can be satisfied, and all terms that satisfy this constraint are solutions. There are infinitely many solutions. For instance, X = 2 is a solution satisfying dif(a(1), a(X)). But in general, it can be hard to see whether the residual constraints can be satisfied, in fact this may not even be decidable.

Interesting... I have some questions about that.

[UWN]

Note that "pattern matching" is an expression best avoided in the context of Prolog. It comes from value-oriented languages (that do not have real variables like Prolog does), and simply means there a comparison of a concrete value against a pattern. But here in Prolog both sides may look like a pattern, and even worse, both sides may share variables.

[jjtolton]

Related, @UWN I realized you already answered this and similar questions for me before 😅 😅 😅