recursion - Prolog：递归后继定义的自然数乘法谓词不终止

Question

我正在使用 prolog 中的自然数定义，它使用 s(0)、s(s(0))) 等等来定义自然数。有添加谓词：

add(0,N,N).
add(s(N),M,s(K)):-
    add(N,M,K).

现在最初 mult 是这样定义的：

mult(0,N,0).
mult(s(N),M,K):-
    mult(N,M,L),
    add(L,M,K).

但是我发现如果我使用变量查询，这会导致堆栈溢出，比如：

mult(A,s(s(0)),s(s(s(s(0))))

所以我添加了两个带有约束的附加子句，说明如果只有一个参数是变量，这意味着只存在一个解决方案，因此在这些情况下找到解决方案后程序不应回溯。这有效并停止了之前发生的堆栈溢出，子句如下所示：

mult(s(N),M,K):-
    (var(N),\+var(M),\+var(K)),
    mult(N,M,L),
    add(L,M,K),!.

mult(s(N),M,K):-
    (var(M),\+var(N),\+var(K)),
    mult(N,M,L),
    add(L,M,K),!.

我现在的问题是找出一种方法来解释以这种方式查询的情况，我希望程序找到一个数字的所有因素。如果我尝试查询

mult(A,B,s(s(s(s(0))))

我会得到因素，但程序会挂起，永远不会终止，然后导致堆栈溢出。我不太确定如何限制这种情况，并且在搜索树上设置手动绑定似乎既不是一个好主意，也不是解决此问题的正确方法。

标签： recursionprologsuccessor-arithmetics