Dividing two integers with an alternative way

问题:

Let's consider that n=s(s(...s(0)...)) (simply n= s^n(0)). How could write a program calculating the division of two integers? I mean s^(n//m) (thats the definition of the division) . Any ideas? For example, if we had the question:

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

i have written the following code:

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

回答1:

Your predicate divide/3 assumes wrongly that the following equation holds when x and y are numbers: (x-1)/(y-1) = x/y
A counter-example is: (16-1)/(4-1) = 5 is different from 16/4 = 4

It seems you are trying to base your predicate on the well-know addition predicate:

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

but division is a multiplicative not an additive operation. A possible way of solving your problem is to think of division as an iterated subtraction (as multiplication is an iterated addition). As your predicate is on natural numbers it must implement integral division as you wrote in the question.

回答2:

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

Example:

| ?- 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

This solution obviously only works for perfect divisions like 4/2 or 6/3 etc. Since we can only represent natural numbers using Peano's numerals.

回答3:

Old post,but i have a same assignment.So the answer is:

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