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

Question

I am doing a very simple exercise in Prolog, and there is something I don’t understand in the trace. The program is "more than" ( > ) for integers represented as successors:

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

My problem: I do not understand why the request greater_than(succ(succ(succ(0))),succ(0)) generates 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 redo here? How can I avoid this (without cutting, of course)?

By the way, before asking: no, this is not some kind of homework ...

Answer 1

OK, so this is a compiler optimization that may or may not have a given compilation / version.

Later versions of SWI do not have this problem. This is probably due to indexing the proposal. This behavior will be seen on implementations without indexing or such that the index is only for the first argument.

But apparently, "SWI-Prolog provides just-in-time indexing for a few arguments . " The SWI 5.6.56 manual states that "no more than 4 arguments can be indexed." Therefore, it probably indexes more than one.

Answer 2

There is a reason why the prologue cannot infer (without examining it) if, following the next sentence, there is an alternative solution. True, in this case, this is just one check of the union (not so that it is always trivial), but it could be something that could take a lot of time (or even never end).

Now this is exactly where you should use the notch: you know that additional selection points will not create a solution (so you don’t change the semantics - the green cut). Alternatively (but basically it's syntactic sugar covering the cut) you can use if-then-else:

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

not that it still does extra calculations that could have been avoided with the cut.

PS: I doubt anyone will think this is XD's homework