dif/2 continues to exist even with non-unifiable terms

[UWN]

?- dif(a,s(X)).
X = _33, dif(a,s(X)).

In this case there is no reason to create anything at all, since the terms are already non-unifiable (that is a \= s(X))

[UWN]

Same is true for more complex cases:

?- dif(-X,-Y), X = a, Y = s(_).
X = a, Y = s(_226), _148 = _226, dif(- X,- Y).

Why does the goal show as dif(-X,-Y) and not as dif(-a,-s(_226))?

[mthom]

I did have a X \= Y check in the original dif/2 definition, but @triska said the unification could lead to unintended effects with attributed variables. I'm not sure how to get around that.

[UWN]

Maybe we should ask @triska for a specific example of unintended effects. For one, taking the success of (\=)/2 is logically sound whereas taking its failure is not. (Ex. X\=2, X = 3)

[mthom]

I can think of one example: unifying variables with frozen attributes. That could result in an irreversible side effect, ie. printing text to the screen.

[UWN]

If you want side-effects you should be aware that you are in a language that has different principles. That is, there are certainly certain forms of side-effect that can be made to fit into the language, but keep in mind that X = Y, false ; G_0 is tantamount to G_0 (provided unification always terminates)

[UWN]

In any case, I suggest that you use the success of (\=)/2 and (==)/2 as safe results not only in the beginning but also during the existence of the dif/2 constraint. (Such entirely fruitless discussions are one of the reasons for slow progress)

[triska]

@UWN: What answer do you expect from:

?- freeze(X, writeln(a)), dif(X, a).

Personally, I would like for example:

freeze(X, writeln(a)),
dif(X, a).

But it seems you are OK with:

?- freeze(X, writeln(a)), dif(X, a).
a
freeze(X, writeln(a)),
dif(X, a).

If that's OK, then yes, please do use (\=)/2 in dif/2.

Personally, I would prefer a predicate that also lets us obtain the m.g.u. of two terms, if any, since that is what is actually needed to implement dif/2, and without executing any pending constraints.

[UWN]

freeze/2 is the goto of constraints. A side effect just like this, without any provision to undo it, no that is not a case of interest for me. Except: freeze(X,(writeq(someone_wants_something_resulting_in(X)),nl)). But this is not a logical observation, only an operational observation.

[triska]

OK, what about:

?- dif(X, a), dif(X, b).

and (\=)/2 triggering the dif/2 goals recursively?

[UWN]

I fail to see the recursion here. Whenever one of the constraints checks for consistency, it must not be present as a constraint indeed.

[triska]

OK. Personally, I recommend to avoid triggering constraints within constraint propagation in such an uncontrolled way, but it may be worth trying it out.

[UWN]

For long there has been this taboo to do things with cuts and constraints at the same time. X \= Y does have a tiny cut inside. Cutting constrains? Never! But exactly in this very configuration the cut has no negative effect.

[triska]

The issue is for implementors of constraint solvers to consider all situations that may arise when a unification or constraint is posted. Calling (\=)/2 from propagators means that other propagators can now also be triggered while a propagation takes place.

But this is exactly what for example verify_attributes/3 disallows in the SICStus interface:

Binding Var will result in undefined behavior.

[UWN]

What happens with frozen goals that are executed? The very same should happen for dif/2

[UWN]

In fact SICStus has when/2 and I do not see any warning about using a goal that does general unification there.

[UWN]

What would make this approach so attractive is that it does not require any explicit term traversal. term_variables/2 is all what is needed.

[UWN]

The fundamental difference between dif/2 and constraints like clpfd, is that for dif(X,Y) there is a single reason to fail, namely, when X == Y. In all other cases execution continues. As an add-on, X \= Y identifies the case when constraints are no longer needed. Compare this to clpfd where there are many intermediate representations that cannot be removed and reinstated on each change.

[triska]

Yet, the very same can also be said about CLP(ℤ) constraints like (#\=)/2: For example, when we have X #\= 3, then the single reason to fail is when X == 3. Does it follow that we should try the unification there too, and remove the constraint when the unification fails?

In my personal view, triggering execution of constraints within a propagator in such a way is not to be taken lightly and may lead to unintended consequences, though as I said, it may be worth trying.

[UWN]

Posting X #\= 3 has the effect of reducing the domain, excluding 3. So there is an internal representation. There is no such representation for dif/2. Worse, the typical dif/2 uses are decided on the level of the argument of a term. Not deeper. But in clpfd, the connections are pretty evolved.

Further: As far as I understand, this \= checking should be performed in the Goals list of verify_attributes/3 and not within verify_attributes/3. And there is no restriction for Goals, whereas there are many for goals being executed directly within verify_attributes/3. Right? So maybe your argument boils down to: Maybe it is faster to program dif/2 within verify_attributes/3. That is possible for many cases.

The current approaches are mainly targeted towards CLPQ. Note that simple minded implementations of clpfd were happy enough using freeze/2 and frozen/2 alone (think of Fages).

[UWN]

Nevertheless, the current baroque dif/2 implementations still fail for cases like:

?- dif(X,Y), X = -XA, Y = -YA.
X = -XA,
Y = -YA,
dif(f(-XA,YA),f(-YA,XA)).
Expected: just X = -XA, Y = -YA, dif(XA,YA)

All their complex paths did not help them to resolve that (and I admit it is probably not worth doing that). And then:

?- dif(X,Y), dif(X,Y).
dif(X,Y),
dif(X,Y).

ad nauseam.

[triska]

I have not even started work on dif/2, please let us first solve the elementary syntactic problems. To implement dif/2, I expect that code will be necessary where the basic check for "unifiable" will fit in naturally. However, in my opinion, triggering a unification within the propagator code is not a good way to solve this particular issue. If someone insists on it, yes, it can be added to the delayed goals in verify_attributes/3, but not in the propagation code, because when unifications appear in propagation code, then unexpected issues may soon arise.

[UWN]

Here is an implementation sketch of dif/2!

dif(X,Y) :- 
   X \== Y,
   ( X \= Y -> true % we are finished
   ; term_variables(dif(X,Y), Vs),
     whenthereisachange(Vs, dif(X,Y))
   ).

So it boils down to this whenthereisachange/2

And, btw, are there any syntactic problems? See the open issues. It's that rather non-ISO stuff is in the kernel. Like cyclic_term/1.

[triska]

I have filed #682 to try this.