#### 5.3.4.3 Infinite Loops

There is an infinite loop in the top-down derivation if there is an
atom *a* that is being proved as a subgoal of *a*. (Here we assume
that being a subgoal is transitive; a subgoal of a subgoal is a
subgoal). Thus, there can be an infinite loop only if the knowledge
base is cyclic. A knowledge base is **cyclic** if there is an
atom *a* such that there is a sequence
of definite clauses of the form

*a ←...a*

_{1}...*a*

_{1}←...a_{2}...*...*

*a*

_{n}←...a ...(where if *n=0* there is a single definite clause with *a* in the head and body).

A knowledge base is **acyclic** if there is an assignment of
natural numbers (non-negative integers) to the atoms so that the atoms
in the body of a definite clause are assigned a lower number than the atom in
the head. All of the knowledge bases given previously in this chapter
are acyclic.
There cannot be an infinite loop in an acyclic knowledge base.

To detect a cyclic knowledge base, the top-down proof procedure can be modified to maintain
the set of all **ancestors** for each atom in the
proof. In the procedure in Figure 5.4, the set *A* can
contain pairs of an atom and its set of ancestors.

Initially the set of ancestors of each atom is empty. When the rule

*a←a*

_{1}∧...∧a_{k}is used to prove *a*, the ancestors of *a _{i}* will
be the ancestors of

*a*together with

*a*. That is,

ancestors(a_{i})= ancestors(a) ∪{a}.

The proof can fail if an atom is in its set of ancestors. This failure only occurs if the knowledge base is cyclic. Note that this is a more refined version of cycle checking, where each atom has its own set of ancestors.

A cyclic knowledge base is often a sign of a bug. When writing a knowledge base, it is often useful to ensure an acyclic knowledge base by identifying a value that is being reduced at each iteration. For example, in the electrical domain, the number of steps away from the outside of the house is meant to be reduced by one each time through the loop. Disciplined and explicit use of a well-founded ordering can be used to prevent infinite loops in the same way that programs in traditional languages must be carefully programmed to prevent infinite looping.

Note that the bottom-up proof procedure does not get into an infinite loop, because it selects a rule only when the head has not been derived.