Search code examples
prologsuccessor-arithmetics

Recursive addition in Prolog with Peano numbers doesn't work


I'm currently trying to practice some Prolog. I just started and I'm facing a problem I don't quite understand. I want to determine recursively if one Peano number is the double of another one. I tried to solve it like this:

isDouble(0, X,X).
isDouble(s(Peano1), Peano1, Peano2) :-
    isDouble(Peano1, s(Peano1), Peano2).

For some reason it doesn't work. Does anyone know why?


Solution

  • You don't need three arguments to define such a predicate. Just consider what relation it should describe: a relation between a number and its double. Hence you only need two arguments and two rules describing the two possibilities. Either the number is zero, then its double is zero as well. Otherwise you have a difference of two s/2 for the double in every recursion but only one for the number:

    nat_double(0,0).
    nat_double(s(X),s(s(Y))) :-
       nat_double(X,Y).
    

    This yields the desired results:

    ?- nat_double(X,Y).
    X = Y, Y = 0 ;                     % X=0, Y=0
    X = s(0),                          % X=1
    Y = s(s(0)) ;                      % Y=2
    X = s(s(0)),                       % X=2
    Y = s(s(s(s(0)))) ;                % Y=4
    X = s(s(s(0))),                    % X=3
    Y = s(s(s(s(s(s(0)))))) ;          % Y=6
    X = s(s(s(s(0)))),                 % X=4
    Y = s(s(s(s(s(s(s(s(0)))))))) ;    % Y=8
    .
    .
    .
    

    Or if you want to test a pair as suggested in the comments:

    ?- nat_double(s(s(0)),s(s(s(s(0))))).
    true.
    

    EDIT:

    If you insist on the interface isDouble/3, as your comment suggests, then you could define it as a calling predicate for nat_double/2 like so:

    isDouble(X,X,Y) :-
       nat_double(X,Y).
    

    That yields the desired result for your example:

    ?- isDouble(s(s(0)),s(s(0)),s(s(s(s(0))))).
    true.