Logic programming with equations

AbstractThis paper is a contribution to the amalgamation of logic programming (as embodied in PROLOG) and functional programming (as embodied in languages like SASL, KRC, HOPE, or in dialects of LISP like LISPKIT LISP or SCHEME). We investigate how equational rewriting, which we assume is an adequate model for functional programming, can be performed within the context of logic programming. The equational program plus the standard equality axioms (reflexivity, symmetry, transitivity, and substitutivity) is our standard of correctness: we regard it as a logic specification from which the result of any evaluation must be a logical consequence. Although the standard equality axioms plus the equations formally qualify as a PROLOG program, their use as such is computationally infeasible because the SLD- resolution search space contains many refutations yielding useless answers and many infinite branches. To obtain feasible evaluations conforming to our standard of correctness, we investigate two approaches: the interpretational one and the compilational one. In the interpretational approach we use as logic program the equations themselves, but replace the standard axioms of equality by suitably chosen logical consequences having the property that the PROLOG interpreter mimics equational rewriting without search. In the compilational approach we obtain an efficient PROLOG program by translating the equations to a set of Horn clauses not involving equality and discarding the equality axioms altogether. We prove correctness for both approaches