Artificial
Intelligence

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

(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

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.