Learn Prolog Now - issues with backtracking in exercise on recursion

Question

I am having troubles understanding what is happening in this example
Learn Prolog Now - Chapter 3 - Example 3: Successor

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

When questioned numeral(X), it will firstly give 0 for X, then continue with succ(0), incrementing the succ(0) part by one in this manner until it runs out of space:

X = 0 ?     
X = succ(0) ? ;
X = succ(succ(0)) ? ;
X = succ(succ(succ(0))) ? ;
X = succ(succ(succ(succ(0)))) ? 

I am struggling to understand why it increments succ(0)?

I know that prolog will firstly find a fact and match it, hence the first 0. Then it will backtrack to see if there are any other solutions and it will "see" the rule. In the rule, it will use the instantiated X to 0. Where I fail, is to see why it keeps incrementing succ(0). Does X become succ(0), as opposed to just 0?

My apologies for the silly brain.

Answer 1

I think Guy Coder gave a good, detailed explanation of what's going on. I'll provide a slight variant of his inductive explanation to, hopefully, help bring more clarity.

Think about what your Prolog rules say:

numeral(0).

This says, 0 is a numeral.

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

This says, succ(X) is a numeral if X is a numeral.

By the first rule, then, 0 is a numeral. That is, numeral(0) is true (succeeds). By the second rule, since 0 is a numeral, then succ(0) must be a numeral (numeral(succ(0)) is true). Since succ(0) is a numeral, then by the second rule again, succ(succ(0)) must be a numeral (numeral(succ(succ(0)) is true). And so on...

Answer 2

I am struggling to understand why it increments succ(0)?

If you read the section again it states:

Here’s yet another way of writing numerals, which is sometimes used in mathematical logic. It makes use of just four symbols: 0, succ , and the left and right parentheses, ( ). This style of numeral is defined by the following inductive definition:

0 is a numeral.
If X is a numeral, then so is succ(X) .

One of the things I see a lot of people having a problem with when first learning higher math is that when you say math the first thing that pops into their head is Arabic numerals and a Cartesian coordinate system.

For this example you have to think symbolically, e.g. Symbolic computation, or more fundamentally, Abstract rewriting system.

For this example they are not using Arabic numerals but a functional way of describing numbers. In other words to describe a number you only have the starting symbol 0 and a function succ(x). Note I say symbol and not number because the symbol 0 only has meaning when put into a context, in this case natural numbers

So

 0 is 0
 1 is succ(0)        - The successor of 0 is 1.
 2 is succ(succ(0))  - The successor of the successor of 0 is 2 or
                       The successor of 1, e.g. succ(0), is 2.

and so on. If you read about Lambda calculus you will see this often.

Another way to think about this is given by the keyword inductive. With induction you need a starting fact and a rule that takes you to the next fact. So 0 is the fact and the rule that takes you to the next fact is succ(X).