An analysis of loop checking mechanisms for logic programs (Q1177923)

All methods of detecting divergence in computations of logic programs have been based on excluding some kinds of repetitions by so called loop checking. Loop checking mechanisms are systematically studied by considering their soundness, completeness and relative strength. It is shown that a natural concept of a simple loop check is too weak: no sound and complete loop checks exist even for programs with no function symbols. A number of sound simple loop checks is introduced and natural classes of Prolog programs without function symbols are identified for which the tests are complete. The loop checks are divided into three groups called equality checks, subsumption checks and context checks. The three groups of loop checks appear to be complete for programs with restricted recursion.