prolog - 使用皮亚诺数字除法

Question

我正在尝试制作一个除以两个 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

Answer 1

正确性。 首先，让我们考虑正确性问题。根据你的定义，0/0 = 0。即division(0, 0, 0) .所以你说0除以0是0。另一个问题是s/1的定义。 .见 successor-arithmetics更多。

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

非终止。 在进入 another answer 中讨论的技术细节之前，让我们先退一步看看你期望从 4/X = Y 得到什么。显然，这些解决方案 (X,Y): [(1,4),(2,2),(4,1)] .但是 0 的解决方案怎么样？ ?