更好地终止s(X)-sum

Question

(让我在中期问题的浪潮中偷偷摸摸.)

两个自然数之和的通用定义是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.

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

鉴于此,现在让我们考虑它的终止属性.实际上,考虑以下故障切片就足够了.也就是说nat_nat_sum/3,如果此切片未终止,则不仅不会终止.这次他们完全一样!所以我们可以说iff.

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

这个失败切片现在暴露了第一个和第三个参数之间的对称性:它们都以完全相同的方式影响非终止!因此,虽然他们描述了完全不同的东西 - 一个是加数,另一个是和 - 它们对终止具有完全相同的影响.可怜的第二个论点没有任何影响.

可以肯定的是,不仅故障片在其读取的公共终止条件(使用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) terminates_if b(A);b(B);b(C).

(如果是,请显示.如果不是,请说明理由)

换句话说,如果新定义的一个参数是有限的和基础的,则新定义nat_nat_sum2/3应该终止.

---

^{细则.只考虑纯粹的,单调的Prolog程序.也就是说,除了(=)/2和之外没有内置插件dif/2}

(我将奖励200美元的奖金)

Answer 1

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

？