prologfailure-sliceprolog-cut# Non-termination of common reverse/2 implementation, and better solutions?

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:**

- What is the choice point prolog is going back to?
- Is this called
**non-termination**? I am not familiar with prolog terminology. - 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? - 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?

Solution

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.

- 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. - Yes.
- 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] ;
...
```

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

- How to identify valid bodies and convertible terms
- Turbo Prolog: Create a palindrome by adding the smallest number of characters to the list
- Prolog order of clause body gives different results when using negation
- Problem With a Predicate to Check if X Occurs Exactly Four Times in a List
- Most General Unifier (Prolog)
- In prolog, functors vs predicates, and goals
- Solving N-queens with Constraint Handling Rules
- 'if' in prolog?
- Are there any Prolog compilers that can optimize by targeting specific queries?
- gprolog: Getting a stacktrace after an exception
- Efficient solution for the same-fringe problem for binary trees
- Understanding prolog \+ and the engine's solution space search
- Prolog, X element before element Y on list
- What is the difference between once and cut in prolog?
- Getting the seed set by the ECLiPSe on loading
- Get simple Prolog example to work
- How to do recursion in a L-system inspired rewrite System, without DCG
- Maximum number of atoms in SICStus Prolog 4
- How to create a list dynamically in Prolog?
- Prolog Syntax for Dependent Conditions
- Guard clauses in prolog?
- phrase_from_stream/2 nontermination (Stream from http_open/3)
- SWI-Prolog: [FATAL ERROR: Could not find system resources]
- DCG LaTeX printer for FOL prover
- Prolog: a person is a sibling of himself?
- When can I safely avoid storing temporary calculations in Prolog?
- Prolog - Solution of a riddle
- Is the structure of my Prolog expression isomorphic to the structure of the Liar Paradox?
- Syntax error: Operator expected in Prolog
- Assertion Failure in SWI-Prolog When Using pyswip to Consult a Prolog File