我无法完全理解这段代码。如果我理解正确，它会尝试通过连续尝试更大的除数来找到除数和余数。因为它div/4只是说明除数和余数的属性，即它测试找到的任何东西是否合适。生成部分被埋在其中为Dr*C=Xtimes/3生成可能。C
我找到了这个：
- 我不知道有什么
mod/3作用。
times/3有问题，因为两个子句有歧义nat/1不是测试，而是自然数的生成器- 无限循环来自这样一个事实，即
div/4不知道如果找到了一个解决方案，就没有更多的解决方案。如果会依次尝试更大的除数。我们可以通过剪切告诉它在子句的远端停止，在那里找到了解决方案。
- 一个人必须付出
这将导致：
div(Dd,s(0),Dd,0).
div(Dd,Dr,C,R) :-
% just a guard
less(Dr,Dd),
% Dr known, C,X free,
% --> C should be incremented by 1 on backtracking, and X computed
% --> and we will stop latest when X > Dd
times(Dr,C,X),
% --> Dd known, X has been generated by the above, R is being computed
plus(X,R,Dd),
less(R,Dr),
% solution found at this point
!.
less(0,s(_)).
less(s(X),s(Y)) :-
less(X,Y).
times(0,_,0).
times(s(X),Y,Z) :-
times(X,Y,M),
plus(Y,M,Z).
plus(0,Y,Y) :-
nat(Y).
plus(s(X),Y,s(Z)) :-
plus(X,Y,Z).
nat(0).
nat(s(X)):-
nat(X).
附录
如前所述，用更易于阅读的... aynthing 列表替换 Peano 递归定义更容易。在这种情况下，匿名变量_. 如果 Peano 知道列表，他可能会改用这些（与 Gödel 相同，他可能会使用适当的数组而不是英雄式的 Gödel 编码）
例如 for times/3（注意 的歧义[_|Rs]，它与[_]和[_,_|Rs]，分为两种不同的情况[_]和[_,_|Rs]；我被这件事难住了一段时间）和plus/3：
times([],X,[]) :- nat(X).
times([_],X,X) :- nat(X).
times([_,S|Rs],Y,Z) :- times([S|Rs],Y,M),plus(Y,M,Z).
% adding two lists
plus([],Y,Y) :- nat(Y).
plus([_|X],Y,[_|Z]) :- plus(X,Y,Z).
% a list of any length is equivalent to a natural number
% this predicate not only tests, but also constructs natural
% numbers; try "nat(X)"
nat([]).
nat([_|X]) :- nat(X).
以上可以测试。测试plus/3工作良好：
:- begin_tests(plus).
% 0 variables (thus a test)
test('0+0=0') :- plus([],[],[]).
test('1+1=2') :- plus([_],[_],[_,_]).
test('2+2=4') :- plus([_,_],[_,_],[_,_,_,_]).
% 1 variable
test('x+1=2') :- bagof(X,plus(X,[_],[_,_]),L),L=[[_]].
test('1+x=2') :- bagof(X,plus([_],X,[_,_]),L),L=[[_]].
test('1+1=x') :- bagof(X,plus([_],[_],X),L),L=[[_,_]].
test('3+x=5') :- bagof(X,plus([_,_,_],X,[_,_,_,_,_]),L),L=[[_,_]].
test('x+3=5') :- bagof(X,plus(X,[_,_,_],[_,_,_,_,_]),L),L=[[_,_]].
% 2 variables
test('x+y=3') :- bagof(sol(X,Y),plus(X,Y,[_,_,_]),L), L= [sol([], [_,_,_]), sol([_], [_, _]), sol([_, _], [_]), sol([_, _, _], [])].
% test('3+x=y') :- ... plus([_,_,_],X,Y) generates infinitely many solutions; good; how to run this 5 times for example??
% test('x+3=y') :- ... plus([_,_,_],X,Y) generates infinitely many solutions; good; how to run this 5 times for example??
% 3 variables (goes to infinity)
% we cannot test plus(X,Y,Z); the coolest would be for plus/3 to then generate
% all possible X,Y,Z triplets with increasing Z for example. How to do that?
:- end_tests(plus).
?- run_tests(plus).
% PL-Unit: plus ......... done
% All 9 tests passed
true.
但是在第一个成功的结果之后，测试times/3进入无穷大。我对此并不高兴。
:- begin_tests(times).
% 0 variables
test('0*0=0') :- times([],[],[]).
test('0*2=0') :- times([],[_,_],[]).
test('2*0=0') :- times([_,_],[],[]).
test('1*1=1') :- times([_],[_],[_]).
test('1*2=1') :- times([_],[_,_],[_]).
test('2*1=1') :- times([_,_],[_],[_]).
% element 0 does not work
% test('0*x=0') :- generates all naturals
% test('x*0=0') :- generates all naturals
% test('x*y=0') :- generates all pairs of naturals
test('1*x=1') :- bagof(X,times([_],X,[_]),L),L=[[_]].
test('2*x=4') :- bagof(X,times([_,_],X,[_,_,_,_]),L),L=[[_,_]]. % blows stack
test('3*x=4',[fail]) :- times([_,_,_],_X,[_,_,_,_]).
test('x*1=1') :- bagof(X,times(X,[],[]),L),L=[[_]].
test('x*2=4') :- bagof(X,times(X,[_,_],[_,_,_,_]),L),L=[[_,_]].
test('1*3=x') :- bagof(X,times(X,[],[]),L),L=[[_]].
test('x*2=x') :- bagof(X,times(X,[_,_],[_,_,_,_]),L),L=[[_,_]].
:- end_tests(times).
?- run_tests(times).
% PL-Unit: times .......^C
Interrupted test times:'2*x=4'