Surprising dif/2 behaviour

Not precisely sure how this is happening, but it looks like the _s are being identified somehow.

?- dif((p(1) :- q),(_B:-_C)).
dif(f(_B, _C), f(p(1), q)).

?- dif((p(1) :- q),(_:-_)).
true.

This explains it:

109 ?- call_residue_vars(dif(a(p, q), a(_,_)), L).
L = [_49086, _49092, _49098],
dif(f(_49086, _49092), f(p, q)).

In other words, the problem is that anonymous variables are not reported and that is also the case if they have constraints on them. If you do this in a real application you get the same problem: the program succeeds with some internal variables that have constraints that have never been bound.

call_residue_vars/2 does two things: it ensures such variables are not garbage collected and it reports them. Once upon a time it was implemented by scanning the entire term stack. Eventually I found a way to implement this that is both efficient and correct. AFAIK this predicate comes from SICStus and is mostly supposed to debug constraint issues.

Note that logically this is correct: there are bindings for the two anonymous variables for which this dif/2 holds :slight_smile: edit but, be aware that constraint solvers may not always have propagated all consequences. Thus, there are cases where a constraint succeeds while there is no possible labeling. In that case the answer is logically wrong!

2 Likes
?- call_residue_vars(dif((p(1):-q), (B:-C)), Vars).
Vars = [B, C, _1736],
dif(f(B, C), f(p(1), q)).

(The output looks a bit weird to me … but basically it shows that B and C have attributes … I have no idea where f/2 comes from.)