Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Termination analysis of logic programs through combination of type-based norms
Bruynooghe M., Codish M., Gallagher J., Genaim S., Vanhoof W. ACM Transactions on Programming Languages and Systems29 (2):10-es,2007.Type:Article
Date Reviewed: Aug 29 2007

Establishing that all computations terminate is a fundamental, though generally undecidable, property of computer programs. Therefore, termination analyses that approximate this property have been developed for different programming languages.

This paper focuses on the definition of a termination analysis for logic programs (roughly speaking, simple Prolog programs). In this context, termination analyses proceed by first identifying the program loops and then by looking for a ranking function that maps every call to a well-founded domain so that its value decreases every time a loop is executed. The so-called global approach considers a single ranking function for all loops, while the more flexible local approach allows the use of different ranking functions. In the context of logic programs, ranking functions are often based on the notion of “norm,” a mapping used to measure the size of the arguments of a call.

In this context, the authors show that by providing type declarations (which is not usually required in Prolog implementations), a collection of simple, type-based norms can be automatically inferred. Intuitively speaking, a type-based norm counts the number of subterms in a term of the given type. Then, the authors show that using the combination of different type-based norms as a basis for the definition of ranking functions (following the local approach) results in a more precise termination analysis than existing analyses.

The paper is well written, includes a good introduction to its main subject, and contains many examples that illustrate the technical developments. It also includes formal proofs of correctness and provides a summary of results from a complete experimental evaluation. The results are not surprising, but show that the new approach is actually useful in practice.

Reviewer:  German Vidal Review #: CR134688 (0807-0684)
Bookmark and Share
  Featured Reviewer  
 
Logic Programming (D.1.6 )
 
 
Pre- And Post-Conditions (F.3.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Logic Programming": Date
Parallel logic programming
Tick E. (ed), MIT Press, Cambridge, MA, 1991. Type: Book (9780262200875)
Aug 1 1992
The standard C library
Plauger P., Prentice-Hall, Inc., Upper Saddle River, NJ, 1992. Type: Book (9780131315082)
Aug 1 1992
Logic and objects
McCabe F., Prentice-Hall, Inc., Upper Saddle River, NJ, 1992. Type: Book (9780135360798)
Nov 1 1993
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy