Debugging recursion in Prolog

Question

Here is my knowledge base:

numeral(0). 
numeral(succ(X))  :-  numeral(X).

Here is my query:

numeral(X).

Here is what SWI Prolog returns in trace mode:

[trace]  ?- numeral(X).
   Call: (8) numeral(_3806) ? creep
   Exit: (8) numeral(0) ? creep
X = 0 ;
   Redo: (8) numeral(_3806) ? creep
   Call: (9) numeral(_4006) ? creep
   Exit: (9) numeral(0) ? creep
   Exit: (8) numeral(succ(0)) ? creep
X = succ(0) ;
   Redo: (9) numeral(_4006) ? creep
   Call: (10) numeral(_4010) ? creep
   Exit: (10) numeral(0) ? creep
   Exit: (9) numeral(succ(0)) ? creep
   Exit: (8) numeral(succ(succ(0))) ? creep
X = succ(succ(0))

I understand how it finds X=0 answer, I do not fully grasp how it obtains: X = succ(succ(0)). I understand that this is correct answer, but I am not sure how Prologs searched for it.

Here is my thinking: When it prints Call: (9) numeral(_4006) ? creep it tries this rule: numeral(succ(X)) :- numeral(X). And in particular it probably substitutes _4006 = succ(X) then it checks that it only holds when numeral(X) holds, which Prolog checks against numeral(0), so result is _4006 = succ(0).

Now if we ask for anther solution it again comes back to numeral(_4006), but what does it guess when is calls numeral(_4010). What is branching process here?

Is there way to get more details?

P.S. This is taken from the following link

Answer 1

Prolog searches trough bactracking. There are two ways Prolog can aim to satisfy an numeral(X) call:

1. with numeral(0) in which case it unifies X with 0; and
2. with numeral(succ(Y)) :- numeral(Y) in which case it unifies X with succ(Y) and makes a recursive call.

I here used Y since this also creates confusion: the variables in a clause are locally scoped in the sense that an X in a clause, is not the same variable as an X in a call.

Now in case Prolog backtracks and aims to satisfy the predicate with the clause, then this means that X = succ(Y) with Y a variable, but it needs to make an extra call with numeral(Y) as specified in the body.

Again there are two choices:

1. with numeral(0) in which case it unifies Y with 0; and
2. with numeral(succ(Z)) :- numeral(Z) in which case it unifies Y with succ(Z) and makes a recursive call.

In case we go for the first one, Y is set to 0, and thus X = succ(Y) hence X = succ(0). In the latter case X = succ(Y), and Y = succ(Z), and we again make a recursive call.

Now in case we again use the first line for numeral(0), this thus means that Z is unified with 0, hence Z = 0, hence Y = succ(0), hence X = succ(succ(0)).