2

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?
Géry Ogam
  • 6,336
  • 4
  • 38
  • 67

1 Answers1

3

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.

false
  • 10,264
  • 13
  • 101
  • 209
  • Thanks for the analysis and solution, it works like a charm! ‘And thus adding a fourth argument for ensuring that the first and third arguments are of same length’ Isn’t it already guaranteed without this fourth argument? I cannot find a goal `revappend` returning yes where the first and third arguments are of different lengths. – Géry Ogam Aug 04 '21 at 16:06
  • I looked at the trace (`trace, rev(X, [a, b, c]).`) and now I understand your length argument. With or without, the recursive calls end up with the current pattern `revappend(_, [_, _, _], [a, b, c])` matching with the ground clause `revappend([], Y, Y, []).`, yielding `[c, b, a]` as the first result. Then the interpreter resumes its search, and without your length argument the same pattern matches with the general clause `revappend([XH|XT], Y, Z)` and therefore calls `revappend(XT, [XH|Y], Z)`, updating the current pattern to `revappend(_, [_, _, _, _], [a, b, c])` (`Y` has 4 items > 3), etc. – Géry Ogam Aug 04 '21 at 18:52
  • @Maggyero: It is significantly simpler to look at the source code and just spot some parts than to watch traces. There are [many alternatives](/a/30791637/772868) to it. By the same token, I never inspect a car's engine when I get lost. Instead I use maps and the like, although I know that the engine somewhat was the cause that I got to the place where I was lost... – false Aug 05 '21 at 10:25
  • This might look trivial to you, but I think I needed more experience to be able to just look at the code and immediately understand your solution. Without the trace or writing down every step on a sheet of paper, I think I would have never understood. Seing the pattern matching in action really helped me. Thanks again for this great answer, I really appreciate. – Géry Ogam Aug 05 '21 at 14:45
  • @Maggyero: That's why failure slices are so useful: You remove some part, and if the remaining part in itself is already the cause for non-termination, it is pointless to look any further. Most will however be tempted to look at each and every line a tracer produces, thereby exhausting their attention span with irrelevant detail. Finding the slice itself is often an intuitive, irrational process, but then it is easy to check since it is smaller. Ah, and one further point: This only works for pure programs! – false Aug 05 '21 at 14:59
  • What do you mean by ‘pure’ programs? – Géry Ogam Aug 05 '21 at 15:08
  • @Maggyero: See [this](/q/27306453/772868) or [that](https://stackoverflow.com/tags/logical-purity/info). – false Aug 05 '21 at 15:13
  • By the way, replacing the clause `revappend([], Y, Y).` with `revappend([], Y, Y) :- !.` (i.e. using a cut) in my original post seems to be an alternative way to solve the non-termination problem. Do you think it is a reasonable alternative? – Géry Ogam Aug 06 '21 at 19:52
  • 1
    @Maggyero: `rev([_|_],[]).` – false Aug 07 '21 at 08:16
  • And apart from that it now hides solutions, like `rev(Xs,Xs), Xs=[a].`. If you are willing to pay such high a price, why not take `false` instead. Terminates perfectly – false Aug 07 '21 at 08:18
  • Alright, so using cuts is a bad practice, you don’t recommend it. – Géry Ogam Aug 07 '21 at 13:17
  • @Maggyero: Cut is [difficult to use](https://stackoverflow.com/search?q=%5Bprolog-cut%5D+user%3A772868) and certainly nothing to start with. You really need a solid relational stance first. – false Aug 07 '21 at 13:20