prolog - infinite rule

Question

I have the next rules

% Signature: natural_number(N)/1
% Purpose: N is a natural number.
natural_number(0).
natural_number(s(X)) :-
   natural_number(X).

ackermann(0, N, s(N)). % rule 1
ackermann(s(M),0,Result):-
   ackermann(M,s(0),Result). % rule 2
ackermann(s(M),s(N),Result):-
   ackermann(M,Result1,Result),
   ackermann(s(M),N,Result1). % rule 3

The query is: ackermann (M,N,s(s(0))).

Now, as I understood, In the third calculation, we got an infinite search (failure branch). I check it, and I got a finite search (failure branch).

I'll explain: In the first, we got a substitution of M=0, N=s(0) (rule 1 - success!). In the second, we got a substitution of M=s(0),N=0 (rule 2 - success!). But what now? I try to match M=s(s(0)) N=0, But it got a finite search - failure branch. Why the compiler doesn't write me "fail".

Thank you.

Answer 1

It was a bit hard to understand exactly what Tom is asking here. Perhaps there's an expectation that the predicate natural_number/1 somehow influences the execution of ackermann/3. It will not. The latter predicate is purely recursive and makes no subgoals that depend on natural_number/1.

When the three clauses shown are defined for ackermann/3, the goal:

?- ackermann(M,N,s(s(0))).

causes SWI-Prolog to find (with backtracking) the two solutions that Tom reports, and then to go into infinite recursion (resulting in an "Out of Stack" error). We can be sure that this infinite recursion involves the third clause given for ackermann/3 (rule 3 per Tom's comments in code) because in its absence we only get the two acknowledged solutions and then explicit failure:

M = 0,
N = s(0) ;
M = s(0),
N = 0 ;
false.

It seems to me Tom asks for an explanation of why changing the submitted query to one that sets M = s(s(0)) and N = 0, producing a finite search (that finds one solution and then fails on backtracking), is consistent with the infinite recursion produced by the previous query. My suspicion here is that there's a misunderstanding of what the Prolog engine attempts in backtracking (for the original query), so I'm going to drill down on that. Hopefully it clears up the matter for Tom, but let's see if it does. Admittedly my treatment is wordy, but the Prolog execution mechanism (unification and resolution of subgoals) is worthy of study.

[Added: The predicate has an obvious connection to the famous Ackermann function that is total computable but not primitive recursive. This function is known for growing rapidly, so we need to be careful in claiming infinite recursion because a very large but finite recursion is also possible. However the third clause puts its two recursive calls in an opposite order to what I would have done, and this reversal seems to play a critical role in the infinite recursion we find in stepping through the code below.]

When the top-level goal ackermann(M,N,s(s(0))) is submitted, SWI-Prolog tries the clauses (facts or rules) defined for ackermann/3 until it finds one whose "head" unifies with the given query. The Prolog engine does not have far to look as the first clause, this fact:

ackermann(0, N, s(N)).

will unify, binding M = 0 and N = s(0) as has already been described as the first success.

If requested to backtrack, e.g. by user typing semi-colon, the Prolog engine checks to see if there is an alternative way to satisfy this first clause. There is not. Then the Prolog engine proceeds to attempt the following clauses for ackermann/3 in their given order.

Again the search does not have to go far because the second clause's head also unifies with the query. In this case we have a rule:

ackermann(s(M),0,Result) :- ackermann(M,s(0),Result).

Unifying the query and the head of this rule yields the bindings M = s(0), N = 0 in terms of the variables used in the query. In terms of the variables used in the rule as stated above, M = 0 and Result = s(s(0)). Note that unification matches terms by their appearance as calling arguments and does not consider variable names reused across the query/rule boundary as signifying identity.

Because this clause is a rule (having body as well as head), unification is just the first step in trying to succeed with it. The Prolog engine now attempts the one subgoal that appears in the body of this rule:

ackermann(0,s(0),s(s(0))).

Note that this subgoal comes from replacing the "local" variables used in the rule by the values of unification, M = 0 and Result = s(s(0)). The Prolog engine is now calling the predicate ackermann/3 recursively, to see if this subgoal can be satisfied.

It can, as the first clause (fact) for ackermann/3 unifies in the obvious way (indeed in essentially the same way as before as regards the variables used in the clause). And thus (upon this recursive call succeeding), we get the second solution succeeding in the outer call (the top-level query).

If the user asks the Prolog engine to backtrack once more, it again checks to see if the current clause (the second one for ackermann/3) can be satisfied in an alternative way. It cannot, and so the search continues by passing to the third (and last) clause for predicate ackermann/3:

ackermann(s(M),s(N),Result) :-
    ackermann(M,Result1,Result),
    ackermann(s(M),N,Result1).

I'm about to explain that this attempt does produce infinite recursion. When we unify the top-level query with the head of this clause, we get bindings for the arguments that can perhaps be clearly understood by aligning the terms in in the query with those in the head:

   query     head
     M       s(M)
     N       s(N)
   s(s(0))  Result

Bearing in mind that variables having the same name in the query as variables in the rule does not constrain unification, this triple of terms can be unified. Query M will be head s(M), that is a compound term involving functor s applied to some as-yet unknown variable M appearing in the head. Same thing for query N. The only "ground" term so far is variable Result appearing in the head (and body) of the rule, which has been bound to s(s(0)) from the query.

Now the third clause is a rule, so the Prolog engine must continue by attempting to satisfy the subgoals appearing in the body of that rule. If you substitute values from the head unification into the body, the first subgoal to satisfy is:

ackermann(M,Result1,s(s(0))).

Let me point out that I've used here the "local" variables of the clause, except that I've replaced Result by the value to which it was bound in unification. Now notice that apart from replacing N of the original top-level query by variable name Result1, we are just asking the same thing as the original query in this subgoal. Certainly it's a big clue we might be about to enter an infinite recursion.

However a bit more discussion is needed to see why we don't get any further solutions reported! This is because the first success of that first subgoal is (just as found earlier) going to require M = 0 and Result1 = s(0), and the Prolog engine must then proceed to attempt the second subgoal of the clause:

ackermann(s(0),N,s(0)).

Unfortunately this new subgoal does not unify with the first clause (fact) for ackermann/3. It does unify with the head of the second clause, as follows:

   subgoal     head
     s(0)      s(M)
      N         0
     s(0)     Result

but this leads to a sub-subgoal (from the body of the second clause):

ackermann(0,s(0),s(0)).

This does not unify with the head of either the first or second clause. It also does not unify with the head of the third clause (which requires the first argument to have the form s(_)). So we reached a point of failure in the search tree. The Prolog engine now backtracks to see if the first subgoal of the third clause's body can be satisfied in an alternative way. As we know, it can be (since this subgoal is basically the same as the original query).

Now M = s(0) and Result1 = 0 of that second solution leads to this for the second subgoal of the third clause's body:

ackermann(s(s(0)),N,0).

While this does not unify with the first clause (fact) of the predicate, it does unify with the head of the second clause:

   subgoal     head
   s(s(0))     s(M)
      N         0
      0       Result

But in order to succeed the Prolog engine must satisfy the body of the second clause as well, which is now:

ackermann(s(s(0)),s(0),0).

We can easily see this cannot unify with the head of either the first or second clause for ackermann/3. It can be unified with the head of the third clause:

  sub-subgoal  head(3rd clause)
    s(s(0))       s(M)
      s(0)        s(N)
       0         Result

As should be familiar now, the Prolog engine checks to see if the first subgoal of the third clause's body can be satisfied, which amounts to this sub-sub-subgoal:

ackermann(s(0),Result1,0).

This fails to unify with the first clause (fact), but does unify with the head of the second clause binding M = 0, Result1 = 0 and Result = 0 , producing (by familiar logic) the sub-sub-sub-subgoal:

ackermann(0,0,0).

Since this cannot be unified with any of the three clauses' heads, this fails. At this point the Prolog engine backtracks to trying to satisfy the above sub-sub-subgoal using the third clause. Unification goes like this:

  sub-sub-subgoal  head(3rd clause)
       s(0)             s(M)
      Result1           s(N)
         0             Result

and the Prolog engine's task is then to satisfy this sub-sub-sub-subgoal derived from the first part of the third clause's body:

ackermann(0,Result1,0).

But this will not unify with the head of any of the three clauses. The search for a solution to the sub-sub-subgoal above terminates in failure. The Prolog engine backtracks all the way to where it first tried to satisfy the second subgoal of the third clause as invoked by the original top-level query, as this has now failed. In other words it tried to satisfy it with the first two solutions of the first subgoal of the third clause, which you will recall was in essence the same except for change of variable names as the original query:

ackermann(M,Result1,s(s(0))).

What we've seen above are that solutions for this subgoal, duplicating the original query, from the first and second clauses of ackermann/3, do not permit the second subgoal of the third clause's body to succeed. Therefore the Prolog engine tries to find solutions that satisfy the third clause. But clearly this is now going into infinite recursion, as that third clause will unify in its head, but the body of the third clause will repeat exactly the same search we just chased through. So the Prolog engine now winds up going into the body of the third clause endlessly.

Answer 2

Let me rephrase your question: The query ackermann(M,N,s(s(0))). finds two solutions and then loops. Ideally, it would terminate after these two solutions, as there is no other N and M whose value is s(s(0)).

So why does the query not terminate universally? Understanding this can be quite complex, and the best advice is to not attempt to understand the precise execution mechanism. There is a very simple reason: Prolog's execution mechanism turns out to be that complex that you easily will misunderstand it anyway if you attempt to understand it by stepping through the code.

Instead, you can try the following: Insert goals false at any place in your program. If the resulting program does not terminate, then also the original program will not terminate.

In your case:

ackermann(0, N, s(N)) :- false.
ackermann(s(M),0,Result):- false,
   ackermann(M,s(0),Result).
ackermann(s(M),s(N),Result):-
   ackermann(M,Result1,Result), false,
   ackermann(s(M),N,Result1).

We can now remove the first and second clause. And in the third clause, we can remove the goal after false. So if the following fragment does not terminate, also the original program will not terminate.

ackermann(s(M),s(N),Result):-ackermann(M,Result1,Result), false.

This program now terminates only if the first argument is known. But in our case it's free...

That is: By considering a small fraction of the program (called a failure-slice) we already were able to deduce a property of the entire program. For details, see this paper and others on the site.

Unfortunately, that kind of reasoning only works for cases of non-termination. For termination, things are more complex. The best is to try a tool like cTI which infers termination conditions and tries to prove their optimality. I entered your program already, so try to modify if and see the effects!

If we are at it: This small fragment also tells us that the second argument does not influence termination¹. That means, that queries like ackermann(s(s(0)),s(s(0)),R). will not terminate either. Exchange the goals to see the difference...

---

^{1 To be precise, a term that does not unify with s(_) will influence termination. Think of 0. But any s(0), s(s(0)), ... will not influence termination.}