Termination Detection in Logic Programs using Argument Sizes.

@inproceedings{DBLP:conf/pods/SohnG91,
  author    = {Kirack Sohn and
               Allen Van Gelder},
  title     = {Termination Detection in Logic Programs using Argument Sizes},
  booktitle = {Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on
               Principles of Database Systems, May 29-31, 1991, Denver, Colorado},
  publisher = {ACM Press},
  year      = {1991},
  isbn      = {0-89791-430-9},
  pages     = {216-226},
  ee        = {http://doi.acm.org/10.1145/113413.113433, db/conf/pods/SohnG91.html},
  crossref  = {DBLP:conf/pods/91},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

Progress on automated termination detection for logic programs is reported. The prospects for handling a large class of programs completely automatically appear promising, in contrast to the bleak picture for procedural languages. The methods reported are based on term size analysis of procedure arguments. Argument sizes of derivable facts involving an n-ary predicate are viewed as points in the positive orthant of Rⁿ. We describe a method of finding a nonnegative linear combination of bound argument sizes that (if it is found) is guaranteed to decrease during top-down execution of recursive rules. Duality theory of linear programming is used.

This methodology can handle nonlinear recursion, mutual recursion, and cases in which no specific argument is certain to decrease; while it requires rules to have a certain form, this form is attainable by known syntactic transformations. Several programs that could not be shown to terminate by earlier published methods are handled successfully. However, it only analyzes a sufficient condition; a procedure may terminate without our methodology detecting that fact.

Copyright © 1991 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

• Windows: Click the letter of your CD drive
  A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
• UNIX/LINUX/Mac: use mount point /pods8298/... or /cdrom/...

• Windows: Click the letter of your CD drive
  A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
• UNIX/LINUX/Mac: use mount point /aDVD1/... or /cdrom/...

Printed Edition

Online Edition: ACM Digital Library

References

[APP+89]

Foto N. Afrati, Christos H. Papadimitriou, George Papageorgiou, Athena Roussou, Yehoshua Sagiv, Jeffrey D. Ullman: On the Convergence of Query Evaluation. J. Comput. Syst. Sci. 38(2): 341-359(1989) BibTeX

[BS89a]

Alexander Brodsky, Yehoshua Sagiv: Inference of Monotonicity Constraints in Datalog Programs. PODS 1989: 190-199 BibTeX

[BS89b]

Alexander Brodsky, Yehoshua Sagiv: On Termination of Datalog Programs. DOOD 1989: 47-64 BibTeX

[BS91]

Alexander Brodsky, Yehoshua Sagiv: Inference of Inequality Constraints in Logic Programs. PODS 1991: 227-240 BibTeX

[ER87]

...

[Las90]

Jean-Louis Lassez: Querying Constraints. PODS 1990: 288-298 BibTeX

[LHM89]

Jean-Louis Lassez, Tien Huynh, Ken McAloon: Simplification and Elimination of Redundant Linear Arithmetic Constraints. NACLP 1989: 37-51 BibTeX

[Nai83]

...

[Plü90]

...

[Ps82]

...

[Sch86]

...

[SU84]

...

[Ull85]

Jeffrey D. Ullman: Implementation of Logical Query Languages for Databases. ACM Trans. Database Syst. 10(3): 289-321(1985) BibTeX

[UVG88]

Jeffrey D. Ullman, Allen Van Gelder: Efficient tests for top-down termination of logical rules. J. ACM 35(2): 345-373(1988) BibTeX

[VG90]

Allen Van Gelder: Deriving Constraints Among Argument Sizes in Logic Programs. PODS 1990: 47-60 BibTeX

[Wal88]

...

Referenced by

1. Kirack Sohn: Constraints among Argument Sizes in Logic Programs. PODS 1994: 68-74
2. Alexander Brodsky, Yehoshua Sagiv: Inference of Inequality Constraints in Logic Programs. PODS 1991: 227-240