How to fix this list reversal?

Question

The following Prolog program defines a predicate rev/2 for reversing a list passed in first argument which results in the list passed in second argument:

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).

The following Prolog program is an alternative implementation of rev/2:

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

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

Both programs work as expected for queries in this argument mode:

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

But both programs exhaust resources for queries in this argument mode:

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

Questions:

1. How to fix both programs?
2. Are both programs equivalent?

Answer 1

In both programs, the third argument has no influence on (universal) termination, as can be seen by the following failure slices:

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

Y can be whatever it wants, it will never cause failure in this fragment. Thus it has no influence on termination. It is termination neutral.

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

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

Similarly, the third argument in revappend/3 is just handed over without any chance of causing failure and thus termination.

In order to fix the problem something has to be added to specialize the remaining visible part. One observation is that the list length of both the first and the last argument is the same. And thus adding an extra fourth argument for ensuring that both arguments are of same length will help to get the optimal termination condition:

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

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

And here is a generalization of this program to better understand how termination is influenced by the arguments:

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

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

So the 2nd and 3rd argument is just replaced by _. This generalization is now exactly same_length/2.