Composition of substitutions for unary addition in prolog?

Question

Can someone explain how the logic of the composition of substitutions works with the following block of code?

plus2(0, X, X).          % 0+X = X
plus2(s(X), Y, s(Z)) :-
    plus2(Y, X, Z).      % (X+1) + Y = Z+1  therefore  Y+X=Z

Answer 1

Here is better naming:

% Reduced to zero
peano_add(0, Sum, Sum).
peano_add(s(N), M, s(Sum)) :-
    % Decrement towards 0
    % Swap N & M, because N + M is M + N
    peano_add(M, N, Sum).

This is using Peano arithmetic, which represents natural numbers (i.e. integers starting from zero) in a relative way, as compound terms, as successors ultimately of 0. For example, s(s(0)) represents 2. Such relativity is convenient and elegant for Prolog, because it can be used ("reasoned with") in an uninstantiated (var) variable.

In swi-prolog, this produces:

?- peano_add(N, M, Sum).
N = 0,
M = Sum ;   % When N is zero, M is same as Sum - could be 0 or successor
N = Sum, Sum = s(_),
M = 0 ;     % When M is zero, N is same as Sum
N = s(0),
M = s(_A),
Sum = s(s(_A)) ;  % 1 + 1 = 2
N = s(s(_A)),
M = s(0),
Sum = s(s(s(_A))) ;  % 2 + 1 = 3
N = s(s(0)),
M = s(s(_A)),
Sum = s(s(s(s(_A)))) ;  % 2 + 2 = 4
N = s(s(s(_A))),
M = s(s(0)),
Sum = s(s(s(s(s(_A)))))  % 3 + 2 = 5  etc.

... and if we ask it how we can add two natural numbers to sum to 2:

?- peano_add(N, M, s(s(0))).
N = 0,
M = s(s(0)) ;      % 0 + 2
N = s(s(0)),
M = 0 ;            % 2 + 0
N = M, M = s(0) ;  % 1 + 1
false.

Whereas if we don't swap the arguments:

% Reduced to zero
peano_add(0, Sum, Sum).
peano_add(s(N), M, s(Sum)) :-
    % Decrement towards 0
    % Not swapping args, to demonstrate weakness
    peano_add(N, M, Sum).

... we get:

?- peano_add(N, M, Sum).
N = 0,
M = Sum ;
N = s(0),
Sum = s(M) ;
N = s(s(0)),
Sum = s(s(M)) ;
N = s(s(s(0))),
Sum = s(s(s(M))) ;
N = s(s(s(s(0)))),
Sum = s(s(s(s(M)))) ;

... which is still correct, but doesn't "involve" M as much as it could.

Both methods are counting from 0 upwards to infinity.

Swapping the parameters brings the advantage of checking the 2nd argument, to fail both fast and when appropriate:

?- peano_add(s(s(N)), z, Sum).
false.   % Correct, because z is not valid

% Versus, when unswapped, this undesirable:
?- peano_add(s(s(N)), z, Sum).
N = 0,
Sum = s(s(z)) ;  % Wrong - did not check whether z is valid
N = s(0),
Sum = s(s(s(z))) ;  % Still wrong
N = s(s(0)),
Sum = s(s(s(s(z)))) ;  % Will keep being wrong

Sadly, there is a common practice in Prolog example code of using meaningless variable names (such as A, B, X, Y), which adds confusion and should be generally avoided.

Addendum: Here is a version which has better determinism, when 2 of the 3 arguments are ground:

peano_add(P, Q, S) :-
    % For first-argument indexing
    (   ground(P)
    ->  peano_add_(P, Q, S)
    ;   peano_add_(Q, P, S)
    ).

peano_add_(0, S, S) :-
    peano(S).
peano_add_(s(P), Q, s(S)) :-
    peano_add_(P, Q, S).

peano(0).
peano(s(P)) :-
    peano(P).

peano_subtract(P, Q, S) :-
    % P - Q equals S means S + Q equals P
    peano_add(S, Q, P).

Answer 2

Composition of substitutions means that if under substitution θ1 we have

A = s(B) 

and under substitution θ2 we have

      B = s(C)

then under the composed substitution θ1 U θ2 we have

A = s(    s(C))

This can be seen e.g. in the call

%% the code, for reference:
plus2(0, X, X).
plus2(s(X), Y, s(Z)) :- plus2(Y, X, Z).

%% the call:
  plus2( s(1), 0, SUM )
 =plus2( s(X), Y, s(Z))     under θ1 = {1=X, 0=Y, SUM=s(Z)}
  :- plus2(  Y, X, Z)       under θ1
    =plus2(  0, 1, Z)
     :-plus2(0,X2,X2)       under θ2 = {1=X2, Z=X2}

Thus the composed substitution is

   θ = θ1 U θ2 = {1=X, 0=Y, SUM=s(Z), 1=X2, Z=X2}

and the original query holds under θ as

  plus2( s(1), 0, SUM  )    % under θ1, SUM=s(Z     )
 =plus2( s(1), 0, s(Z) )    % under θ2,       Z=X2
 =plus2( s(1), 0, s(X2))    % under θ2,         X2=1
 =plus2( s(1), 0, s(1) ).   % under θ,  SUM=s(     1)

Thus, as the proof progresses, the answer term SUM is progressively instantiated in the top-down manner.