Specialization of Lazy Functional Logic Programs^{∗}

M. Alpuente^{‡}  M. Falaschi^{§}  P. Julián^{¶}  G. Vidal^{‡}

‡ DSIC, UPV, Camino de Vera s/n, 46071 Valencia, Spain. E-mail: {alpuente,gvidal}@dsic.upv.es.

§ Dip. Matematica e Informatica, Via delle Scienze 206, 33100 Udine, Italy. E-mail: falaschi@dimi.uniud.it.

¶Dep. de Informática, Ronda de Calatrava s/n, 13.071 Ciudad Real, Spain. E-mail: pjulian@inf-cr.uclm.es.

Abstract

Partial evaluation is a method for program specialization based on fold/unfold transformations [8, 25]. Partial evaluation of pure functional programs uses mainly static values of given data to specialize the program [15, 44]. In logic programming, the so-called static/dynamic distinction is hardly present, whereas considerations of determinacy and choice points are far more important for control [12]. We discuss these issues in the context of a (lazy) functional logic language. We formalize a two-phase specialization method for a non-strict, first order, integrated language which makes use of lazy narrowing to specialize the program w.r.t. a goal. The basic algorithm (first phase) is formalized as an instance of the framework for the partial evaluation of functional logic programs of [2, 3], using lazy narrowing. However, the results inherited by [2, 3] mainly regard the termination of the PE method, while the (strong) soundness and completeness results must be restated for the lazy strategy. A post-processing renaming scheme (second phase) is necessary which we describe and illustrate on the well-known matching example. This phase is essential also for other nonlazy narrowing strategies, like innermost narrowing, and our method can be easily extended to these strategies. We show that our method preserves the lazy narrowing semantics and that the inclusion of simplification steps in narrowing derivations can improve control during specialization.

Keywords: integration of functional and logic programming, term rewriting systems, lazy narrowing, partial evaluation, post-processing renaming.

1 Introduction

Many proposals for the integration of functional and logic programming are based on narrowing (see [18] for a recent survey). Narrowing is a natural extension of the evaluation mechanism of functional languages to incorporate unification. Narrowing solves equations by computing unifiers w.r.t. an equational theory usually described by means of a (conditional) term rewriting system. In order to avoid useless computations and to deal with nonterminating and nonstrict functions, lazy narrowing strategies have recently been proposed [4, 29, 35, 39]. One main advantage of an integrated functional logic language is the reduction of the search space by exploiting functional computations. Hence, an important improvement of (lazy) narrowing is the incorporation of deterministic simplification steps which can largely reduce both run time and search space in comparison to pure logic programs, since normalization can avoid the creation of useless choice points in sequential implementations [17, 18].

Program specialization refers to the technique of how to derive a specialized instance of a program to a restricted set of inputs. Particular cases include Partial Evaluation (PE) of functional [25] and logic [12, 34] programs. PE of functional programs, as in [25], is usually restricted to constant (static values) propagation, whereas PE techniques for logic languages exploit unification-based information propagation, which results in more powerful transformations. The basic technique for PE of logic programs was presented in [12]. Turchin’s driving transformation for functional programs achieves the same effect as the PE of logic programs, by virtue of unification [15, 45, 46].

The PE of functional logic languages is a relatively new area of research. As far as we know, [2, 3] formalize the first PE scheme for functional logic languages which can improve the original program w.r.t. the ability of computing the set of answer substitutions. In contrast to the approach usually taken with pure functional languages, in [2] we use the unification-based computation mechanism of narrowing for the specialization of the program as well as for the execution. The basic PE algorithm is parametric w.r.t. the narrowing strategy which is used for the automatic construction of (finite) narrowing trees. We have defined the notions of closedness and independence that are essential to prove the computational equivalence of the original and the partially evaluated programs, for a restricted set of goals. We have proved that these conditions suffice for correctness in the case of unrestricted narrowing. An appropriate abstraction operator is also introduced which guarantees termination of the PE process. However, the independence condition which guarantees that the derived program does not produce additional answers is not obtained automatically and, for some particular narrowing strategies, the partially evaluated program might not satisfy the restrictions on the theories which are necessary for the completeness of the strategy.

In this paper, we formalize a call-by-name partial evaluator for functional logic languages with a lazy narrowing semantics like that of [39]. Then, we formalize a renaming transformation of the residual program, which removes any remaining lack of independence. This is a post-processing stage whereby new function symbols are introduced and a transformed program and goal are obtained. We prove that, for the renamed queries, the transformed program computes the same answers as the original program. We note that the post-processing phase is also crucial to guarantee the correctness of the whole process. In general, the partially evaluated program resulting from the PE phase might not satisfy one of the basic assumptions for the completeness of lazy narrowing (the so-called ‘constructor discipline’), which may prevent the lazy strategy from being able to narrow a goal in the partially evaluated program. As a rough example, consider the following

∗This work has been partially supported by CICYT TIC 95-0433-C03-03 and by HCM project CONSOLE.

Example 1 Consider the program R ≡ {f(x) → x} which derives the residual program R′:

\begin{aligned}f(0) & → & 0 \\ f(f(x)) & → & x \end{aligned}

when specialized w.r.t. the function calls f(f(x)) and f(0). This program contains a nested function application f(f(x)). Also, the considered set of specialized calls {f(0), f(f(x))} is not independent, since it contains two different pairs of interfering calls, namely f(0) with f(x) and f(x) with f(f(x)).

The post-processing phase generates a constructor based program, i.e., no left-hand side argument contains a defined function symbol, and the renamed set of calls is independent. Our method is also useful for non lazy narrowing strategies, such as innermost narrowing. Also in this case the resulting program must be constructor based. The extension of our method is easy [1].

Our method passes the so-called Knuth-Morris-Pratt test [15, 24], i.e. the specialization of a naïve pattern matcher w.r.t. a fixed pattern essentially obtains the efficiency of the Knuth, Morris and Pratt matching algorithm [27].

We show that the inclusion of a normalization process between narrowing steps not only saves time and space but also yields a better optimization strategy which does not increase the size of the program since no choices are unfolded. We show that, by using normalization, it is possible to improve the ability to eliminate intermediate data structures with a narrowing-based partial evaluator. We also prove that the partial evaluator can achieve in a principled, non ad-hoc way, the same transformation effect as some (postunfolding) techniques that eliminate intermediate functions in the driving approach to program specialization [15, 42, 43]. The preference for deterministic computations is a good heuristic to avoid code explosion which is also comparable to the determinism-based criterium of [13] that explores maximal deterministic paths.

1.1 Plan of the Paper

The structure of the paper is as follows. Basic definitions are given in Section 2. Section 3 recalls the general scheme for the PE of functional logic languages of [2]. In Section 4, a two-phase specialization method is described and shown to be correct. Section 5 discusses the related work and Section 6 concludes. More details and missing proofs can be found in [1].

2 Preliminaries

We briefly recall some known results about rewrite systems and functional logic programming [10, 18, 21, 26]. Throughout this paper, V will denote a countably infinite set of variables and Σ denotes a set of function symbols f/n, each with a fixed associated arity n. τ(Σ ∪ V) and τ(Σ) denote the sets of terms and ground terms built on Σ and V, respectively. We assume that the alphabet Σ contains some primitive symbols, including at least the nullary constructor true and a binary equality function symbol, say =, written in infix notation, which allows us to interpret equations s = t as terms, with s, t ∈ τ(Σ ∪ V). The term true is also considered an equation. Terms are viewed as labeled trees in the usual way. Occurrences are represented by sequences, possibly empty, of natural numbers used to address subterms of t, and they are ordered by the prefix ordering: u ≤ v if there exists w such that uw = v. We let Λ denote the empty sequence. O(t) denotes the set of occurrences of a term t. O_{V}(t) and Ō(t) denote the set of variable occurrences and nonvariable occurrences of the term t, respectively. t_{|u} is the subterm at the occurrence u of t. t[r]_{u} is the term t with the subterm at the occurrence u replaced with r. These notions extend to sequences of equations in a natural way. For instance, the nonvariable occurrence set of a sequence of equations g ≡ (e_{1}, …, e_{n}) can be defined as follows: Ō(g) = {i.u | u ∈ Ō(e_{i}), i = 1, …, n}. Identity of syntactic objects is denoted by ≡. Var(s) is the set of distinct variables occurring in the syntactic object s.

We restrict our interest to the set of idempotent substitutions over τ(Σ ∪ V), which is denoted by Sub. The identity function on V is called the empty substitution and denoted ϵ. In abuse of notation, Dom(σ) = {x ∈ V | xσ ≢ x} is called the domain of σ and Cod(σ) = {xσ | x ∈ Dom(σ)} is called the codomain of σ. Given a substitution θ and a set of variables W ⊆ V, we denote by θ_{|` W} the substitution obtained from θ by restricting its domain, Dom(θ), to W. We write θ = γ [W] if xθ = xγ ∀x ∈ W. We consider the usual preorder on substitutions ≤: θ ≤ σ iff ∃γ.σ ≡ θγ. This preorder induces a partial (pre-)ordering on terms given by: t ≤ t′ iff ∃γ. t′ ≡ tγ. The equational representation of a substitution θ = {x_{1}/t_{1}, …, x_{n}/t_{n}} is the set of equations θ̂ = {x_{1} = t_{1}, …, x_{n} = t_{n}}. A substitution θ is a unifier of an equation set E iff θ̂ ⇒ E. A set of equations E is unifiable, if there exists ϑ ∈ Sub such that for all s = t in E. sϑ ≡ tϑ. ϑ is called a unifier of E. We let mgu(E) denote the most general unifier of the equation set E (see, e.g., [30]). A renaming is a substitution ρ for which there exists the inverse ρ^{−1} such that ρρ^{−1} ≡ ρ^{−1}ρ ≡ ϵ. Two terms t and t′ are variants (of each other), if there exists a renaming ρ such that tρ ≡ t′. A generalization of the nonempty set of terms {t_{1}, …, t_{n}} is a pair ⟨t, {θ_{1}, …, θ_{n}}⟩ such that, for all i = 1, …, n, tθ_{i} = t_{i}. The pair ⟨t, Θ⟩ is the most specific generalization (msg) of a set of terms S, written ⟨t, Θ⟩ = msg(S), if 1) ⟨t, Θ⟩ is a generalization of S, and 2) for every other generalization ⟨t′, Θ′⟩ of S, t′ is more general than t (i.e. t′ ≤ t). The msg of a set of terms is unique up to variable renaming.

An equational Horn theory E consists of a finite set of equational Horn clauses of the form e ⇐ C. The head e is an equation (λ = ρ) and the condition C is a (possibly empty) sequence e_{1}, …, e_{n}, n ≥ 0, of equations. Variables in C or ρ that do not occur in λ are called extra-variables. An equational goal is an equational Horn clause with no head. We let Goal denote the set of equational goals. We often leave out the ⇐ symbol when we write goals.

Each equational Horn theory E generates a smallest congruence relation =_{E} called E-equality on the set of terms τ(Σ∪V) (the least equational theory which contains all logic consequences of E under the entailment relation ⊧ obeying the axioms of equality for E). E is a presentation or axiomatization of =_{E}. In abuse of notation, we sometimes speak of the equational theory E to denote the theory axiomatized by E. Given two terms s and t, we say that they are E-unifiable iff there exists a substitution σ such that sσ =_{E} tσ. The substitution σ is called an E-unifier of s and t. By abuse of notation, it is often called solution. E-unification is semidecidable. Given a set of variables W ⊆ V, E-equality is extended to substitutions in the standard way, by σ =_{E} θ [W] iff xσ =_{E} xθ ∀x ∈ W. W will be omitted if equal to V. We say σ is an E-instance of σ′ and σ′ is more general than σ on W, in symbols σ′ ≤_{E} σ [W] iff (∃ρ) σ =_{E} σ′ρ [W]. A set S of E-unifiers of the equation set E is complete iff every E-unifier σ of E factors into σ =_{E} θγ [Var(E)] for some substitutions θ ∈ S and γ. A complete set of E-unifiers of a system of equations may be infinite.

A Conditional Term Rewriting System (CTRS for short) is a pair (Σ, R), where R is a finite set of reduction (or rewrite) rule schemes of the form r ≡ (λ → ρ ⇐ C), λ, ρ ∈ τ(Σ ∪ V), λ ∉ V and Var(ρ) ⊆ Var(λ). The reduction rule r is left–linear if λ is a linear term, i.e. no variable occurs twice or more in λ. If a rewrite rule has no condition we write λ → ρ. We will often write just R instead of (Σ, R).

Operationally, equational Horn clauses will be used as conditional rewrite rules. A term s conditionally rewrites to a term t, written s →_{R} t, if there exists u ∈ O(s), (λ → ρ ⇐ s_{1} = t_{1}, …, s_{n} = t_{n}) ∈ R and substitution σ such that s_{|u} = λσ, t = s[ρσ]_{u} and ∀i. 1 ≤ i ≤ n. ∃w_{i} such that s_{i}σ →_{R}^{∗} w_{i} _{R}^{∗}← t_{i}σ. The CTRS R is said to be confluent if, for all terms s, t_{1}, t_{2} with t_{1} _{R}^{∗} ← s →_{R}^{∗} t_{2}, there exists a term t_{3} such that t_{1} →_{R}^{∗} t_{3} _{R}^{∗}← t_{2}. R is weak orthogonal if each rule of R is left–linear and R contains only trivial critical pairs. R is normal if the terms t_{1}, …, t_{n} in the condition s_{1} = t_{1}, …, s_{n} = t_{n} of each program rule are ground normal forms w.r.t. the unconditional part of the CTRS. Weakly orthogonal normal CTRSs are confluent [6, 26]. A term s is a normal form, if there is no term t with s →_{R} t. We let s ↓ denote the normal form of s. A substitution σ is normalized, if xσ is a normal form for all x ∈ Dom(σ). For CTRS R, r < < R denotes that r is a new variant of a rule in R such that r contains no variable previously met during computation (standardised apart). A CTRS is decreasing if there exists a well-founded extension ≻ of the rewrite relation →_{R} with the following properties: 1) ≻ has the subterm property, i.e. t ≻ t_{|u} for all u ∈ O(t) − {Λ}, and 2) if (λ → ρ ⇐ C) ∈ R and σ is a substitution, then λσ ≻ ρσ and λσ ≻ sσ, λσ ≻ tσ for all s = t in C (roughly speaking, in each conditional equation used for rewriting, the rhs and the condition terms must be smaller than the lhs w.r.t. some termination ordering).

A function symbol f ∈ Σ is irreducible iff there is no rule (λ → ρ ⇐ C) ∈ R such that f occurs as the outermost function symbol in λ, otherwise it is a defined function symbol. In theories where the above distinction is made, the signature Σ is partitioned as Σ = C ⨄ F, where C is the set of irreducible (constructor) function symbols and F is the set of defined function symbols or operations. The terms in τ(C ∪ V) are called constructor terms. A substitution σ is (ground) constructor, if xσ is (ground) constructor for all x ∈ Dom(σ).

Narrowing Semantics

The computation mechanism of functional logic languages is based on narrowing, an evaluation mechanism that uses unification for parameter passing [40]. Narrowing solves equations by computing unifiers with respect to a given CTRS (which is called the ‘program’). Given a CTRS R, an equational goal g conditionally narrows into a goal clause g′

(in symbols g ⇝^{[u,r,θ]} g′, g ⇝^{[u,θ]} g′ or simply g ⇝^{θ} g′), if there exists an occurrence u ∈ Ō(g), a standardised apart variant r ≡ (λ → ρ ⇐ C) < < R and a substitution θ such that θ = mgu({g_{|u} = λ}) and g′ = (C, g[ρ]_{u})θ. s is called a (narrowing) redex (reducible expression) iff there exists a new variant (λ → ρ ⇐ C) of a reduction rule in R and a substitution σ such that sσ ≡ λσ. A redex t_{|u} is an outermost redex if there is no redex t_{|u′} of t with u′ ≤ u. A narrowing derivation for g in R is defined by

g ⇝^{θ ∗} g′ iff ∃θ_{1}, …, θ_{n}. g ⇝^{θ_{1}} … ⇝^{θ_{n}} g′ and θ = θ_{1} … θ_{n}.

We say that the derivation has length n. If n = 0, then θ = ϵ. In order to treat syntactical unification as a narrowing step, we add the rule (x = x → true), x ∈ V, to the CTRS R. Then s = t ⇝^{σ} true holds iff σ = mgu({s = t}). We use ⊤ as a notation for sequences of the form true, …, true. A successful derivation for g in R is a narrowing derivation g ⇝^{θ ∗} ⊤, and θ_{|` Var(g)} is called a computed answer substitution (c.a.s.) for g in R. The narrowing derivations can be represented by a (possibly infinite) finitely branching tree. A failing leaf is a goal which is not ⊤ and which cannot be further narrowed. Following [34], we adopt the convention in this paper that any derivation is potentially incomplete (a branch thus can be failed, incomplete, successful or infinite). A narrowing algorithm is complete if it generates a complete set of E-unifiers for all input equation systems. Formally, (a kind of) narrowing is complete for (a class of) CTRS’s if the following condition holds: If sσ =_{E} tσ, then there exists a narrowing derivation s = t ⇝^{θ ∗} ⊤ such that θ ≤_{E} σ[Var(s)∪Var(t)]. It is well-known that the subscript E in θ ≤_{E} σ can be dropped if we only consider completeness w.r.t. normalized substitutions [37]. Conditional narrowing has been shown to be a complete E-unification algorithm for theories satisfying different restrictions [18, 21, 37].

Since unrestricted narrowing has quite a large search space, several strategies to control the selection of redexes have been devised to improve the efficiency of narrowing by getting rid of some useless derivations. A narrowing strategy (or position constraint) is any well-defined criterion which obtains a smaller search space by permitting narrowing to reduce only some chosen positions, e.g. basic [22], innermost [11], innermost basic [21] or lazy narrowing [40]. The innermost and the lazy strategies mimic the strict and lazy evaluation known from functional programming languages. Formally, a narrowing strategy φ is a mapping that assigns to every goal g (different from ⊤) a set of triples [4]. If ⟨u, r, σ⟩ ∈ φ(g), then u ∈ Ō(g), r < < R, and σ is a sub-

stitution such that g ⇝^{[u,r,σ]} g′. An important property of a narrowing strategy φ is completeness, meaning that the narrowing constrained by φ is still complete. A survey of results about the completeness of narrowing strategies can be found in [18].

In the case of a confluent and decreasing CTRS R, we can further improve narrowing without losing completeness by normalizing the goal before a narrowing step is applied [23]. It is useful to apply rewriting between narrowing steps, whenever it is possible, since rewriting may reduce an infinite search space to a finite one and can save a lot of time and space [18]. A normalizing conditional narrowing step w.r.t. R, is given by a normalization g →_{R}^{∗} g↓ followed by a narrowing step g↓⇝^{σ} g′. The idea of exploiting deterministic computations by including normalization has been applied to almost all narrowing strategies, e.g. basic [21, 41], innermost [11], innermost basic [21], and lazy narrowing [17].

Lazy narrowing reduces expressions at outermost narrowable positions. Narrowing at inner positions is performed only if it is demanded (by the pattern in the lhs of some rule) and contributes to some later narrowing step at an outer position. Since the notion of “demanded position” is not unique, different lazy narrowing strategies have been proposed [4, 29, 35, 39, 40] (although some lazy strategies are “lazier” than others). In the following, we specify our lazy narrowing strategy, similar to [39].

Lazy Narrowing

The following definitions are necessary for our formalization of lazy narrowing. An pattern t is an operation applied to constructor terms, i.e. t = f(t_{1}, …, t_{k}), where f ∈ F and, for all i = 1, …, k, t_{i} ∈ τ(C ∪ V). A CTRS is constructorbased (CB) if the left-hand side (lhs) of each rule is a pattern. It implies that there can be neither functional nestings on the lhs of the head of the clauses nor equations between constructors. This is a reasonable class from the functional programming point of view. Many functional logic languages follow this discipline, e.g. ALF [16], Babel [39], K-LEAF [14], LPG [7], and SLOG [11]. A head normal form is a variable or a constructor-rooted term. In CB normal programs, each condition s = t in the body of a program rule has the property that t is ground constructor [19]. We assume that these conditions hold for all programs we consider in this paper. This requirement is also made in Babel and K-LEAF. In practice, this is not a real restriction, since we can provide an explicit definition of a boolean–valued equality function ≈ between constructor terms and consider that an equation s ≈ t in a condition of a CB normal CTRS denotes the equation (s ≈ t) = true [19].

The unification of redexes of the goal with lhs’s of program rules gives rise to the following particular kind of unification problems.

Definition 2.1 (linear unification problem) A linear unification problem is a pair of terms:

⟨f(d_{1}, …, d_{n}), f(t_{1}, …, t_{n})⟩, where f(d_{1}, …, d_{n}) and f(t_{1}, …, t_{n}) do not share variables, and the term f(d_{1}, …, d_{n}) is linear and innermost.

Linear unification problems can be solved by any version of the unification algorithm (see, e.g., [30]). Following [39], we distinguish the case when an attempted unification does not succeed because of a clash between a constructor c and an operation f, since such a situation can be thought of as a demand of further evaluation of f. This differs from the standard syntactic unification algorithm [30]. The following is a reformulation of the unification algorithm for linear unification problems of [39].

Definition 2.2 (LU configuration) An LU configuration is a pair (U, σ), where U is a set and σ is a substitution.

The following definition adapts the standard syntactic unification algorithm [30] to the linear unification case. Because of linearity, an occur-check is not needed.

Definition 2.3 (unification relation →_{LU})

We define the unification relation →_{LU} between LU configurations as the smallest relation satisfying:

1. ({c(d_{1}, …, d_{m}) ↓_{u} c(t_{1}, …, t_{m})} ∪ U, σ)
→_{LU} ({d_{1} ↓_{u.1} t_{1}, …, d_{m} ↓_{u.m} t_{m}} ∪ U, σ),
where (c/m) ∈ C, m ≥ 0.
2. ({x ↓_{u} t} ∪ U, σ) →_{LU} (U{x/t}, σ{x/t}),
where t ∉ V.
3. ({d ↓_{u} x} ∪ U, σ) →_{LU} (U{x/d}, σ{x/d}).
4. ({c(d_{1}, …, d_{m}) ↓_{u} c′(t_{1}, …, t_{p})} ∪ U, σ)
→_{LU} ({fail}, σ),
where (c/m), (c′/p) ∈ C, c ≢ c′, and m, p ≥ 0.

Definition 2.4 (initial LU configuration)

Let ⟨f(d_{1}, …, d_{n}), f(t_{1}, …, t_{n})⟩ be a linear unification problem. The initial LU configuration is: (U_{0}, σ_{0}) ≡ ({d_{1} ↓_{1} t_{1}, …, d_{n} ↓_{n} t_{n}}, ϵ).

Linear unification (LU) can either succeed, fail or suspend. When it suspends, it returns the set of positions which “demand” further evaluation. Formally, given a LU configuration (U, σ), a position u is demanded, if (c(d_{1}, …, d_{m}) ↓_{u} g(t_{1}, …, t_{p})) ∈ U.

Definition 2.5 (behaviour of →_{LU})

Let Γ ≡ ⟨f(d_{1}, …, d_{n}), f(t_{1}, …, t_{n})⟩ be a linear unification problem. Let (U_{0}, σ_{0}) ≡ ({d_{1} ↓_{1} t_{1}, …, d_{n} ↓_{n} t_{n}}, ϵ) →LU^{∗} (U, σ)↛_{LU}. We define the function LU(Γ) as follows:

LU(Γ) = \{ \begin{matrix}(Succ, σ) & if U = ∅ \\ (Fail, ∅) & if U = \{fail\} \\ (Demand, P) & otherwise, where P is the set \\ & of demanded positions \end{matrix}

Let us define a lazy narrowing strategy (φ_{▶}) as follows. Roughly speaking, in the following definition, the set-valued function φ_{▶}(g) returns the set of triples (u, k, σ) such that u ∈ Ō(g) is a demanded position of g which can be narrowed by the rule r_{k} with narrowing substitution σ. We assume the rules of R to be numbered with r_{1}, …, r_{m}.

Definition 2.6 (lazy narrowing strategy) We define a lazy narrowing strategy φ_{▶} : Goal → ℘(IN^{∗} × IN × Sub) which, for a given goal g ≡ (e_{1}, …, e_{n}), computes the set of triples ⟨u, k, σ⟩, with u ∈ Ō(g), k a natural number (indicating the program rule r_{k}) and σ a substitution, as follows:

φ_{▶}(g)  = φ (g, i),

where i = select don′t care({1, …, n})

φ (g, u)  = ⋃_{k=1}^{m} φ (g, u, k)
φ (g, u, k) = if λ_{k}[Λ] ≡ g[u] then

case LU(⟨λ_{k}, g_{|u}⟩) of

\begin{cases}(Succ, σ) : & \{(u, k, σ)\} \\ (Fail, ∅) : & ∅ \\ (Demand, P) : & ⋃_{u′∈P} φ (g, u.u′) \end{cases}

else ∅

where r_{k} ≡ (λ_{k} → ρ_{k} ⇐ C_{k}) < < R and the “choice” function select don′t care(S) arbitrarily chooses one element of the set S accordingly to some fixed criterium.

Our lazy strategy is essentially equivalent to the demand driven reduction mechanism formalized in [39], where sequences of equations are interpreted as terms by defining the boolean conjunction operation ‘,’ as a binary predefined symbol (whose rules are implicitly added to the program). As opposed to [39], our lazy narrowing calculus manipulates sequences of equations rather than terms, as in other lazy narrowing calculi (e.g. [21]).

We would like to note that there are three sources of nondeterminism in our narrowing calculus: the choice of the equation, given by i, the choice of the subterm, given by u, and the choice of the program rule, given by k. The last two choices are don’t-know nondeterministic, meaning that in general all possible choices have to be considered to ensure completeness. Only the choice of the equation is don’t-care nondeterministic. In general, for the selected equation, the set of lazy redexes is not a singleton, and all such redexes have to be narrowed (trying to apply all program rules to each one) to guarantee completeness.

Definition 2.7 (lazy conditional narrowing) We define lazy conditional narrowing as a labeled transition system (Goal, Sub, ⇝_{▶}) whose transition relation ⇝_{▶}⊆ (Goal× Sub × Goal) is the smallest relation which satisfies:

\frac{(u, k, σ) ∈ φ_{▶}(g) ∧ r_{k} ≡ (λ → ρ ⇐ C) < < R}{g ⇝_{▶}^{σ} (C, g[ρ]_{u})σ}

Similarly to the formalization of [39], our calculus allows some narrowing derivations that do not contribute to any later steps. It is not difficult to strengthen the demand driven nature of our strategy by somehow forcing the use of the rule that demands evaluation of a suspended argument [18, 29, 35, 39]. [4] presents an optimal lazy narrowing strategy (for a restricted class of programs) which avoids superfluous steps by dropping the restriction to mgu’s. Since these types of optimizations are not relevant to the subject of this paper, we do not consider them here for the sake of simplicity.

Due to the presence of nonterminating functions, completeness results for lazy narrowing are stated w.r.t. a nonstandard interpretation of equality. Functional logic languages with a lazy narrowing operational semantics define the validity of an equation as a strict equality ≈ on terms. Strict equality regards two terms as equal iff they have the same ground constructor normal form. The semantics of ≈ is defined by the following set StrEq of confluent CB rules: StrEq = {c(x_{1}, …, x_{n}) ≈ c(y_{1}, …, y_{n}) → true ⇐ x_{1} ≈ y_{1}, …, x_{n} ≈ y_{n} | (c/n) ∈ C, n ≥ 0}. Note that strict equality does not have the reflexivity property t ≈ t for all terms t. When we consider lazy narrowing, we assume that the equality symbol in the goal (and in the conditions of program rules) is ≈.

In weakly orthogonal, CB programs, lazy narrowing is complete w.r.t. StrEq for constructor substitutions:

Proposition 2.8 [18, 39] Let R be a weakly orthogonal, CB program, g be a goal and σ be a (ground constructor) substitution such that, for all s = t in g, there exists a ground constructor term u s.t. sσ →_{R}^{∗} u and tσ →_{R}^{∗} u. Then, there is a c.a.s. θ of (R ∪ StrEq) ∪ {g} using ⇝_{▶}, and a substitution γ such that θγ = σ[Var(g)].

In [17], Hanus showed how deterministic (lazy) simplification steps can be performed between nondeterministic (lazy) narrowing steps without loosing completeness. Roughly speaking, in the presence of nonterminating functions, only a terminating subset of the program rules is used for simplification^{1}. Example 3 in Section 4 shows how the integration of simplification into (lazy) narrowing derivations is not only a main source for speedups but can also strengthen the specialization, with the added benefit that the optimization is ‘compiled-in’ in the program.

3 Partial Evaluation of Functional Logic Programs

In this section, we recall a generic procedure for the PE of functional logic programs which appeared in [2]. Our algorithm is generic w.r.t. 1) the narrowing relation that constructs search trees, 2) the unfolding rule which determines when and how to terminate the construction of the trees, and 3) an abstraction operator used to guarantee the finiteness of the PE process. We let ⇝_{φ} denote a generic (possibly normalizing) narrowing relation which uses the narrowing strategy φ. The definitions of this section are quoted from [2].

Definition 3.1 (resultant)

Let R be a program and s = y an equation, where the variable y ∉ Var(s). Let [(s = y) ⇝_{φ}^{θ ∗} g, e] be a derivation in R. Let σ = mgu(e). Then the resultant of the derivation is: ((s → y)θ ⇐ g)σ.

Example 2 Let the rule (f(x) → x ⇐ a ≈ x, b ≈ x) be in R. The resultant of the lazy narrowing derivation:

1. [f(z) ≈ y ⇝_{▶}^{{z/x}} a ≈ x, b ≈ x, x ≈ y] is the rule: f(y) → y ⇐ a ≈ y, b ≈ y. Note that, without applying the mgu σ = {x/y} (σ = {y/x}) of the last equation x ≈ y, we would have obtained the rule: f(x) → y ⇐ a ≈ x, b ≈ x, x ≈ y, which contains an extra-variable y in the rhs of the head.

2. [f(z) ≈ y ⇝_{▶}^{{z/x}} a ≈ x, b ≈ x, x ≈ y ⇝_{▶}^{{x/a}} true, b ≈ a, a ≈ y] is: f(a) → a ⇐ true, b ≈ a.

A PE is derived by extracting rules from non–failing, root–to–leaf paths in a narrowing tree.

Definition 3.2 (partial evaluation of a term)

Let τ be a finite (possibly incomplete) narrowing tree for the goal s = y (y ∉ Var(s)) in the program R containing at least one nonroot node. Let {g_{i} | i = 1, …, k} be the nonfailing leaves of τ and R′ = {r_{i} | i = 1, …, k} the resultants associated with the derivations {(s = y) ⇝_{φ}^{σ_{i} +} g_{i} | i = 1, …, k}. Then, R′ is a PE of s in R (using τ).

The above definition lifts in the natural way to partial evaluation of a set of terms S (which are considered modulo variants). A partial evaluation of an equational goal s_{1} = t_{1}, …, s_{n} = t_{n} in R is the partial evaluation in R of the set {s_{1}, t_{1}, …, s_{n}, t_{n}}.

Following [34], we introduce a closedness condition which guarantees that all calls which might occur during the execution of the resulting program are covered by some program rule. The function terms(O) extracts the terms appearing in the syntactic object O.

1In the conditional case, the additional requirement for decreasing rules is needed [18].

Definition 3.3 (closedness) Let S and T be two finite sets of terms. We say that T is S-closed if closed(S, T), where the predicate closed is defined inductively as follows: closed(S, O) ⇔

true if O ≡ Ø or O ≡ x ∈ V closed(S, t_{1}) ∧ … ∧ closed(S, t_{n})

if O ≡ {t_{1}, …, t_{n}}

closed(S, {t_{1}, …, t_{n}})

if O ≡ c(t_{1}, …, t_{n}), c ∈ C

(∃s ∈ S. sθ = O) ∧ closed(S, terms(θ̂)) if O ≡ f(t_{1}, …, t_{n}), f ∈ F

We say that a program R is S-closed if closed(S, terms(R)).

Now we introduce an independence condition which guarantees that the derived program R′ does not produce additional answers. In the case of pure logic programming, only (pairwise) non-unifiability of the partially evaluated calls (atoms) in S is required for ensuring the independence of the resultant procedures thus guaranteeing the strong correctness of the transformation. We need a more involved condition. Namely, we have to consider overlaps among the specialized calls (see [3]).

Definition 3.4 (overlap) A term s overlaps a term t if there is a nonvariable subterm s_{|u} of s such that s_{|u} and t unify. If s ≡ t, we require that t be unifiable with a proper nonvariable subterm of s.

Definition 3.5 (independence) A set of terms S is independent if there are no terms s and t in S such that s overlaps t.

Given a goal g and a program R, in general, there exists an infinite number of different partial evaluations of g in R. A fixed rule for generating resultants called an unfolding rule is used, which ensures that infinite unfolding is not attempted.

Definition 3.6 (unfolding rule) An unfolding rule U_{φ} is a function which, when given a program R, a term s and a narrowing relation ⇝_{φ}, returns a finite set of resultants U_{φ}(s, R) that is a partial evaluation of s in R using ⇝_{φ}.

This definition lifts naturally to a set of terms S.

Starting with the set of calls (terms) which appear in the initial goal g, we partially evaluate them by using a finite unfolding strategy, and recursively specialize the terms which are introduced dynamically during this process. Assuming that it terminates, the procedure computes a set of partially evaluated terms S′ and a set of rules R′ (the PE of S′ in R) such that the closedness condition for R′ ∪ {g} is satisfied.

We let c[S] ∈ State denote a generic configuration whose structure is left unspecified as it depends on the specific PE algorithm, but which includes at least the set of partially evaluated terms S. When S is clear from the context, c[S] will simply be denoted by c.

Definition 3.7 (PE transition relation ⟼_{P}) We define the PE relation ⟼_{P}⊆ State × State as the smallest relation satisfying:

\frac{R′ = U_{φ}(S, R)}{c[S] ⟼_{P} abstract(c[S], terms(R′))}

where the function abstract(c, T) extends the current configuration c with (an abstraction of) the set of terms T which are not closed w.r.t. S, giving a new PE configuration.

Similarly to [36], applying abstract in every iteration allows us to tune the control of polyvariance as much as needed. Also, it is within the abstract operator that the progress towards termination resides.

Definition 3.8 (behaviour of the ⟼_{P} calculus) Let c_{0} be the “empty” PE state. We define the function: P(R, g) = S if abstract(c_{0}, terms(g)) ⟼_{P}^{∗} c[S] and c[S] ⟼_{P} c[S].

The PE procedure in Definition 3.8 computes the set of partially evaluated terms S which unambiguously determines its associated PE R′ in R (using U_{φ}).

4 A Call-by-Name Partial Evaluator

In this section, we formulate an instance of the generic PE procedure introduced in Definition 3.8 and show how it works. We consider the (normalizing) lazy conditional narrowing ⇝_{▶} of Section 2 to construct search trees. We define a hnf-PE R′ of s in R as a PE of s in R such that each derivation used to build R′ has the form [(s ≈ y) ⇝_{▶}^{θ ∗} g, (s′ ≈ y)], where the equality symbol of the original equation is not narrowed using the rules StrEq. This restriction avoids the term s to be evaluated beyond the form possibly demanded by a context.

In [2], we have developed a rather simple criterium for avoiding looping. Our strategy is based on the intuitive notion of orderings in which a term that is “syntactically simpler” than another is smaller than the other. The following definition extends the homeomorphic embedding (“syntactically simpler”) relation [10] to nonground terms. In [31], an extension of this relation is defined which provides a finer handle of variables.

Definition 4.1 (embedding relation [43]) The homeomorphic embedding relation ⊴ on terms in τ(Σ∪V) is defined as the smallest relation satisfying: x ⊴ y for all x, y ∈ V, and s ≡ f(s_{1}, …, s_{m}) ⊴ g(t_{1}, …, t_{n}) ≡ t, if and only if:

1. f ≡ g (and m ≡ n) and s_{i} ⊴ t_{i} for all i = 1, …, n, or

2. s ⊴ t_{j}, for some j, 1 ≤ j ≤ n.

The embedding relation ⊴ is a well-quasi ordering of the set τ(Σ ∪ V) for finite Σ [2, 28], that is, any infinite sequence of terms t_{1}, t_{2}, … with a finite number of operators is self-embedding, i.e., there are numbers j, k with j < k and t_{j} ⊴ t_{k}. In order to avoid an infinite sequence of “diverging” calls, we compare each narrowing redex of the current goal with the selected redexes in the ancestor goals. When the compared calls are in the embedding relation, the derivation is stopped. We consider here this nonembedding unfolding rule (instantiated with the lazy calculus relation) U⊴_{⇝_{▶}} to control the expansion of the trees.

We define a PE^{⊴} configuration as a sequence of terms (t_{1}, …, t_{n}) ∈ State^{⊴}. Upon each iteration of the algorithm in Definition 3.7, the current configuration q ≡ (t_{1}, …, t_{n}) is transformed in order to ‘cover’ the set T of terms which result from the PE of q in R, that is:

T = terms(U⊴_{⇝_{▶}} ({t_{1}, …, t_{n}}, R)). This transformation is done using a specific abstraction operation abstract^{⊴} [2]. Informally, this operator does the following. Let T be the set of new terms introduced by the unfolding. They are compared to those already generated (recorded in q) and, if the new term is not larger than any of the preceding ones, it is just appended to q. Otherwise, if the new term s is an instance of some term t = sσ in q, then the terms in σ are recursively abstracted and introduced in q; else the two terms are slightly generalized by taking their most specific generalization [30]. The abstraction operator abstract^{⊴} guarantees the global termination of the algorithm and the closedness of the partially evaluated program.

Our first example, the ‘double-append’, is a standard test of elimination of intermediate data structures. It illustrates the fact that our method can eliminate intermediate data structures and turn multiple–pass programs into one– pass programs. This effect is also achieved by deforestation [47], tupling [9] and positive supercompilation [42], among others, while standard PE generally does not get this optimization [44]. This example also shows that normalization between narrowing steps can be used as a safe replacement for some ad-hoc optimizations used in other methodologies for program transformation. This normalization does not risk looping, because by using a terminating subset of the program rules for normalization, each single narrowing step terminates and thus narrowing trees are built in finite time. It does not lose completeness either, because alternative clauses are discarded only if no solutions are lost.

Example 3 (double-append) Consider the well-known, terminating, program app/2:

app(nil, y_{s}) → y_{s}
app(x : x_{s}, y_{s}) → x : app(x_{s}, y_{s})

with initial query app(app(x_{s}, y_{s}), z_{s}) ≈ y. This goal appends three lists by appending the two first, yielding an intermediate list, and then appending the last one to that. We evaluate the goal by using normalizing lazy narrowing. Starting with the sequence: q = app(app(x_{s}, y_{s}), z_{s}), and by using the procedure described in Definition 3.8, we compute the trees depicted in Figure 3 for the sequence of terms: q′ = app(app(x_{s}, y_{s}), z_{s}), app(x_{s}, y_{s}). Note that “app” has been abbreviated to “a” in the picture. Then we get the following residual program R′:

app(app(nil, y_{s}), z_{s}) → app(y_{s}, z_{s})
app(app(x : x_{s}, y_{s}), z_{s}) → x : app(app(x_{s}, y_{s}), z_{s})
app(nil, z_{s}) → z_{s}
app(y : y_{s}, z_{s}) → y : app(y_{s}, z_{s})

which is able to append the three lists by traversing its input only once. Note that the key to success in this example is the use of normalization. Without the simplification step, the embedding ordering would have been satisfied too early in the rightmost branch of the top tree of Figure 3. The driving algorithm in [43] (the only version of positive supercompilation guaranteeing termination) achieves the same effect by means of an ad-hoc technique like the ‘transient reductions’ [43], which can incur the risk of nontermination, as opposed to our method.

[figure: \{x_{s}/nil\}; \{x_{s}/x′ : x′_{s}\}; x′ : a(\underline{a(x′_{s}, y_{s})}, z_{s}) ≈ y; a(x′ : a(x′_{s}, y_{s}), z_{s}) ≈ y; \underline{a(y_{s}, z_{s})} ≈ y; a(\underline{a(x_{s}, y_{s})}, z_{s}) ≈ y; \{y_{s}/nil\}; \{y_{s}/y′ : y′_{s}\}; y′ : \underline{a(y′_{s}, z_{s})} ≈ y; z_{s} ≈ y; \underline{a(y_{s}, z_{s})} ≈ y]

Figure 1: Normalizing lazy narrowing trees for

a(a(x_{s}, y_{s}), z_{s}) ≈ y and a(x_{s}, y_{s}) ≈ y.

In [31], characteristic trees have been proposed as an alternative to transient reductions which ensure termination. We note that the normalization of goals implements a strategy where we compute in a deterministic way as long as possible, and it is thus comparable to Gallagher’s preference for unfolding determinate goals [12, 43] in that it avoids the creation of superfluous choice points for alternative rules but it requires a sort of “looking-ahead” in the search trees.

Example 3 illustrates the fact that the resulting partially evaluated program is not guaranteed to be CB, which may prevent the lazy strategy from being able to narrow a goal in the transformed, partially evaluated program. Example 3 also shows that the resulting set of (partially evaluated) terms is not guaranteed to be independent. In our example, PE uses the same function symbol for two different specializations of a definition (namely, for the procedures app(app(x_{s}, y_{s}), z_{s}) and app(x_{s}, y_{s})). Some type of transformation is required to guarantee that there is no interference between the corresponding sets of rules, as would be the case if the definition of ‘double-append’ were used to narrow a nested call app( , ) in a goal app(\underline{app( , )}, ).

4.1 Post-Processing Renaming

In this section, we formalize a suitable renaming phase able to guarantee that lazy narrowing can execute the goal in the transformed program and that different specializations of a function are not confused, while the (lazy) computed answer semantics is preserved.

Definition 4.2 (independent renaming) Let S be a set of terms. We define an independent renaming S′ of S as follows:

S′ = {⟨s, s′⟩ | s ∈ S ∧ s′ = f^{s}(x_{1}, …, x_{m})}

where {x_{1}, …, x_{m}} are the distinct variables in s in the order of their first occurrence, and the f^{s}’s are new function symbols, which are different from those in R and S.

The post-processing renaming can be formally defined as follows.

Definition 4.3 (post-processing renaming) Let R be a program and S a set of terms. Let R′ be a partial evaluation of R w.r.t. S, and S′ an independent renaming of S. We define the post-processing renaming R′′ = ppren_{▶}(R′, S′) of R′ w.r.t. S′ as follows: ppren_{▶}(R′, S′) =

⋃⟨s,s′⟩∈S′{r′ | (sθ → ρ ⇐ C) ∈ R′, and

r′ ≡ (s′θ → ren(ρ, S′) ⇐ ren(C, S′))}

where the nondeterministic function ren(o, S′) is defined inductively as follows: ren(o, S′) =

ren(e_{1}, S′), …, ren(e_{n}, S′)

if o ≡ (e_{1}, …, e_{n})

ren(s, S′) ≈ ren(t, S′)

if o ≡ (s ≈ t)

x if o ≡ x ∈ V c(ren(t_{1}, S′), …, ren(t_{n}, S′))

if o ≡ c(t_{1}, …, t_{n}), c ∈ C, n ≥ 0

s′θ′ if o = sθ, ⟨s, s′⟩ ∈ S′, and θ′ = {(x/ren(xθ, S′)) | x ∈ Dom(θ)}.

Roughly speaking, in Definition 4.3 we derive specialized procedures for each term in S′, and perform fold on every function call in R′ (replacing the original term by a call to the newly defined function) using the corresponding renaming in S′, to produce the new, renamed, filtered program R′′. The idea behind this transformation is that, for any Sclosed query g, lazy narrowing computes the same answers for g in R as for the goal which results from the renaming of g (according to S′) in R′′. Note that the postunfolding process terminates.

We now illustrate these definitions with an example.

Example 4 Consider again the double-append goal and program app/2 of Example 3. An independent renaming S′ of S is:

S′ = { ⟨app(x_{s}, y_{s}), a_{1}(x_{s}, y_{s})⟩,

⟨app(app(x_{s}, y_{s}), z_{s}), a_{2}(x_{s}, y_{s}, z_{s})⟩ }.

The post-processing renaming R′′ of R′ w.r.t. S′ is:

a_{2}(nil, y_{s}, z_{s}) → a_{1}(y_{s}, z_{s})
a_{2}(x : x_{s}, y_{s}, z_{s}) → x : a_{2}(x_{s}, y_{s}, z_{s})
a_{1}(nil, y_{s}) → y_{s}
a_{1}(x : x_{s}, y_{s}) → x : a_{1}(x_{s}, y_{s})

We note that, for a given set of terms S′, the filtered form of a program may depend on the strategy which selects the term from S′ which is used to rename a given term o in S, since there may exist, in general, more than one s in S′ that covers the call o. Hence, the specialized form of a program is not unique. Some potential specialization might be lost due to an inconvenient choice. The problem of defining some plausible heuristics able to produce the better potential specialization is still pending research.

Renaming ensures independence of the specialized procedures, as stated in the following.

Proposition 4.4 (independence) Let R be a weakly orthogonal, CB program, S be a finite set of terms, and g be an S-closed goal. Let R′ be a hnf-PE of R w.r.t. S such that R′ is S-closed. Let S′ be an independent renaming of S, R′′ = ppren_{▶}(R′, S′) the renaming of R′ w.r.t. S′, and g′′ = ren(g, S′) the renaming of the goal g w.r.t. S′. Then,

1. A ≡ {s′ | ⟨s, s′⟩ ∈ S′} is independent,

2. R′′ is a left linear CB program, and

3. R′′ ∪ {g′′} is A-closed.

We now state the correctness of the partial evaluator with the post-processing renaming.

Theorem 4.5 (strong soundness and completeness) Let R be a weakly orthogonal, CB program, g a goal, and S be a finite set of terms. Let R′ be a hnf-PE of R w.r.t. S such that R′ ∪ {g} is S-closed. Let S′ be an independent renaming of S, R′′ be a renaming of R′ w.r.t. S′, and g′′ = ren(g, S′). Then θ is a computed answer substitution for g in R iff θ is a computed answer substitution for g′′ in R′′.

We finally illustrate the power of the call-by-name PE procedure on the matching program match of [27]. This example is discussed by [24, 43, 44], among others.

4.2 Pattern matching in strings

A standard example in the literature on PE is the derivation of an efficient string matcher by PE of a (more or less) naïve pattern matcher w.r.t. a given pattern [15, 44]. The source program R listed below checks whether a string pattern p occurs within another string s by iteratively comparing p with a prefix of s. In the case of a mismatch, the first element of the target string s is cut off and the process is restarted with the tail of s. The strategy is not optimal because the same elements in the string may be tested several times. The power of a transformation can be made evident by checking whether it automatically performs the optimization central to the Knuth-Morris-Pratt (KMP) string matching algorithm which constructs a deterministic finite automaton. The ‘KMP test’ is often used to compare the strength of specializers. This example is particularly interesting because it is a kind of transformation that neither (conventional) PE nor deforestation can perform automatically [44]. Partial deduction of logic programs and positive supercompilation of functional programs can pass the test [44]. Our method also performs satisfactorily on the problem, as the following example illustrates. We assume that matching is on bit-strings, i.e. strings containing only zeroes and ones. Note that this choice of a binary (or finite) alphabet is sensible for an equational definition of the false value for equalities, but it is not essential for the specialization, since the algorithm does not rely on it and is not exploited during the specialization process.

Example 5 Let R be the naïve pattern matching program (a) of Figure 2. Suppose that the fixed pattern 001 is given and we want to solve the pattern matching problem for the subject string s. Applying the call-by-name evaluator to the term match(001, s), and subsequently evaluating new terms according to our method, gives the program R′^{2} (Figure 2, (b)). After the post-processing renaming transformation, we obtain the specialized program R′′ (Figure 2, (c)). The amount of specialization obtained in this program is essentially analogous to that of the rules produced by the algorithm in [43]. The specialized algorithm acts like a KMPstyle pattern matcher. This gives the same advantages of the KMP algorithm over the naïve one in terms of complexity. Namely, for each fixed pattern p the specialized algorithm makes much less comparisons, furthermore as p gets larger the complexity of the naïve algorithm becomes larger, while for the specialized algorithm there exists an upper bound which does not depend on p.

2For simplicity, we have omitted the rules that reduce functions to false. We have used the simplification and eager variable elimination [38] rules in order to get better specialization.

(a) Naïve pattern matcher R:

match(p, s) → loop(p, s, p, s)
loop(nil, ss, op, os) → true
loop(p : pp, nil, op, os) → false
loop(p : pp, s : ss, op, os) → loop(pp, ss, op, os) ⇐ p ≈ s  % continue
loop(p : pp, s : ss, op, os) → next(op, os) ⇐ (p ≈ s) ≈ false % shift string
next(op, nil) → false  % restart loop
next(op, s : ss) → loop(op, ss, op, ss)

(b) CBN PE R′ of match(001, s) in R:

match(001, s) → loop(001, s, 001, s)
loop(001, 0 : ss, 001, 0 : ss) → loop(01, ss, 001, 0 : ss)
loop(001, s : ss, 001, s : ss) → loop(001, ss, 001, ss) ⇐ (0 ≈ s) ≈ false
loop(01, 0 : ss′, 001, 00 : ss′) → loop(1, ss′, 001, 00 : ss′)
loop(01, s′ : ss′, 001, 0 : s′ : ss′) → loop(001, ss′, 001, s′ : ss′) ⇐ (0 ≈ s′) ≈ false
loop(1, 1 : ss′′, 001, 001 : ss′′) → true
loop(1, s′′ : ss′′, 001, 00 : s′′ : ss′′) → loop(01, s′′ : ss′′, 001, 0 : s′′ : ss′′) ⇐ (1 ≈ s′′) ≈ false

(c) Post-processing renaming R′′ of R′:

match′(s)  → loop 001(s)
loop 001(0 : ss) → loop 01(ss)  loop 001(s : ss) → loop 001(ss) ⇐ (0 ≈ s) ≈ false
loop 01(0 : ss) → loop 1(ss)  loop 01(s : ss) → loop 001(ss) ⇐ (0 ≈ s) ≈ false
loop 1(1 : ss)  → true  loop 1(s : ss)  → loop 01(s : ss) ⇐ (1 ≈ s) ≈ false

Figure 2: KMP example.

Let us conclude with an example that illustrates the fact that, in some cases, a call-by-name partial evaluator can derive more efficient residual programs than a call-by-value partial evaluator and hence it can be worthwhile constructing them, even for terminating programs. We note that most of the actual partial evaluators are based on call-by-value procedures.

Example 6 Consider the following program R ≡ {g(x) → 0, f(0) → 0, f(c(x)) → f(x)}. Let us consider a call-by-value partial evaluation based on innermost narrowing [11]. If we evaluate the goal g(f(x)) = y in R using innermost narrowing, we obtain the following renamed specialized program R′′_{1} ≡ {g′(0) → 0, g′(c(x)) → g′(x)}. The partial evaluator based on our lazy narrowing strategy produces the following residual program R′′_{2} ≡ {g′(x) → 0}, whose complexity is O(1), whereas the complexity of R′′_{1} is O(n) (where n is the number of 0’s in the input argument).

5 Related Work

Early work on automatic specialization of functional programs includes Turchin’s supercompiler [45] and the positive supercompiler [44]. Supercompilation is based on driving, a unification-based (call-by-name) transformation technique for a strict (call-by-value) functional language tailored for supercompilation. The mechanism of driving covers the activities of specializing and unfolding in PE. The positive supercompiler is a reformulation of Turchin’s supercompiler for a simpler call-by-name language with tree-structured patterns. In this language, all arguments of a function are input parameters. Furthermore, there is only pattern-matching for non-nested linear patterns. The formulation is generalizable to less restrictive languages at the cost of more complex driving algorithms. In our functional logic language, this is not the case, since we allow for more powerful matching via unification on all arguments, both in execution and during specialization.

In positive supercompilation [15], local and global control are not (explicitly) distinguished as only one-step unfolding is performed. A large evaluation structure is built which comprises something similar to both the local narrowing trees and the global configurations of [36]. Each call t in the driving process graph produces a residual function. The body of the definition of the new function is derived from the descendants of t in the graph. As in Partial Deduction, the body of each residual rule in our framework is built from the final node of the derivation, which results in a fewer number of rules [15].

The post-processing renaming we have introduced in this paper can be seen as an extension of the post-processing renaming defined in [5] to the case of nested functions in expressions. For simple patterns, our post-unfolding renaming essentially boils down to the simpler transformation of [5].

A more closely related approach can be found in [32], where conjunctions of calls (atoms) can appear in the heads of partially evaluated programs, which is somehow comparable to nested function applications. As in our framework, in [32] renaming is mandatory in order to derive an executable specialized program from the partially evaluated one. There exist two main differences between our postprocessing renaming and the renaming function introduced in [32]. First, their definition describes renaming functions which can erase variables of the renamed calls. As noted in [32], this approach can produce incorrect transformations. A safe technique has been later introduced in [33]. The second difference is in the renaming of clause bodies. As we pointed out before, our renaming transformation is nondeterministic, and thus the function ren of Definition 4.3 can produce different outcomes. Similarly, the renaming transformation of [32] involves some nondeterminism concerning the selection of conjunctions from the clause bodies to be renamed. However, they introduce a partitioning function in order to deterministically choose one of the possible renamings. This extension is also possible in our framework, by simply adding a new parameter to the renaming function ren to indicate how the specialized calls have been proved S-closed, which might be used to guide the renaming process.

6 Conclusions

The interest in combining the most important declarative paradigms, namely functional and logic programming, has grown over the last decade (see [18] for a survey). However, integrated functional logic languages are currently not widely used. In order to develop useful and practical integrated languages, it is essential to succeed in shrinking the efficiency gap with respect to imperative languages, as is already being done for Prolog. To this goal, formally based, practical tools for the analysis and transformation of functional logic programs which are able to improve the current implementations are a pressing need. Since functional logic languages have been widely investigated from the point of view of the semantics, it becomes of natural concern to study formal manipulation techniques based on the semantics, which are able to improve program performances without changing the computational meaning.

PE is a semantics-preserving program transformation based on unfolding and specializing procedures. In this paper we have considered the case of (normalizing) lazy narrowing, which has been shown to be a reasonable improvement over pure logic SLD resolution strategy [17]. The main innovations in our work are: 1) our procedure applies to (lazy) functional logic languages such as Babel whose (lazy narrowing) operational semantics corresponds to SLD resolution but with the additional feature of exploiting determinism by the ‘dynamic cut’ [18], and 2) we present a renaming transformation for guaranteeing: (a) the independence of the set of partially evaluated terms, (b) that the partially evaluated program does not lose some of the basic requirements for the completeness of lazy narrowing and (c) the equivalence of the computed answer substitution semantics of the original and the partially evaluated programs for the intended queries.

We note that our post-processing transformation is necessary also for some non-lazy strategies, such as innermost narrowing, and the extension results straightforward [1].

As future work we mention the investigation of the application of our framework to optimal versions of lazy narrowing strategies, such as needed narrowing [4] (and its extension to a higher order framework) which has been proposed as the basic operational principle of Curry [20], a language which is intended to become a standard in this area.

Acknowledgements

We thank Morten Sørensen for providing us with very valuable feedback on a draft of the paper.

References

[1] M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Callby-Name Partial Evaluation of Functional Logic Programs. TR DSIC-II/34/96, U.P. Valencia, 1996.

[2] M. Alpuente, M. Falaschi, and G. Vidal. Narrowingdriven Partial Evaluation of Functional Logic Programs. In H. Riis Nielson, editor, Proc. of the 6th European Symp. on Programming, ESOP’96, pages 45–61. Springer LNCS 1058, 1996.

[3] M. Alpuente, M. Falaschi, and G. Vidal. Narrowingdriven Specialization of Functional Logic Programs. TR DSIC-II/33/96, U.P. Valencia. Extended and revised version of [2]. Available from URL http://www.dsic.upv.es/users/elp/papers.html, 1996.

[4] S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proc. 21st ACM Symp. on Principles of Programming Languages, Portland, pages 268– 279, 1994.

[5] K. Benkerimi and P.M. Hill. Supporting Transformations for the Partial Evaluation of Logic Programs. Journal of Logic and Computation, 3(5):469–486, 1993.

[6] J.A. Bergstra and J.W. Klop. Conditional Rewrite Rules: confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.

[7] D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proc. of First European Symp. on Programming, ESOP’86, pages 119–132. Springer LNCS 213, 1986.

[8] R.M. Burstall and J. Darlington. A Transformation System for Developing Recursive Programs. Journal of the ACM, 24(1):44–67, 1977.

[9] W. Chin. Towards an Automated Tupling Strategy. In Proc. of Partial Evaluation and Semantics-Based Program Manipulation, Copenhagen, Denmark, June 1993, pages 119–132. ACM, New York, 1993.

[10] N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243–320. Elsevier, Amsterdam, 1990.

[11] L. Fribourg. SLOG: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. of Second IEEE Int’l Symp. on Logic Programming, pages 172–185. IEEE, New York, 1985.

[12] J. Gallagher. Tutorial on Specialisation of Logic Programs. In Proc. of Partial Evaluation and Semantics-Based Program Manipulation, Copenhagen, Denmark, June 1993, pages 88–98. ACM, New York, 1993.

[13] J. Gallagher and M. Bruynooghe. Some Low-Level Source Transformations for Logic Programs. In M. Bruynooghe, editor, Proc. of 2nd Workshop on Meta-Programming in Logic, pages 229–246. Department of Computer Science, KU Leuven, Belgium, 1990.

[14] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences, 42, 1991.

[15] R. Glück and M.H. Sørensen. Partial Deduction and Driving are Equivalent. In Proc. Int’l Symp. on Programming Language Implementation and Logic Programming, PLILP’94, pages 165–181. Springer LNCS 844, 1994.

[16] M. Hanus. Compiling Logic Programs with Equality. In Proc. of 2nd Int’l Workshop on Programming Language Implementation and Logic Programming, pages 387–401. Springer LNCS 456, 1990.

[17] M. Hanus. Combining Lazy Narrowing with Simplification. In Proc. of 6th Int’l Symp. on Programming Language Implementation and Logic Programming, pages 370–384. Springer LNCS 844, 1994.

[18] M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming, 19&20:583–628, 1994.

[19] M. Hanus. On Extra Variables in (Equational) Logic Programming. In Proc. of 20th Int’l Conf. on Logic Programming, pages 665–678. The MIT Press, Cambridge, MA, 1995.

[20] M. Hanus, H. Kuchen, and J.J. Moreno-Navarro. Curry: A Truly Functional Logic Language. In Proc. ILPS’95 Workshop on Visions for the Future of Logic Programming, pages 95–107, 1995.

[21] S. Hölldobler. Foundations of Equational Logic Programming. Springer LNAI 353, 1989.

[22] J.M. Hullot. Canonical Forms and Unification. In Proc of 5th Int’l Conf. on Automated Deduction, pages 318– 334. Springer LNCS 87, 1980.

[23] H. Hussman. Unification in Conditional-Equational Theories. In Proc. European Conf. on Computer Algebra EUROCAL’85, pages 543–553. Springer LNCS 204, 1985.

[24] N.D. Jones. The Essence of Program Transformation by Partial Evaluation and Driving. In N.D. Jones, M. Hagiya, and M. Sato, editors, Logic, Language and Computation, pages 206–224. Springer LNCS 792, 1994.

[25] N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs, NJ, 1993.

[26] J.W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume I, pages 1–112. Oxford University Press, 1992.

[27] D.E. Knuth, J.H. Morris, and V.R. Pratt. Fast Pattern Matching in Strings. SIAM Journal of Computation, 6(2):323–350, 1977.

[28] J. B. Kruskal. The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept. Journal of Combinatorial Theory, A(13):297–305, 1972.

[29] H. Kuchen, R. Loogen, J.J. Moreno-Navarro, and M. Rodríguez-Artalejo. Lazy Narrowing in a Graph Machine. In Proc. of the Int’l Conf. on Algebraic and Logic Programming, volume 463 of Lecture Notes in Computer Science, pages 298–317, 1990.

[30] J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

[31] M. Leuschel and B. Martens. Global Control for Partial Deduction through Characteristic Atoms and Global Trees. Technical Report CW-220, Department of Computer Science, K.U. Leuven, Belgium, December 1995.

[32] M. Leuschel, D. De Schreye, and A. de Waal. A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration. In M. Maher, editor, Proc. of the Joint International Conference and Symposium on Logic Programming JICSLP’96, pages 319– 332. The MIT Press, Cambridge, MA, 1996.

[33] M. Leuschel and M.H. Sørensen. Redundant Argument Filtering of Logic Programs. In Proc. of Int’l Workshop on Logic Programming Synthesis and Transformation, LOPSTR’96. To appear in Springer LNCS, 1996.

[34] J.W. Lloyd and J.C. Shepherdson. Partial Evaluation in Logic Programming. Journal of Logic Programming, 11:217–242, 1991.

[35] R. Loogen, F. López-Fraguas, and M. Rodríguez-Artalejo. A Demand Driven Computation Strategy for Lazy Narrowing. In J. Penjam and M. Bruynooghe, editors, Proc. of PLILP’93, Tallinn (Estonia), pages 184–200. Springer LNCS 714, 1993.

[36] B. Martens and J. Gallagher. Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance. In L. Sterling, editor, Proc. of ICLP’95, pages 597–611. MIT Press, 1995.

[37] A. Middeldorp and E. Hamoen. Completeness Results for Basic Narrowing. Applicable Algebra in Engineering, Communication and Computing, 5:213–253, 1994.

[38] A. Middeldorp and S. Okui. A Deterministic Lazy Narrowing Calculus. In Proc. of the Fuji Int’l Workshop on Functional and Logic Programming, pages 104–118. World Scientific, 1995.

[39] J.J. Moreno-Navarro and M. Rodriguez-Artalejo. Logic Programming with Functions and Predicates: The language Babel. Journal of Logic Programming, 12(3):191– 224, 1992.

[40] U.S. Reddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. of Second IEEE Int’l Symp. on Logic Programming, pages 138–151. IEEE, New York, 1985.

[41] P. Réty. Improving basic narrowing techniques. In Proc. of the Conf. on Rewriting Techniques and Applications, pages 228–241. Springer LNCS 256, 1987.

[42] M.H. Sørensen. Turchin’s Supercompiler Revisited: An Operational Theory of Positive Information Propagation. Technical Report 94/7, Master’s Thesis, DIKU, University of Copenhagen, Denmark, 1994.

[43] M.H. Sørensen and R. Glück. An Algorithm of Generalization in Positive Supercompilation. In J.W. Lloyd, editor, Proc. of ILPS’95, pages 465–479. The MIT Press, Cambridge, MA, 1995.

[44] M.H. Sørensen, R. Glück, and N.D. Jones. A Positive Supercompiler. Journal of Functional Programming, 1996. To appear.

[45] V.F. Turchin. Program Transformation by Supercompilation. In H. Ganzinger and N.D. Jones, editors, Programs as Data Objects, 1985, pages 257–281. Springer LNCS 217, 1986.

[46] V.F. Turchin. The Algorithm of Generalization in the Supercompiler. In D. Bjørner, A.P. Ershov, and N.D. Jones, editors, Proc. of the Int’l Workshop on Partial Evaluation and Mixed Computation, pages 531–549. North-Holland, Amsterdam, 1988.

[47] P.L. Wadler. Deforestation: transforming programs to eliminate trees. In Proc of the European Symp. on Programming, ESOP’88, pages 344–358. Springer LNCS 300, 1988.