Prolog - 具有非常基本规则定义的无限循环

Prolog - Infinite loop with very basic rule definition

我正在尝试练习 Prolog,按照我的助教的建议,我正在尝试创建规则 append3(A,B,C,D),这意味着 D 是 A、B 和 C 的附加结果。

给出append(A,B,C)的定义

append([],B,B).
append([X|A],B,[X|C]):-append(A,B,C).

所以我简单地写了以下,这对我来说很有意义,作为 append3

的规则
append3(A,B,C,D) :- append(A,B,X),append(X,C,D).

之后,我尝试了一些查询,例如append3(A,B,C,[1,2,3])。一开始一切都很好,它给了我正确的结果。然而,有一次我按下;,它进入了一个无限循环试图搜索另一个答案。

我不太确定为什么会这样?我想 append3(A,B,C,D) 是一个非常基本的定义规则。有什么我遗漏或没有考虑到的吗?

我该如何解决这个问题?

你需要翻转谓词append(A, B, X), append(X, C, D)。由于所有三个变量 ABXappend(A, B, X) 中都是未绑定的,序言试图满足它,然后用 append(X, C, D) 约束它,这将在为您提供现有的解决方案。于是进入死循环。

尝试只执行 append(A, B, X). 所有这些都未绑定。 Prolog 应该向您展示无限的解决方案序列,这些解决方案在下一个子句 append(X, C, D).

中失败

翻转谓词,你应该没问题。

append3(A, B, C, D) :-
    append(T, C, D),
    append(A, B, T).

与面向命令的编程语言相比,Prolog 的执行机制相当复杂 a.k.a。命令式语言(简称:imps)。你的助教给了你一个很好的例子,你可以在其中提高你对 Prolog 的掌握程度。

首先,你需要了解append/3的终止行为。最好的方法是通过 ,它可以帮助您专注于与终止 相关的 部分。在这种情况下是:

append([],B,B) :- false.
append([X|A],B,[X|C]):-append(A,B,C), false.

此片段或故障切片现在在您的原始定义终止的所有情况下都准确终止!而且由于它更短,因此更容易理解终止。当然,这个新程序将不再为 append([a],[b],[a,b]) 寻找答案——它会失败。但仅就终止而言,它是完美的。

现在让我们一一分析:

  1. argument 需要有一个非空列表元素,并且如果参数是 [] 或任何其他术语,将会失败(并终止)。非终止可能只发生在部分列表中(这是一个带有变量而不是末尾 [] 的列表,如 [a,b|L])或只是一个变量。

  2. 参数就是变量B。这个 B 不可能与任何术语有何不同。因此,B 对终止完全没有影响。 终止中立

  3. 参数与第一个参数基本相同。事实上,这些论点看起来很对称,尽管它们描述的是不同的东西。

总而言之,如果第一个或最后一个参数是(完全实例化的)列表,append/3 将终止。

注意,我刚才说的是if,不是iff。毕竟,第一个和第三个参数通过变量 X 相互关联。对于此分析,让我们忽略它。

现在,你的定义失败了。

append3(A,B,C,D) :- append(A,B,X), false, append(X,C,D).

请注意,可见部分不再出现D!因此,第四个参数对这个片段的终止没有影响。由于 X 是第一次出现,因此只有 A 对其终止有影响。因此,如果 A 只是一个变量(或部分列表),程序将不会终止!无需再看。不用再看满屏痕迹

要为像您的查询 append3(A,B,C,[1,2,3]). 这样的查询修复此问题,D 必须对第一个目标有所影响。

另一个答案建议的一个可能的解决方法是交换目标:

append3(A,B,C,D) :- append(X,C,D), false, append(A,B,X).

我们来看看append(X,C,D)的变量! C 是终止中立的,X 是第一次出现,因此对终止完全没有影响。只有 D 可以使这个目标终止。因此像 append3([1],[2],[3], D) 这样的查询现在会循环!以一种情况下的不终止换取另一种情况,真是划算!

要使您的程序适用于 两种 情况,append/3 的第一个目标必须同时包含 DA 中的至少一个]、BC。尝试自己找到它!这里是剧透:

append3(A, B, C, D) :- append(A, BC, D), append(B, C, BC).

现在,如果 AD 是一个(完全实例化的)列表,则第一个目标终止。第二个目标要求 BBC 成为列表。 BC 来自第一个目标,如果 D 是一个,那么它是一个列表。

因此append3(A, B, C, D) terminates_if b(A), b(B) ; (D).

请参阅 another answer 了解有关终止、故障切片和我在此未提及的技术的更多信息,即 终止推理


并且,请注意,还有更多定义终止的情况,尽管它们相当模糊,如 append([a|_],_,[b|_])append3([a|_],_,_,[b|_])) 都失败(并因此终止),尽管他们只有部分清单。因此它是 terminates_if 而不是 terminates_iff.