Automatic Termination Inference for Numerical Loops in Prolog

Title: Automatic Termination Inference for Numerical Loops in Prolog

Abstract: This research focuses on automatic termination inference for logic programs that depend on numerical computations. The study investigates the termination behavior of integer computations and proposes two approaches to solve the problem. The first approach involves changing the definition of the level mapping to map atoms to integers, ensuring that the mapping is to some well-founded subset of integers. The second approach, which is presented in the paper, does not require changing the definition of the level mapping. It incorporates techniques from [8] and the well-known framework of acceptability with respect to a set, providing a better understanding of termination behavior and enabling automatic analysis.

Main Research Question: How can we automatically infer termination conditions for numerical loops in Prolog?

Methodology: The study employs a transformation that allows for the automatic definition of level mappings. It uses an example to illustrate the process and then presents it more formally. The transformation incorporates techniques from [8] and the framework of [5,6].

Results: The research presents an algorithm that implements the termination inference, proving termination of programs depending on numerical computations.

Implications: The findings of this research have practical implications, as they enable the automatic analysis of termination inference for logic programs that depend on numerical computations. This can lead to more efficient and accurate programs, benefiting the wider Prolog community and beyond.

Related Work: The study reviews related work, including [7], and concludes that the proposed approach provides a better understanding of termination behavior and enables automatic analysis.

Link to Article: https://arxiv.org/abs/0110034v1 Authors: arXiv ID: 0110034v1