序言中一元加法的替换组成？

Question

有人可以解释替换组合的逻辑如何与以下代码块一起工作吗？

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

这是更好的命名：

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

这是使用皮亚诺算术，它以相对的方式表示自然数（即从零开始的整数），作为复合项，作为0的最终后继。例如，

s(s(0))

代表2。这种相对性既方便又优雅对于 Prolog，因为它可以在未实例化的 (var) 变量中使用（“推理”）。

在 swi-prolog 中，这会产生：

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

...如果我们问它如何将两个自然数相加总和为 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.

如果我们不交换参数：

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

...我们得到：

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

...这仍然是正确的，但并没有尽可能地“涉及”

M

。

两种方法都是从 0 向上计数到无穷大。

交换参数带来了检查第二个参数的优点，可以在fast和适当的时候失败：

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

遗憾的是，Prolog 示例代码中有一种常见做法，即使用无意义的变量名称（例如 A、B、X、Y），这会增加混乱，通常应该避免。

附录： 这是一个具有更好确定性的版本，当 3 个参数中的 2 个为基础时：

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

替换的组成意味着如果在替换下

θ1

我们有

A = s(B) 

并且在替换下

θ2

我们有

      B = s(C)

然后在组合替换下

θ1 U θ2

我们有

A = s(    s(C))

这可以看出，例如在通话中

%% 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}

因此组合替换是

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

原始查询保存在

θ

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)

因此，随着证明的进展，答案项

SUM

以自上而下的方式逐步实例化。