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 :cry:

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.

[UWN]

In SWI 6.6.4, 7.6.4, 8.4.1 I get:

?- dif(A-C,B-D), C-D=z-z.
false.              % unexpected

And in Scryer it's:

?- dif(A-C,B-D), C-D=z-z.
   C = z, D = z, dif:dif(A-z,B-z). % expected

Again a case of simultaneous unification.

[JanWielemaker]

Thanks. That may well be the ultimate simplification for this case. My random tests found another one that does not involve a simultaneous unification (instead, some subterm sharing).

[jacobfriedman]

For testing dif, I'm looking at: https://github.com/LogtalkDotOrg/logtalk3/blob/6afbc6f33ecc243f9427dcc5a8d2e3418d8a668f/library/dif/tests.lgt

Are there any other tests that may help describe what is expected, and how we can arrive at something unexpected?

If attvars are not described in the ISO spec, then the dif we have come to recognize is not necessarily correct. The only recent implementation I know of that satisfies most of what is discussed, excluding attvar functionality, is in trealla. It model's UWN's sketch - an error is thrown in the case where suspended/auxiliary goals would lie.

[EricGT]

how we can arrive at something unexpected?

Concolic testing 🤔(thinking emoji)

Concolic Testing in Logic Programming (pdf)

[JanWielemaker]

Looks like the issue is fixed with SWI-Prolog/swipl-devel@0286dc4251099426dfb718b2a0df4906ba77299f. This implements a different technique to decide on or nodes to be exhausted. It fixes four issues, the two reported here and two that resulted from the random tests. The random tests no longer trigger issues in a reasonable time. But of course, they do not cover all possible dif/2 scenarios.

[UWN]

g1> cmake --version
cmake version 3.18.4

CMake suite maintained and supported by Kitware (kitware.com/cmake).
g1> cd /opt/gupu/swipl-devel/build/
g1> cmake -G Ninja ..
CMake Error: CMake was unable to find a build program corresponding to "Ninja".  CMAKE_MAKE_PROGRAM is not set.  You probably need to select a different build tool.
CMake Error: CMAKE_C_COMPILER not set, after EnableLanguage
CMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguage
-- Configuring incomplete, errors occurred!
See also "/opt/gupu/swipl-devel/build/CMakeFiles/CMakeOutput.log".

Seems I can wait for the next release.

[JanWielemaker]

Your cmake is fine. Seems you do not have ninja installed. See https://www.swi-prolog.org/build/Debian.txt for the dependencies for Debian based systems. Build should be smooth on virtually any Linux system that provides CMake 3.9 or later.

[dgelessus]

Alternatively you can also build with regular Make: remove the -G Ninja part of the CMake command line, and then use make instead of ninja for the build. Works just as well as Ninja, though Make can be a bit slower at build time.

[dgelessus]

Also, thank you from a quiet reader to everyone who helped with diagnosing and fixing this 🙂 I was coincidentally also debugging some odd dif-related test failures when running ProB on SWI, but wasn't able to figure out why some unifications were failing. (I would have posted here earlier, but I didn't have a good compact test case for reproducing the problem.) The recent dif fixes seem to have corrected all the incorrect unification failures I was encountering.

[UWN]

g1> cat /etc/issue
Ubuntu 21.10 \n \l

Following instructions, with apt-get build-dep swi-prolog I got a message to (quoting from memory) update some sources. No way, I am not the admin nor want to take over such duties. And

sudo apt-get install \
        build-essential cmake ninja-build pkg-config \
        ncurses-dev libreadline-dev libedit-dev \
        libgoogle-perftools-dev \
...

wanted to update the kernel for a 21.10.

[JanWielemaker]

There is little we can do about that. If you want to build software on Linux you need to have the dependencies and if you want to install something it also wants to update (can be avoided, but merely makes life complicated). Of course, you can build all dependencies in your home. That is a lot of work though. There is little choice but asking the sysadmin to install the dependencies. I'm not sure whether apt-get build-dep swi-prolog does the job as that are the deps for the current swi-prolog package. It is probably good enough, but getting them from the page surely has the right deps.

[UWN]

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

Is this fixed, too?

[JanWielemaker]

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

SWISH is updated, see https://swish.swi-prolog.org/p/ZlxpkePr.swinb (and add tests if you like).

[UWN]

Further testing continues with a new Ubuntu-snap-release. The current version is 8.4.1

[JanWielemaker]

Taked the edge snap instead. That follows the development release, currently 8.5.2. That is updated roughly every 2 weeks. Within a week it will be updated to 8.5.3 with these patches.