(让我在期中问题的浪潮中偷偷地把它放进去。
两个自然数之和的常见定义是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不会终止。这次完全一样！所以我们可以说。
nat_nat_sum(0， N， N( ：- 假。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的赏金(
nat_nat_sum(0, B, B).
nat_nat_sum(s(A), B, s(C)) :-
nat_nat_sum(B, A, C).
？
好吧，似乎结束了。我想到的解决方案是：
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相同。这真的是更好的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(
显而易见的技巧是翻转参数：
sum(0,N,N).
sum(N,0,N).
sum(s(A),B,s(C)):- sum(B,A,C) ; sum(A,B,C).
采用以下两个定义：
定义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不终止模式添加 (-,-,+(。看：
定义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 更好。
再见