Might specialized versions of all-solutions predicates recover some algebraic properties?

[dcnorris]

In the DEDUCTION project, I frequently invoke findall/3 or setof/3 and then foldl/4 some binary operation over the resulting list.

reduce(P_3 [X|Xs], R) :- foldl(P_3, Xs, X, R).

d_rx_join(D, X, Jx) :-
    setof(Q, d_tally_dose(D, Q, X), Qxs),
    reduce(join, Qxs, Jx).

d_rx_meet(D, X, Mx) :-
    setof(Q, d_tally_dose(D, Q, X), Qxs),
    reduce(meet, Qxs, Mx).

% Here, join/3 and meet/3 are commutative binary ops akin to clpz:max_/3 and
% clpz:min_/3, but operating on terms of a non-integer type.

As @triska describes here, however, such all-solutions predicates destroy monotonicity "in general".

What I'm wondering is, are there specific circumstances when such modes of reasoning can be used while retaining monotonicity? Or is every attempt to even conceive of sets-of-solutions provably doomed in this way? Obviously, the code below uses impure constructs—and indeed must, since

In pure Prolog, all information about a certain branch of the computation is lost on backtracking.
— Sterling & Shapiro, Ch.16 p.301.

But I am hoping that sufficient conditions might be placed on the predicate P_3 (and perhaps Goal as well) to enable recovery of some algebraic properties.

:- meta_predicate reduce_all(3, ?, 0, ?).
:- meta_predicate reduce_all_(3, ?, 0, ?).

% Akin to reduce(P_3, {X : Goal(X)}, R), and operationally
% equivalent to (findall(X, Goal, Xs), reduce(P_3, Xs, R)),
% where X is a free variable in Goal.
reduce_all(P_3, X, Goal, R) :-
    asserta('$reducing'([])),
    (   reduce_all_(P_3, X, Goal, R)
    ;   call('$reducing'([R])),
        retract('$reducing'([R]))
    ).

reduce_all_(P_3, X, Goal, R) :-
    call(Goal),
    (   retract('$reducing'([R0])), % succeeds on 2nd & subsequent instantiations of Goal
        call(P_3, R0, X, R),
        asserta('$reducing'([R]))
    ;   retract('$reducing'([])), % succeeds on the 1st instantiation of Goal only
        asserta('$reducing'([X]))
    ),
    fail.

%?- reduce_all(sum_, X, (X in 1..10, indomain(X)), R).
%@    R = 55.

At a basic level, I'm motivated here by the hope I could factor findall/3 and setof/3 out of my code entirely, and replace them with somehow 'less-impure' constructs.

[UWN]

The goal setof(t, G_0, _) certainly retains monotonicity.

Also, constructs such as "has at least n solutions" retain monotonicity.

Otherwise, you probably would have to settle for less. Giving up monotonicity does not mean to give up purity as such.

Going beyond Section 7 might be another way.