Backtracking in recursive predicates

Question

Assume we have the following predicates (This is an example from Programming in Prolog):

[F0] isInteger(0).
[F1] isInteger(X):- isInteger(Y), X is Y+1.

1. The first result for query isInteger(R), the marker is placed at F0, and will return R=0

2. If user presses ; , the marker is placed at F1, we move to subgoal(isInteger(Y), which is satisfied with F0) and R=1.

I understand the above. Now here are my questions:

1. If user presses ; again, where is the marker? How does the search proceed to return R=2? I have tried to understand the images in page 78-79 of the book, but it is not clear to me. The online tutorials that I found, do not handle backtracking in presence of recursion.

I am looking for any tutorials that explain backtracking in presence of recursion, hopefully with images of stack contents that helps me understand.

Thank you in advance Suzanne

Answer 1

Understanding backtracking and recursion by using images works for very tiny examples, but it does not scale to larger programs. Also, by stepping through a program you easily miss the most interesting properties. Fortunately, there are better notions than that. Let's take your example isInteger/1.

Set of solutions/answers

Your primary interest is to ensure that you are describing the right thing. Here, the second rule is most interesting. Read it in the direction of the arrow :-. That is, right-to-left: Provided Y is an integer, and X is Y+1 then also X is an integer.

Then, you can estimate the set of solutions which is infinite in this case.

Termination properties

The next question concerns the termination properties of the predicate. Note, that it cannot – in fact must not – terminate, if it has to produce infinitely many answers. On the other hand, ground queries like isInteger(1) have either one or no solution. So it is desirable that the predicate terminates for such cases. However, your definition does not terminate here!

Failure slices

To better understand this, I will use a failure-slice. That is, I will insert goals false into your program. If the resulting program fragment does not terminate, then the original doesn't.

?- isInteger(1), false

isInteger(0) :- false.
isInteger(X) :-
   isInteger(Y), false,
   X is Y+1.

Only a very small part is responsible for non-termination! The remaining part does not even look at the value of X at all. Therefore your program terminates never. No matter how you call it.

See failure-slice for more examples.