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

问题描述

(让我潜入期中问题之列.)

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

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

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.

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

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

现在我的问题:

是否存在具有终止条件的nat_nat_sum/3替代定义:

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

(如果是，请显示.如果否，请说明原因)

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

换句话说，如果新定义nat_nat_sum2/3的自变量已经一个是有限且固定的，则应终止.

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

^{精美打印.仅考虑纯净的，单调的Prolog程序.也就是说，除了(=)/2和dif/2}

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

(我将为此奖励200个赏金)

(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屋！