(Click on the :- button in the doc)
reverse(Xs, Ys) :- reverse(Xs, , Ys, Ys). reverse(, Ys, Ys, ). reverse([X|Xs], Rs, Ys, [_|Bound]) :- reverse(Xs, [X|Rs], Ys, Bound).
It is tail-recursive, thus can be optimized into a loop by the compiler. Instead of keeping the elements on a stack with the depth of the list, to be collected and prepended to result list when coming back from the recursion, it constructs the result as a structure on the heap:
[X|Rs] to be unified with the result variable Ys in the base case.
The Bound is there to make the call symmetric, and make sure the call fails early when both lists are of unequal length or makes sure the list are of equal length when there is one open list among the arguments. But I can't get my head around all of the special cases covered by it. Alien technology!
... so that your list comes out right without you having to invoke reverse/2 after processing.
Note that reverse/2 works for "open lists", i.e. lists for which the backbone ends in an empty cell.
Evidently a successful reverse/2 will not leave an open list behind. You just get longer and longer list on backtracking:
?- reverse([1,2,3|X],B). X = , B = [3, 2, 1] ; X = [_3934], B = [_3934, 3, 2, 1] ; X = [_3946, _3934], B = [_3934, _3946, 3, 2, 1] ; X = [_3958, _3946, _3934], B = [_3934, _3946, _3958, 3, 2, 1] . ?- reverse(F,[1,2,3|X]). F = [3, 2, 1], X =  ; F = [_9572, 3, 2, 1], X = [_9572] ; F = [_9572, _9584, 3, 2, 1], X = [_9584, _9572] ; F = [_9572, _9584, _9596, 3, 2, 1], X = [_9596, _9584, _9572] ; ?- reverse(F,B). F = B, B =  ; F = B, B = [_17142] ; F = [_17142, _17148], B = [_17148, _17142] ; F = [_17142, _18018, _17148], B = [_17148, _18018, _17142]
Reverse can ruin your day
By infinite loop on a cyclic structure:
?- reverse([1,2,3|X],X). ERROR: Stack limit (1.0Gb) exceeded
This predicate could perform length determination/verification at the same time:
reversel(Xs, Ys, L) :- reversel(Xs, , Ys, Ys, 0, L). reversel(, Ys, Ys, , L, L). reversel([X|Xs], Rs, Ys, [_|Bound], Lc, Lf) :- succ(Lc,Ln), (nonvar(Lf) -> Ln=<Lf ; true), reversel(Xs, [X|Rs], Ys, Bound, Ln, Lf).
?- Len=10000000,numlist(1,Len,L1),time(reversel(L1,L2,Length)). % 20,000,002 inferences, 4.820 CPU in 4.841 seconds (100% CPU, 4149503 Lips) ?- Len=10000000,numlist(1,Len,L1),time((reverse(L1,L2),length(L1,Length))). % 10,000,004 inferences, 3.530 CPU in 3.549 seconds (99% CPU, 2832708 Lips)