dif/2 incorrect Ⅲ

[UWN]

Welcome to SWI-Prolog (threaded, 64 bits, version 8.5.4)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- D = [], A=[B|A], C=[D|B], dif(A, C), A=[D|A].
D = B, B = [],
A = [[]|A],
C = [[]].

?-         A=[B|A], C=[D|B], dif(A, C), A=[D|A]. % generalization
false.   % unexpected

(It also does not terminate)

[JanWielemaker]

Thanks. Both seem to be related to cyclic terms. For now I'm tempted to document this limitation and point people at using when/2 for a cycle safe but sometimes slow alternative. No time to dive into this. PRs welcome of course.

dif(X,Y) :-
    when(?=(X,Y), X\=Y).

[UWN]

For now I'm tempted to document this limitation...

Cyclic structures are much more compact for reproducing errors. It is much easier to find them. So far each and every error with dif/2 encountered had incorrect cases for both cyclic and acyclic terms but where the counterexamples with acyclic terms were quite more complex. Giving a precise criterion for when "no cycles" are present is very challenging. It starts with cases like dif(X,-X) (not a problem in SWI). It is definitely much more complex than the STO criterion which needed years to be formulated.

[UWN]

This is a mere speculation, but could it be that the original implementation was not that bad after all? At least I did not observe any case of non-termination, whereas the current implementation is full of them. The original implementation only had a single problem in that it required (as far as I can conclude this from the counterexamples) unifications with atvs to happen one atv at a time. Isn't this the same issue discussed some time ago with your conclusion here? At least for dif/2, your argument given does not seem to hold.

[JanWielemaker]

No. My random tests also found failing cases that only performed single unifications. If I recall well, it was possible to get contradicting unifications in the list of pending unifications and if then the count reached zero we would conclude the terms to be equal when they where not.

I've done a little tracing on the first. Here we go into a loop walking deeper into the term while keep adding unifications to the pending list. That either needs to be fixed or documented as a limitation. If you have counter examples that do not involve cyclic terms, please share them.

[UWN]

My random tests also found failing cases that only performed single unifications.

Do you have concrete examples of your findings that only single unifications have been performed? This could clarify your notions.

If you have counter examples that do not involve cyclic terms, please share them.

Not yet. And my educated guess is that they will require a lot of compute to be located. After all I fail to find a good criterion for NSTO-ness for dif/2 (grosso modo your not involve cyclic terms) so the only way to find them is to run those tests with library(timeout) which requires a lot more extra compute in particular because there are so many loops encountered. On the positive side, so far all such loops were interruptible by library(timeout) which is not the case for other systems with looping dif/2.

[UWN]

For completeness: finite counterexample found: #112

[JanWielemaker]

A=[B|A], C=[D|B], dif(A, C), A=[D|A].

After SWI-Prolog/swipl-devel@e8c2e0dd02446e61543e6c41bb76429c8186c5f0 we now get this. That looks correct to me. Even better, the displayed result looks great :smile:

?- A=[B|A], C=[D|B], dif(A, C), A=[D|A].
A = [D|A],
B = D,
C = [D|D],
dif(D, [D|A]).

[UWN]

Continued at #113