Termination analysis of logic programs through combination of type-based norms

This article makes two contributions to the work on semantics-based termination analysis for logic programs. The first involves a novel notion of type - based norm where for a given type, a corresponding norm is defined to count in a term the number of subterms of that type. This provides a collecti...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 2007-04, Vol.29 (2), p.10
Main Authors: BRUYNOOGHE, Maurice, CODISH, Michael, GALLAGHER, John P, GENAIM, Samir, VANHOOF, Wim
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Programming languages
Software
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This article makes two contributions to the work on semantics-based termination analysis for logic programs. The first involves a novel notion of type - based norm where for a given type, a corresponding norm is defined to count in a term the number of subterms of that type. This provides a collection of candidate norms, one for each type defined in the program. The second enables an analyzer to base termination proofs on the combination of several different norms. This is useful when different norms are better suited to justify the termination of different parts of the program. Application of the two contributions together consists in considering the combination of the type-based candidate norms for a given program. This results in a powerful and practical technique. Both contributions have been introduced into a working termination analyzer. Experimentation indicates that they yield state-of-the-art results in a fully automatic analysis tool, improving with respect to methods that do not use both types and combined norms.
ISSN:0164-0925
1558-4593
DOI:10.1145/1216374.1216378