dif/2: unexpected redundant residuum

[UWN]

?- A = [_|_], dif([],A).
   A = [_A|_B]. % expected
?- dif([],A), A = [_|_].
   A = [_A|_B], dif:dif([],[_A|_B]). % unexpected ; expected as above

[UWN]

This one here is very much related to the incorrectness of unification. Doesn't that mean that the entire atv-mechanism isn't working correctly?

[UWN]

?- dif([],A), A=a.
   A = a.
?- dif([],A), A=s(_).
   A = s(_A), dif:dif([],s(_A)), unexpected. % solved
?- dif([],A), A=s(_).
   A = s(_A).

[UWN]

UWN_blocking

[UWN]

Please do not forget this. Here is another such unexpected residuum:

?- set_prolog_flag(occurs_check, true). 
   true.
?- X = Y, dif(X,f(Y)).
   X = Y.
?- dif(X,f(Y)), X = Y.
   X = Y, dif:dif(X,f(X)), unexpected.

Here is a sketch for it.

[triska]

I think all but the very last example now work correctly? Could you please update the issue if possible?

[triska]

And the very last example seems to be captured by #1382 ?

[UWN]

How has this been solved? It seems that only the projection removes the redundant goal. That is, the dif/2 goals persist, but are at the end removed superficially. Right? Consider:

?- +_=A, dif(0-B,A-C).
   A = +_A.
?- dif(0-B,A-C),+_=A.
   A = +_A, dif:dif(0-B,+_A-C), unexpected.

[UWN]

Maybe consider this approach.

[UWN]

?- dif(0-B,A-C),+_=A,+1=A,C=c.
   A = +1, C = c, dif:dif(0-B,+1-c), unexpected.

[UWN]

And, as a general comment, sorting variables is a highly implementation dependent operation. It is not evident to me why sorting is necessary at all. A much stronger test is performed ahead (X \= Y).

[mthom]

dif:attribute_goals could first test whether X and Y are unifiable:

gather_dif_goals(_, []) --> [].
gather_dif_goals(V, [(X \== Y) | Goals]) -->
    (  { \+ \+ X = Y,
         term_variables(X, [V0 | _]),
         V == V0 } ->
       [dif:dif(X, Y)]
    ;  []
    ),
    gather_dif_goals(V, Goals).

attribute_goals(X) -->
    { get_atts(X, +dif(Goals)) },
    gather_dif_goals(X, Goals),
    { put_atts(X, -dif(_)) }.

I'm not sure if this is a bad idea for some other subtle reason.

[UWN]

The difs should go away as soon as possible. Otherwise Scryer will leak. (That is, it would leak even with a GC.) Projection should only show what is here. So it is good that projection shows this problem already.

Also, \+ \+ X = Y may trigger a side effect that would be intended in another place.

[triska]

How has this been solved?

I can no longer reproduce the issues you post in https://github.com/mthom/scryer-prolog/issues/1433#issue-1206843797 and https://github.com/mthom/scryer-prolog/issues/1433#issuecomment-1120154051. If possible, please update the posts with issues that still exist or remove the no longer relevant posts, so that time is saved for everyone who looks into this issue.

[UWN]

Updated. The issue itself is not solved, "unexpected redundant residuum" still happens, as indicated.

[triska]

Yes, nobody suggested this issue is solved. You can use strikeout text in the code snippet to make clear what need no longer be considered.

[UWN]

Please note that as long as this (now dif#21) is not fixed, further testing dif/2 does not make any sense.

[UWN]

Yes, seems to be solved on the atv-level! Congratulations!

But not beyond that (this you cannot fix on the Prolog level):

?- call_residue_vars( ( dif(X,f(Y)), X = Y ), Vs).
   X = Y, Vs = [X], unexpected.  % leak
   X = Y, Vs = []. % expected, but not found