Reasoning about termination of pure Prolog programs (Q1308986)

Prolog is a programming language based on logic programming which uses a fixed (left to right) selection rule and the depth first search strategy to explore the resulting search trees. This restrictions introduce incompleteness (wrt the logic programming operational model) in the Prolog interpreter: a Prolog interpreter will miss a solution if all the success nodes lie to the right of an infinite path in the search tree. Therefore, the issue of termination is essential in order to apply to Prolog various completeness results linking the procedural and operational model of logic programming. The paper studies termination of (general) logic programs with the Prolog leftmost selection rule. Termination here means finiteness of all possible Prolog derivations starting in the initial goal. In particular, the class of left terminating programs is studied, i.e., the class of logic programs which are terminating for all ground goals. Left terminating programs are characterized by means of the notion of acceptable programs. This provides a practical method for proving termination. The approach is then extended to general programs by modifying the concept of acceptability. It is also shown that several different semantics coincide on acceptable general programs. The results are interesting also in relation to verification of Prolog programs. In fact the notion of acceptability provides an easy way to verify that a Herbrand interpretation is the least Herbrand model of a program. This simplifies the study of partial correctness of Prolog programs based on the least Herbrand model. Moreover, as argued by the authors, the method proposed for the ``a posteriori'' verification of termination can also provide a guideline for the development of terminating programs.