Partial evaluation of functional logic programs

Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution principle of logic languages. In this article, we present a partial evaluation scheme for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. The method is formalized within the theoretical framework established by Lloyd and Shepherdson for the partial deduction of logic programs, which we have generalized for dealing with functional computations. A generic specialization algorithm is proposed which does not depend on the eager or lazy nature of the narrower being used. To the best of our knowledge, this is the first generic algorithm for the specialization of functional logic programs. We study the semantic properties of the transformation and the conditions under which the technique terminates, is sound and complete, and is generally applicable to a wide class of programs. We also discuss the relation to work on partial evaluation in functional programming, term-rewriting systems, and logic programming. Finally, we present some experimental results with an implementation of the algorithm which show in practice that the narrowing-driven partial evaluator effectively combines the propagation of partial data structures (by means of logical variables and unification) with better opportunities for optimization (thanks to the functional dimension).