如何修复此列表反转？

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

问题：

1. 如何修复这两个程序？
2. 两个程序是否等效？

Answer 1

在这两个程序中，第三个参数对（通用）终止没有影响，如以下故障切片所示：

rev([], []) :- false。 转（[XH|XT]，Y）：- 转（XT，Z），假， 追加（Z，[XH]，Y）。

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

转（X，Y）：- 重新附加（X，[]，Y），假。 revappend([], Y, Y) :- false。 重新附加（[XH|XT]，Y，Z）：- 重新附加（XT，[XH|Y]，Z），假。

同样，revappend/3 中的第三个参数只是被移交，没有任何可能导致失败并因此终止。

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

转（X，Y）：- 重新附加（X，[]，Y，Y）。 重新附加（[]，Y，Y，[]）。 重新附加（[XH|XT]，Y，Z，[_|Ylen]）：- 重新附加（XT，[XH|Y]，Z，Ylen）。

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

转（X，Y）：- 重新附加（X，_，_，Y）。 重新附加（[]，_，_，[]）。 重新附加（[_|XT]，_，_，[_|Ylen]）：- 重新附加（XT，_，_，Ylen）。

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