Transformational methodology for proving termination of logic programs

M. R.K. Krishna Rao; Deepak Kapur; R. K. Shyamasundar

doi:10.1016/S0743-1066(97)00028-9

Transformational methodology for proving termination of logic programs

M. R.K. Krishna Rao, Deepak Kapur, R. K. Shyamasundar^*

^*Corresponding author for this work

King Fahd University of Petroleum & Minerals

Research output: Contribution to journal › Article › peer-review

15 Scopus citations

Abstract

A methodology for proving the termination of well-moded logic programs is developed by reducing the termination problem of logic programs to that of term rewriting systems. A transformation procedure is presented to derive a term rewriting system from a given well-moded logic program such that the termination of the derived rewrite system implies the termination of the logic program for all well-moded queries under a class of selection rules. This facilitates applicability of a vast source of termination orderings proposed in the literature on term rewriting, for proving termination of logic programs. The termination of various benchmark programs has been established with this approach. Unlike other mechanizable approaches, the proposed approach does not require any preprocessing and works well, even in the presence of mutual recursion. The transformation has also been implemented as a front end to Rewrite Rule Laboratory (RRL) and has been used in establishing termination of nontrivial Prolog programs such as a prototype compiler for ProCoS, PL₀ language.

Original language	English
Pages (from-to)	1-41
Number of pages	41
Journal	Journal of Logic Programming
Volume	34
Issue number	1
DOIs	https://doi.org/10.1016/S0743-1066(97)00028-9
State	Published - Jan 1998

Bibliographical note

Funding Information:
PROOF (By Contradiction). Assume that the selected atom at a resolution step has variables in its input positions. By the above lemma, there are producers that are smaller (under the evaluation order) than the selected atom contradicting the minimality of the selected atom. Therefore, input terms of the selected atom are ground at every resolution step. Hence every SLD-derivation starting with a well-moded query is a data-driven evaluation. \[\] We thank Prof. K. R. Apt and Prof. J. W. Klop of CWI for their helpful comments. Thanks are also due to the anonymous referees, whose comments have greatly improved the presentation. Dr. Kaput was partially supported by National Science Foundation Grant CCR-9303394 and National Science Foundation Indo-US Grant INT-9416687. Dr. Shyamasundar was partially supported by National Science Foundation lndo-US Grant INT-9416687.

ASJC Scopus subject areas

Logic

Access to Document

10.1016/S0743-1066(97)00028-9

Cite this

@article{2fa36b4ca9424690aa889289f304fe44,

title = "Transformational methodology for proving termination of logic programs",

abstract = "A methodology for proving the termination of well-moded logic programs is developed by reducing the termination problem of logic programs to that of term rewriting systems. A transformation procedure is presented to derive a term rewriting system from a given well-moded logic program such that the termination of the derived rewrite system implies the termination of the logic program for all well-moded queries under a class of selection rules. This facilitates applicability of a vast source of termination orderings proposed in the literature on term rewriting, for proving termination of logic programs. The termination of various benchmark programs has been established with this approach. Unlike other mechanizable approaches, the proposed approach does not require any preprocessing and works well, even in the presence of mutual recursion. The transformation has also been implemented as a front end to Rewrite Rule Laboratory (RRL) and has been used in establishing termination of nontrivial Prolog programs such as a prototype compiler for ProCoS, PL0 language.",

author = "\{Krishna Rao\}, \{M. R.K.\} and Deepak Kapur and Shyamasundar, \{R. K.\}",

note = "Funding Information: PROOF (By Contradiction). Assume that the selected atom at a resolution step has variables in its input positions. By the above lemma, there are producers that are smaller (under the evaluation order) than the selected atom contradicting the minimality of the selected atom. Therefore, input terms of the selected atom are ground at every resolution step. Hence every SLD-derivation starting with a well-moded query is a data-driven evaluation. \textbackslash{}[\textbackslash{}] We thank Prof. K. R. Apt and Prof. J. W. Klop of CWI for their helpful comments. Thanks are also due to the anonymous referees, whose comments have greatly improved the presentation. Dr. Kaput was partially supported by National Science Foundation Grant CCR-9303394 and National Science Foundation Indo-US Grant INT-9416687. Dr. Shyamasundar was partially supported by National Science Foundation lndo-US Grant INT-9416687.",

year = "1998",

month = jan,

doi = "10.1016/S0743-1066(97)00028-9",

language = "English",

volume = "34",

pages = "1--41",

journal = "Journal of Logic Programming",

issn = "0743-1066",

publisher = "Elsevier B.V.",

number = "1",

}

TY - JOUR

T1 - Transformational methodology for proving termination of logic programs

AU - Krishna Rao, M. R.K.

AU - Kapur, Deepak

AU - Shyamasundar, R. K.

N1 - Funding Information: PROOF (By Contradiction). Assume that the selected atom at a resolution step has variables in its input positions. By the above lemma, there are producers that are smaller (under the evaluation order) than the selected atom contradicting the minimality of the selected atom. Therefore, input terms of the selected atom are ground at every resolution step. Hence every SLD-derivation starting with a well-moded query is a data-driven evaluation. \[\] We thank Prof. K. R. Apt and Prof. J. W. Klop of CWI for their helpful comments. Thanks are also due to the anonymous referees, whose comments have greatly improved the presentation. Dr. Kaput was partially supported by National Science Foundation Grant CCR-9303394 and National Science Foundation Indo-US Grant INT-9416687. Dr. Shyamasundar was partially supported by National Science Foundation lndo-US Grant INT-9416687.

PY - 1998/1

Y1 - 1998/1

N2 - A methodology for proving the termination of well-moded logic programs is developed by reducing the termination problem of logic programs to that of term rewriting systems. A transformation procedure is presented to derive a term rewriting system from a given well-moded logic program such that the termination of the derived rewrite system implies the termination of the logic program for all well-moded queries under a class of selection rules. This facilitates applicability of a vast source of termination orderings proposed in the literature on term rewriting, for proving termination of logic programs. The termination of various benchmark programs has been established with this approach. Unlike other mechanizable approaches, the proposed approach does not require any preprocessing and works well, even in the presence of mutual recursion. The transformation has also been implemented as a front end to Rewrite Rule Laboratory (RRL) and has been used in establishing termination of nontrivial Prolog programs such as a prototype compiler for ProCoS, PL0 language.

AB - A methodology for proving the termination of well-moded logic programs is developed by reducing the termination problem of logic programs to that of term rewriting systems. A transformation procedure is presented to derive a term rewriting system from a given well-moded logic program such that the termination of the derived rewrite system implies the termination of the logic program for all well-moded queries under a class of selection rules. This facilitates applicability of a vast source of termination orderings proposed in the literature on term rewriting, for proving termination of logic programs. The termination of various benchmark programs has been established with this approach. Unlike other mechanizable approaches, the proposed approach does not require any preprocessing and works well, even in the presence of mutual recursion. The transformation has also been implemented as a front end to Rewrite Rule Laboratory (RRL) and has been used in establishing termination of nontrivial Prolog programs such as a prototype compiler for ProCoS, PL0 language.

UR - https://www.scopus.com/pages/publications/0039346788

U2 - 10.1016/S0743-1066(97)00028-9

DO - 10.1016/S0743-1066(97)00028-9

M3 - Article

AN - SCOPUS:0039346788

SN - 0743-1066

VL - 34

SP - 1

EP - 41

JO - Journal of Logic Programming

JF - Journal of Logic Programming

IS - 1

ER -

Transformational methodology for proving termination of logic programs

Abstract

Bibliographical note

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this