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

Question

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?

Ynes

In the second definition: 2 unresolved: [sum(b,f,f),sum(f,b,f)].! So again this is a weakness of cTI. By unfolding the definition once you get the optimal result which is sump(A,B,C)terminates_if b(A);b(B);b(C). Voir. – Rooseveltroost

Answer 1

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.

---

1) And don't be upset if we get a resource_error(memory), it's just a finite system.

2) And no residual constraints to be precise.

3) My favorite numbers are 7^7^7 and 9^9^9. With current implementations this will take some time and space.

Rooseveltroost

Thanks false! ‘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.’ I thought that termination meant finite result set. So you claim that it actually means finite representation of the result set, allowing infinite result sets provided that the interpreter is able to express them with logic variables? – Threegaited

The common notion is answers represented in particular by answer substitutions which are capable of representing an infinity of solutions. Here, and here are some more. – Rooseveltroost

I see: the evaluation of a goal returns a sequence of answers; each answer represents a subset of solutions; the union of the solution subsets is the solution set of the goal. A goal terminates when it has a finite answer sequence (e.g. sump(A,B,C)terminates_if b(A);b(B);b(C). means that the goal sump(A, B, C). has a finite answer sequence when A, B, or C is bound—despite having an infinite solution set). Thanks for the links and explanation. – Threegaited

@Maggyero: You can define termination as a finite answer sequence, yes. But then, that is already too much detail. Universal termination in Prolog is simply G_0, false terminating. Often the precise answers are highly distracting if you are interested in termination only. – Rooseveltroost

An argument in favor of sumB that I think about is that its first and second arguments are symmetric with respect to termination (sumB(A,B,C)terminates_if b(A),b(B);b(C).). – Threegaited

@Maggyero: All three arguments are symmetric w.r.t. termination. The actual termination condition is sumB(A,B,C)terminates_if b(A);b(B);b(C). – Rooseveltroost

Yes you are right. Whereas cTI gives an asymmetry with respect to termination for the second argument of sumA: sumA(A,B,C)terminates_if b(A);b(C). – Threegaited

In sumA/3 the second argument is termination neutral. – Rooseveltroost

Can I request again your expertise on this Prolog post? – Threegaited