I am trying to work out calculating the difference for 'Peano numbers' (Recursive definition of natural numbers represented as s(0), s(s(0)) etc.) but I am kind of stuck with one problem.
The definition for subtraction is the following:
s(X) - 0 = s(X)
s(X) - s(s(X)) = 0
s(X) - s(X) = 0
s(s(X)) - s(X) = s(0)
0 - s(X) = 0
This is my current code:
nat(0).
nat(s(X)) :- nat(X).
% sub/3
% Subtracts right operand from left operand and returns difference
sub(0, _, 0).
sub(X, 0, X).
sub(s(X), s(Y), X) :-
sub(X,Y,X).
My thought process behind this:
Since I don't really need to recursively increase the difference I can just use the last X i have left after the recursion as my result.
For some reason the following question works:
?- sub(s(0), s(0), X).
X = 0 ;
But this one doesn't:
?- sub(s(s(0)), s(s(0)), X).
false.
Can anyone point out my mistake or suggest a better way to implement the sub procedure?
This might be a beginner mistake, since i really haven't done much. Sorry if that's the case.
//EDIT This is how i resolved it
sub(X, 0, X).
sub(0, _, 0).
% not sure why I didn't test this before, thought I did.
sub(s(X), s(Y), Diff) :-
sub(X,Y,Diff).
sub(s(X), s(Y), X) :- sub(X,Y,X).
says that
You can prove that s(X)-s(Y) = X
if you can prove that X-Y = X
which is a bit weird. There should be a third variable in there, Z.
Prolog tries to prove (make true)
sub(s(s(0)), s(s(0)), X).
which can be done if
sub(s(0),s(0),s(0)).
because the right-hand side of the rule is set thus by positing X=s(0) and Y=s(0) through pattern-matching the LHS.
Trying to prove this sub(s(0),s(0),s(0)) again means using the rule (nothing else is applicable), positing X=0, Y=0, X=s(0). But X cannot be both 0 and s(0). Impasse! false.