Abstract Partial Evaluation for Termination Analysis

7th International Workshop on Termination (WST 2004); 2004

Abstract:

Current techniques for proving termination of logic programs focus on size and instantiation information. Structure information is ignored and for many examples this leads to imprecision in the analysis. There are two approaches to consider structure information: either to enhance the abstract domain over which the analysis is performed; or to transform the program so that structure in the concrete program is considered before abstract interpretation is applied. In ite{adornments-lopstr03}, the authors propose a technique to transform a program so that the predicate names are adorned to reflect different structure patterns. In this approach, the adorned program is equivalent to the original program and termination analysis of the adorned program is more precise. In this paper we present an alternative approach based on well-studied techniques of partial evaluation (unfolding) and abstract interpretation. Partial evaluation is a natural choice when the intention is to pre-evaluate just so much as to consider the structure present in the program. The advantage of this approach is that it relies completely on well-studied formal techniques. In addition to partial evaluation we also abstract the program, maintaining structure, but possibly adding computations. This process preserves nontermination and hence is safe for termination analysis. This often simplifies the transformation. We obtain results similar to those illustrated in ite{adornments-lopstr03}. We also compare our results to those obtained using ECCE ite{ecce} which is an off-the-shelf partial evaluator. Our results are more precise and analyses are considerably faster than those obtained using ECCE.

Available: bibtex entry postscript

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il