Prolog后继符号得到的结果不完整并导致无限循环。

Question

Prolog后继符号得到的结果不完整并导致无限循环。

prologinfinite-loopfailure-slicesuccessor-arithmeticsnon-termination

42

我开始学习Prolog，并了解了后继符号。

这就是我了解在Prolog中编写Peano公理的地方。

请参阅PDF第12页：

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

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

我把乘法规则放到Prolog中。然后我进行查询：

?- prod(X,Y,s(s(s(s(s(s(0))))))).

这意味着基本上要找到6的因数。

以下是结果。

X = s(0),
Y = s(s(s(s(s(s(0)))))) ? ;
X = s(s(0)),
Y = s(s(s(0))) ? ;
X = s(s(s(0))),
Y = s(s(0)) ? ;
infinite loop

此结果存在两个问题：

未显示所有结果，注意缺少结果X=6，Y=1。
它不会停止，除非我Ctrl+C然后选择中止。

所以... 我的问题是：

为什么会这样？我尝试交换“prod”和“sum”。得到的代码给我所有结果。再次问一句：为什么这样？它仍然处于死循环状态。
如何解决这个问题？

我阅读了关于无限循环的其他答案。但我希望有人能根据这种情况回答我的问题。这对我非常有帮助。

- Felastine

在比较标签维基之后，[tag:non-termination] 似乎更加合适。实际上，从标签维基来看，我们目前几乎所有使用 [tag:infinite-loop] 和 [tag:prolog] 的情况都应该被标记为 [tag:non-termination] 或者同时标记。什么是讨论这种标记最佳实践的最佳场所？个人而言，我更喜欢 [tag:non-termination]，至少要同时使用 [tag:infinite-loop]。 - mat

2个回答

17

第一个问题（为什么）相当容易发现，特别是如果您了解 left recursion。 sum(A,B,C) 在 C 被绑定时绑定 A 和 B，但原始程序 prod(A,B,C) 没有使用那些绑定，而是仍然未绑定 A、B 进行递归。

如果我们交换 sum 和 prod，我们将从 sum 中获得 2 个有用的绑定，以供递归调用使用：

sum(M, K, P)

现在M已经绑定，并将用于终止左递归。我们可以交换N和M，因为我们知道乘积是可交换的。

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

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

请注意，如果我们交换M和K（即求和K、M、P），当使用未知的P调用prod3时，我们会再次遇到一个无限循环，但是在求和中。

?- prod3(X,Y,s(s(s(s(s(s(0))))))).
X = s(s(s(s(s(s(0)))))),
Y = s(0) ;
X = s(s(s(0))),
Y = s(s(0)) ;
X = s(s(0)),
Y = s(s(s(0))) ;
X = s(0),
Y = s(s(s(s(s(s(0)))))) ;
false.

OT 我对cTI报告感到困惑：prod3(A,B,C)在满足b(A),b(B);b(A),b(C)条件下终止。

- CapelliC

关于cTI：系统告诉您有2 unresolved: [prod3(f,b,b),prod3(f,f,b)]。这意味着cTI无法推断这些情况，而NTI也无法证明非终止。因此，cTI不知道这些情况。请参见手册。 - false

你的程序的cTI报告是sum(A,B,C)terminates_if b(A);b(C).和prod3(A,B,C)terminates_if b(A),b(B);b(A),b(C).，这两个规则都明显是错误的。我期望的是sum(A,B,C)terminates_if b(A),b(B);b(C).和prod3(A,B,C)terminates_if b(A),b(B);b(C). - Géry Ogam

@Maggyero：这是一个误解。看一下sum(0, B,C)，你会发现它确实是有终止的。 - false

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- false · Accepted Answer

如果你想深入研究终止性质，使用successor-arithmetics的程序是一个理想的研究对象：你事先知道它们应该描述什么，因此可以集中精力处理更多的技术细节。你需要理解几个概念。

全局终止

最简单的方法是考虑Goal, false。当且仅当Goal普遍终止时，它才终止。也就是说：查看跟踪器是最无效的方式——它们只会向你展示单个执行路径。但你需要同时理解所有路径！而当你想要普遍终止时，永远不要查看答案，它们只会让你分心。如上所述：你得到了三个整洁而正确的答案，然后你的程序循环。因此最好用false“关闭”答案。这样可以消除所有干扰。

失败切片

你需要了解的下一个概念是失败切片。取一个纯单调逻辑程序并添加一些false目标。如果得到的失败切片不会（普遍地）终止，则原始程序也不会。在您的示例中，请考虑以下内容：这些false目标有助于消除程序中的不相关装饰：剩余部分清楚地显示了为什么prod(X，Y，s(s(s(s(s(s(0)))))))。不终止。它不终止，因为该片段根本不关心P！您希望第三个参数有助于使prod/3终止，但该片段向您展示这一切都是徒劳的，因为P在任何目标中都不出现。不需要啰嗦的跟踪器。

通常很难找到最小的故障片段。但一旦找到了，确定其终止或非终止属性就变得非常简单。经过一段时间后，您可以使用直觉来想象一个片段，然后使用理性来检查该片段是否相关。

关于故障片段的概念，最引人注目的是：如果您想改进程序，则必须修改上述片段中可见的部分！只要不更改它，问题就会持续存在。因此，故障片段是程序中非常重要的部分。

终止推断

那是你所需要的最后一件事情：一个终止推断器（或分析器），例如 cTI，将帮助您快速识别终止条件。查看 prod/3 和改进后的 prod2/3 的推断终止条件这里！

编辑：由于这是一个作业问题，我没有发布最终解决方案。但为了明确起见，以下是迄今为止获得的终止条件：

    如果 b(A)，b(B)，则 prod(A,B,C) 终止。
    如果 b(A)，b(B) 或者 b(A)，b(C)，则 prod2(A,B,C) 终止。

因此，新的 prod2/3 比原始程序严格更好！

现在，你需要找到最终程序。它的终止条件是：

   如果 b(A)，b(B) 或者 b(C)，则 prod3(A,B,C) 终止。

首先，试着找到 prod2(A,B,s(s(s(s(s(s(0))))))) 的失败切片！我们期望它会终止，但它仍然没有。所以把程序加上手动的 false 目标！剩下的部分将向你展示关键！

最后一个提示：你需要添加一个额外的目标和一个事实。

编辑：根据要求，这里是prod2(A,B,s(s(s(s(s(s(0)))))))的失败片段：

prod2(0,_,0) ：false。
prod2（s（N），M，P）：
   sum（M，K，P），
   prod2（N，M，K），false。
sum（0，M，M）。
sum（s（N），M，s（K））： false，
    sum（N，M，K）。

请注意sum/3的显着简化定义。它只说：0加上任何东西都是任何东西。没有更多了。因此，即使是更专业的prod2（A，0，s（s（s（s（s（s（0）））））））也会循环，而prod2（0，X，Y）则优雅地终止...