Narrowing Approximations as an Optimization for Equational Logic Programs ^{⋆}

María Alpuente^{1}, Moreno Falaschi^{2}, María José Ramis^{1} and Germán Vidal^{1}

1 Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020 Valencia, Spain.

2 Dipartimento di Elettronica e Informatica, Università di Padova, Via Gradenigo 6/A, 35131 Padova, Italy.

Abstract. Solving equations in equational theories is a relevant programming paradigm which integrates logic and equational programming into one unified framework. Efficient methods based on narrowing strategies to solve systems of equations have been devised. In this paper, we formulate a narrowing-based equation solving calculus which makes use of a top-down abstract interpretation strategy to control the branching of the search tree. We define a refined, but still complete, equation solving procedure which allows us to reduce the branching factor. Our main idea consists of building an abstract narrower for equational theories and executing the set of equations to be solved in the approximated narrower. We define a generic technique of loop detection to ensure termination of our method. We prove that the set of answers computed by the abstract narrower has the property that each concrete solution of the set of equations is an instance of one of the substitutions in the answer set. Thus we define a strategy which computes such a set and uses the substitutions in it for cutting down the search space of the program without losing completeness. We also report on experimental results which demonstrate that our optimization can result in significant speed-ups in program execution.

Keywords: Abstract interpretation, equational logic programming, term rewriting systems, universal unification.

1 Introduction

The recent interest in logic programming with equations [12,16,18] has promoted much work on equational unification [14,16,27] and narrowing [16,23]. Equational unification (E-unification) characterizes the problem of solving equations modulo an equational theory E. The narrowing mechanism is a powerful

⋆ This work has been partially supported by CICYT under grant TIC 92-0793-C02-02. M.J. Ramis is supported by Spanish Conselleria de Cultura, Educació i Ciència de la Generalitat Valenciana.

tool for constructing complete E-unification algorithms for useful classes of equational theories. In this context, completeness means that for every solution to a given set of equations, a more general solution can be found by narrowing. 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 [7,16,17,23]. Narrowing at only basic positions has been proven to be a complete method for solving equations in the theory defined by a level-canonical conditional term rewriting system [15,16,17,23,24]. In [7,15] a further refinement is considered which derives from simulating SLD-resolution on flattened equations and in which the search reduces to an innermost selection strategy.

The ability to detect the unsatisfiability of a set of equations is also very important to prune useless paths from the search tree and to save a lot of unnecessary computations. This problem is, in general, undecidable. [5] defines a scheme based on abstract interpretation for the (static) analysis of the unsatisfiability of equation sets, and shows how various analyses such as [2,4,12,13] can be seen as instances of the scheme.

In this work, we are concerned with equation solving or E-unification with respect to a given set E of equations. We define an optimization of (basic) conditional narrowing for the purpose of generating complete sets of E-unifiers in equational theories that can be described by a (level-canonical) conditional term rewriting system. The optimization is based on the idea that narrowing derivations can be approximated by means of an abstract calculus whose derivations cover all concrete computations. [4,5] define an abstract narrower which approximates the decision problem of the unsatisfiability of an equation set E with respect to an equational theory E. The abstract narrower always terminates and, if it terminates computing a “finitely failed tree”, it states that the set of equations has no E-unifier. In this paper we show that this abstract narrower yields useful information also when it is unable to state that an equation set is unsatisfiable. In this case a finite description of the set of E-unifiers of E can be collected. We show that this description can be used to filter those derivations that give rise to substitutions which are ‘incompatible’ with the description. Thus we present a calculus which on one side is able to detect unsatisfiability of equation sets, and if it fails to do so then it collects a finite description which allows us to prune the (concrete) narrowing search tree. We prove that the completeness result of basic conditional narrowing is preserved in the optimization. To the best of our knowledge this method is new and it allows an immediate combination with the existing interpreters of equational logic programs whose computational engine is narrowing [3,7,16]. In practice, the branches of the narrowing search tree whose root contains a substitution which is ‘incompatible’ with the set of collected abstract substitutions can be safely pruned. We show that this ‘consistency check’ can be performed compositionally. We define a composition of abstract substitutions which would allow a parallel implementation of the test. In the paper we show some experimental results for the case of a sequential implementation, we have not tried with a parallel interpreter yet.

The paper is organized as follows. After introducing some preliminary notions in Section 2, we present the basic solution procedure in Section 3. Section 4 recalls an abstract algorithm to analyze the unsatisfiability of equation sets [4,5], and Section 5 defines a strategy that exploits the abstractions computed by this algorithm to reduce the alternatives that the solution procedure has to explore. Section 6 presents some experimental results for our method and concludes. More details and missing proofs can be found in [6].

2 Preliminaries

Let us first summarize some known results about equations, conditional rewrite systems and equational unification. For full definitions refer to [11,19]. Throughout this paper, V will denote a countably infinite set of variables and Σ denotes a set of function symbols, each with a fixed associated arity. τ(Σ ∪ V ) and τ(Σ) denote the sets of terms and ground terms built on Σ and V , respectively. A Σ-equation s = t is a pair of terms s, t ∈ τ(Σ ∪V ). Terms are viewed as labelled trees in the usual way. Occurrences are represented by sequences, possibly empty, of naturals. Ō(t) denotes the set of nonvariable occurrences of a term t. 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. t[u] denotes the label in t at occurrence u ∈ Ō(t). These notions extend to equations in a natural way. Identity of syntactic objects is denoted by ≡. Var(s) is the set of distinct variables occurring in the syntactic object s. A fresh variable is a variable that appears nowhere else. The symbol denotes a finite sequence of symbols.

We describe the lattice of equation sets following [10]. We let Eqn denote the set of possibly existentially quantified finite sets of equations over terms. We let fail denote the unsatisfiable equation set, which (logically) implies all other equation sets. Likewise, the empty equation set, denoted true, is implied by all elements of Eqn. We write E ≤ E′ if E′ logically implies E. Thus Eqn is a lattice ordered by ≤ with bottom element true and top element fail. An equation set is solved if it is either fail or it has the form ∃y_{1} … ∃y_{m} . {x_{1} = t_{1},…, x_{n} = t_{n}} where each x_{i} is a distinct variable not occurring in any of the terms t_{i} and each y_{i} occurs in some t_{j} . Any set of equations E can be transformed into an equivalent one solve(E) which is solved. We restrict our interest to the set of idempotent substitutions over τ(Σ ∪ V ), which is denoted by Sub. There is a natural isomorphism between substitutions and unquantified equation sets.

We use the same notation for a substitution {x_{1}/t_{1},…, x_{n}/t_{n}}, the corresponding set of equations {x_{1} = t_{1},…, x_{n} = t_{n}} and the corresponding conjunction of equations x_{1} = t_{1} ∧…∧x_{n} = t_{n}. For example we may write θ ∧xθ, where the first occurrence of θ is a conjunction of equations and the second occurrence is the application of a substitution.

We consider the usual preorder on substitutions ≤: θ ≤ σ iff ∃γ.σ ≡ θγ. Note that θ ≤ σ iff σ ⇒ θ [25]. A substitution {x_{1}/t_{1},…, x_{n}/t_{n}} is a unifier of an equation set E iff {x_{1} = t_{1},…, x_{n} = t_{n}} ⇒ E. We denote the set of unifiers of E by unif (E) and mgu(E) denotes the most general unifier of the unquantified equation set E. While every unquantified equation set has a most general unifier [20], this is not true in general for equation sets with existentially quantified variables. We write s =^{?} t when we want to point out the fact that two terms s and t do unify.

We note that quantifiers will not be used when dealing with the concrete operational semantics. It is only when arguing the relation between the concrete and abstract operational semantics that we need to consider quantified equation sets, since our abstract algorithm replaces some of the terms in the term rewriting system by occurrences of a special symbol which from the logical viewpoint stands for a quantified variable.

A Horn equational Σ-theory E consists of a finite set of equational Horn clauses of the form e ⇐ e_{1},…, e_{n}, n ≥ 0, where e, e_{i}, i = 1,…, n, are Σ-equations. Σ-equations and Σ-theories will often be called equations and theories, respectively. An equational goal is an equational Horn clause with no head.

A Term Rewriting System (TRS for short) is a pair (Σ, R) where R is a finite set of reduction (or rewrite) rule schemes of the form (λ → ρ ⇐ ẽ), λ, ρ ∈ τ(Σ ∪ V ), λ ∉ V and Var(ρ) ⊆ Var(λ). The condition ẽ is a possibly empty conjunction e_{1},…, e_{n}, n ≥ 0, of equations. We will often write just R instead of (Σ, R).

A Horn equational theory E which satisfies the above assumptions can be viewed as a term rewriting system R where the rules are the heads (implicitely oriented from left to right) and the conditions are the respective bodies. We assume that these assumptions hold for all theories we consider in this paper. The equational theory E is said to be canonical if the binary one-step rewriting relation →_{R} defined by R is noetherian and confluent [19].

A function symbol f ∈ Σ is irreducible iff there is no rule (λ → ρ ⇐ ẽ) ∈ 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 function symbols and F is the set of defined function symbols.

For TRS 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). Given a conditional TRS R, an equational goal clause G conditionally narrows into a goal clause G′ if there exists an equation e ∈ G, u ∈ Ō(e), a standardised apart variant (λ → ρ ⇐ ẽ) << R and a substitution σ such that σ = mgu({e_{|u} = λ}) and G′ = ((G ∼ {e}) ∪ {e[ρ]_{u}} ∪ ẽ)σ. s is called a (narrowing) redex (reducible expression) iff there exists a new variant (λ → ρ ⇐ ẽ) of a reduction rule in R and a substitution σ such that sσ ≡ λσ.

Given a set of equations E, we say that E is E-unifiable iff there exists a substitution σ such that E ⊧ Eσ [22]. The substitution σ is called an Eunifier of E. The set of all E-unifiers of E is recursively enumerable [14,16,27]. Conditional narrowing has been shown to be a complete E-unification algorithm for equational theories satisfying different restrictions [16,23].

3 Basic Conditional Narrowing

Basic (conditional) narrowing is a restricted form of (conditional) narrowing where only terms at basic occurrences are considered to be narrowed [17,23]. Informally, a basic occurrence is a nonvariable occurrence of the original goal or one that was introduced into the goal by the nonvariable part of the righthand side or the condition of a rule applied in a preceeding narrowing step. The idea behind the concept of basic is to avoid narrowing steps on subterms that are introduced by instantiation. Basic Conditional Narrowing is a complete E-unification algorithm for level-canonical Horn equational theories [23].

Let R be a level-canonical TRS. We formulate a Basic Conditional Narrowing calculus according to the partition of equational goals into a skeleton and an environment part, as in [16]. The skeleton part is a set of equations g and the environment part is a substitution θ. Substitutions are composed in the environment part, but are not applied to the terms in the skeleton part. Due to this representation, the basic occurrences in gθ are all in g, whereas the non-basic occurrences are all in the codomain of θ. We let State denote the set of goals (states). The calculus is defined as a transition system, which is a directed graph that has states as nodes. The initial state is a ‘source’ node and edges correspond to reductions between the states. Thus reduction sequences correspond to paths in the graph starting from the source. To solve the equation set g, the algorithm starts with the initial state ⟨g, ϵ⟩ and tries to derive new goals until a terminal goal ⟨true, σ⟩ is reached. Each substitution σ in a terminal goal is an E-unifier of g. By abuse of notation, it is often called solution. A successful derivation is a reduction sequence which ends in a terminal goal. A basic Conditional N arrowing calculus (bCN) is defined by the two following rules:

unification rule:

\frac{σ = mgu(gθ)}{⟨g, θ⟩ ⇝_{bCN} ⟨true, θσ⟩}

narrowing rule:

\frac{e ∈ g ∧ u ∈ Ō(e) ∧ (λ → ρ ⇐ ẽ) << R ∧ σ = mgu(\{(e_{|u})θ = λ\})}{⟨g, θ⟩ ⇝_{bCN} ⟨(g ∼ \{e\}) ∪ \{e[ρ]_{u}\} ∪ ẽ, θσ⟩}

4 Abstract Basic Conditional Narrowing

Abstract interpretation is a theory of semantic approximations which is used to provide statically sound answers to some questions about the run-time behaviour of programs. In this section, we formulate in terms of abstract interpretation an algorithm that approximates the problem of the E-unification of a given set of equations. The main idea behind our method is to abstract the transition system semantics bCN we introduced in Section 3. For this purpose, we follow the topdown approach to abstract interpretation which is based on constructing and examining abstract transition systems as defined in [10].

Most of the definitions at the beginning of this section are already in [4,5] and are reported for completeness. A difference with respect to [4] is in the definition of abstract most general unifier (Definition 5) which has been revised and simplified. Another difference is that we present Definition 10 as parametric with respect to a functional dependency graph (or loop-check). The corresponding definition in [5] is an instance for the specific dependency graph considered there.

A description is the association of an abstract domain (D, ≤) (a poset) with a concrete domain (E, ≤) (a poset). When E = Eqn, E = Sub or E = State, the description is called an equation description, a substitution description or a state description, respectively. The correspondence between the abstract and concrete domain is established through a ‘concretization’ function γ : D → ℘E. We say that d approximates e, written d ∝ e, iff e ∈ γ(d). The approximation relation can be lifted to relations and cross products as usual [5].

In the following, we approximate the behaviour of a TRS and initial state by an abstract transition system which can be viewed as a finite transition graph with nodes labeled by state descriptions, where transitions are proved by (abstract) narrowing reduction [4,5]. State descriptions consist of a set of equations with substitution descriptions. The descriptions for equations, substitutions and term rewriting systems are defined as follows:

Definition 1. By T = (τ(Σ ∪ V ), ≤) we denote the standard domain of (equivalence classes of) terms ordered by the standard partial order ≤ induced by the preorder on terms given by the relation of being “more general”. Let ⊥ be an irreducible symbol, where ⊥ ∉ Σ. Roughly speaking, the special symbol ⊥ introduced in the abstract domains represents any concrete term. Let T^{⊥} = (τ(Σ ∪ V ∪ {⊥}), ⪯) be the domain of terms over the signature augmented by ⊥, where the partial order ⪯ is defined as follows:

(a) ∀t ∈ T^{⊥}. ⊥ ⪯ t and t ⪯ t and

(b) ∀s_{1},…, s_{n}, s′_{1},…, s′_{n} ∈ T^{⊥}, ∀f /n ∈ Σ. s′_{1} ⪯ s_{1} ∧ … ∧ s′_{n} ⪯ s_{n} ⇒ f (s′_{1},…, s′_{n}) ⪯ f (s_{1},…, s_{n}). This order can be extended to equations: s′ = t′ ⪯ s = t iff s′ ⪯ s and t′ ⪯ t, and to sets of equations S, S′:

1) S′ ⪯ S iff ∀e′ ∈ S′.∃e ∈ S such that e′ ⪯ e. Note that S′ ⪯ true ⇒ S′ ≡ true.

2) S′ ⊑ S iff (S′ ⪯ S) and (S ⪯ S′ implies S′ ⊆ S).

The behaviour of the symbol ⊥ from a programming viewpoint resembles that of an “anonymous” variable in Prolog. From a logical viewpoint, ⊥ stands for an existentially quantified variable [5,21,22]. Define [[S]] = S′, where the n-tuple of occurrences of ⊥ in S is replaced by an n-tuple of existentially quantified fresh variables in S′. We note that S′ ⪯ S implies [[S]] ⇒ [[S′]] [5].

Definition 2. An abstract substitution is a set of the form {x_{1}/t_{1},…, x_{n}/t_{n}} where, for each i = 1,…, n, x_{i} is a distinct variable in V not occurring in any of the terms t_{1},…, t_{n} and t_{i} ∈ τ(Σ ∪ V ∪ {⊥}).

We can now characterize the ordering on abstract substitutions as logical implication of the corresponding logical expressions: let θ, κ ∈ Sub^{⊥}, κ ⪯ θ iff [[θ]] ⇒ [[κ]].

We can now introduce the abstract domains which we will use in our analysis.

Definition 3. upward Let (X , ≤) be a poset and let Y ⊆ X . Define upw(Y ) = {x ∈ X |∃y ∈ Y .y ≤ x}.

Definition 4. Let T = (τ(Σ ∪V ), ≤) and T^{⊥} = (τ(Σ ∪V ∪{⊥}), ⪯). The term description is ⟨T^{⊥}, γ, T ⟩ where γ : T^{⊥} → ℘ T is defined by: γ(t′) = {t ∈ T | t ∈ upw({t′})}.

Let Eqn be the set of finite sets of equations over τ(Σ ∪ V ) and Eqn^{⊥} be the set of finite sets of equations over τ(Σ ∪ V ∪ {⊥}). The equation description is ⟨(Eqn^{⊥}, ⊑), γ, (Eqn, ≤)⟩, where γ : Eqn^{⊥} → ℘ Eqn is defined by: γ(g′) = {g ∈ Eqn | g ∈ upw({g′}) and g is unquantified }.

Let Sub be the set of substitutions over τ(Σ ∪ V ) and Sub^{⊥} be the set of substitutions over τ(Σ ∪ V ∪ {⊥}). The substitution description is ⟨(Sub^{⊥}, ⪯), γ, (Sub, ≤)⟩, where γ : Sub^{⊥} → ℘ Sub is defined by: γ(κ) = {θ ∈ Sub | θ ∈ upw({κ})}.

Define the abstract state domain State^{⊥} induced by Eqn^{⊥} and Sub^{⊥} to be State^{⊥} = {⟨g, κ⟩ | g ∈ Eqn^{⊥}, κ ∈ Sub^{⊥}}.

Abstract states are intended to describe states which are equivalent modulo variable renaming. To ensure finiteness of the analysis, we collapse states which are variable renamings of each other into a single ‘equivalent’ state, as in [10]. A formal description can be found in [4,5] and is omitted here for brevity.

In the following, we formalize the idea that abstract narrowing reduction approximates narrowing reduction with abstract states, abstract unification and abstract term rewriting systems replacing concrete states, unification and term rewriting systems. The abstract most general unifier for our method is very simple and roughly speaking it boils down to computing a solved form of an equation set with (possibly) existentially quantified variables.

We define the abstract most general unifier for an equation set E′ ∈ Eqn^{⊥} as follows. First replace all occurrences of ⊥ in E′ by existentially quantified fresh variables. Then take a solved form of the resulting quantified equation set and finally replace the existentially quantified variables again by ⊥. Formally:

Definition 5. Abstract most general unifier Let solve([[E′]]) = ∃y_{1} … y_{n}. E and κ = {y_{1}/⊥,…, y_{n}/⊥}. Then,

mgu_{A}(E′) = Eκ.

Example 1. Let E = {f (g(⊥), h(z, z)) = f (x, h(x, g(a))), y = g(⊥)}. Then, mgu_{A}(E) = {x/g(a), y/g(⊥), z/g(a)}.

The following proposition justifies our use of ‘most general’.

Proposition 6. [5] ∀θ ∈ unif ([[E]]). mgu_{A}(E) ⪯ θ.

The safety of the abstract unification algorithm has been proven in [5] as stated by the following proposition.

Proposition 7. [5] Let g, g′ be (quantifier free) finite sets of equations over τ(Σ∪V ) and τ(Σ∪V ∪{⊥}), respectively. If g′ ∝ g and there exists mgu(g) = σ, then there exists mgu_{A}(g′) = σ_{A} where σ_{A} ∝ σ.

In general, the use of narrowing results in a semidecision procedure for testing the solvability of equation sets. A few approaches to improve the termination of narrowing have been reported [1,8,9,17,26]. For example, [8,26] consider a graph of terms which allows the detection of some loops in the search tree which do not lead to any solution. The improved algorithms described in [8,26] are still complete but termination is only guaranteed for theories which satisfy some rather strong conditions. The graphs are built using information about the equations being narrowed as well as the reduction rules being used for narrowing. In the following we propose a generic technique of loop detection which is used to obtain a form of ‘compiled’ program which always satisfies a simple termination condition.

Our notion of abstract term rewriting system is parametric with respect to a loop-check.

Definition 8. loop-check A loop-check is a graph G_{R} associated with a term rewriting system R, i.e. a relation consisting of a set of pairs of terms, such that: (1) the transitive closure G_{R}^{+} is decidable and (2) Let t̂ = t′ be a function which assigns to any term t some node t′ in G_{R}. If there is an infinite sequence:

⟨g_{0}, θ_{0}⟩ ⇝_{bCN} ⟨g_{1}, θ_{1}⟩ ⇝_{bCN} … then

∃i ≥ 0. ⟨t̂_{i}, t̂_{i}⟩ ∈ G_{R}^{+}, where t_{i} = e_{|u}θ_{i}, e ∈ g_{i} and u ∈ Ō(e).

(we refer to ⟨t̂_{i}, t̂_{i}⟩ as a ’cycle’ of G_{R}^{+}.)

Any node of the graph represents one or more variable renamings of itself, to avoid variable names clash. We refer to G_{R} as “the graph of functional dependencies”. The graph can be useful to prove the termination of basic narrowing derivations for simple cases as stated by the following proposition.

Proposition 9. Let R be a term rewriting system and G_{R} be the corresponding graph of functional dependencies. If there is no cycle in G_{R}, then every basic narrowing derivation terminates.

A TRS is abstracted by simplifying the right-hand side and the body of each rule. This definition is given inductively on the structure of terms and equations. Terms whose main functor f is a defined symbol are drastically simplified by replacing them by ⊥. Notice that we do not perform this approximation when there is no cycle in G_{R} for the term which we are considering. In this case, we can be more accurate and retain the subterm originating in f .

Definition 10. Abstract term rewriting system Let R be a TRS. Let G_{R} be the corresponding graph of functional dependencies. We define the abstraction of R as follows:

R_{A} = {λ → sh(ρ) ⇐ sh(ẽ) | λ → ρ ⇐ ẽ ∈ R}, where the shell sh(x) of an expression x is defined inductively

sh(x) = \{ \begin{matrix}x & if x ∈ V \\ f (sh(t_{1}),…, sh(t_{k})) & if x = f (t_{1},…, t_{k}) and ⟨x̂, x̂⟩ ∉ G_{R}^{+} \\ sh(l) = sh(r) & if x = (l = r) \\ sh(e_{1}),…, sh(e_{n}) & if x = e_{1},…, e_{n} \\ ⊥ & otherwise \end{matrix}

Note that a corresponding concretization function for abstract term rewriting systems can be easily defined. We can now define abstract basic narrowing.

Definition 11. Let R_{A} be an abstract TRS. Abstract (basic) narrowing is a relation B^{R_{A}} ⊆ State^{⊥} × State^{⊥}, defined as follows.

Let t, t′ ∈ State^{⊥}. ⟨t, t′⟩ ∈ B^{R_{A}} (we also say that there is an abstract (basic) narrowing reduction from t to t′) iff:

1) ∃λ → ρ ⇐ ẽ << R_{A} such that t = ⟨g, κ⟩ and t′ = ⟨g′, κ′⟩ where g′ = (g ∼ {e}) ∪ {e[ρ]_{u}} ∪ ẽ, e ∈ g, u ∈ Ō(e), σ = mgu_{A}({(e_{|u})κ = λ}) and κ′ = κσ; or,

2) t = ⟨g, κ⟩, σ = mgu_{A}(gκ) and t′ = ⟨true, κσ⟩; or,

3) t = t′.

The following lemma is proven in [5] and basically states that abstract (basic) narrowing reduction approximates (basic) narrowing reduction.

Lemma 12. [5] Let s′ ∝ s. If there is a (basic) narrowing reduction from s to t, then there is an abstract (basic) narrowing reduction from s′ to some t′ such that t′ ∝ t.

The following proposition shows that our analysis terminates.

Proposition 13. [5] Let R_{A} be an abstract TRS. The (abstract) transition system for B^{R_{A}}, state s and State^{⊥} has a finite number of (distinct) nodes.

The following auxiliary notions will be used below.

Definition 14. An abstract (basic) narrowing derivation for R_{A}, s and State^{⊥} is relevant if the last node in the derivation is labeled by ⟨true, κ⟩.

Definition 15. Let R_{A} be an abstract TRS. Define Δ(R_{A}, s) to be the set of abstract substitutions κ in the terminal states ⟨true, κ⟩ of the abstract (basic) narrowing derivations which are relevant for R_{A}, s and State^{⊥}.

Δ(R_{A}, s) is the set of the ’computed answer abstract substitutions’ for s. At the end of this section we show that Δ(R_{A}, s) allows us to detect branches of the concrete narrowing search tree which can be safely pruned. We give an example which can help to understand these definitions and motivates the remainder of the section. Let us introduce the auxiliary function ⌊x⌋, which inductively replaces by a fresh variable any term whose outermost symbol is not an irreducible function symbol, i.e.

⌊x⌋ = \{ \begin{matrix}c(⌊t_{1}⌋,…, ⌊t_{k}⌋) & if x = c(t_{1},…, t_{k}) and c ∈ C \\ y & otherwise, where y is a new fresh variable \end{matrix}

The following definition introduces a particular case of graph that satisfies the condition of loop-check of Definition 8. Another different instance can be found in [4,5].

Definition 16. Let R be a TRS. The following transformation defines a directed graph G_{R} of functional dependencies induced by R. Define t̂ = f (⌊t_{1}⌋,…, ⌊t_{n}⌋) if t = f (t_{1},…, t_{n}). To build G_{R}, the algorithm starts with ⟨R, ∅⟩ and applies the inference rules as long as they add new arrows. The symbol ∪ stands for set union.

(1) \frac{r = (λ → ρ ⇐ ẽ) << R}{⟨R, G_{R}⟩ ⟼ ⟨R ∼ \{r\}, G_{R} ∪ \{λ →^{R} t̂ | (t = ρ_{|u} ∧ u ∈ Ō(ρ)) or (t = e_{|u} ∧ e ∈ ẽ ∧ u ∈ (Ō(e) ∼ \{Λ\}))\}⟩}

(2) \frac{(λ →^{R} r) ∈ G_{R} ∧ (λ′ →^{R} r′) ∈ G_{R} ∧ r =^{?} λ′}{⟨R, G_{R}⟩ ⟼ ⟨R, G_{R} ∪ \{r →^{u} λ′\}⟩}

Termination of this calculus is ensured since the number of terms occurring in the rules in R is finite. Roughly speaking, in Definition 16, for each rule (λ → ρ ⇐ ẽ) in R and for each term f (t_{1},…, t_{n}) occurring in ρ or in ẽ, rule (1) adds an arrow λ →^{R} f (⌊t_{1}⌋,…, ⌊t_{n}⌋) to G_{R}. Rule (2) adds an arrow r →^{u} λ′ between the right-hand side r of an arrow λ →^{R} r in G_{R} and the left-hand side λ′ of each arrow λ′ →^{R} r′ with which r unifies. We note that G_{R} associates a path with every basic narrowing derivation issued from a given goal and that it does not require the inspection of the equation set to be solved, as opposed to [8]. We also note that G_{R} consists of the graph of top symbols in [4,5] when t̂ is defined as the function t̂ = f if t = f (t_{1},…, t_{n}). In the following, →^{∗} denotes a path in the graph that may contain arrows →^{R} and arrows →^{u}.

Proposition 17. Let R be a TRS and G_{R} be the graph of terms built from R according to Definition 16. Then G_{R} satisfies the condition of loop-check as established in Definition 8.

Example 2. Let us consider the following level-canonical TRS R and its abstraction R_{A}. Note that R_{A} yields no infinite abstract basic narrowing sequences.

R = {  R_{A} = {
r1) h(0) → 0.  r1_{A}) h(0) → 0.
r2) f (0) → 0. r2_{A}) f (0) → 0.
r3) f (c(X )) → c(f (X )) ⇐ g(X ) = X . r3_{A}) f (c(X )) → c(⊥) ⇐ g(X ) = X .
r4) g(c(X )) → c(X ). }  r4_{A}) g(c(X )) → c(X ). }

We depict in Figure 1 the dependency graph built from R. There is a cycle f (X ) →^{∗} f (X ) →^{∗} … in the graph.

[figure: h(0); 0; f (c(X )); f (X ); c(X ); g(X ); f (0); g(c(X )); R; u; R; u; R; u; R; R; R]

Fig. 1. Graph of functional dependencies

From Lemma 12, there is an abstract narrowing reduction that approximates each basic narrowing reduction from a given goal. The correspondence is most clearly seen in a diagram. We give here an example.

Example 3. Consider again the TRS R from Example 2. Figures 2 and 3 depict the search space of basic narrowing and abstract basic narrowing with initial state s = ⟨h(f (Z )) = 0, ϵ⟩. The leftmost derivation in Figure 3 is relevant. Δ(R_{A}, s) = {Z /0}.

We now establish a preliminary result that clarifies our interest in abstract narrowing reduction.

Theorem 18. Let R be a TRS, s = ⟨g, ϵ⟩ and s′ ∝ s. Let Δ′ = Δ(R_{A}, s′). Then, for every solution θ computed in any successful basic narrowing derivation for R with s, there exists κ ∈ Δ′ such that κ ∝ θ.

This theorem suggests that Δ′ can be used to detect useless concrete computations, i.e. computations which do not lead to any success. We now introduce a relation ♢ which is used to compare two abstract substitutions. In particular, we use ♢ to compare the abstract substitutions in Δ′ with concrete substitutions.

Definition 19. Let ϕ, κ ∈ Sub^{⊥}. We define the relation ϕ ♢ κ by:

ϕ ♢ κ iff ∃θ ∈ Sub^{⊥} such that ϕ ⪯ θ and κ ⪯ θ.

[figure: ⟨{h(c(f (X )))=0,g(X )=X },{Z /c(X )}⟩; ⟨{h(f (Z ))=0},ϵ⟩; ⟨{h(0)=0},{Z /0}⟩; ⟨{0=0},{Z /0}⟩; ⟨true,{Z /0}⟩; ×; …; …; ∞; ∞; ⟨{h(c(0))=0,g(X )=X },; {Z /c(0),X /0}⟩; ⟨{h(c(c(f (X′))))=0,; g(X )=X ,g(X′)=X′},; {Z /c(c(X′)),X /c(X′)}⟩; ⟨{h(c(f (X )))=0,c(X′)=X },; {Z /c(c(X′)),X /c(X′)}⟩]

Fig. 2. Basic narrowing

[figure: ⟨{h(c(⊥))=0,g(X )=X },{Z /c(X )}⟩; ⟨{h(f (Z ))=0},ϵ⟩; ⟨{h(0)=0},{Z /0}⟩; ⟨{0=0},{Z /0}⟩; ⟨true,{Z /0}⟩; ×; ⟨{h(c(⊥))=0,c(X′)=X },{Z /c(c(X′)),X /c(X′)}⟩]

Fig. 3. Abstract basic narrowing

Roughly speaking, two abstract substitutions are in the relation ♢ if and only if they have a common instance. This definition does not provide much intuition about how the test ♢ on abstract substitutions can be performed. At the end of Section 5 we formulate an algorithm which decides this relation.

From Theorem 18 we derive a stronger characterization of successful narrowing derivations. Actually, successful derivations are distinguishable by the following property.

Theorem 20. Let R be a TRS, s = ⟨g, ϵ⟩ and s′ ∝ s. Let Δ′ = Δ(R_{A}, s′). Then, for every substitution θ in any successful basic narrowing derivation for R with s, there exists κ ∈ Δ′ such that κ ♢ θ.

The following result follows immediately from Theorem 20 and represents the basis for our optimization:

Corollary 21. Let R be a TRS and s an initial state. Let ⟨g, θ⟩ be any state of the (basic) conditional narrowing tree for R with s. If there is no κ ∈ Δ(R_{A}, s) such that κ ♢ θ, then there is no successful basic narrowing derivation for ⟨g, θ⟩.

Since the subtree originating in any node which satisfies the requirements of Corollary 21 does not contain any solution, it is useless to explore it. This remark suggests a method to reduce the size of the search tree while still retaining completeness as we formalize in the following section.

5 Using Abstract Narrowing to optimize Narrowing

Let us first introduce a collecting narrowing calculus which explores with a depthfirst strategy the nodes of the abstract transition system for a given set of equations and picks up every abstract substitution in the terminal state of any relevant abstract basic narrowing derivation. Since the number of nodes to be visited is finite, any search strategy which visits the whole graph is complete. We use a depth-first strategy since it results in a ‘programmed’ search which is easy to be tackled formally and easy to implement.

Definition 22. collecting Conditional N arrowing calculus (cCN) Let (Σ, R_{A}) be an abstract term rewriting system. A cCN -state is a pair ⟨L, Δ⟩. The first component L is a list of pairs (s, S), where s = ⟨g, κ⟩ ∈ State^{⊥} and S is a set. The elements of the set are triples ⟨e, u, r⟩, where e is a Σ-equation, u is an occurrence of e and r is (a variant of) a reduction rule in R_{A}. ⟨⟩ is a distinguished element of the sets. The second component Δ of a cCN -state is a set of (abstract) substitutions.

The cCN transition relation is defined as follows:

Unification Rule:

(1) \frac{⟨⟩ ∉ S ∧ σ = mgu_{A}(gκ)}{⟨(⟨g, κ⟩, S) • L, Δ⟩ →_{cCN} ⟨(⟨g, κ⟩, S ∪ \{⟨⟩\}) • L, Δ ∪ κσ⟩}

Narrowing Rule:

(2) \frac{e ∈ g ∧ u ∈ Ō(e) ∧ r = (λ → ρ ⇐ ẽ) << R_{A} ∧ ⟨e, u, r⟩ ∉ S ∧ σ = mgu_{A}(\{(e_{|u})κ = λ\})}{⟨(⟨g, κ⟩, S) • L, Δ⟩ →_{cCN} ⟨(⟨(g ∼ \{e\}) ∪ \{e[ρ]_{u}\} ∪ ẽ, κσ⟩, Ø) • (⟨g, κ⟩, S ∪ \{ ⟨e, u, r⟩\}) • L, Δ⟩}

Removal Rule:

(3) \frac{(1) and (2) do not apply}{⟨(⟨g, κ⟩, S) • L, Δ⟩ →_{cCN} ⟨L, Δ⟩}

Roughly speaking, the abstract state in the left part of a pair (s, S) represents a node of the abstract transition system. The right part of the pair records the redexes of the equation in the abstract state which are reduced together with the corresponding applied rule. ⟨⟩ represents the fact that an abstract mgu of the equations in the state has been found. List constructors are denoted by [ ] and •. The list representing an execution state of the above collecting Conditional N arrowing calculus is treated as a stack to emulate a depth-first strategy. The derivations can be represented as a finite tree. Leaves which have already been visited are simply removed. The calculus can be slightly improved if failed nodes are recognized and removed from the list. A failed node is any node ⟨g, κ⟩ such that one equation e ∈ g is not (abstractly) unifiable and no abstract narrowing step can be applied to any of the occurrences in e.

Definition 23. Behaviour of the cCN calculus Let L = [ ( s, Ø ) ], s ∈ State. Define the function cN (s) as follows:

cN (s) = Δ if ⟨ L, Ø ⟩ →_{cCN}^{∗} ⟨ [ ], Δ ⟩.

We notice that in the case when cN (s) = Ø, the set of equations in s is unsatisfiable.

The following theorem can easily be proved for the collecting narrowing algorithm given in Definitions 22 and 23.

Theorem 24. completeness of collecting Conditional N arrowing Let R_{A} be an abstract TRS. For every substitution κ in the terminal state of any relevant abstract basic narrowing derivation for R_{A} with s, κ ∈ cN (s).

We can now refine the basic Conditional N arrowing calculus in Section 3 by considering the abstract substitutions which are gathered by collecting Conditional N arrowing.

We define a refined Conditional N arrowing calculus (rCN) by means of a two-rule transition system. To solve the equation set g_{0}, the algorithm starts with the initial state s = ⟨g_{0}, ϵ⟩ and tries to derive new goals until a terminal state ⟨true, σ⟩ is reached. In the rules below, we assume Δ = cN (s).

Unification rule:

\frac{σ = mgu(gθ)}{⟨g, θ⟩ ⇝_{r CN} ⟨true, θσ⟩}

Narrowing rule:

\frac{e ∈ g ∧ u ∈ Ō(e) ∧ (λ → ρ ⇐ ẽ) << R ∧ σ = mgu(\{(e_{|u})θ = λ\}) ∧ ∃ρ ∈ Δ. ρ ♢ θσ}{⟨g, θ⟩ ⇝_{r CN} ⟨(g ∼ \{e\}) ∪ \{e[ρ]_{u}\} ∪ ẽ, θσ⟩}

We give an example which illustrates how the optimization works.

Example 4. Consider the TRS R from Example 3. Applying rCN for R with initial state ⟨h(f (Z )) = 0, ϵ⟩ results in the tree which is depicted in Figure 4. Let us notice that the subtree originating from the right-hand descendant of the root of the tree in Figure 2 has been eliminated. We note also that the removed subtree could not have been dropped using either of the standard simplifying strategies of narrowing which rest on the use of loop-checking [8], unification rules [13], operator joinability [12] or eager normalization [2,12] techniques.

[figure: ⟨{h(f (Z ))=0},ϵ⟩; ⟨{h(0)=0},{Z /0}⟩; ⟨{0=0},{Z /0}⟩; ⟨true,{Z /0}⟩; ×]

Fig. 4. Refined basic narrowing

The following theorem proves that our approach is sound and complete.

Theorem 25. correctness and completeness of refined Conditional N arrowing Let E be a level-canonical Horn equational theory with associated TRS R. The set {σ_{|V̀ar(g)} | ⟨g, ϵ⟩ ⇝_{r CN}^{∗} ⟨true, σ⟩} is a complete set of E-unifiers of g.

Finally we show how the test ♢ of ‘compatibility’ on abstract substitutions can be effectively checked by providing an algorithm to decide it. First we need to extend the notion of parallel composition [25] from substitutions to abstract substitutions.

Parallel composition was proposed in [25] in order to provide a compositional characterization of the semantics of Horn Clause Logic. The formalization was also extended to a parallel execution model of logic programs. When two atoms (in the same goal) are run in parallel, the associated computed answer substitutions have to be combined afterwards in order to get the final result. Parallel composition of substitutions exactly corresponds to the least upper bound.

Roughly speaking, parallel composition is the operation of unification generalized to substitutions. It can be performed in the following way [25]. Given two idempotent substitutions ϑ_{1} and ϑ_{2}, consider the set of all pairs corresponding to the bindings of both ϑ_{1} and ϑ_{2}. Then, compute the most general unifier of such a set. Note that the consistency check can be thought of as a simple verification that such a set is unifiable.

We extend the notion of parallel composition from substitutions to abstract substitutions by replacing unification by abstract unification. In the following definition we introduce the notion of abstract parallel composition, denoted by ⇑.

Definition 26. abstract parallel composition Let ϕ, κ ∈ Sub^{⊥}. We define the abstract parallel composition ϕ ⇑ κ by:

ϕ ⇑ κ = mgu_{A}(ϕ ∪ κ).

Now the compatibility ϕ ♢ κ of two abstract substitutions exactly corresponds to check that ϕ ⇑ κ is not fail.

Proposition 27. Let ϕ, κ ∈ Sub^{⊥}. Then ϕ ♢ κ iff (ϕ ⇑ κ) ≢ fail.

6 Conclusions

We have formalized an optimization of basic conditional narrowing which makes use of an abstract interpretation algorithm to identify the narrowing derivations possibly leading to solutions. Thus the other derivations are not computed. The notions of relevant abstract basic narrowing derivation and abstract parallel composition have been introduced for this purpose. We have proved that the completeness result of the basic procedure is preserved in the refinement. An example illustrates the fact that this optimization can increase the efficiency of narrowing in addition to improving its termination. We note that the refinement applies also to full conditional narrowing, although the search tree exhibits, in this case, a much larger branching factor.

A prototype system based on the ideas described in this work has been implemented. In spite of the fact that it does not have the simplicity of simple basic narrowing, we have chosen to implement an innermost selection basic conditional narrowing procedure [3,15,16] since it further reduces the size of the search space.

It is difficult to state a general result for the efficiency improvement of the optimization. Table 1 gives an impression of some achievable speed-ups. We report the timings relative to some simple benchmarks for the program:

   h(s(X)) → h(X) ⇐ g(s(X))=s(X), g(X)=X.
   f(c(X)) → c(f(X)) ⇐ g(X)=X.
   g(c(X)) → c(X).
   g(s(X)) → s(X).
   h(0) → 0.
   f(0) → s(s(0)).
   g(0) → 0.

In these tests we are able to avoid up to 70% of unnecessary narrowing attempts,

                    first solution found  termination achieved

Goal  basic  refined  basic  refined  cT

 g(h(s(0))) = X.      0.14       0.18      0.94       1.12       1.30
   h(f(Z))=0.        8.22       1.48  ∞  0.00       0.74
  h(f(g(Z)))=0.       8.38       1.64  ∞  0.00       1.02
f(g(X)) = Z, h(Z)=0.  111.56     13.44  ∞  0.00       8.84

Table 1. Basic vs. refined narrowing times (secs, using BIM-Prolog, SUN 3/80)

with no prohibitive time overhead due to collecting Conditional N arrowing (column cT ). Our experiments indicate that the strategy can be a useful tool in the optimization of equational logic programs.

Since our method can be seen as parametric with respect to the loop check, any improvement on the loop-checking technique would correspondingly yield to an improvement of the accuracy of our description. An interesting topic for further research is the question of how it is possible to improve our method by strengthening the construction of the dependency graph in order to get more accurate approximations. This seems dificult to do while retaining the ability to check the rewrite rules without inspecting the goal. Another topic of further research concerns the parallel implementation of the consistency check.

References

1. G. Aguzzi, U. Modigliani, and M.C. Verri. A Universal Unification Condition for Solving Goals in Equational Languages. In Proc. of CTRS’90, volume 516 of Lecture Notes in Computer Science, pages 416–423. Springer-Verlag, Berlin, 1990.

2. H. Aït-Kaci, P. Lincoln, and R. Nasr. Le Fun: Logic, equations, and Functions. In Proc. of the Fourth IEEE Symposium on Logic Programming, pages 17–23. IEEE Computer Society Press, 1987.

3. M. Alpuente, M. Falaschi, and G. Levi. Incremental Constraint Satisfaction for Equational Logic Programming. Technical Report TR-20/91, Dipartimento di Informatica, Università di Pisa, 1991. to appear in Theoretical Computer Science.

4. M. Alpuente, M. Falaschi, and F. Manzo. Analyses of Inconsistency for Incremental Equational Logic Programming. In M. Bruynooghe and M. Wirsing, editors, Proc. of PLILP’92, Leuven (Belgium), volume 631 of Lecture Notes in Computer Science, pages 443–457. Springer-Verlag, Berlin, 1992.

5. M. Alpuente, M. Falaschi, and F. Manzo. Analyses of Unsatisfiability for Equational Logic Programming. Technical Report DSIC-II/29/92, UPV, 1992. submitted for publication.

6. M. Alpuente, M. Falaschi, M.J. Ramis, and G. Vidal. Narrowing Aproximations as an optimization for Equational Logic Programs. Technical Report DSIC-II/1/93, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, 1993.

7. P. Bosco, E. Giovannetti, and C. Moiso. Narrowing vs. SLD-resolution. Theoretical Computer Science, 59:3–23, 1988.

8. J. Chabin and P. Réty. Narrowing directed by a graph of terms. In G. Goos and J. Hartmanis, editors, Proc. of RTA’91, volume 488 of Lecture Notes in Computer Science, pages 112–123. Springer-Verlag, Berlin, 1991.

9. J. Christian. Some termination criteria for narrowing and E-narrowing. In 11th Int’l Conf. on Automated Deduction, volume 607 of Lecture Notes in Computer Science, pages 582–588. Springer-Verlag, Berlin, 1992.

10. M. Codish, M. Falaschi, and K. Marriott. Suspension Analysis for Concurrent Logic Programs. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 331– 345. The MIT Press, Cambridge, Mass., 1991.

11. 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 and The MIT Press, Cambridge, 1990.

12. N. Dershowitz and G. Sivakumar. Solving Goals in Equational Languages. In S. Kaplan and J. Joaunnaud, editors, Proc. First Int’l Workshop on Conditional Term Rewriting, volume 308 of Lecture Notes in Computer Science, pages 45–55. Springer-Verlag, Berlin, 1987.

13. L. Fribourg. Slog: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. Second IEEE Int’l Symp. on Logic Programming, pages 172–185. IEEE, 1985.

14. J.H. Gallier and S. Raatz. Extending SLD-resolution to equational Horn clauses using E-unification. Journal of Logic Programming, 6:3–43, 1989.

15. E. Giovannetti and C. Moiso. A completeness result for E-unification algorithms based on Conditional Narrowing. In M. Boscarol, L. Carlucci, and G. Levi, editors, Foundations of Logic and Functional Programming, volume 306 of Lecture Notes in Computer Science, pages 157–167. Springer-Verlag, Berlin, 1986.

16. S. Hölldobler. Foundations of Equational Logic Programming, volume 353 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1989.

17. J.M. Hullot. Canonical Forms and Unification. In 5th Int’l Conf. on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 318–334. Springer-Verlag, Berlin, 1980.

18. J. Jaffar, J.-L. Lassez, and M.J. Maher. A logic programming language scheme. In D. de Groot and G. Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 441–468. Prentice Hall, Englewood Cliffs, NJ, 1986.

19. J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume I. Oxford University Press, 1991.

20. 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.

21. M. J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proc. Third IEEE Symp. on Logic In Computer Science, pages 348–357. Computer Science Press, New York, 1988.

22. M. J. Maher. On parameterized substitutions. Technical Report RC 16042, IBM - T.J. Watson Research Center, Yorktown Heights, NY, 1990.

23. A. Middeldorp and E. Hamoen. Counterexamples to completeness results for basic narrowing. In H. Kirchner and G. Levi, editors, Proc. Third Int’l Conf. on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 244–258. Springer-Verlag, Berlin, 1992.

24. W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295–317, 1989.

25. C. Palamidessi. Algebraic properties of idempotent substitutions. In M. S. Paterson, editor, Proc. of the 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 386– 399. Springer-Verlag, Berlin, 1990.

26. P. Réty, C. Kirchner, H. Kirchner, and P. Lescanne. NARROWER: A new algorithm for unification and its applications to logic programming. In Proc. of RTA’85, volume 202 of Lecture Notes in Computer Science, pages 141–157. Springer-Verlag, Berlin, 1985.

27. J.H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7:207–274, 1989.

This article was processed using the LaTEX macro package with LLNCS style