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.

• Type: Conference
• Year: 2009
• Where: WFLP
• Authors: Michael Leuschel, Salvador Tamarit, Germán Vidal
• Keywords: Algorithms, Prolog’s Leftmost Selection, Selection Rules, Strong Termination, WFLP 2009