6

(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)

false
  • 10,264
  • 13
  • 101
  • 209

4 Answers4

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

?

mat
  • 40,498
  • 3
  • 51
  • 78
  • Can we see a counter-example from this output? – mat Nov 29 '14 at 22:36
  • 1
    [A minimal rewrite](http://www.complang.tuwien.ac.at/cti/cgi/cti?texta=nat_nat_sum%280%2C+B%2C+B%29.%0D%0Anat_nat_sum%28s%28A%29%2C+B%2C+s%28C%29%29+%3A-%0D%0A++++++++nat_nat_sum2%28B%2C+A%2C+C%29.%0D%0A%0D%0Anat_nat_sum2%280%2C+B%2C+B%29.%0D%0Anat_nat_sum2%28s%28A%29%2C+B%2C+s%28C%29%29+%3A-%0D%0A++++++++nat_nat_sum%28B%2C+A%2C+C%29.) gets `nat_nat_sum(A,B,C)terminates_if b(A);b(B);b(C).` – false Nov 29 '14 at 22:41
  • The key idea of my solution is to *cyclically* rotate the summands, so that periodically, *each of them* is in the first argument position, which can influence termination. This strategy is admissible in this case because addition is commutative. It works for any number of summands. The minimal rewrite is what I started with. I then shortened it to the version above. – mat Dec 03 '14 at 08:12
  • Could you put this into your answer? – false Apr 07 '16 at 14:28
3

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)

false
  • 10,264
  • 13
  • 101
  • 209
  • I'd say my variant is closer to your "minimal rewrite" than Mat's. His was the first I considered, but then I tried to tweak it further. Your tweak moves my 2nd clause one level down so to speak. But we both didn't solve it. You should really accept your own (this) answer. – Will Ness Nov 30 '14 at 11:16
  • now that I see this variant, it makes that much more sense than anything else. :) – Will Ness Nov 30 '14 at 11:23
  • @WillNess: It certainly is easier to understand, as each argument decreases independently in the recursive rule which is also the reason that cTI had problems. But now imagine `nat_nat_nat_sum/4`! @mat's version works here just as smoothly guaranteeing termination for: `nat_nat_nat_sum(A,B,C,D)terminates_if b(A),b(B);b(A),b(C);b(B),b(C);b(D).` – false Nov 30 '14 at 11:34
  • (seeing some code would help...) but that's a different question, about the sum/4. here, yours is the answer. – Will Ness Nov 30 '14 at 11:42
1

The obvious trick is to flip the arguments:

sum(0,N,N).
sum(N,0,N).
sum(s(A),B,s(C)):- sum(B,A,C) ; sum(A,B,C).
Will Ness
  • 70,110
  • 9
  • 98
  • 181
  • 1
    But `sum(s(0),B,C), false` does not terminate, right? – false Nov 29 '14 at 19:09
  • Hmm, yes. Should it? I didn't understand the termination conditions: what does `b(A)` mean? – Will Ness Nov 29 '14 at 19:24
  • b(A): finite and ground. vulgo: bound or bounded - I never know which one :-) – false Nov 29 '14 at 19:25
  • Thanks. It's a tough one. :) – Will Ness Nov 29 '14 at 19:26
  • 1
    [Evidence](http://www.complang.tuwien.ac.at/cti/cgi/cti?texta=sum%280%2CN%2CN%29.%0D%0Asum%28N%2C0%2CN%29.%0D%0Asum%28s%28A%29%2CB%2Cs%28C%29%29%3A-+sum%28B%2CA%2CC%29.%0D%0Asum%28s%28A%29%2CB%2Cs%28C%29%29%3A-+sum%28A%2CB%2CC%29.%0D%0A%0D%0A%0D%0A%25+original+version+by+Will+Ness+http%3A%2F%2Fstackoverflow.com%2Fa%2F27205837%2F772868%0D%0A%0D%0Asum0%280%2CN%2CN%29.%0D%0Asum0%28N%2C0%2CN%29.%0D%0Asum0%28s%28A%29%2CB%2Cs%28C%29%29%3A-+sum0%28B%2CA%2CC%29+%3B+sum0%28A%2CB%2CC%29.). Just use another answer for another attempt! – false Nov 29 '14 at 19:28
  • 1
    It means that cTI's nTI (non-termination inferencer) was not able to infer/find/prove an example with that mode. See http://www.complang.tuwien.ac.at/cti/help#NTI – false Nov 29 '14 at 19:33
  • but what does "f" mean? – Will Ness Nov 29 '14 at 19:35
  • @false wow, thanks! I appreciate it. Thank you for the interesting challenge, I wish I'd solved it fully. :) The real solution as your answer shows is not to introduce any duplication in any of the clauses, while covering all corners so to speak. Nice. – Will Ness Dec 02 '14 at 19:27
1

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 terminates for pattern add(-,-,+), whereas definition 2 does not terminate for pattern add(-,-,+). Look see:

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 guess definition 1 is better than definition 2.

Bye

  • 1
    Definition 2 is termination-neutral for Arg2 and Arg3. – false Dec 06 '14 at 09:25
  • 1
    The notion of termination is well established in the context of logic programming and Prolog. To be precise, we are talking about **universal termination**. If you have a counterexample of two queries with some terms `A, B, C1, C2` such that `add(A,B,C1), false` and `add(A,B,C2), false` (with definition 2) terminate differently, then please tell me them. I claim: there is no such counterexample. – false Dec 07 '14 at 11:43