Understanding Recursive Rule and Unification in Prolog

Question

I'm a beginning Prolog student following the "LearnPrologNow!" set of tutorials. I'm doing my best to get a grip on the concepts and vocabulary. I've been able to understand everything up until Chapter 3 on Recursive Definitions when presented with this problem:

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

given the query

numeral(X).

Now, I understand that the idea of the program is that Prolog will begin counting numbers in this system in a sequence such as

X=0
X=succ(0)
X=succ(succ(0))

But I do not understand what causes it to "scale back" and ascend each time. I understand the principle of unification in that the program is trying to unify the query of X, but should it just follow the recursive rule once, and then return zero? What allows it to add a succ() around the query? Is that not traversing the recursive rule in the opposite direction?

Answer 1

Please think declaratively:

The rule

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

means:

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

:- is like an arrow used in logical implication (it looks similar to <==).

Seeing that you successfully derived that 0 is a numeral (first answer), it is thus no surprise that succ(0) is another solution.

I recommend you think in terms of such relations, instead of trying to trace the actual control flow.

Notice that succ/1 is not added "around the query", but is a part of the actual answer. The term succ(0) is just a normal Prolog term, with functor succ and argument 0.

Answer 2

Already given answer being good, i'll add some more:

Prolog uses denotational syntax (or declarative syntax) to define logical relations/"equations" between terms

A term is an object comprised of variables/functions/placeholders etc..

Unification is the process to check if two expressions (or two terms) can be equal with respect to the given relations/equations.

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

Is such a relation/equation which says that the fact that variable-term X is of numeral type (or class), implies the successor functional succ is also of same type. So Prolog here can unify the expression (in other words solve the equation) and replace X with succ(X) and so on, untill the domain of X is covered. So this unification implies X replaced by succ(X) and then unification can be re-applied.