A Prolog Nerdsnipe

I saw a post about Prolog recently, wherein the author used Prolog to solve a Clue-style problem. The post was a reasonable introduction to using Prolog for this sort of problem, I think¹, but there were some things that seemed kind of awkward to me.

In general, there was a lot of use of a construct like \+ A = B, where I would tend to prefer dif(A, B) if you want to make to variables not equal.

In particular, there was a predicate called uniq_ppl/6 that took six variables and asserted they were all different by manually saying \+ A = B, \+ A = C, ..., \+ E = F. At first I thought that they could just use all_distinct/1 from the CLP(FD) library, but then realized that wasn’t actually an option, because all_distinct/1 only works for variables holding integers, and in this case, they wanted to use atoms.

I then managed to nerd-snipe myself into implementing a simple way to say “all of these list of variables are different”; this is that story.

My plan was to generate the cartesian product of the variables, then call dif/2 on all the pairs. dif is a neat predicate that prevents two variables from becoming unifiable, which is subtly different from what \+ A = B does.

\+ A = B² is true only if it can be proved that A can’t be unified with B. This means that just the query ?- \+ A = B., in the absence of other information is false. I find this somewhat counter-intuitive and generally try to avoid using \+ for this reason – it seems inelegant.

dif/2, on the other hand, is pretty neat and more declarative. If A & B are already determined to be unifiable or not, it fails or succeeds immediately. If it isn’t yet determined though, it delays goals, using SWI-Prolog’s coroutining system to wait until enough has been established to determine if A & B can be unified or not and fails then.

The coroutining system is pretty great and really facilitates writing very declarative code; I use it heavily in my HTTP/2 library and mentioned it as an aside my last post.

Anyway, my initial attempt went something like this:

First, I’ll define a predicate to enumerate all possible pairs of a list.

pairs(Xs, Pairs) :-
  findall(X-Y,
          (select(X, Xs, Other),
           member(Y, Other),
           % add an ordering constraint to avoid generating
           % both A-B and B-A
           X @< Y),
          Pairs).

This seems to work when I test it with atoms:

?- pairs([a, b, c, d, e], Pairs), write(Pairs).

[a-b,a-c,a-d,a-e,b-c,b-d,b-e,c-d,c-e,d-e]

Okay, so next step is to call dif/2 on the pairs:

uniq(Vs) :-
  pairs(Vs, Pairs),
  maplist([A-B]>>dif(A, B), Pairs).

However, if we try to use this, we’ll find that our uniq/1 predicate doesn’t seem to be working:

?- findall(('A'=A, 'B'=B, 'C'=C),
    (Vars = [A, B, C], % three variables
     uniq(Vars), % all the variables must have unique values
     Vals = [1,2,3],
     % all of the variables are either 1, 2, or 3
     member(A, Vals), member(B, Vals), member(C, Vals),
     % ...and let's specify that A = 1
     A = 1),
    Solns),
   format("Solutions: ~w", [Solns]).

Solutions: [(A=1,B=1,C=1),(A=1,B=1,C=2),(A=1,B=1,C=3),(A=1,B=2,C=1),(A=1,B=2,C=2),(A=1,B=2,C=3),(A=1,B=3,C=1),(A=1,B=3,C=2),(A=1,B=3,C=3)]

Why is this happening? Let’s take a look at what pairs/2 outputs if we give it uninstantiated variables, like uniq/1 is doing.

?- pairs([A, B, C], Pairs), write(Pairs).

[_4812-_4814,_4800-_4802,_4788-_4790]

Looking at the output, we can see that the variables being bound in the pairs are actually all fresh!

I’m not completely sure, but I believe this is something to do with how findall/3 will automatically qualify unbound variables in the goal it finds all solutions for. In any case, we can try redefining pairs/2 in terms of bagof/3, which doesn’t automatically qualify vars:

pairs(Xs, Pairs) :-
    bagof(X-Y,
          Other^(select(X, Xs, Other),
                 member(Y, Other),
                 X @< Y),
          Pairs).

We can see that it works the same way with atoms:

?- pairs([a, b, c, d, e], Pairs), write(Pairs).

[a-b,a-c,a-d,a-e,b-c,b-d,b-e,c-d,c-e,d-e]

But what happens when we try with variables this time?

?- pairs([A, B, C], Pairs), write(Pairs).

[_4350-_4368,_4350-_4386,_4368-_4386]

We still get the output as numbered variables, but looking at the numbers there, we can see they actually are being reused (if you run this in a Prolog toplevel, it will actually show [A-B, A-C, ...])!

Now, we can put this with the same definition of uniq/1 and have a nice little helper predicate.

pairs(Xs, Pairs) :-
    bagof(X-Y,
          Other^(select(X, Xs, Other),
                 member(Y, Other),
                 X @< Y),
          Pairs).

uniq(Vs) :-
    pairs(Vs, Pairs),
    maplist([A-B]>>dif(A, B), Pairs).

?- findall(('A'=A, 'B'=B, 'C'=C),
    (Vars = [A, B, C],
     Vals = [1,2,3],
     uniq(Vars),
     member(A, Vals), member(B, Vals), member(C, Vals),
     A = 1),
    Solns),
   format("Solutions: ~w", [Solns]).

Solutions: [(A=1,B=2,C=3),(A=1,B=3,C=2)]