为什么我的列表反转只能在一个方向上正常工作？

Question

我已经生成了以下代码。

list_reverse([],[]). 
list_reverse([X],[X]).
list_reverse(Ls,[R|Rs]) :-
    last_elem(Ls,R),
    without_last_elem(Ls,Next),
    list_reverse(Next,Rs).

last_elem([E],E).
last_elem([_|Xs],E) :-
    last_elem(Xs,E).

without_last_elem([X,_|[]],[X|[]]).
without_last_elem([X|T0],[X|T1]) :-
    without_last_elem(T0,T1).

旋转：

?- list_reverse([1,2,3],X).
X = [3, 2, 1] ;
false.

这正是我想要的。

然而，如果我朝相反的方向前进，我会成功，然后是非终止。

?- list_reverse(X,[1,2,3]).
X = [3, 2, 1] ;
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted

我很难理解的是为什么我首先得到了 X 的正确解决方案。我的程序是否正确？

我并不担心颠倒列表，而是担心这种先获得正确解决方案后不终止的模式。这种模式我已经遇到过几次了。

Answer 1

last_elem/2可以继续构建更大的列表，应该全部拒绝。但是你因此陷入了无限循环。

我们可以创建一个与累加器一起工作的函数，并同时迭代 both 这两个列表。这意味着一旦左侧或右侧列表用完，将不再进行递归调用：

reverse(L1, L2) :-
    reverse(L1, [], L2, L2).

reverse([], L, L, []).
reverse(<b>[H|T]</b>, L1, R, <b>[_|T2]</b>) :-
    reverse(T, [H|L1], R, T2).

这里 [H|T] 和 [_|T2] 模式因此都弹出列表的第一项，我们只在两个列表都用完时才匹配。

Answer 2

I am [worried] about this pattern of getting a correct solution followed by non-termination.

这是由于 Prolog 中非常具体的（通用）终止概念。在其他编程语言中，终止是一个简单得多的野兽（尽管如此仍然是一个不可判定的野兽）。如果，比方说，一个函数 returns 那么它终止（对于这种情况）。但在 Prolog 中，产生一个答案并不是终点，因为可能还有更多的解决方案或只是一个无效的循环。事实上，最好不要考虑您的查询 ?- list_reverse(X,[1,2,3]).，而是考虑以下查询。

?- list_reverse(X,[1,2,3]), false.

以这种方式，所有分散注意力的答案都被关闭了。此查询的唯一目的现在是显示终止或 non-termination.

之后，您可以尝试遵循 Prolog 的精确执行路径，但这就像您迷路时盯着汽车变速箱一样有见地（齿轮导致您移动到您迷路的地方，因此它们是某种原因......）。或者，您退后一步，考虑与您的原始程序共享某些属性的相关程序片段（称为切片）。对于终止，failure-slice 可以帮助您更好地理解什么是利害攸关的。在你的情况下考虑：

list_reverse([],[]) :- false. 
list_reverse([X],[X]) :- false.
list_reverse(Ls,[R|Rs]) :-
    last_elem(Ls,R), false,
    without_last_elem(Ls,Next),
    list_reverse(Next,Rs).

last_elem([E],E) :- false.
last_elem([_|Xs],E) :-
    last_elem(Xs,E), false.

?- list_reverse(X,[1,2,3]), false.

由于这个故障片没有终止，所以你原来的程序也没有终止！而且，在这个较小的片段中推理起来要容易得多。如果你想修复这个问题，你需要在可见部分修改一些东西。否则你会一直陷入循环。

请注意，none 的事实是循环的一部分。因此它们与 non-termination.

无关

另请注意，在 list_reverse/2 中，可见部分从未使用变量 Rs。因此 Rs 对终止没有影响！请注意，这已经是属性的证明。这是否意味着 list_reverse/2 的第二个参数对终止没有影响？你怎么看？

为什么我的列表反转只能在一个方向上正常工作？

Why does my list reversal only work correctly in one direction?

prolog

failure-slice