prolog - 用另一种方法将两个整数相除

Question

让我们考虑 n=s(s(...s(0)...)) （简单地说 n= s^n(0)）。如何编写一个计算两个整数相除的程序？我的意思是 s^(n//m) （这是除法的定义）。有任何想法吗？例如，如果我们有一个问题：

?-divide(s(s(s(s(0)))),s(0),D). 

我写了以下代码：

 nat(0).
 nat(s(X)) :- nat(X).
 divide(0,_,D) :- D is 0.
 divide(s(X),s(Y),D) :- divide(X,Y,D). 

Answer 1

当 x 和 y 是数字时，您的谓词divide/3错误地假设以下等式成立： (x-1)/(y-1) = x/y
反例是： (16-1)/(4-1) = 5不同于16/4 = 4

您似乎正试图将您的谓词建立在众所周知的加法谓词上：

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

但是除法是乘法而不是加法运算。解决问题的一种可能方法是将除法视为迭代减法（因为乘法是迭代加法）。由于您的谓词是关于自然数的，因此它必须按照您在问题中所写的那样实现整数除法。

Answer 2

旧帖子，但我有相同的任务。所以答案是：

%nat:Is X natural?,nat2:Is X,Y naturals?
nat(0).
nat(s(X)) :- nat(X).
nat2(0,s(Y)) :- nat(Y).
nat2(s(X),s(Y)) :- nat2(X,Y). 

%Summary of X+Y=Z
sum(X,0,X) :- nat(X).
sum(X,s(Y),s(Z)) :- sum(X,Y,Z).

%Minus of X-Y=Z is same as Y+Z=X
minus(X,Y,Z) :- sum(Y,Z,X). 

%Multiplication of X*Y,add X+0(Z) Y times(recursive)
mult(X,0,0).
mult(X,s(Y),D):-mult(X,Y,Z), sum(X,Z,D).

%Divide,check special occasions,add to W the s(0)(1) recursive.
divide(X,Y,D) :- div(X,Y,D,_).
div(s(X),0,undefined,_).
div(0,s(Y),0,_).
div(0,0,undefined,_).
div(X,Y,0,X) :- X \== 0,Y \== 0,nat2(X,Y).
div(X,Y,D,L) :- X \== 0,Y \== 0,minus(X,Y,Z),div(Z,Y,W,L),sum(W,s(0),D).

Answer 3

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

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

例子：

| ?- divide(s(s(s(0))), s(0), N).

N = s(s(s(0))) ?

yes
| ?- divide(s(s(s(s(0)))), s(s(0)), N).

N = s(s(0)) ?

yes

这个解决方案显然只适用于完美的除法，如 4/2 或 6/3 等。因为我们只能使用 Peano 数字表示自然数。