prolog - Power with successor arithmetic - 如何防止无限循环？ [序言]

Question

我一整天都在想这个问题。我终于承认，我对 Prolog 的理解并没有我想象的那么好。

今天开始的时候，我在实现后继算术时遇到了麻烦，它乘以 2 个 s-Numbers，结构是这样的:

nat(0).
nat(s(X)):-nat(X).

我的第一次尝试是这样的:

 mul(0,_,0).
 mul(s(F1),F2,P):-mul(F1,F2,Tmp),add(F2,Tmp,P)

有效，但查询 mul(X,Y,s(0)) 以无限循环结束。为什么？我已阅读以下帖子:Prolog successor notation yields incomplete result and infinite loop

我从中了解到:如果我在调用 add 之前调用 mul，并且我在 mul/3 谓词中有变量，但在两个 mul/3 调用中都没有使用，Prolog 会尝试为它所做的变量找到新的可能性不绑定(bind)。因此它进入了无限循环。

为了解决这个问题，我先调用了add:

mul(0,_,0).
mul(s(F1),F2,P):-add(F2,Tmp,P),mul(F2,F1,Tmp).

做到了。然后我尝试实现 power 函数，并认为“好吧，这很容易，首先尝试是:

pow(_,0,s(0)).
pow(B,s(E),R):-pow(B,E,Tmp), mul(Tmp,B,R).

但是，我必须把 mul 放在前面，以防止 R 和 Tmp 的左递归。

简单!”男孩，我错了。我不知道如何在不进入无限循环的情况下实现它，即使我把 mul 放在前面也是如此。

非常感谢任何建议。你可以节省我周六的工作精力并提高我的自尊心!提前谢谢你。

编辑:添加了我缺少的求和谓词:

add(0, Y, Y).
add(s(S1), S2, s(Sum)):-  add(S1,S2,Sum).

Answer 1

我们希望满足以下终止条件:

pow(B, E, P) terminates_if b(B), b(E).
pow(B, E, P) terminates_if b(P).

或短暂

pow(B, E, P) terminates_if b(B), b(E) ; b(P).

我们不能要求更多。不止于此将是 b(B)单独或b(E)独自的。但在那些情况下，我们需要无限多个暗示不终止的答案。当然，我们可以采用一个总是终止的定义，并且它对所有测试用例都成功，比如

pow(_B, _E, _P).

唉，这个定义也适用于我们不想要的任何其他情况。因此，除非您只接受成功测试，否则您必须采用更详细的定义。

另一种避免不终止的方法是求助于自然数的另一种定义。使用 library(clpz) (SWI 的 library(clpfd) 是一个较弱的前体)

pow(B, E, P) :-
   B #>= 0,
   E #>= 0,
   P #= B^E.

但目前，我们坚持使用后继算术。 CapelliC 已经给了你一个终止于 b(B), b(E) 的定义。 .因此，让我们尝试改进它!一种方法是以某种方式使用 P将推理的数量限制为有限数量。一种方法是考虑参数之间的关系。

pow/3 的参数之间有什么有趣的关系吗？ ？我真的很想这样:

b^e ≥ e, b^e ≥ b for e, b ≥ 0

这几乎是真的。它实际上通过添加 b ≥ 2 成立。

只是为了确保我会检查我没有完全错，我会试试这个¹:

?- M #= 10^150, [B,E,P]ins 0..M, P #= B^E, B #>= 2, P #< E.
false.

我会认为这是一个证明，尽管它不是一个证明。

现在是定义。这个想法是通过添加额外的参数来限制递归的次数来处理一般情况。一极限LP对于 pow和一个限制 LM对于 mult .这些参数由额外的空格分隔，以明确它们的添加位置。

pow(_, 0, s(0)).
pow(0, s(_), 0).
pow(s(B), s(0), s(B)).
pow(s(0), s(s(_)), s(0)).
pow(B, E, P) :-
   B = s(s(_)), E = s(s(_)), P = s(s(s(s(_)))), 
   powx(B, E, P,     P, P).
%                    ^^^^^ added arguments to limit pow and mult

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

mul(0,_,0,_).
mul(s(F1),F2,P,    s(LM)) :-
   mul(F1,F2,Tmp,    LM),
   sum(Tmp, F2, P).   % note: arguments exchanged!

powx(_,0,s(0),    _, _).
powx(B,s(E),R,    s(LP), LM) :-
   powx(B,E,Tmp,     LP, LM),
   mul(Tmp,B,R,      LM).

对于简单的案例 pow(b,b,f)开销应该是最小的。对于新案例，pow(f,f,b)以某种方式降低限制可能会减少开销。

---

<支持>脚注

1 我只尝试了 10¹⁵⁰。没有一般的证明。让我们希望一切都好。出于某种原因，较大的值会产生 stackoverflow™。这是最后一个目标P #< E这会导致大量的重新计算。否则它最多工作 10¹⁰⁷。