An Improved Non-Termination Criterion for Binary Constraint Logic Programs

TL;DR

This paper introduces an improved static non-termination criterion for binary constraint logic programs, enhancing the ability to detect non-terminating queries with a rigorous logical foundation.

Contribution

It presents a generalized non-termination detection criterion for binary CLP clauses, with a formal logical characterization and proof of correctness and completeness.

Findings

The criterion strictly generalizes previous non-termination detection methods.

The logical form of the criterion is proven correct and complete.

It provides a more effective static analysis tool for non-termination in logic programs.

Abstract

On one hand, termination analysis of logic programs is now a fairly established research topic within the logic programming community. On the other hand, non-termination analysis seems to remain a much less attractive subject. If we divide this line of research into two kinds of approaches: dynamic versus static analysis, this paper belongs to the latter. It proposes a criterion for detecting non-terminating atomic queries with respect to binary CLP clauses, which strictly generalizes our previous works on this subject. We give a generic operational definition and a logical form of this criterion. Then we show that the logical form is correct and complete with respect to the operational definition.