Non-termination of common reverse/2 implementation, and better solutions?

Question

The following is a standard textbook definition of reverse(X,Y) which is true if the list Y is the reverse of the list X. The code is often used to introduce or illustrate the use of an accumulator.

% recursive definition
step([], L2, L2).
step([H1|T1], X, L2) :- step(T1, X, [H1|L2]).

% convenience property around step/3
reverse(X, Y) :- step(X, Y, []).

The following query works as expcted.

?- reverse([1,2,3], Y).

Y = [3,2,1]

But the following fails after it prompts to search for more solutions after the first one.

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

X = [3,2,1]
Stack limit (0.2Gb) exceeded
Stack sizes: local: 3Kb, global: 0.2Gb, trail: 0Kb
Stack depth: 4,463,497, last-call: 100%, Choice points: 12 
...

Questions:

1. What is the choice point prolog is going back to?
2. Is this called non-termination? I am not familiar with prolog terminology.
3. Is there a better way to define reverse(X,Y) such that it is reversible, in the sense that both of the above queries work and terminate?
4. I have found that using a cut step([], L2, L2):- !. appears to work, but this seems like we've waded into procedural programming and have drifted far away from declarative logic programming. Is this a fair judgement?

Answer 1

Yes, you have correctly noted that this predicate does not terminate when you pass a variable in the first argument. It also does not terminate if the first argument is a partial list.

1. The first witness that you reported comes from the fact step([], L2, L2)., which is clearly the base case for your recursion/induction. When you ask the Prolog engine for additional witnesses, it proceeds by trying to do so using the induction rule step([H1|T1], X, L2) :- step(T1, X, [H1|L2]). Note that your implementation here is defined recursively on the first argument, and so this unifies the unbound first argument with [H1|T1], and then makes a recursive call with T1 as the first argument, which then unifies with a fresh [H1|T1], which makes a recursive call... This is the cause of the infinite loop you're observing.
2. Yes.
3. Often times with nontermination issues, it's helpful to understand Prolog's execution model. That doesn't necessarily mean we can't come up with a "pure logic" solution, though. In this case, the query doesn't terminate if the first argument is a partial list, so we simply need to ensure that the first argument has a fixed length. What should its length be? Well, since we're reversing a list it should be the same as the other list. Try out this definition instead:

reverse(X, Y) :- same_length(X, Y), step(X, Y, []).

This solves the problem for both of the queries you posed. As an added bonus, it's actually possible to pose the "most general query" and get a sensible infinite sequence of results with this definition:

?- reverse(X, Y).
X = Y, Y = [] ;
X = Y, Y = [_] ;
X = [_A, _B],
Y = [_B, _A] ;
X = [_A, _B, _C],
Y = [_C, _B, _A] ;
X = [_A, _B, _C, _D],
Y = [_D, _C, _B, _A] ;
...

4. As far as I know, there isn't really a clear way to describe Prolog's cut operator in the language of first order logic. All of the literature I've read on the topic describe it operationally within the context of Prolog's execution model — by this I mean that its semantics are defined in terms of choice points/backtracking rather than propositions and logical connectives. That being said, it's hard to write Prolog code that is fast or has good termination properties without being aware of the execution model, and "practical" Prolog programs often use it for this reason (look up "Prolog red and green cuts"). I think your judgement that the cut is "procedural" is on the right track, but personally I think it's still a valuable tool when used appropriately.