Loop checking in SLD-derivations by well-quasi-ordering of goals

AbstractLoop checking mechanisms are used to detect and prune infinite SLD derivations, through run time checks which are introduced in logic program interpreters. Simple loop checks, i.e. checks which do not depend on the specific logic program, have been widely studied in literature. Since no sound and complete loop check exists even in the case of function-free programs, several subclasses have been characterized for which sound and complete loop checks can be determined. In this paper a theoretical framework for analysing properties of loop check mechanisms for logic programs is proposed, which exploits general mathematical results about well-quasi-ordered (wqo) sets. In a way, the method can be viewed as a counterpart of well known techniques based on well-founded partial-ordering, used in termination proofs for rewriting systems and for logic programs. The main results are obtained on the basis of a combinatorial analysis of properties of wqo sets of goals. As shown in the paper, subclasses of programs, for which sound and complete simple loop checks exist, can be easily framed in the wqo approach. Reasons for the different behaviours of subsumption loop checks based on list and multiset goal comparisons are also plainly highlighted