Sciweavers

WFLP
2009
Springer

Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation

14 years 2 months ago
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation
A logic program strongly terminates if it terminates for any selection rule. Clearly, considering a particular selection rule—like Prolog’s leftmost selection rule—allows one to prove more goals terminating. In contrast, a strong termination analysis gives valuable information for those applications in which the selection rule cannot be fixed in advance (e.g., partial evaluation, dynamic selection rules, parallel execution). In this paper, we introduce a fast and accurate size-change analysis that can be used to infer conditions for both strong termination and strong quasitermination of logic programs. We also provide several ways to increase the accuracy of the analysis without sacrificing scalability. In the experimental evaluation, we show that the new algorithm is up to three orders of magnitude faster than the previous implementation, meaning that we can efficiently deal with programs exceeding 25,000 lines of Prolog.
Michael Leuschel, Salvador Tamarit, Germán
Added 25 May 2010
Updated 25 May 2010
Type Conference
Year 2009
Where WFLP
Authors Michael Leuschel, Salvador Tamarit, Germán Vidal
Comments (0)