Termination of Logic Programs with Dynamic Scheduling

Title: Termination of Logic Programs with Dynamic Scheduling

Abstract: This research investigates the termination properties of logic programs that use dynamic scheduling. Dynamic scheduling is a mechanism that determines which atoms in a query are selectable and which ones are not, allowing for features like coroutining and parallel execution. The study focuses on nicely-moded programs and queries, and presents a weak version of the well-known switching lemma for input-consuming derivations. Additionally, it demonstrates that under certain conditions, there exists an algebraic characterization of the termination of input-consuming derivations.

Main Research Question: Can we develop a method to verify the termination of logic programs with dynamic scheduling?

Methodology: The research employs a bottom-up approach, starting with the definition of nicely-moded programs and queries. These programs and queries are designed to work with dynamic scheduling, ensuring that only sufficiently instantiated atoms can be selected. The study then presents a weak version of the switching lemma for input-consuming derivations, which is a key result in the field of termination for logic programs. Finally, it demonstrates an algebraic characterization of the termination of input-consuming derivations under certain conditions.

Results: The main result of this research is an algebraic characterization of the termination of input-consuming derivations. This characterization provides a clear and concise way to determine whether a logic program with dynamic scheduling will terminate. Additionally, the study presents a weak version of the switching lemma for input-consuming derivations, which is a significant advancement in the field of termination for logic programs with dynamic scheduling.

Implications: The results of this research have several implications for the field of logic programming. First, the algebraic characterization of termination for input-consuming derivations provides a practical tool for verifying the termination of logic programs with dynamic scheduling. Second, the weak version of the switching lemma for input-consuming derivations extends the existing body of knowledge on termination for logic programs, allowing for a more comprehensive understanding of these programs. Finally, the research highlights the importance of dynamic scheduling in the context of logic programming, and the potential benefits of incorporating this mechanism into existing logic programming languages.

Link to Article: https://arxiv.org/abs/0101023v1 Authors: arXiv ID: 0101023v1