Inferring Left-terminating Classes of Queries for Constraint Logic Programs

This paper presents an approach for universal left-termination of constraint logic programs, based on approximations. An approximation is basically an algebraic morphism between two constraint structures. By moving from the original domain to natural numbers, we compute inter-argument relations and some control information about a program. By moving from the natural numbers to the booleans, we compute a boolean term called a termination condition such that if the boolean approximation of a goal entails the termination condition, then the Prolog computation tree for that goal is finite.