Best completion for s (X) -total

Question

(Let me sneak into a wave of intermediate questions.)

The general definition of 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, since now we are successful for

 ?- nat_nat_sum(A, B, unnatural_number). 

Similarly, we get the following substitution of answers:

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

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

Given this, now consider its completion property. In fact, it is enough to consider the following fragment of failure . That is, not only nat_nat_sum/3 does not end if this slice does not end. This time they are exactly the same! Therefore, we can say that 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 fragment now displays the symmetry between the first and third arguments: they both affect non-ending in exactly the same way! Therefore, when they describe completely different things - one term, the other - the sum, they have exactly the same effect on the termination. And the poor second argument has no effect.

To be sure that not only the failure fragment is identical in its general termination condition ( use cTI ), which reads

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

It also ends in exactly the same way for cases that are not covered by this condition, for example

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

Now my question is:

Is there an alternative definition for nat_nat_sum/3 that has a termination condition:

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

(If yes, show it. If not, explain why)

In other words, the new definition of nat_nat_sum2/3 should end if only one of its arguments is finite and justified.

---

^{Great print . Consider only clean, monotonous Prolog programs. That is, no built-in functions except (=)/2 and dif/2}

(I reward 200 bounties for 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

Well, it seems it's over. The solution I was thinking about 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 understand it, this is exactly the same as @mat, which is almost the same as @ WillNess'es.

Is this really better than nat_nat_sum/3 ? The initial execution time does not depend on B (if we ignore one (1), a check will occur at the moment).

There is another drawback of my solution compared to the @mat 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). 

What 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 deployed version with cTI )

Answer 3

The obvious trick is translating the arguments:

 sum(0,N,N). sum(N,0,N). sum(s(A),B,s(C)):- sum(B,A,C) ; sum(A,B,C). 

Answer 4

We take the following two definitions:

Definition 1:

 add(n,X,X). add(s(X),Y,s(Z)) :- add(X,Y,Z). 

Definition 2:

 add(n,X,X). add(s(X),Y,Z) :- add(X,s(Y),Z). 

Definition 1 is completed to add the pattern (-, -, +), while definition 2 does not end for the add (-, -, +) pattern. Take a look:

Definition 1:

 ?- add(X,Y,s(s(s(n)))). X = n, Y = s(s(s(n))) ; X = s(n), Y = s(s(n)) ; X = s(s(n)), Y = s(n) ; X = s(s(s(n))), Y = n ?- 

Definition 2:

 ?- add(X,Y,s(s(s(n)))). X = n, Y = s(s(s(n))) ; X = s(n), Y = s(s(n)) ; X = s(s(n)), Y = s(n) ; X = s(s(s(n))), Y = n ; Error: Execution aborted since memory threshold exceeded. add/3 add/3 ?- 

So, I think Definition 1 is better than Definition 2.

Bye