如何修复此递归乘法？

Question

我是逻辑编程和 Prolog 的新手。下面的 Prolog 程序定义了一个谓词 mul/3，用于将第一个参数乘以第二个参数，结果是第三个参数，基于等式 x * y = z 相当于 (x − 1) * y + y = z:

mul(0, _, 0).
mul(X, Y, Z) :-
  ground(X),
  succ(U, X),
  add(V, Y, Z),
  mul(U, Y, V).
mul(X, Y, Z) :-
  var(X),
  add(V, Y, Z),
  mul(U, Y, V),
  succ(U, X).

add(0, Y, Y).
add(X, Y, Z) :-
  ground(X),
  ground(Z),
  succ(U, X),
  succ(V, Z),
  add(U, Y, V).
add(X, Y, Z) :-
  ground(X),
  var(Z),
  succ(U, X),
  add(U, Y, V),
  succ(V, Z).
add(X, Y, Z) :-
  ground(Z),
  var(X),
  succ(V, Z),
  add(U, Y, V),
  succ(U, X).

但是在这种参数模式下查询会耗尽资源:

?- mul(X, Y, 2).
   X = 1, Y = 2
;  X = 2, Y = 1
;
Stack limit (0.2Gb) exceeded
  Stack sizes: local: 0.2Gb, global: 20.8Mb, trail: 10.4Mb
  Stack depth: 452,739, last-call: 0%, Choice points: 452,716
  In:
    [452,739] add(_1326, 0, 0)
    [452,738] add(_1354, 0, 1)
    [452,737] add(_1382, 0, 2)
    [452,736] mul(_1410, 0, 2)
    [452,735] mul(_1438, 0, 2)

如何解决这个递归乘法问题？

Answer 1

该程序在给出两个解决方案 X = 1, Y = 2 和 X = 2, Y = 1 的意义上运行良好。然后它会无限搜索其他解决方案。

这条规则有问题：

mul(X, Y, Z) :-
  var(X),
  add(V, Y, Z),
  mul(U, Y, V),
  succ(U, X).

这里 mul(U, Y, V) 以第一个参数不为基础的方式递归，但之前的规则假设它是（当 V 不为零时）。只需交换前两个参数即可解决问题。

虽然还不够完美，可以考虑

?- mul(2, 3, X).
   false.

这里的问题出在之前的规则中：

mul(X, Y, Z) :-
  ground(X),
  succ(U, X),
  add(V, Y, Z),
  mul(U, Y, V).

对add(V, Y, Z)的调用变为add(V, 3, Z)，这是未定义的。将其与下一个 mul 交换可解决此问题：

mul(X, Y, Z) :-
  ground(X),
  succ(U, X),
  mul(U, Y, V),
  add(V, Y, Z).

所以现在还好吗？不是真的，例如

?- mul(X, 3, 6).
   false.

尝试通过

?- trace, mul(X,3,6).

找出问题所在

--- 编辑 ---

好的，让我们从头开始尝试。

为了简单起见，先看前两个参数不是变量的情况：

% add1(+X, +Y, ?Z) [semidet]
add1(0, Y, Y) :-
  !.
add1(X, Y, Z) :-
  succ(X1, X),
  add1(X1, Y, Z1),
  succ(Z1, Z).

% mul1(+X, +Y, ?Z) [semidet]
mul1(0, _, 0) :-
  !.
mul1(X, Y, Z) :-
  succ(X1, X),
  mul1(X1, Y, Z1),
  add1(Z1, Y, Z).

然后另一种情况，当sum/product已知时：

% add2(?X, ?Y, +Z) [nondet]
add2(0, Y, Y).
add2(X, Y, Z) :-
  succ(Z1, Z),
  add2(X1, Y, Z1),
  succ(X1, X).

% mul2(?X, ?Y, +Z) [nondet]
mul2(X, Y, 0) :-
  !,
  (X = 0; Y = 0).
mul2(X, Y, Z) :-
  nonvar(Y),
  !,
  succ(Y1, Y),
  add2(Z1, X, Z),
  mul2(X, Y1, Z1).
mul2(X, Y, Z) :-
  add2(Z1, Y, Z),
  mul2(X1, Y, Z1),
  succ(X1, X).

注意当mul2中的第三条规则递归时，它的第二个参数将是已知的，并且被第二条规则使用。这与您最初写的非常相似。

最后，您可以创建一个规则来选择您需要的：

add(X, Y, Z) :-
  nonvar(Z) -> add2(X, Y, Z); add1(X, Y, Z).

mul(X, Y, Z) :-
  nonvar(Z) -> mul2(X, Y, Z); mul1(X, Y, Z).

（当然你也可以用var(X)等方式统一这些规则，但我觉得这样更清晰。）

如何修复此递归乘法？

How to fix this recursive multiplication?

recursion

termination

prolog

multiplication

failure-slice