Too much backtracking: why is there a “redo” here?

问题:

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

回答1:

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.

回答2:

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