Is (\+)/1 monotonic when sufficiently instantiated?

[Garklein]

My new project is rewriting all my past Prolog to be monotonic, and I've come across this Reddit answer which states that many undesirable predicates are monotonic in the specific context where you, the programmer, verifies they are sufficiently instantiated:

Built-ins that are only correct if they are called with sufficiently instantiated arguments, but which are not protected by instantiation errors, provided they are called with sufficiently instantiated arguments. So for these built-ins you have to identify that property yourself. The burden rests upon you.

So, my question is, does this apply to (\+)/1 as well?

I very much do not like (\+)/1, and I am only considering it for speed reasons (my solution with \+ takes 2 seconds while all my alternate solutions take at least 20 minutes. Not sure how long exactly they take because I get impatient and kill the processes).

[bakaq]

No, (\+)/2 is in the "even more complex to formulate" camp. I'm not even sure how to use it in a way that is monotonic, though you can probably argue that any use of it is logically pure because negation as failure has a well defined logical meaning under closed world assumption.

When I want negation in pure and monotonic Prolog I reify it and do it explicitly. How exactly are you using (\+)/2 such that the monotonic alternative is 600 times slower?

[Garklein]

No, (\+)/2 is in the "even more complex to formulate" camp.

I see, thank you.

How exactly are you using (\+)/2 such that the monotonic alternative is 600 times slower?

For Advent of Code Day 9, I need to check millions of times if lines intersect rectangles. I have a predicate that holds if two rectangles intersect:

intersect_rects((RX1,RY1)-(RX2,RY2),(LX1,LY1)-(LX2,LY2)) :- #LX1 #< #RX2, #LY1 #< #RY2, #RX1 #< #LX2, #RY1 #< #LY2.

I want to find a specific rectangle that intersects no edges:

rect(Rect,Es) :- maplist(\E^(\+intersect_rects(Rect,E)),Es).

So in this case, since rectangle intersection is a logical property, to remove the (\+)/1, we can manually negate intersect_rects:

not_intersect_rects((RX1,RY1)-(RX2,RY2),(LX1,LY1)-(LX2,LY2)) :- #LX1 #>= #RX2 ; #LY1 #>= #RY2 ; #RX1 #>= #LX2 ; #RY1 #>= #LY2.

% or

not_intersect_rects((RX1,RY1)-(RX2,RY2),(LX1,LY1)-(LX2,LY2)) :- (#LX1 #>= #RX2) #\/ (#LY1 #>= #RY2) #\/ (#RX1 #>= #LX2) #\/ (#RY1 #>= #LY2).

However, both of these are much too slow. For the first, I suspect it is because it is leaving behind millions of choice points; and for the second, clpz is much much more work for Prolog. Even if you wrap the first version in a once, it is still too slow. Any ideas?

[bakaq]

The form of the rect/2 predicate that you showed seems to imply that you do a kind of "generate and test", which is usually very slow, especially if you need to test many cases. Why not do a predicate rects_edges_non_intersecting/3 that relates a list of rects and a list of edges to a list of rectangles in the first list which don't intersect any edges? I would also use better terms for lines and rects instead of the very problematic (,)/2, something like rect(point(_,_), point(_,_)) or even just rect(_,_,_,_).

For intersect rects, I would do a single reified predicate rect_line_intersects/3 using either (#<==>)/2 or clpz_t/2, depending on if using true/false or 1/0 makes more sense in your case:

% library(reif) version
rect_line_intersects_t(
    (RX1, RY1)-(RX2,RY2),
    (LX1, LY1)-(LX2,LY2),
    T
) :-
    clpz_t(
        #LX1 #< #RX2 #/\
        #LY1 #< #RY2 #/\
        #RX1 #< #LX2 #/\
        #RY1 #< #LY2,
        T
    ).

% library(clpz) version
rect_line_intersects_z(
    (RX1, RY1)-(RX2,RY2),
    (LX1, LY1)-(LX2,LY2),
    Intersects
) :-
    #LX1 #< #RX2 #/\
    #LY1 #< #RY2 #/\
    #RX1 #< #LX2 #/\
    #RY1 #< #LY2 #<==> Intersects.

I'm not sure if that would be faster though. One other thing that is always worth to try is to reorder your goals to put the more strict constraints first. That reduces the search space, but may actually make it slower because of the constraint propagation overhead.

[Garklein]

The form of the rect/2 predicate that you showed seems to imply that you do a kind of "generate and test", which is usually very slow, especially if you need to test many cases. Why not do a predicate rects_edges_non_intersecting/3 that relates a list of rects and a list of edges to a list of rectangles in the first list which don't intersect any edges?

Sorry, I don't really understand what you mean by "generate and test" 😅
I have a sorted list of rectangles, and I want to find the largest valid rectangle: member(area(P2,Rect),Pairs), rect(Rect,Edges) (P2 is the variable that is part 2's answer). Is this the generate and test that you're talking about?

Thanks for the tip about (,)/2 and ideas for a reified predicate, I will try them out!

[UWN]

Consider:

p(1).

?- \+ p(2).
   true.

Now add a further fact:

p(1).
p(2).

?- \+ p(2).
   false.

And thus, what has been true before, is now false. That is, even in a case when the argument of (\+)/1 is sufficiently instantiated (and is terminating), monotonicity is not maintained. This is not an accidental implementation bug. It is intended.

[bakaq]

This actually gave me an epiphany. It made me finally realize that the 2 different kinds of monotonicity in Prolog that I formulated a long time ago aren't actually equivalent, which I suspected but couldn't think of a counter-example.

The first one is query monotonicity, which is what I feel people mean usually when talking about this casually. It is roughly¹ "if you generalize a query, the set of solutions only increases". A counter example for (\+)/1 is that \+ 2 = 1. succeeds but \+ _ = 1. fails.

The second one is database monotonicity, which is the more straightforward translation of monotonicity of entailment from substructural logic. It is roughly "if you add a clause to the database, the set of solutions only increases". UWN's answer here is a counter example for (\+)/1.

If you define a predicate a :- \+ p(2)., this is "query monotonic" (like any non control construct 0-arity predicate), but not "database monotonic", because adding a clause makes it fail.

Goes to show how complex actually formally defining these properties is.

Footnotes

1. I'm still working on a precise definition because errors, non-termination, constraints, STO unification, and other things makes defining this in Prolog orders of magnitude more complicated than in textbook sequent calculus. ↩

[UWN]

It made me finally realize that the 2 different kinds of monotonicity

Both are the same. Take your "query monotonicity" example, that \+ 2 = 1. succeeds but \+ _ = 1. fails.

This is a shorthand for

eq(X,X).

?- \+ eq(2,1).
   true.

And now, we generalize it by adding a further fact (some insist on calling this a clause because of the variables):

eq(X,X).
eq(_,_).

?- \+ eq(2,1).
   false.

Now consider clpz's negation (#\)/1. Is this a monotonic construct or rather a non-monotonic one?

[bakaq]

This doesn't prove they are the same (as in a bijection), you only maybe proved that "database monotonicity" is a superset of "query monotonicity". For the bijection you would also need to prove that the a/0 that I defined is also "query monotonic", aka (more or less) that a generalization of a successful query fails. But there are no arguments to generalize!

Now consider clpz's negation (#\)/1. Is this a monotonic construct or rather a non-monotonic one?

As far as I understand it, it's completely query monotonic. I can't think of a counter-example for query monotonicity at least (in monotonic execution mode), though in this case it's a bit complicated because of errors (which I have a rough idea of how to deal with but I don't want to write 4 pages of my incomplete lattice theoretical formalization of query monotonicity right now) and constraints (which I have a very very preliminary idea of how to deal with, but I don't want to deal with it in a first formulation).

?- #\ (#1 #= #2 ).
   true.
?- #\ (#1 #= #A ).
   clpz:(A in inf..0\/2..sup).

[UWN]

How can it be that in one case negation is non-monotonic, and with (#\)/1 it is monotonic?

[bakaq]

Because (\+)/1 is not negation, it's "not provable". It's effectively a procedural control construct and I treat it as one in my code. (#\)/1 "reifies" actual negation at a level of indirection with constraints, kinda like dif/2 does with (\=)/1, and I can't think of a place where either breaks query monotonicity as I defined it (generalizations of queries always increase solutions).

[Garklein]

As another monotonicity question, is countall/2 monotonic? It feels similar enough to findall/3 to not be, but it's so useful that I hope it is 😁.

[triska]

For instance:

t.

?- countall(t, 1).
   true.

Now we add a fact:

t.
t.

?- countall(t, 1).
   false.

[Garklein]

My understand of monotonicity is it means that adding constraints should never yield more answers. Here, the constraint that was added is an additional fact, but I don't understand how we're getting another answer. For example, why isn't the following logical behaviour also problematic (UWN's example but with the \+ removed)?

t(a).

?- t(b).
   false.

Then adding a fact:

t(a).
t(b).

?- t(b).
   true.

The difference that I see between what I wrote above and you and UWN's examples is that in my example, a false turns to true; while in your examples, a true turns to false. So, then my guess is that a constraint that turns a true to false is non-monotonic. But this makes no sense to me, since that's what a constraint is supposed to do: restrict solutions.

[haijinSk]

Here, the constraint that was added is an additional fact [...]
[...] a constraint is supposed to do: restrict solutions.

Adding a new fact/clause (as here: t(a). and then adding t(b).) is not adding a constraint/reduction of solutions, on the contrary. It would be adding a goal to a clause/rule.

I see (or hear) it like this: false. does not mean: "there is one false-value solution, and I will keep it, if your program will stay in the monotonic realm".

But, in my naive view, once a result/answer is true., and if true. means "deductively valid" (or a solution), then it "cannot become invalid by the addition of extra premises", in the monotonic realm.

This "false becoming true" case, in my imagination, is not invalidating something added before. The query t(b). was false., because there was only the t(a). factoid, then. Adding t(b). to facts did not change anything valid before the addition. If \+ t(b) were part of the program, then yes, it would mean change after the addition, and it would mean that we were not in the realm of monotonicity.

[Garklein]

That makes sense, thanks!