A rewrite approach for constraint logic programming

Abstract

Constraint Logic Programming (CLP) is an extension of Logic Programming aimed at replacing the unification mechanism used in Prolog, by a more general operation called constraint satisfaction. This yields a more efficient evaluation process due to the use of appropriate algorithms designed specifically for a given constraint domain. On the other hand, it is known that pure logic programs can be represented as rewrite rules, and executed using a version of Knuth-Bendix completion procedure, called linear completion. Taking advantage of the simplification techniques available with rewriting, linear completion acts as a loopavoiding mechanism, pruning unnecessary computations when possible. A very powerful feature must also be emphasized: for a given query, linear completion may halt with a finite set of simple formulas representing the whole set of answers while the corresponding logic program loops, producing an infinite set of distinct answers: linear completion is a kind of program synthesis mechanism. Our aim is to adapt linear completion to CLP in order to combine the considerable expressiveness of CLP with the operational advantages of linear completion. First, we define how to transform a CLP program into a set of constrained rewrite rules and we propose a precise declarative semantics of such a constrained rewrite program. Next, we give an inference system which defines the new evaluation mechanism and prove its soundness and completeness with regard to our declarative semantics. We also prove that our transformation function is “semantics preserving”: a CLP program and its associated constrained rewrite program have indeed the same declarative semantics. This can be seen as extending the work of M.P Bonacina and J. Hsiang to CLP.