Declarative Compilation for Constraint Logic Programming

Abstract. We present a new declarative compilation of logic programs with constraints into variable-free relational theories which are then exe-cuted by rewriting. This translation provides an algebraic formulation of the abstract syntax of logic programs. Management of logic variables, unification, and renaming apart is completely elided in favor of alge-braic manipulation of variable-free relation expressions. We prove the translation is sound, and the rewriting system complete with respect to traditional SLD semantics