CODEWITHSUNDEEP
recursionprologunificationsuccessor-arithmetics
RockMan
RockMan

Reputation: 53

Understanding Recursive Rule and Unification in Prolog

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?

Upvotes: 1

Views: 576

Answers (3)

PySeeker
PySeeker

Reputation: 874

Just to add a proof tree to this answers, which may make things more clear for others:

Base call:  numeral(succ(succ(0))).
                    : ^
           rule1    : :  {X/0}
                    : :
                    V :
              numeral(succ(X)).
                    : ^
           rule1    : :  {X/0}
                    : :
                    V :
                numeral(X).
                    : ^
          fact1     : :  {X/0}
                    : :
                    V :
      Found proof   [.]

You start with the downwards arrows and move then back up to the previous calls with the new found unificator in the last step. Please note that Prolog declares each variable in each step as a new variable, which I omitted in this scheme.

Upvotes: 0

Nikos M.
Nikos M.

Reputation: 8345

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.

Upvotes: 2

mat
mat

Reputation: 40768

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.

Upvotes: 3

Related Questions