Automatic Termination Analysis of Programs Containing Arithmetic Predicates

TL;DR

This paper introduces an automatic method for proving termination of logic programs with arithmetic predicates by combining finite abstraction, abstract interpretation, and query-mapping pairs, enabling simpler and case-based termination proofs.

Contribution

The paper presents a novel approach that automatically proves termination of programs with arithmetic predicates using finite abstraction and case-specific termination functions, improving over classical methods.

Findings

Successfully applied to McCarthy's 91 function

Automatically generates simple termination functions for each case

Integrates with the TermiLog system for automation

Abstract

For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system for automatic termination analysis, is presented for showing termination in this case. The method consists of the following steps: First, a finite abstract domain for representing the range of integers is deduced automatically. Based on this abstraction, abstract interpretation is applied to the program. The result is a finite number of atoms abstracting answers to queries which are used to extend the technique of query-mapping pairs. For each query-mapping pair that is potentially non-terminating, a bounded (integer-valued) termination function is guessed. If traversing the pair decreases the value of the termination function, then termination is established. Simple functions often suffice for each query-mapping pair, and that gives our approach an edge over the classical approach of using a single termination function for all loops, which must inevitably be more complicated and harder to guess automatically. It is worth noting that the termination of McCarthy's 91 function can be shown automatically using our method. In summary, the proposed approach is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing a termination proof into several cases, such that a simple termination function suffices for each case. Consequently, the whole process of proving termination can be done automatically in the framework of TermiLog and similar systems.