dif/2 incorrect

[UWN]

An otherwise pure program with dif/2 fails incorrectly (SICStus succeeds here) for

?- permutation_no_dup([x,y,Z,Z],P), P=[x,y,z,z].

but correctly succeeds for

?- P=[x,y,z,z], permutation_no_dup([x,y,Z,Z],P).

See this for more.

[JanWielemaker]

I'm a little lost. The code below is what I've assembled from the exchange and made working on both SICStus and SWI-Prolog. It gives the same results on both systems. This is version 8.5.1. There should be no difference to 8.4.0. I guess I assembled the program wrong.

pnod.txt

[UWN]

You used the "corrected" version that works everywhere. In the original version dif/2 was at the beginning:

permutation_no_dup([], _, LMax/LCur-L, PL, PL1):-
  dif(PL, PL1),
  next(LCur, LMax, NLCur),
  permutation_no_dup(NLCur, L, LMax/NLCur-L, [], PL1).

[JanWielemaker]

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/bug-fix-bounties/4645/1

[JanWielemaker]

Just a little remark is that this works fine with dif/2 defined as below.

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

Considering the significantly simpler implementation of when/2 this may be the direction to go, either simply using this definition or building a new dif/2 based on the techniques from when/2 and getting rid of one complicated algorithm.

[UWN]

Another approach would be even simpler, but it is more expensive for some (probably irrelevant) worst cases. Also, this one interacts with other constraints which is probably desirable but at least operationally different to the current approach.

[JanWielemaker]

Not really sore how realistic it is, but this is a nice test:

bench(N) :-
    numlist(1, N, L1),
    length(L2, N),
    dif(L1, L2),
    \+ numlist(1, N, L2).

Where, unfortunately, the when/2 based approach is quadratic and the current dif/1 is linear.

[UWN]

Definitely unrealistic. Most difs have just constants (atomic), variables and (already much rarer) constrained variables as arguments.

[JanWielemaker]

Most maybe. The example that started this is already a counter example. I've learned my lesson that getting the O wrong typically results in people complaining.

[UWN]

If that lesson you learned is important to you, you will have to stick to the current implementation. Just keep in mind that it does not lead to correctness easily. In fact, just testing it is hard.

[JanWielemaker]

In fact, just testing it is hard

That makes me wonder. Anyone thought about a random test generator? Luckily the wizard that tells is the correct answer is easy enough to write. The problem is in generating all meaningful sequences of unifications.

[UWN]

Random test generators have their use, but when it comes to more complex situations, I have not seen any hit at all. clpfd/clpz comes to my mind. Contrast this to systematic testing which even in the case it does not find an error can convey some information. In the concrete case of permutation_no_dup/2 there is no counterexample with a smaller list of constants and variables. And in fact, any further instantiation of the elements makes the example work, like adding P = [x|_].

[jacobfriedman]

Jan- definitely look at Paulo's implementation here: https://logtalk.org/manuals/devtools/lgtunit.html#quickcheck. Still, the problem with CLP is when you introduce floating points and your tests fail that type of precision-based arithmetic.

[JanWielemaker]

The problem with generated tests is to explore the potential problem space properly. That is often hard. I created something along these lines:

1. Generate a random term.
2. Randomly generalise the term.
3. dif/2 these two terms.
4. Loop
   • Find the current unifier
   • Randomly take an element from there
   • Randomly unify to this variable
     • The right hand
     • Something incompatible to the right hand
     • A generalised form of the right hand

But, what is a good random term? It turned out dif/2 had a bug if the term from step 1 contains shared subterm and a bunch of other conditions on the generalization. Examples were be found in a few seconds. I fixed that (not sure whether the fix is "the way it should be fixed"; I've contacted the original author on that). Unfortunately that doesn't fix this issue 😢

Note that we need some knowledge on the implementation. For example, we know atomic data is handled uniformly by the implementation, so there is no point in having more than two constants in the test (two, so they can be equal or not).

Now there is clearly something that is not explored by the test. I suspect that we are dealing with multiple open dif/2 constraints that act on partly overlapping terms.

[jacobfriedman]

By original author, do you mean whoever wrote dif(X, Y) :- when(?=(X,Y), X\==Y). - and by 'constraints' do you mean attributed variables?

I can see in Scryer the sorted goal-collection in dif... and the attempt to dedupe goals. I'm not sure that's ideal.

[JanWielemaker]

I tried the when/2 alternative. It works fine, but its complexity is O(n^2) rather than O(n). Possibly that is the thing that needs to be fixed. Constraints and attributed variables are more or less the same. Tom Schrijvers wrote the original when/2 and dif/2 implementations. Some work has been done on these by various authors since.