Undesirable properties of CLPB

Question

library(clpb) is currently available in SICStus (original version), and SWI (by mat). Let me come to the essence quite rapidly:

?- X = 1+1, sat(X), X = 1+1.
X = 1+1.

?-          sat(X), X = 1+1.
false.

So this is a similar problem as it exists in the default state of library(clpfd).

What to do in such a situation?

Update: In library(clpfd) of mat, there is now the functor # /1 for this purpose. Ideally, accompanied with an operator declaration op(150,fx,#), we now can write:

?- X = 1+1, #X #= Y.
ERROR: Type error: `integer' expected, found `1+1' (a compound)

To ensure full algebraic properties one has to declare:

:- set_prolog_flag(clpfd_monotonic, true).

Now, variables that are left ambiguous (thus, being either integers only, or expressions) produce instantiation errors:

?-  1 + 1 #= Y.
ERROR: Arguments are not sufficiently instantiated
?- 1 + 1 #= #Y.
Y = 2.

Would it be acceptable if query #2 threw an adequate exception? Or should it succeed just like query #1? — repeat, Nov 13 '15 at 18:27
I was considering as a quick fix something like `safe_sat(Expr) :- term_variables(Expr,Vs), maplist(\V^freeze(V,(integer(V) -> true ; throw(some_proper_exn(V)))),Vs), sat(Expr).` IMO it is safe to have `sat/1` as the first goal in `safe_sat/1`. — repeat, Nov 13 '15 at 18:38
This does not help in the case above. So why should this be safe? — false, Nov 13 '15 at 18:51
The fix should ensure that no variable in `Expr` is ever bound to anything non-atomic -- I wrote "integer" above, but meant "atomic". IMO `sat` can be moved before the freeze goals, as `sat` will never instantiate any variable in `Expr` to anything non-atomic. This way, `sat(X), X=1+1` does not fail. — repeat, Nov 13 '15 at 20:09
I can't follow your argument, maybe give an answer. `sat(X), X = 1+1` **has** to fail... — false, Nov 13 '15 at 20:13
If `sat(X), X=1+1` does and must fail, what's the problem? IMO it should not fail, as `X=1+1, sat(X)` succeeds; if making it succeed too, however, isn't possible, raising an exception is the next best thing. — repeat, Nov 15 '15 at 07:57
@repeat: Maybe look at `library(clpfd)` which features `(?)/1`. Actually, it would be much more helpful to call this rather `(#)/1`. So far, we have almost no examples on SO for this... — false, Nov 15 '15 at 13:03
I get this. Regarding `(#)` vs `(?)` I'm somewhat on the fence. clpb uses `(#)/2` for expressing "xor". How about yet another ways?-) Consider these ones: `?(X) + ?(Y) #= ?(Z)` vs `?X + ?Y #= ?Z` vs `X? + Y? #= Z?` vs `X# + Y# #= Z#` vs `#X + #Y #= #Z` vs `#(X) + #(Y) #= #(Z)`. At least for the moment I would prefer making `(?)/1` a unary postfix operator. And using it uniformly in clpfd and clpb... — repeat, Nov 15 '15 at 14:10
@repeat: Often, SWI uses an infix operator `(?)/2` which collides with `+` which is prefix and infix. It is for this reason that a postfix `?` is *de facto* impossible. The safest is a prefix `#` which somewhat suggests for `#X + #Y #= #Z` the reading *number `X` plus number `Y` is number `Z`. — false, Nov 15 '15 at 14:14
@repeat: `find -name '*.pl'|xargs grep 'op(.*[?]'` for more: It's `xpce` — false, Nov 15 '15 at 14:51
I second what @repeat wrote: `#` makes perfect sense in the context of CLP(FD) for this, but a lot less sense in the context for CLP(B), where `#` only occurs in the sense of "exclusive or" and *not*, as in CLP(FD), almost all constraints. Instead of `?(Var)`, we could also use `var(Var)`. — mat, Nov 15 '15 at 14:52
@mat: Any symbol for `0` and `1`? `var(Var)` is not ideal as it suggests that it is *any* variable, whereas it should be only a 01-variable. `01var` is not legal... — false, Nov 15 '15 at 14:58
@j4nbur53: Above discussion is about an appropriate name, only. — false, Mar 22 '16 at 18:59
@j4nbur53: you need `set_prolog_flag(clpfd_monotonic, true).` for this. — false, Mar 22 '16 at 19:13
Please refer to the context of constraint logic programming. There, monotonic is used in exactly that manner. I agree, that in logic in general, the view is a different one. — false, Mar 22 '16 at 19:51
Mathematical logic knows a = b -> (P(a) -> P(b)). But Prolog doesn't know this rule since (=)/2 is fixed on the Herbrand doman. Therefore any variable asignment x=a will never change to x=b, and hence THIS monotonicity is always the case. Situation is different if we look at _ #= _ or sat(_ =:= _). Again i have the feeling your expectations about (=)/2 are wrong. — , Mar 22 '16 at 20:27

false · Accepted Answer · 2022-08-11T14:26:33.490

What to do in such a situation?

In the meantime, also library(clpb) ensures monotonicity similar to library(clpz)/library(clfd). Within this execution mode, explicit variables have to be decorated with (v)/1.

?- current_prolog_flag(clpb_monotonic,B).
B = false.                             % the default

?- sat(X).
X = 1.

?- set_prolog_flag(clpb_monotonic,true).
true.

?- sat(X).
ERROR: Arguments are not sufficiently instantiated

?- sat(v(X)).
X = 1.

In Scryer, say:

?- use_module(library(clpb)).
   true.
?- asserta(clpb:monotonic).
   true.
?- sat(X).
   error(instantiation_error,instantiation_error(unknown(_67),1)).
?- sat(v(X)).
   X = 1.

score 0 · Answer 2 · 2016-03-22T18:59:11.250

Yes, same in CLP(FD) and CLP(B):

Situation

CLP(FD), the (+)/2 acts as addition in finite domain:

?- X = 1+1, X #= 2.
X = 1+1.

?- X #= 2.
X = 2

?- X #= 2, X = 1+1.
false.

CLP(B), the (+)/2 acts as disjunction in boolean domain:

?- X = 1+1, sat(X)
X = 1+1

?- sat(X)
X = 1

?- sat(X), X = 1+1.
false

But now watch out, such things happen already in ordinary prolog:

?- X = 3, X \= 4.
X = 3.

?- X \= 4, X = 3.
false.

Problem

So what should we tell the students? I don't think that CLP(FD) or CLP(B) is to blame here.

Its more ingrained into (=)/2, and the impossibility to hook into (=)/2 so that it does more than a verify_attribute/3.

In an ideal world (=)/2 would work algebraically, and the X=1+1 wouldn't fail, the system would see that 1+1 equals 2 (FD case) respectively 1+1 equals 1 (B case).

But for this the Prolog system would need types as a start, otherwise the (=)/2 cannot interpret the (+)/2, it has two different interpretations in our example.

Solution

The solution is to refrain from using (=)/2 where particular types are needed. Hereby I recommend reading:

Constraint Logic Programming using ECLiPSe
Krzysztof R. Apt and Mark Wallace,
May 16, 2006, Full Text PDF

The above paper highlights a little bit the motivation of the hash sign (#) as a prefix for operators such as (=)/2, (<)/2, etc.. Its already a type annotation. There is also another prefix in this paper, namely the dollar sign ($).

In ECLiPSe Prolog the hash sign (#) implies the constraint integers/1, and the dollar sign ($) implies the constraint reals/1. These constraints can also be used independently as in the following example shows:

?- integers([X,Y]), X = 3, Y = 4.5.
No

?- reals(X), X = [1,2.1,a].
No

Coming back to your problem of non commutativity of (=)/2. Although (=)/2 is non-commutativ, the (#=)/2 and its boolean brother are of course commutative. We have:

CLP(FD), the (+)/2 acts as addition in finite domain, and with (#=)/2 commutativiy is there:

?- X #= 1+1, X #= 2.
X = 2

?- X #= 2, X #= 1+1.
X = 2

CLP(B), the (+)/2 acts as disjunction in boolean domain, and with sat/1 and (=:=)/2 commutativity is there:

?- sat(X=:=1+1), sat(X).
X = 1.

?- sat(X), sat(X=:=1+1).
X = 1

A verify_attribute/3 hook will only wake up constraints which can additionally fail a Herbrand domain unification. But they cannot evaluate terms on the fly before assigning them to a Prolog variable.

Only the woken up constraints might assign values to other variables. But for example the current SICStus Spec of verify_atribute/3 even recommends not doing this directly, and only in the continuation queue. See recent SWI-Prolog group discussion.

So long talk, short explanation: Never forget that (=)/1 only works for the Herbrand domain in Prolog, even if we hook in constraints. I dont say a Prolog system couldnt work differently, but this is the state of the Art of a Herd or Prolog systems.

Bye

For `library(clpfd)` things have improved in the meantime. See my question's update. — false, Mar 20 '16 at 12:40
`(\=)/2` is not a constraint. It is only a crude approximation of `dif/2`. — false, Mar 20 '16 at 12:42
Please give **concrete examples** where you believe that your cancer-analogy holds. — false, Mar 21 '16 at 14:23
`eval/1` only makes sense in the context of the right-hand side of `(is)/2`. — false, Mar 21 '16 at 14:43
The very notion "compiled at compile time" is highly problematic. It would introduce many problems similar to the difficulty in handling call/1 and the meta-call. You can study this in SICStus, if you're interested. — false, Mar 21 '16 at 16:51
FYI: SWI's `library(clpfd)` was built to overcome the deficiencies of SICStus. The compilation in SWI is completely different to that of SICStus. SWI's compilation does not complicate unfolding, whereas SICStus' semantics makes unfolding next-to-impossible. — false, Mar 21 '16 at 17:08
`maplist(#<(X), Xs)` is not equivalent to `p1([],_X). p1([E|Es], X) :- X#< E, p1(Es, X).` in SICStus. But this holds in SWI. — false, Mar 21 '16 at 18:57

Undesirable properties of CLPB

2 Answers2

Linked