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

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)`.