Inference of termination conditions for numerical loops in Prolog

TL;DR

This paper introduces a novel method for analyzing the termination of numerical loops in Prolog, overcoming traditional challenges posed by the non well-foundedness of integers, and enabling automatic, accurate termination analysis.

Contribution

It presents an innovative technique that combines query-mapping pairs with acceptability frameworks to analyze numerical termination in logic programs.

Findings

The approach successfully analyzes termination of numerical loops in Prolog.

It extends previous constraint-based termination methods.

The technique can be potentially extended with general term orderings.

Abstract

We present a new approach to termination analysis of numerical computations in logic programs. Traditional approaches fail to analyse them due to non well-foundedness of the integers. We present a technique that allows overcoming these difficulties. Our approach is based on transforming a program in a way that allows integrating and extending techniques originally developed for analysis of numerical computations in the framework of query-mapping pairs with the well-known framework of acceptability. Such an integration not only contributes to the understanding of termination behaviour of numerical computations, but also allows us to perform a correct analysis of such computations automatically, by extending previous work on a constraint-based approach to termination. Finally, we discuss possible extensions of the technique, including incorporating general term orderings.