Too much backtracking: why is there a "redo" here?

Asked 30/8, 2012 at 7:38 Answered 30/8, 2012 at 9:30

Solved prolog backtracking successor-arithmetics

I'm doing a very simple exercise in Prolog and there's something I don't understand in the trace. The program is a "greater than" (>) on integers represented as successors:

greater_than(succ(_), 0).
greater_than(succ(A), succ(B)) :-
  greater_than(A, B).

My problem: I don't understand why the request greater_than(succ(succ(succ(0))),succ(0)) generates a redo in the following trace:

[trace] ?- greater_than(succ(succ(succ(0))),succ(0)).
Call: (6) greater_than(succ(succ(succ(0))), succ(0)) ? creep
Call: (7) greater_than(succ(succ(0)), 0) ? creep
Exit: (7) greater_than(succ(succ(0)), 0) ? creep
Exit: (6) greater_than(succ(succ(succ(0))), succ(0)) ? creep
true ;
Redo: (7) greater_than(succ(succ(0)), 0) ? creep
Fail: (7) greater_than(succ(succ(0)), 0) ? creep
Fail: (6) greater_than(succ(succ(succ(0))), succ(0)) ? creep
false.

Why is there a redo here? How can I avoid it (without a cut, of course)?

BTW, before you ask : no, it's not some kind of homework...

Diaghilev answered 30/8, 2012 at 7:38 Comment(4)

It's just an optimization you're asking about, which a given compiler might or might not have. – Genesia 30/8, 2012 at 8:23

Well, in general I guess optimization of one's code is a legitimate programming concern, even if one codes only on one kind of compiler (SWI here). However, I've just updated SWI and I don't even see this behaviour anymore, so it really was internal to SWI and I guess the question is truly not of interest. Sorry about the noise. – Diaghilev 30/8, 2012 at 8:42

I tried your code on my SWI installation and it did not try any redo's. It's not only compiler, it's its version too. I see you updated it; perhaps it was a really old version. – Genesia 30/8, 2012 at 9:7

Yes it's definitely a version issue (I can't tell which one, but it's solved as of 5.10.4). I'll post an answer and accept it as soon as I can (because of my reputation I must wait 8 hours), or you can do it. – Diaghilev 30/8, 2012 at 9:17

OK, so it's a compiler optimization that a given compiler/version combination might or might not have.

Later versions of SWI do not have this problem. It is probably related to clause indexing. This behaviour would be seen on implementations without indexing, or such that index on the first argument only.

But apparently, "SWI-Prolog provides `just-in-time' indexing over multiple arguments". SWI 5.6.56 manual states that "at most 4 arguments can be indexed". So it probably indexes more than one.

Genesia answered 30/8, 2012 at 9:30 Comment(2)

Thanks for the detailed info. I confirm that the issue seems solved in version 5.10.4 (but probably also in some earlier versions). – Diaghilev 30/8, 2012 at 9:37

Looking again into Prolog after a few years, I see this behaviour again in 7.2.3... I'm not sure I'm in love with the way this language (and the intended behaviour of compilers and interpreters) is specified. – Diaghilev 6/5, 2020 at 13:37

There reason there is a redo is that prolog cannot deduce (without examining it) if, by following the next clause, there would be an alternative solution. True, in this case it is just one head unification check (not that this is always trivial) but it could be something that could take a lot of time (or even never terminate).

Now, this is exactly where you should use cut: you know that the extra choice points wont produce a solution (so you are not changing the semantics - a green cut). Alternatively (but it's mostly syntactic sugar covering a cut) you can use if-then-else:

greater_than(succ(A), B):-
    B = succ(BI) ->
    greater_than(A,BI)
    ; B = 0.

not that this still does extra computations which would be avoided with cut.

PS: I doubt that anyone would think it's homework XD

Ringmaster answered 30/8, 2012 at 8:53 Comment(3)

unfortunately this is not a green cut. greater_than(A,B) works differently. – Genesia 30/8, 2012 at 9:11

There was no "extra choice point" here: there is only one way to perform unification on the clause head on which there was a redo. There is no need of cut in this program, apparently it was only a transitional bug in SWI. – Diaghilev 30/8, 2012 at 9:13

It's not a bug. Choice points are left from left to right and top to bottom. A Prolog compiler doesn't have to even look at clauses under a clause that fits before backtracking. If now SWI optimizes it it doesn't mean that before it was a bug. – Metic 30/8, 2012 at 9:25

Recommended topics

Hot tags