Unfolding of Equational Logic Programs

Equational Logic Programming is a programming paradigm which integrates both Equational and Logic Programming (see [10, 11, 14, 15] for surveys on this area). In this paradigm, an equational logic program can be seen as a Conditional Term Rewriting System (CTRS for short), i.e. a set of conditional equations which are implicitely oriented from left to right, and the operational semantics is usually based on some variant of narrowing [17]. The aim of this work is to develop a transformation technique for equational logic programs based on unfolding. In general, program transformation is a method for deriving correct and efficient programs. Unfolding is a well-known program transformation strategy which was first formulated in the case of equational programs by Burstall and Darlington [4] and later introduced in logic programming by Komorowski [13]. The combined effect of unification with simplification is also achieved in [5, 7, 16] by means of some superposition procedure for program synthesis. We want to define an unfolding transformation on equational logic programs which preserves the computed answers substitutions (obtained by narrowing) along the synthesising process. To the best of our knowledge this is the first approach to this problem. At first we might think that a generic unfolding, possibly valid for any narrowing strategy, would simply consist of applying narrowing steps to the right-hand side and the condition of the rules to obtain the unfolded program. However, with this simple method we can lose completeness when the program is not completely defined (even if it is a constructor based canonical TRS). Example 1 Let R be the following program, R = { f(c(X)) → c(f(X)) }. The term c(f(X)) can only be narrowed to c(c(f(Y ))) with substitution {X/s(Y )}. Then we obtain the following unfolded program: Unf(R) = { f(c(c(Y ))) → c(c(f(Y ))) }. Therefore, an equational goal of the form ⇐ f(c(a)) = c(f(a)) is only true w.r.t. the original program. Moreover, the computed answers substitutions (c.a.s.) are not preserved in the unfolding transformation when we use certain narrowing strategies (even if the program is completely defined). Consider the following example which shows how the c.a.s. obtained by basic narrowing [12] are not preserved in the unfolded program. This work has been partially supported by CICYT under grant TIC 92-0793-C02-02. DSIC, Universidad Politecnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020 Valencia, Spain. Dipartimento di Elettronica e Informatica, Universita di Padova, Via Gradenigo 6/A, 35131 Padova, Italy.