Onterminationof meta-programs: Difference between revisions
Created page with "Title: Onterminationof meta-programs Research Question: How can we develop a methodology for performing correct termination analysis for a broad class of practical 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 the well-known acceptability condition, used in proving termination of logic programs. This approach allows for the reuse of termination..." |
No edit summary |
||
| Line 1: | Line 1: | ||
Title: Onterminationof meta-programs | Title: Onterminationof meta-programs | ||
Research Question: How can we develop a methodology for performing correct termination analysis for a broad class of | 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 the well-known acceptability condition, used in proving termination of logic programs | 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 | 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 | |||
Link to Article: https://arxiv.org/abs/ | |||
Authors: | Authors: | ||
arXiv ID: | arXiv ID: 0110035v3 | ||
[[Category:Computer Science]] | [[Category:Computer Science]] | ||
| Line 21: | Line 19: | ||
[[Category:Meta]] | [[Category:Meta]] | ||
[[Category:Methodology]] | [[Category:Methodology]] | ||
[[Category: | [[Category:Program]] | ||
[[Category: | [[Category:This]] | ||
Latest revision as of 03:18, 24 December 2023
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