s(X)-sum 的更好终止 [英] Better termination for s(X)-sum

问题描述

(让我在期中问题的浪潮中潜入.)

两个自然数之和的常见定义是nat_nat_sum/3:

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

严格来说，这个定义太笼统了，因为我们现在也成功了

?- nat_nat_sum(A, B, unnatural_number).

同样，我们得到以下答案替换:

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

我们将此答案替换解释为包括所有自然数并且不关心其他术语.

鉴于此，现在让我们考虑它的终止属性.事实上，考虑下面的 failure slice 就足够了.也就是说，如果该切片没有终止，则不仅 nat_nat_sum/3 不会终止.这一次他们完全一样！所以我们可以说如果.

<上一页>nat_nat_sum(0, N, N) :- false.nat_nat_sum(s(M), N, s(O)) :-nat_nat_sum(M, N, O), 假.

这个失败切片现在暴露了第一个和第三个参数之间的对称性:它们都以完全相同的方式影响非终止！因此，尽管它们描述了完全不同的事物——一个是总和，另一个是总和——但它们对终止的影响完全相同.可怜的第二个论点没有任何影响.

为了确定，不仅故障片在其通用终止条件上相同(使用 cTI) 读取

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

对于那些不属于此条件的情况，它也以完全相同的方式终止，例如

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

现在我的问题:

<块引用>

nat_nat_sum/3是否有另一种具有终止条件的定义:

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

(如果是，请出示.如果不是，请说明原因)

换句话说，如果新定义 nat_nat_sum2/3 已经有 一个 的参数是有限且接地的，则应该终止.

<小时>

^{细则.只考虑纯粹的、单调的 Prolog 程序.也就是说，除了 (=)/2 和 dif/2}

之外没有内置插件

(我将为此奖励 200 赏金)

解决方案

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

?

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

解决方案

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

?

这篇关于s(X)-sum 的更好终止的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！