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.

[dcnorris]

It may prove interesting to consider what modes of Section-7 extension might be motivated on purely formal grounds here. Logical conjunction and disjunction are respectively the meet and join operations on
the partial order Bool = {false ≤ true}. Furthermore, certain efficiencies achieved by library(reif) depend on the fact that Bool has least and greatest elements, which in categorial language would be called initial and final objects.

As it happens, the much larger partial orders (isomorphic to bounded subsets of ℕⁿ) over which I compute my meets and joins will generally also have initial and final objects — these being the worst-case and
best-case toxicity tallies possible under some given dose-escalation protocol. So one direction for generalization would be to identify meet/3 and join/3 with (=)/3. This would greatly enlarge the type of the 3rd argument of (=)/3, but simultaneously the type of its args 1 & 2 could contract substantially (as I understand it, (=)/3 takes any valid Prolog terms in those positions).

While inflating [false,true] up to a rather large semilattice (which is what my tally space seems to be) might seem preposterous, I would offer the vague suggestion that library(reif) seems somehow to achieve something akin to expanding a subobject classifier from Ω = {true,fail} to Ω' = {true,false,fail}. Why not expand it yet further? (And indeed, the tallies in my application do have some 'judgmental' functions resembling those of truth-values.)