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.

Answer 1

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.

Answer 2

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