dif/2 used to expose confusion

[flexoron]

NOTE:  UWN detected that this issue is not dif/2 related. See #2333 
Thanks UWN.

Version 0.9.3-214-g70795134-modified

# Note: dif/2 used to provoke the issue

$ scryer-prolog -f
?- use_module(library(dif)).
   true.
?- dif(W,V),V=[V].
   V = [V], dif:dif(W,[[]]).    % [[]] fault?
?- dif(V,W),V=[V].
   V = [V], dif:dif([[]],[[]]). % unexpected

?- dif(V,W), V=[V|x].
   V = [V|x], dif:dif([x|x],[x|x]). % should be dif:dif([V|x],W)?
?- 

[UWN]

Excellent find! But this is not a problem of the dif/2 but rather of the projection.

?- dif(W,V),V=[V].
   V = [V], dif:dif(W,[[]]), unexpected.
?- dif(W,V),V=[V], W = [[]].
   W = [[]], V = [V]. % perfect
?- dif(W,V),V=[V], W = [W].
   false. % perfect!
?- dif(V,W),V=[V].
   V = [V], dif:dif([[]],[[]]), unexpected.
?- dif(V,W),V=[V], W = [W].
   false.
?- dif(V,W),V=[V], W = [].
   V = [V], W = [].

So the internal implementation of dif/2 itself maintains the right consistency. It's just the projection which produces these goals.

Note to self: do test copy_term/3 as well...

[flexoron]

$ swipl -q  # v9.0.4 
?- dif([W|[V]],[V|[W]]), V=[[W|V]|X],W=[[V|W]|Y].
W = _S1, % where
    _S1 = [[_S2|_S1]|Y],
    _S2 = [[_S1|_S2]|X],
V = [[_S1|_S2]|X],
dif(f([[_S1|_S2]|X], Y), f([[_S2|_S1]|Y], X)).  % No printing delay
    ^                    ^
% Not sure why dif( f(...), f(...) ) , 
% and how to check whether scryer-prolog does the same:

$ scryer-prolog
?- dif([W|[V]],[V|[W]]), V=[[W|V]|X],W=[[V|W]|Y].
W = [[[[W|V]|X]|W]|Y], V = [[[[V|W]|Y]|V]|X],
% Takes a long time to display (unreadable) dif:dif(...)

[UWN]

For the f, see #2029

[UWN]

And this is not about constraints at all.

?- findall(G_0s, ( call_residue_vars(( dif([W|[V]],[V|[W]]), V=[[W|V]|X],W=[[V|W]|Y] ), Vs), copy_term(Vs,Vs,G_0s), \+ acyclic_term(G_0s) ), L).
   L = ..., loops.

So a term is created that can be copied with findall/3, and still is not representable.

[flexoron]

?- dif(V,W), dif(W,V), V=[V].
   V = [V], dif:dif([[]],[[]]). % missing dif:dif(...) displayed below 

?- dif(W,V), dif(V,W), V=[V].
   V = [V], dif:dif(W,[[]]).    % missing dif:dif(...) displayed above

[UWN]

That example does not clarify the situation, after all, recall that

?- dif(V,W), dif(W,V).
   dif:dif(V,W).
?- dif(W,V), dif(V,W).
   dif:dif(W,V).
?- dif(V,W), V\=W.
   dif:dif(V,W).

And this is all intended as is.

[flexoron]

Ah,thanks. Unfortunately I've only swipl to compare results,
and this seems not very effective. (sorry)

$ swipl -q
?- dif(V,W), dif(W,V).
dif(V, W),
dif(W, V).

[UWN]

swipl to compare results,

That system is incorrect in a manner that Scryer is not. And SWI never was correct for dif/2.

Also, rather consider to exploit algebraic properties. Like the commutativity for conjunction of (=)/2 and dif/2 goals.

If you want the perfect reference implementation take dif_si/2 which tells you when it is OK, and when it is not (upon instantiation_errors) — and lest I forget, in general modulo STO-ness.

[flexoron]

Ok, thank you.
One last scryer (faulty) example:

?- dif(fu(W),fu(V)), V=[V].
   V = [V], dif:dif(fu(W),fu([[]])).

?- dif(fu(V),fu(W)), V=[V].
   V = [V], dif:dif(fu([[]]),[[]]). % unexpected

According to the very first example
?- dif(V,W),V=[V].
   V = [V], dif:dif([[]],[[]])
dif:dif(fu([[]]),fu([[]])) is expected

[UWN]

dif:dif(fu([[]]),fu([[]])) is expected

Not that is not expected. the first example was incorrect.

[flexoron]

Yes. The example refers to functor fu which get lost as well.