Reasoning About Termination of Prolog Programs

摘要

A theoretical basis for studying termination of (general) logic programs with thePROLOG selection rule is presented. To this end, the class of 'left terminating' programs is studied. These are logic programs that terminate with the PROLOG selection rule for all ground goals. A characterization of left terminating positive programs is offered by means of the notion of an 'acceptable program' that provides a practical method of proving termination. The method is illustrated by giving a simple proof of termination of the quicksort program for the desired class of goals. This approach is extended to the class of general logic programs by modifying the concept of acceptability. Acceptable general programs are proved to be left terminating. The converse implication does not hold but it is shown that under the assumption of non-floundering from ground goals every left terminating general program is acceptable. Various ways of defining semantics are shown to coincide for acceptable general programs. The use of this extension is illustrated by giving simple proofs of termination of a 'game' program and the transitive closure program for the desired class of goals.