Should the first and second arguments be swapped in a rule defining addition?

There are two possible rules for addition in Prolog, with different termination properties according to cTI:

1. cTI reports sum(A,B,C)terminates_if b(A);b(C). for the following rule:

sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
  sum(X, Y, Z).

2. cTI reports sum(A,B,C)terminates_if b(A),b(B);b(C). for the following rule (X and Y are swapped):

sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
  sum(Y, X, Z).

The difference can be observed for instance by executing the query sum(X, 0, Z). with SWISH, the online SWI-Prolog implementation of Prolog.

It returns the following solutions for the first rule:

?- sum(X, 0, Z).
   X = Z, Z = 0
;  X = Z, Z = s(0)
;  X = Z, Z = s(s(0))
;  X = Z, Z = s(s(s(0)))
;  X = Z, Z = s(s(s(s(0))))
;  …

And it returns the following solutions for the second rule:

?- sum(X, 0, Z).
   X = Z, Z = 0
;  X = Z, Z = s(_1302)
;  false.

Which of these two rules is correct?

When discussing various versions of the same program, it helps a lot to rename those versions such that they can cohabit in the same program:

sumA(0, Y, Y).
sumA(s(X), Y, s(Z)) :- sumA(X, Y, Z).

sumB(0, Y, Y).
sumB(s(X), Y, s(Z)) :- sumB(Y, X, Z).


?- sumA(X, 0, Z).
   X = 0, Z = 0
;  X = s(0), Z = s(0)
;  X = s(s(0)), Z = s(s(0))
;  X = s(s(s(0))), Z = s(s(s(0)))
;  ... .
?- sumB(X, 0, Z).
   X = 0, Z = 0
;  X = s(_A), Z = s(_A).

(Above output is from Scryer, which is better readable)

Before looking at the concrete definitions, think of the set of solutions that we expect for X and Z. Both should be the same, and they should describe all natural s(X)-numbers 0, s(0), s(s(0)) ... So we have infinitely many solutions. How shall we, finite beings with our finite Prolog systems, describe infinitely many solutions? Well, we can give it a try and just start¹. That's what we see in sumA. What is nice here, is that each and every answer is actually a solution (that is, there are no variables remaining²). Just a pity that the program does not terminate (universally). At least it produces all solutions in a fair manner. Wait long enough and also your favorite solution³ will appear.

In sumB that infinite set of natural numbers is enumerated in a quite different manner. First, we get a solution for 0 and then we get a single answer which includes all other numbers ≥ 1. So we have compressed this infinite set into a single variable! That's the power of logic variables. Of course, we paid a tiny price here, for now we also include really everything in the argument of s(_A). Everything, including s(nothing).

?- Z = s(nothing), sumA(Z, 0, Z).
   false.
?- Z = s(nothing), sumB(Z, 0, Z).
   Z = s(nothing).

Which of these two rules is correct?

Both sumA and sumB are correct. And sumB as long as we can distinguish our numbers from other terms (that's what roughly corresponds to a well typed program).

But which one is preferable? It all depends. Usually the predicate will be used in some context. Maybe a subsequent goal will only terminate if one of its arguments is ground. In this case, sumA may be preferable. If there is no further goal then sumB is always preferable. It all depends a bit.

What is most important to see is that some of the infinities of solutions can be elegantly subsumed with logic variables thereby improving the termination property. For more complex situations this will not be enough but then constraints will be attached to those variables.