Onterminationof meta-programs

Title: Onterminationof meta-programs

Research Question: How can we develop a methodology for performing a correct termination analysis for a broad class of meta-interpreters?

Methodology: The methodology is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs.

Results: The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of these implies termination of the other, i.e., the meta-interpreter preserves termination.

Implications: This methodology allows for the reuse of termination proofs obtained for the interpreted program as a basis for the termination proof of the meta-program. This makes it easier to prove termination for a broad class of meta-interpreters, including proof trees, different kinds of tracers, and reasoners.

Significance: This research is significant because it provides a methodology for performing a correct termination analysis for a broad class of meta-interpreters, which is a practical and theoretical advantage in the field of meta-programming. It also contributes to the ongoing research in termination analysis and logic programming.

Link to Article: https://arxiv.org/abs/0110035v3 Authors: arXiv ID: 0110035v3