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.

Answer 2

Tracing this in the swish console:

% Handover to indenting predicate

isInteger(X) :- isInteger(X,0).

% As isInteger(), with printouts

isInteger(0,I) :- ws(I), format('0 reached\n').
isInteger(X,I) :- wrout('>', X,Y,I), ID is I+1, isInteger(Y,ID), wrout('<', X,Y,I), X is Y+1, wsucc(I).

% Writing out

wrout(C,X,Y,I) :-ws(I),format('~a X=',C),write(X),format(',Y='),write(Y),format('\n').

% Writing "success"

wsucc(I) :- ws(I),format('success\n').

% Indenting by 2*N underscores

ws(0).
ws(N) :- N>0, format('__'), ND is N-1, ws(ND).

Check whether 2 is an integer via ? - isInteger(2). (but do not call Next for this or an never-ending search will occur!)

> X=2,Y=_G5707
__0 reached
< X=2,Y=0
__> X=_G5707,Y=_G6473
____0 reached
__< X=_G5707,Y=0
__success
< X=2,Y=1
success
true

Enumerate integers using ?- isInteger(I)

0 reached
I = 0

"Next"

> X=_G5328,Y=_G5926
__0 reached
< X=_G5328,Y=0
success
I = 1

"Next" (note that we restart at indentation '__')

__> X=_G5926,Y=_G391
____0 reached
__< X=_G289,Y=0
__success
< X=_G257,Y=1
success
I = 2

"Next" (note that we restart at indentation '____')

____> X=_G391,Y=_G3260
______0 reached
____< X=_G391,Y=0
____success
__< X=_G289,Y=1
__success
< X=_G257,Y=2
success
I = 3

Very nice.

I am going to explain this to the local team. Here is an illustration of the integer enumeration process with some "original notation". Hopefully self-explanatory.