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 think1, 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:
except a brief mention of “friendzoning”, which is usually a red flag for me
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)
.