Relying on rule order

问题:

To calculate the hamming distance between two lists of the same length, I use foldl(hamm, A, B, 0, R). with this definition of hamm/4:

hamm(A, A, V, V) :- !.
hamm(A, B, V0, V1) :- A \= B, V1 is V0 + 1.

The cut in the first rule prevents the unnecessary backtracking. The second rule, however, could have been written differently:

hamm2(A, A, V, V) :- !.
hamm2(_, _, V0, V1) :- V1 is V0 + 1.

and hamm2/4 will still be correct together with foldl/5 or for queries where both A and B are ground.

So is there a really good reason to prefer the one over the other? Or is there a reason to keep the rules in that order or switch them around?

I know that the query

hamm(a, B, 0, 1).

is false, while

hamm2(a, B, 0, 1).

is true, but I can't quite decide which one makes more sense . . .

回答1:

You already spotted the differences between those definitions: efficiency apart, you should decide about your requirements. Are you going to accept variables in your data structures? Such programming style introduces some of advanced Prolog features (incomplete data structures).

Anyway, I think the first form is more accurate (not really sure about, I would say steadfast on 4° argument)

?- hamm(a, B, 0, 1).
false.

?- hamm(a, B, 0, 0).
B = a.

while hamm2 is

?- hamm2(a, B, 0, 1).
true.

?- hamm2(a, B, 0, 0).
B = a.

回答2:

The OP implemented two accumulator-style predicates for calculating the Hamming distance (hamm/4 and hamm2/4), but wasn't sure which one made more sense.

Let's read the query that puzzled the OP: "Is there an X such that distance(a,X) is 1?". Here are the "answers" Prolog gives:

?- hamm(a,X,0,1). 
false.                          % wrong: should succeed conditionally
?- hamm2(a,X,0,1).              % wrong: should succeed, but not unconditionally
true.

From a logical perspective, both implementations misbehave in above test. Let's do a few tests for steadfastness:

?- hamm(a,X,0,1),X=a.           % right
false.
?- hamm(a,X,0,1),X=b.           % wrong: should succeed as distance(a,b) is 1
false.

?- hamm2(a,X,0,1),X=a.          % wrong: should fail as distance(a,a) is 0
X = a.
?- hamm2(a,X,0,1),X=b.          % right 
X = b.

Note that in previous queries hamm/4 rightly fails when hamm2/4 wrongly succeeded, and vice-versa. So both are half-right/half-wrong, and neither one is steadfast.

---

What can be done?

Based on if_/3 and (=)/3 presented by @false in this answer, I implemented the following pure code for predicate hamm3/4:

:- use_module(library(clpfd)).

hamm3(A,B,V0,V) :-
   if_(A = B, V0 = V, V #= V0+1).

Now let's repeat above queries using hamm3/4:

?- hamm3(a,X,0,1). 
dif(X,a).
?- hamm3(a,X,0,1),X=a.
false.
?- hamm3(a,X,0,1),X=b.
X = b.

It works! Finally, let's ask the most general query to see the entire solution set of hamm3/4:

?- hamm3(A,B,N0,N).
A = B,    N0 = N ;
dif(A,B), N0+1 #= N.