prolog - 终止条件序言

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不终止，那么您的原始程序也不会终止。注意“如果”。这是你的程序:

反向([]，[]): - 假。
反向([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)和:

反向([]，[]): - 假。
反向([X|Xs],Zs) :-
追加(Ys，[X]，Zs)，假，
反向(Xs，Ys)。

append([], Zs, Zs) :- 假。
追加([X|Xs], Ys, [X|Zs]) :-
追加(Xs，Ys，Zs)，假。

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

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