Better termination for s(X)-sum

Question

(Let me sneak that in within the wave of midterm questions.)

A common definition for the sum of two natural numbers is nat_nat_sum/3:

nat_nat_sum(0, N, N).
nat_nat_sum(s(M), N, s(O)) :-
   nat_nat_sum(M, N, O).

Strictly speaking, this definition is too general, for we have now also success for

?- nat_nat_sum(A, B, unnatural_number).

Similarly, we get the following answer substitution:

?- nat_nat_sum(0, A, B).
   A = B.

We interpret this answer substitution as including all natural numbers and do not care about other terms.

Given that, now lets consider its termination property. In fact, it suffices to consider the following failure slice. That is, not only will nat_nat_sum/3 not terminate, if this slice does not terminate. This time they are completely the same! So we can say iff.

nat_nat_sum(0, N, N) :- false.
nat_nat_sum(s(M), N, s(O)) :-
   nat_nat_sum(M, N, O), false.

This failure slice now exposes the symmetry between the first and third argument: They both influence non-termination in exactly the same manner! So while they describe entirely different things — one a summand, the other a sum — they have exactly the same influence on termination. And the poor second argument has no influence whatsoever.

Just to be sure, not only is the failure slice identical in its common termination condition (use cTI) which reads

nat_nat_sum(A,B,C)terminates_if b(A);b(C).

It also terminates exactly the same for those cases that are not covered by this condition, like

?- nat_nat_sum(f(X),Y,Z).

Now my question:

Is there an alternate definition of nat_nat_sum/3 which possesses the termination condition:

nat_nat_sum2(A,B,C) terminates_if b(A);b(B);b(C).

(If yes, show it. If no, justify why)

In other words, the new definition nat_nat_sum2/3 should terminate if already one of its arguments is finite and ground.

---

^{Fine print. Consider only pure, monotonic, Prolog programs. That is, no built-ins apart from (=)/2 and dif/2}

(I will award a 200 bounty on this)

Answer 1

nat_nat_sum(0, B, B).
nat_nat_sum(s(A), B, s(C)) :-
        nat_nat_sum(B, A, C).

?

Answer 2

Ok, seems its over. The solution I was thinking of was:

nat_nat_sum2(0, N,N).
nat_nat_sum2(s(N), 0, s(N)).
nat_nat_sum2(s(N), s(M), s(s(O))) :-
   nat_nat_sum2(N, M, O).

But as I realize, that's just the same as @mat's one which is almost the same as @WillNess'es.

Is this really the better nat_nat_sum/3? The original's runtime is independent of B (if we ignore one (1) occurs check for the moment).

There is another downside of my solution compared to @mat's solution which naturally extends to nat_nat_nat_sum/3

nat_nat_nat_sum(0, B, C, D) :-
   nat_nat_sum(B, C, D).
nat_nat_nat_sum(s(A), B, C, s(D)) :-
   nat_nat_nat_sum2(B, C, A, D).

Which gives

nat_nat_nat_sum(A,B,C,D)terminates_if b(A),b(B);b(A),b(C);b(B),b(C);b(D).

(provable in the unfolded version with cTI)