Title: When size does matter - Termination analysis for typed logic programs
Authors: Vanhoof, Wim ×
Bruynooghe, Maurice #
Issue Date: 2002
Publisher: Springer
Host Document: Lecture notes in computer science vol:2372 pages:129-147
Conference: Logic-based Program Synthesis and Transformation location:Paphos, Cyprus date:November 28-30, 2001
Abstract: Proofs of termination typically proceed by mapping program states to a well founded domain and showing that successive states of the computation are mapped to elements decreasing in size. Automated termination analysers for logic programs achieve this by measuring and comparing the sizes of successive calls to recursive predicates. The size of the call is measured by a level mapping that in turn is based on a norm on the arguments of the call. A norm maps a term to a natural number. The choice of the norm is crucial for the ability to prove termination. For some programs a fairly complex norm is required. The automated selection of an appropriate norm is a missing link in this research domain and is addressed in this paper. Our proposal is to use the type of a predicate to generate a number of simple norms and to try them in turn for proving the termination of the predicate. Given a term of a certain type, we consider a norm for each of its subtypes, a norm that counts the number of subterms of the term that are of the considered subtype.
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Status SizeFormat
39276.pdf Published 256KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science