0

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
false
  • 10,264
  • 13
  • 101
  • 209
Carpediem
  • 31
  • 4
  • Sorry, it was supposed to be plus2 just updated the code, and I don't think swapping X and Y changes the logic here. – Carpediem Dec 26 '22 at 19:24
  • "*I don't think swapping X and Y changes the logic here.*" - It doesn't change the logic for the computer, it changes the difficulty of explaining it for the human. In your code X+1=Z and the next step is 0+X=X, and X=1, X=0, X=1 (again), X=Y and X=Z, but they're different Xs in different parts of the call stack. If you're struggling to understand it, that isn't gonna help. Name the first line `plus2(0, YZ, YZ).` to show that the recursion stops when you've taken enough units from Z that it's down to being the same value as Y, for example. – TessellatingHeckler Dec 27 '22 at 11:21
  • @TessellatingHeckler, I can see it, but the logic here is adapted from the workbook!. – Carpediem Dec 28 '22 at 10:19
  • Swapping the two numbers being summed is advantageous - see my answer. – brebs Dec 28 '22 at 11:31
  • `(X+1) + Y = Z+1 therefore Y+X=Z` when reading `=` as "must be equal". But if we read `=` is "equals" (which is more usually done) then "therefore" becomes "if". (i.e. the direction changes to the opposite!) – Will Ness Jul 23 '23 at 10:13

2 Answers2

2

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 1st-argument indexing
    (   ground(P)
    ->  peano_add_(P, Q, S)
    ;   peano_add_(Q, P, S)
    ).

peano_add_(0, S, S) :-
    (   S == 0
    % 1st arg can only be 0
    ->  !
    ;   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 is S means S + Q is P
    peano_add(S, Q, P).
brebs
  • 3,462
  • 2
  • 3
  • 12
0

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.

Will Ness
  • 70,110
  • 9
  • 98
  • 181