Input-termination of logic programs

In this paper, we study termination properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. A class of logic programs called linear bounded programs is introduced and input-termination of these programs is investigated. It is proved that linear bounded programs have only input-consuming LD-derivations (i.e., under Prolog's selection) of finite length. An attempt is then made to extend this result to all input-consuming derivations (not ncessarily under Prolog's selection). Through a counterexample, it is shown that the above result does not hold for the whole class of linear bounded programs under arbitrary selection. However, it is proved that simply-moded linear bounded programs have only input-consuming derivations of finite length, i.e., simply-moded linear bounded programs are input-terminating with dynamic scheduling. This class contains many programs like append, delete, insert, reverse, permute, count, listsum, listproduct, insertion-sort, quick-sort on lists, various tree traversal programs and addition, multiplication, factorial, power on natural numbers. Further, it is decidable whether a given logic program is linear bounded or not, in contrast to the notions of acceptable and recurrent programs.