如何修复此列表反转？

Question

以下 Prolog 程序定义了一个谓词 rev/2 用于反转第一个参数中传递的列表，结果是第二个参数中传递的列表：

rev([], []).
rev([XH|XT], Y) :-
  rev(XT, Z),
  append(Z, [XH], Y).

append([], Y, Y).
append([XH|XT], Y, [XH|ZT]) :-
  append(XT, Y, ZT).

以下 Prolog 程序是 rev/2 的替代实现：

rev(X, Y) :-
  revappend(X, [], Y).

revappend([], Y, Y).
revappend([XH|XT], Y, Z) :-
  revappend(XT, [XH|Y], Z).

对于此参数模式下的查询，这两个程序都按预期工作：

?- rev([a, b, c], Y).
   Y = [c, b, a]
;  false.

但是在这种参数模式下，两个程序都耗尽了查询资源：

?- rev(X, [a, b, c]).
   X = [c, b, a]
;
Time limit exceeded

问题：

Answer 1

在这两个程序中，第三个参数对（通用）终止没有影响，从以下失败切片可以看出：

rev([], []) :- false.
rev([XH|XT], Y) :-
  rev(XT, Z), false,
  append(Z, [XH], Y).

Y可以随便，永远不会导致这个片段失败。因此它对终止没有影响。 终止中立。

rev(X, Y) :-
  revappend(X, [], Y), false.

revappend([], Y, Y) :- false.
revappend([XH|XT], Y, Z) :-
  revappend(XT, [XH|Y], Z), false.

同理，revappend/3中的第三个参数也是刚刚交出，没有任何失败导致终止的可能。

为了解决这个问题，必须添加一些东西来专门化剩余的可见部分。一个观察是第一个和最后一个参数的列表长度是相同的。因此添加额外的第四个参数以确保两个参数的长度相同将有助于获得 optimal 终止条件：

rev(X, Y) :-
  revappend(X, [], Y, Y).

revappend([], Y, Y, []).
revappend([XH|XT], Y, Z, [_|Ylen]) :-
  revappend(XT, [XH|Y], Z, Ylen).

下面是这个程序的概括，以更好地理解参数如何影响终止：

rev(X, Y) :-
  revappend(X, _, _, Y).

revappend([], _, _, []).
revappend([_|XT], _, _, [_|Ylen]) :-
  revappend(XT, _, _, Ylen).

所以第二个和第三个参数只是被_替换了。这个概括现在正好是 same_length/2.

How to fix this list reversal?