终止条件序言

Question

我的老师为我们提供了一些关于 Prolog 的幻灯片，我发现有些奇怪。

reverse([],[]).
reverse([X|Xs],Zs) :- reverse(Xs,Ys), append(Ys, [X], Zs).

据他说，当第一个参数reverse([],..) 是一个完整列表时，程序就会终止。 此外，如果您将谓词中的目标切换为reverse([X|Xs],Zs) :- append(Ys, [X], Zs), reverse(Xs,Ys).，则程序应在第二个参数是完整列表时终止reverse(..,[]).

这与我目前所学的有点背道而驰。我认为这两个论点都影响了程序的终止条件，显然他们没有按照我老师的例子。 谁能给我一些意见？

Answer 1

由于 Prolog 的控制流程相对复杂，Prolog 程序的终止属性有点难以掌握。有一些方法可以降低复杂性。一是通过在您的计划中插入额外的目标false，只考虑您计划的部分内容。你可以把它们放在任何地方。并且无论您将它们放在哪里，以下内容都成立：如果这个名为 failure-slice 的新程序没有终止，那么您的原始程序也不会终止。注意“如果”。这是你的程序：

reverse([],[]) :- false。 反向（[X|Xs]，Zs）：- 反向（Xs，Ys），假， 追加（Ys，[X]，Zs）。

这个故障片对于理解你的关系所描述的是完全没有用的。它永远不会成功。但是，它可以帮助我们更好地了解如何终止。

请注意，该事实已完全消除。事实上，无论事实如何，它都不能改善reverse/2 的这个故障片的终止。 （不过，它可能会恶化终止）。

还请注意第二个参数Zs：没有进一步提及此Zs。因此：reverse/2 的第二个参数可以是它想要的任何值。它也不会改善终止。

要使reverse/2 终止，必须实例化第一个参数，以使该片段终止。因此[]、[X|[]] 将终止，甚至[X|nonlist] 也会终止。但部分列表如Xs、[a|Xs]等不会终止。

如果您想改进 reverse(Xs,[]) 的终止，您需要更改可见的剩余部分中的某些内容。一种方法是交换目标。现在，Zs 可能会导致终止。但是——唉——第一个论点现在不再像以前那样有影响力了。考虑reverse([a], Zs) 和：

reverse([],[]) :- false。 反向（[X|Xs]，Zs）：- 附加（Ys，[X]，Zs），假， 反向（Xs，Ys）。 append([], Zs, Zs) :- false。 附加（[X|Xs]，Ys，[X|Zs]）：- 追加（Xs，Ys，Zs），假。

所以虽然这个片段仍然坚持第一个参数是[_|_]，但它没有考虑剩余的术语。因此，目标不会终止。

如果您想了解更多信息，请查看failure-slice。同样，考虑using cTI。要培养良好的直觉，您需要亲自尝试。