6

（让我在期中问题的浪潮中偷偷摸摸。）

两个自然数之和的常见定义是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) :-假。
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) terminates_if b(A);b(B);b(C).

（如果是，请出示。如果不是，请说明原因）

换句话说，如果新定义的一个论点已经是有限且有基础的，则新定义nat_nat_sum2/3应该终止。

精美的印刷品。只考虑纯粹的、单调的 Prolog 程序。也就是说，除了(=)/2和之外没有内置插件dif/2

（我将为此奖励 200 赏金）

4

4 回答 4

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

?

于 2014-11-29T22:30:49.997 回答
3

好吧，似乎结束了。我想到的解决方案是：

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

但正如我意识到的那样，这与@mat 的相同，与@WillNess'es 几乎相同。

这真的更好nat_nat_sum/3吗？原始的运行时是独立的B（如果我们暂时忽略一 (1) 次发生的检查）。

与@mat 的解决方案相比，我的解决方案还有另一个缺点，它自然扩展到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).

这使

nat_nat_nat_sum(A,B,C,D)terminates_if b(A),b(B);b(A),b(C);b(B),b(C);b(D).

（可在cTI的展开版本 中证明）

于 2014-11-29T22:57:04.073 回答
1

显而易见的技巧是翻转论点：

sum(0,N,N).
sum(N,0,N).
sum(s(A),B,s(C)):- sum(B,A,C) ; sum(A,B,C).
于 2014-11-29T18:58:55.747 回答
1

取以下两个定义：

定义 1：

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

定义 2：

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

定义 1 终止于模式 add(-,-,+)，而定义 2 不终止于模式 add(-,-,+)。看看看看：

定义 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
?-

定义 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
?-

所以我猜定义 1 比定义 2 好。

再见

于 2014-12-05T23:17:15.130 回答