Monotonicity of var/1 in library(diadem)

[bakaq]

I was reading the source for library(diadem) and this line caught my attention.

I think it implies that var/1 is monotonic, which I think is obviously false:

?- [user].
a(A) :- var(A), A = 1.

?- a(A), A = 1.
   A = 1.
?- A = 1, a(A).
   false.

Am I misunderstanding this or is this an error in the library?

---

Edit:

Wait, I think I understand now. I thought that monotonicity implied that the order of predicates doesn't matter, but I think that is a strictly stronger condition. Monotonicity just implies that I can't increase the number of solutions by adding a goal, and that is indeed the case here:

?- var(A).
   true. % This is already true in the general case.
?- A = 1, var(A).
   false. % Any instantiation of A will decrease the number of solutions, but nothing can increase it.

Has this commutativity property (does it have another name?) already been studied? I was thinking of making a macro that automatically reorders goals if they are monotonic to improve termination and error properties, but now I see that this is not the right property they should have.

[UWN]

Refer to the comment 10 lines above! "montonicity is not strictly required".

Diadem generalizes failing queries. In that context, a var(X) alone does no harm. Since a generalization can make it only succeed more often but not less.

[bakaq]

Yes, makes sense, this is a weaker requirement than monotonicity. But am I right in my observation that var/1 is actually monotonic, just not commutative, or is it actually non-monotonic? I can't think of any counter examples to the monotonicity of var/1.

[UWN]

?- var(X).
   true.
?- var(X), X = 1.
   true.
?- var(X), X = 1, var(X).
   false.

It seems you are exploring the very notions we are using here. In fact, these notions have been originally defined by others who did not consider Prolog as it is, and thus the notions might not always apply that precisely. So it is easy to come here into the crossfire of different definitional authorities. Monotonic has at least two meanings (and we mean them both), one is as in montonic logic were adding new information does not retract what we know. And the other one is in the context of constraints.

Similarly, the notion of commutativity can only be applied partially to an actual system. Think of

?- false, repeat.
   false.
?- repeat, false.
   loops.

Is this a violation of commutativity or not? What we mostly do is to consider commutativity modulo resource consumption and in that context, above example does not violate commutativity.

[bakaq]

Thank you a lot!