4

我正在尝试制作一个除以两个 Peano 数字的程序。不幸的是，在我寻找其他答案后，循环开始运行。有什么方法可以避免使用我的方法重复吗？

    s(0).
    s(X):- X.

    plus(0,Y,Y).
    plus(s(X), Y, s(Z)):- plus(X,Y,Z).

    minus(A, B, C) :- plus(C, B, A).

    division(0, _ , 0).
    division(X, s(0), X).
    division(A, B, s(N)) :- minus(A, B, R), division(R, B, N).

输出

?- division(s(s(s(s(0)))), s(0),X).
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
false.

输出#2

?- divide(s(s(s(s(0)))), Y,X).
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(s(s(s(0)))),
X = s(0) ;
Y = X, X = s(s(0)) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
;ERROR: Out of local stack
4

1 回答 1

5

正确性。首先，让我们考虑正确性问题。根据您的定义，0/0 = 0。即division(0, 0, 0). 所以你说 0 除以 0 就是 0。另一个问题是 的定义s/1。有关更多信息，请参阅。

多余的答案。要确定冗余的来源，请考虑每个谓词的子句。他们是否可能都申请相同的地面查询？让我们看看：因为plus/3这不可能发生，因为事实需要0在第一个参数中，但规则需要s(_)。这永远不可能同时发生。因此，没有冗余的来源。division/3然而，两者都适用于进一步division(0, s(0), 0).的第二个事实，并且该规则也可能适用于两者。

不终止。在进入另一个答案中讨论的技术细节之前，让我们先回顾一下您期望从 4/X = Y 得到什么。显然，这些解决方案(X,Y): [(1,4),(2,2),(4,1)]。但是解决方案0呢？

于 2017-11-06T08:16:29.607 回答