# A Prolog Nerdsnipe

Uniqueness & A Surprising Edge-Case

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^{1}, 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`

^{2} 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)]

## Footnotes:

^{1}

except a brief mention of “friendzoning”, which is usually a red flag for me

^{2}

bonus trick: For expressions with confusing operators, you can use `write_canonical/1`

to print out an expression in “canonical” form, to see exactly what’s happening. For example, `write_canonical(\+ A = B).`

outputs something like `\+(=(_A,_B))`

, so you can see it’s applying the `\+`

predicate to the term `=(A, B)`

.