Conditional Narrowing without Conditions^{∗}

Sergio Antoy

Department of Computer Science

Portland State University P.O. Box 751, Portland, OR 97207, U.S.A.

antoy@cs.pdx.edu Bernd Brassel Michael Hanus

Institut f� ur Informatik Christian-Albrechts-Universit� at Kiel

Olshausenstr. 40, D-24098 Kiel, Germany

Phone: +49-431/880-7271 / Fax: +49-431/880-7613

{bbr,mh}@informatik.uni-kiel.de

ABSTRACT

We present a new evaluation strategy for functional logic programs described by weakly orthogonal conditional term rewriting systems. Our notion of weakly orthogonal conditional rewrite system extends a notion of Bergstra and Klop and covers a large part of programs defined by conditional equations. Our strategy combines the flexibility of logic programming (computation of solutions for logic variables) with efficient evaluation methods from functional programming. In particular, it is the first known narrowing strategy for this class of programs that evaluates ground terms deterministically. This is achieved by a transformation of conditional term rewriting systems (CTRS) into unconditional ones which is sound and complete w.r.t. the semantics of the original CTRS. We show that the transformation preserves weak orthogonality for the terms of interest. This property allows us to apply a relatively efficient evaluation strategy for weakly orthogonal unconditional term rewriting systems (parallel narrowing) on the transformed programs.

Categories and Subject Descriptors

D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.1.6 [Programming Techniques]: Logic Programming; F.4.2 [Mathematical Logic and Formal Languages]: Grammars and other Rewriting Systems; I.2.2 [Automatic Programming]: Program Transformation

General Terms

Languages, Theory

Keywords

Functional Logic Programming, Narrowing, Evaluation Strategies, Conditional Rewriting

∗This research has been partially supported by the DAAD/NSF grant INT-9981317, the German Research Council (DFG) grant Ha 2457/1-2 and the NSF grants CCR-0110496 and CCR-0218224.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for pro�t or commercial advantage and that copies bear this notice and the full citation on the �rst page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior speci�c permission and/or a fee. PPDP’03, August 27�29, 2003, Uppsala, Sweden. Copyright 2003 ACM 1-58113-705-2/03/0008 ...$5.00.

1. MOTIVATION

Functional logic programming is an approach to combine the best features of functional and logic programming in a single programming model. A reasonable functional logic language should combine the (functional programming) idea of efficient evaluation by demand-driven and deterministic reduction, if possible, with the flexibility of logic programming by dealing with logic variables, partial data structures, and goal solving (see [18] for a survey on functional logic programming). Many language proposals (see, for instance, [18, 21, 26, 28, 35, 34]) have shown that such a combination is possible in principle. However, the choice of a “good” evaluation strategy is a crucial point in this combination. Simple narrowing calculi support completeness for large classes of programs but are often not an appropriate basis for a good evaluation strategy (compare also the discussion in [2] on this topic). On the other hand, sophisticated narrowing strategies have often stronger restrictions on the programs. For instance, innermost narrowing strategies require the termination of the rewrite relation in order to ensure completeness. Clearly, a termination requirement is too strong for practical programming since it inhibits the formulation of some programs (e.g., interpreters).^{1} Needed narrowing [5] is a sound, complete, and optimal strategy for the class of inductively sequential programs [1] where functions are defined by induction on the term structure and can be evaluated sequentially. This class is also characterized as the strongly sequential constructor systems [20]. Although this covers a large part of typical declarative programs, it excludes functions defined by rules with overlapping lefthand sides (like the classical “parallel or” example). In order to support the latter kind of function definitions, weakly needed narrowing has been proposed [4, 27] which guesses the next reducible expression (redex) non-deterministically in case of functions defined by overlapping rules. The amount of nondeterminism is reduced in parallel narrowing [4] by guessing only variable instantiations and reducing disjoint outermost redexes in parallel. This has the positive effect that ground terms are evaluated in a deterministic manner. Weakly needed narrowing and parallel narrowing have been proved to be complete for the class of weakly orthogonal (see Definition 10) constructor-based unconditional term rewriting systems (TRS).

In this paper we want to exploit the positive properties of parallel narrowing to develop a new strategy for conditional term rewriting

1Note that strict functional languages are based on innermost reduction (and some non-strict constructs like if-then-else) but do not have a termination requirement since they do not ensure completeness w.r.t. an equational interpretation of the defining rules. This requires a more careful construction of programs in comparison to languages with more sophisticated evaluation strategies, as discussed in [19]. systems (CTRS) that is deterministic on ground terms, i.e., inherits an important property from functional programming. Since we are interested in programming languages (rather than specification languages), we do not require terminating TRSs but restrict ourselves to left-linear and constructor-based TRSs. Without always mentioning this explicitly, we assume that all considered TRSs belong to this class. The class of CTRSs is of considerable interest since it is often natural to express functions by the use of conditions as shown in the following example.

Example 1. Conditional TRS for the absolute value

abs(x) → x if x ≥ 0 →^{∗} true
abs(x) → −x if x < 0 →^{∗} true

The question is how to deal with the evaluation of conditions. In the deterministic world of functional programming, conditions are normally tested in a sequential if-then-else style. This works well for many functions, like abs. However, problems arise when the test of some (but not all) of the conditions might lead to infinite computations. To understand this problem, refer to the next example.

Example 2. A specialized multiplication

gmult(x, y) → 0  if g(x) →^{∗} 0
gmult(x, y) → 0  if g(y) →^{∗} 0

gmult(x, y) → g(x) ∗ g(y)

if g(x) > 0 ∧ g(y) > 0 →^{∗} true

The function in Example 2 specializes the multiplication of terms that will be processed by the unary function g. It is not necessary to consider the details of g’s definition. It is enough to remark that the computation of g(x) can be long and tedious (or even infinite) for some values of x. Thus, it makes sense to take a “shortcut” when the result of g(x) ∗ g(y) is known to be 0 before finishing the evaluation for both arguments.^{2} It is intended that gmult has a well defined normal form if possible, even if one of the arguments is undefined (e.g., leads to an infinite computation). Suppose that g(0) →^{∗} 0 and g(∞) → g(∞), both terms gmult(0, ∞) and gmult(∞, 0) should evaluate to 0.

It is easy to see that no sequential evaluation in a fixed order can obtain both results. Testing rule one first will lead into an infinite computation with the term gmult(∞, 0), while preferring the second rule does not lead to the desired result in the opposite case gmult(0, ∞).

Logic programming implementations test conditions in a “don’t know” nondeterministic manner. However, this does not solve the problem of possible infinite computations but depends on the search strategy employed. Using a depth-first search (i.e., backtracking), the problem is identical to the functional case, since one has to decide which condition should be evaluated first. A breadthfirst search gives rise to another problem. Beside being relatively expensive, a breadth-first search would still go on looking for possible answers after a first solution is found, thereby still computing infinitely for both terms. Note that this infinite computation is not necessary, as the first computed answer is the only interesting for gmult. This is due to the fact that gmult is a weakly orthogonal CTRS (see Definition 14 below).

2The apparent loss in efficiency because of computing g(x) and g(y) more than once can easily be remedied by employing a technique called sharing in the implementation of the functional logic language. Sharing allows one to define that all the occurrences of g(x) are identical (share the same value) consequently omitting repeated computations.

In this paper we present a different approach which avoids the described problems and yields the desired semantics. For this purpose, we will transform the conditional program into an unconditional one and then apply parallel narrowing to the transformed program. As mentioned above, parallel narrowing keeps the advantages of functional programming since the strategy works deterministically on ground terms. As we shall see, this advantage will also be present for conditional TRSs due to our transformation. The source systems of our transformation are the constructor-based conditional weakly orthogonal term rewriting systems. We impose an additional condition, Definition 16, which does not actually restrict the source systems. We require that if two rules’ left-hand sides overlap, then the rules’ left-hand sides are equal (modulo a renaming of variables). Every source system can be easily transformed to satisfy this additional condition.

This paper is organized as follows. Section 2 gives definitions for some standard notions and clarifies our notation. Section 3 surveys some former work on transforming conditional TRSs to unconditional ones and then introduces our own transformation, followed by proofs of its key properties. In Sections 3 and 4 we apply our transformation to conditional functional logic programs and prove that important properties of the conditional programs will be preserved by the transformation. These properties enable us to apply parallel narrowing on the result of our transformation, as we will show in Section 5. Finally, Section 6 contains our conclusions along with further discussion of related work based on the results of sections 3-5.

2. PRELIMINARIES

The following definitions are quite standard but necessary to fix our notations. We define term rewriting, both conditional and unconditional, and narrowing together with the necessary notions. We use the standard notations according to [7, 12, 25].

Definition 1. (Signature, T (Σ, X), Var(t), Ground Term, Linear Term) A many-sorted signature Σ is a pair (S, Ω) where S is a set of sorts and Ω is a family of sets of operations of the form Ω = (Ω_{w,s}|w ∈ S^{∗}, s ∈ S). Let X = (X_{s}|s ∈ S) be an S-sorted, countably infinite set of variables. Then the set T (Σ, X)_{s} of terms of sort s built from Σ and X is the smallest set containing X_{s} such that f(t_{1}, …, t_{n}) ∈ T (Σ, X)_{s} whenever f ∈ Ω_{(s_{1},...,s_{n}),s} and t_{i} ∈ T (Σ, X)_{s_{i}}. If f ∈ Ω_{ϵ,s}, we write f instead of f(). T (Σ, X) denotes the set of all terms. The set of variables occurring in a term t is denoted by Var(t). A term t is called ground term if Var(t) = ∅. A term is called linear if it does not contain multiple occurrences of one variable. In the following, Σ stands for a manysorted signature. ⋄

Next we define the notion of a constructor-based term rewriting system. In such a TRS there is a distinction between reducible terms and pure data structures. This distinction is made by dividing the set of operation symbols of a signature into constructors and defined operations. Data structures are built with constructors (constructor terms) and the actual rewriting logic is formulated with defined operations.

Definition 2. (Constructor(-Rooted) Term, Pattern, Constructor-Based TRS) The set of operations Ω of a signature Σ is partitioned into two disjoint sets C and D. C is the set of constructors and D is the set of defined operations. The terms in T (C, X) are called constructor terms. A term f(t_{1}, …, t_{n}) (n ≥ 0) is called a pattern if f ∈ D and t_{1}, …, t_{n} are constructor terms. A term f(t_{1}, …, t_{n}) (n ≥ 0) is called operation-rooted (constructorrooted) if f ∈ D (f ∈ C). A constructor-based term rewriting system is a set of rewrite rules, l → r, such that l and r have the same sort, l is a pattern, and Var(r) ⊆ Var(l). ⋄

As we shall see in the next section, constructor-based TRSs are easier to handle than general TRSs, and consequently most functional logic programs are constructor-based.^{3} Therefore, we define a program as follows:

Definition 3. (Left-Linear TRS, Program) A constructor-based term rewriting system is called left-linear if for each of its rewrite rules l → r the pattern l is linear. A program is a left-linear constructor-based rewriting system. In the following, R denotes a program and Σ_{R} its signature. ⋄

The main purpose of this paper is to give a transformation for conditional term rewriting systems in order to apply parallel narrowing on the resulting unconditional TRS. We therefore have to introduce the syntax of CTRSs:

Definition 4. ((Constructor-Based) Conditional TRS, (Un-) Conditional Rule) A conditional term rewriting system (CTRS) is a set of rewrite rules which have either the form “l → r if u →^{∗} v” or “l → r” such that l and r, u and v have the same sort, respectively, and Var(r) ∪ Var(u) ∪ Var(v) ⊆ Var(l). The rules of the form “l → r if u →^{∗} v” are called conditional rules, the remaining rules are called unconditional. In the following, CTRSs will be denoted as ℜ.^{4} If for each rule in ℜ l is a pattern and for each conditional rule in ℜ v is a ground constructor term, then ℜ is called constructor-based. In this paper, we will exclusively be concerned with left-linear CTRSs. ⋄

Our definition of conditional TRSs seems rather restricted. However, a few considerations show that the restrictions are not too serious: First, the definition allows only a single condition for each rule. Using tuples, multiple conditions of the form

l → r if u_{0} →^{∗} v_{0} ∧ … ∧ u_{n} →^{∗} v_{n}

can easily be expressed with a single condition

l → r if (u_{0}, …, u_{n}) →^{∗} (v_{0}, …, v_{n})

Second, the restriction to conditions where a term is tested for reducibility to a ground constructor term is also reasonable since it covers the equation solving capabilities of current functional logic languages with a lazy operational semantics, like Curry [21] or TOY [28]. These languages are based on strict equality “≈” tests in conditions (t_{1} ≈ t_{2} holds if t_{1} and t_{2} are reducible to the same ground constructor term). Strict equality can be defined as a binary operation by a set of orthogonal rewrite rules (e.g., see [5]). In this case, a conditional rule with a strict equality condition “u ≈ v” can be expressed as l → r if (u ≈ v) →^{∗} true. Similarly, non-left-linear rules f(x, x) → r can be transformed into f(x, y) → r if x ≈ y →^{∗} true. For a discussion that this elimination of non-linearity makes good sense cf. [2, section 4.1].

3See, for instance, the Equational Interpreter [32] and the functional logic languages ALF [17], BABEL [31], Curry [21], K-LEAF [15], LPG [10], SLOG [14], and TOY [28]. 4There is a reason for the notation of R for an unconditional and ℜ for a conditional TRS and it is thus easy to memorize: Both Rs stand for ”rewriting system” and choosing the old style letter to denote a CTRS is a metaphor for our aim to transform TRSs into CTRSs; in the flow of time old things change to new ones and ℜ becomes R.

Finally, it will be discussed in the last section that omitting extra variables for local definitions like let-clauses (cf. [33]) is not a restriction, since let-clauses can be eliminated by standard lambda lifting [24].

We now turn to the semantics of TRSs, but we need a few more notions to define rewriting. One of the key operations on terms is substitution:

Definition 5. ((Constructor) Substitution, Instance, Variant, Unifier) A substitution is a mapping σ: X → T (Σ, X) with σ(x) ∈ T (Σ, X)_{s} for all x ∈ X_{s} such that its domain Dom(σ) = {x ∈ X | σ(x) ≠ x} is finite. We frequently identify a substitution σ with the set {x ↦ σ(x) | x ∈ Dom(σ)}. Substitutions are extended to morphisms on T (Σ, X) by σ(f(t_{1}, …, t_{n})) = f(σ(t_{1}), …, σ(t_{n})) for every term f(t_{1}, …, t_{n}). A substitution σ is called a constructor substitution if σ(x) is a constructor term for all x ∈ Dom(σ). A term t′ is an instance of t if there is a substitution σ with t′ = σ(t). If t is an instance of t′ and vice versa, we call t′ a variant of t. A unifier of two terms s and t is an idempotent substitution σ with σ(s) = σ(t). ⋄

When dealing with terms, one wants to be able to identify unambiguously each of its parts (subterms). This is done by defining the positions of a term:

Definition 6. (Occurrence, Position, Λ, t|_{p}, t[s]_{p}, p ≤ q, p ∥ q, p · q) An occurrence or position is a sequence of positive integers identifying a subterm in a term. For every term t, the empty sequence is denoted by Λ and identifies t itself. For every term of the form f(t_{1}, …, t_{k}), the sequence i · p, where i is a positive integer not greater than k and p is a position, identifies the subterm of t_{i} at p. The subterm of t at p is denoted by t|_{p} and the result of replacing t|_{p} with s in t is denoted by t[s]_{p}. If p and q are positions, we write p ≤ q if p is a prefix of q and we say that p is above q. We write p ∥ q if the positions are disjoint, i.e., none of them is above the other (see [12] for details). The expression p · q denotes the position resulting from the concatenation of the positions p and q, i.e., the symbol “·” is overloaded. ⋄

Now we are ready to define rewriting.

Definition 7. (Reduction t →_{p, R} s, Redex, →^{∗}, Normal Form) A reduction step is an application of a rewrite rule to a term, i.e., t →_{p, R} s if there exist a position p, a rewrite rule R = l → r and a substitution σ with t|_{p} = σ(l) and s = t[σ(r)]_{p}. In this case we say t is rewritten (at position p) to s and t|_{p} is a redex of t. We will omit the subscripts p and R if they are clear from the context. →^{∗} denotes the transitive and reflexive closure of →. A term t is reducible to a term s if t →^{∗} s. A term t is called irreducible or in normal form if there is no term s with t → s. A term s is a normal form of t if t is reducible to the irreducible term s. When considering two TRSs R and R′ simultaneously, we write →^{∗}_{R} and →^{∗}_{R′} to distinguish the rewrite relation defined by R and R′, respectively. ⋄

Rewriting in conditional TRSs is defined by extending unconditional rewriting by the evaluation of conditions:

Definition 8. (Conditional Rewriting) The rewrite relation →^{∗}_{ℜ} for a CTRS ℜ is defined by induction: →_{ℜ_{0}}=→_{R}, where R is the set of unconditional rules in ℜ. s →_{ℜ_{n+1}} t iff either s →_{ℜ_{n}} t or there exists a rule l → r if

u →^{∗} v in ℜ with s →_{l→r} t and u →^{∗}_{ℜ_{n}} v.

Then s →^{∗}_{ℜ} t iff there is a natural number n with s →^{∗}_{ℜ_{n}} t. ⋄ Rewriting is computing, i.e., the value of a functional expression is its normal form obtained by rewriting. Functional logic programs compute with partial information, i.e., a functional expression may contain logic variables. The goal is to compute values for these variables such that the expression is evaluable to a particular normal form, e.g., a constructor term [15, 31]. This is done by narrowing.

Definition 9. (Narrowing t ⇝_{p, l→r, σ} s, t ⇝^{∗}_{σ} s) A term t is narrowable to a term s if there exist a non-variable position p of t (i.e., t|_{p} ∉ X), a variant l → r of a rewrite rule in R with Var(t) ∩ Var(l → r) = ∅ and a unifier σ of t|_{p} and l such that s = σ(t[r]_{p}). In this case we write t ⇝_{p, l→r, σ} s. ⋄

Finally, we need the notion of orthogonal programs:

Definition 10. ((Weak) Orthogonality, Overlapping Rule) A program R is called orthogonal if, for all distinct rules l_{1} → r_{1} and l_{2} → r_{2}, chosen with no variables in common, there is no unifier for l_{1} and l_{2}. If there is a unifier of l_{1} and l_{2}, the rules are called overlapping. R is called weakly orthogonal if all unifiers of l_{1} and l_{2} are also unifiers of r_{1} and r_{2}.^{5} ⋄

We will transfer the notion of (weak) orthogonality to conditional TRSs. Since our notion is not standard, we will present the definition later in Section 4.

3. TRANSFORMATION OF CONDITIO-NAL TERM REWRITING SYSTEMS

A lot of research has been invested in conditional TRSs, particularly, in attempts to transform them into unconditional ones. Early work has been done by Bergstra and Klop [8]. The transformation presented there has been later shown to be unsound in [13] (see also [36, 11]). Further transformations were introduced in [16] and [22] but they demand terminating conditional TRSs. As mentioned in Section 1, a termination requirement is too restrictive for functional logic programming.

In [9] it was shown that CTRSs have in a sense more expressive power since they are more compact: an equivalent unconditional system has to use more function symbols or function symbols with greater arity to express the same content. Nevertheless, it is possible to construct an equivalent (see Theorems 1 and 3 to see in detail what the notion “equivalence” means in this context) TRS for a given CTRS. It is the aim of this section to introduce such a transformation for constructor-based left-linear CTRSs. Further related work will be discussed in the last section when we have some results to remark upon.

Antoy [2] has presented a transformation for arbitrary constructor-based CTRSs into the class of “overlapping inductively sequential” TRSs. These are inductively sequential TRSs with possibly multiple right-hand sides for a single rule. Since this transformation maps different conditional rules into multiple right-hand sides that are non-deterministically evaluated, the transformation does not lead to a deterministic evaluation of ground terms. Therefore, our transformation is based on the idea to join all conditions into a single structure. This idea was proposed by Viry [36] for general CTRSs so that we present his transformation first:

Definition 11. (Transformation of Viry, t^{X}, t^{⊥}, \overline{t}, Instantiating Rule, Reducing Rule) Let ℜ be a conditional term rewriting system. For each n-ary defined function f ∈ ℜ let

5Note that our definition of (weak) orthogonality makes use of the restriction to constructor-based TRSs. In such systems overlapping of different rules can only occur at root position. ρ_{f,1}, …, ρ_{f,m} be the conditional and ρ_{f,m+1}, …, ρ_{f,m+k} the unconditional rules defining f in ℜ. Each defined n-ary function f is replaced by an (n + m)-ary function f (i.e., for each conditional rule an argument is added) and the new set of unconditional rules R_{V} contains for each conditional rule

ρ_{f,i} : f(t_{1}, …, t_{n}) → r_{f,i} if u_{f,i} →^{∗} v_{f,i}

two unconditional rules

\begin{matrix}ρ′_{f,i} : & f(t_{1}^{X}, …, t_{n}^{X} | y_{1}, …, & ⊥_{i}, & …, y_{m}) \\ → f(t_{1}^{X}, …, t_{n}^{X} | y_{1}, …, & [u_{f,i}^{⊥}, x⃗], & …, y_{m}) \end{matrix}

(the notation ⊥_{i} denotes ⊥ at argument i) and

ρ′′_{f,i} : f(z_{1}, …, z_{n} | y_{1}, …, [v_{f,i}^{X}, x⃗], …, y_{m}) → r_{f,i}^{⊥},

where x⃗ = (x_{1}, …, x_{j}) if Var(r_{f,i}) = {x_{1}, …, x_{j}}, for some arbitrary, but fixed, ordering of the variables. For replacing the unconditional rules, one needs new variables. X denotes an infinite set of fresh variables. Each unconditional rule ρ_{f,i} : f(t_{1}, …, t_{n}) → r_{f,i} is replaced by the rule

ρ′′_{f,i} : f(t_{1}^{X}, …, t_{n}^{X} | y_{1}, …, y_{m}) → r_{f,i}^{⊥}

The new conditional arguments are filled via the mappings t^{X} and t^{⊥} of type T (Σ_{ℜ}, X) → T (Σ_{R_{V}} , X). t^{X} and t^{⊥} put fresh variables and the symbol ⊥ at these new arguments, respectively:

t^{X} = \begin{cases}t & if t ∈ X \\ f(t_{1}^{X_{1}}, …, t_{n}^{X_{n}} | y_{1}, …, y_{m}) & if t = f(t_{1}, …, t_{n}) \end{cases}

where X_{1}, …, X_{n}, {y_{1}, …, y_{m}} are pairwise disjoint subsets of X with X_{1}, …, X_{n} infinite.

t^{⊥} = \begin{cases}t & if t ∈ X \\ f(t_{1}^{⊥}, …, t_{n}^{⊥} | ⊥, …, ⊥) & if t = f(t_{1}, …, t_{n}) \end{cases}

The symbol ⊥ is a constructor not in Σ and the grouping of terms with parentheses and square brackets is only syntactic sugar to avoid the introduction of new symbols. The mapping t̄ : T (Σ_{R_{V}} , X) → T (Σ_{ℜ}, X) deletes the conditional arguments in a term t:

t̄= \begin{cases}t & if t ∈ X \\ f(t̄_{1}, …, t̄_{n}) & if t = f(t_{1}, …, t_{n} | s_{1}, …, s_{m}) \end{cases}

The ρ′-rules will be called instantiating rules, because they instantiate the new conditional positions, and the ρ′′-rules will be called reducing rules, because they correspond to the reduction steps of the original system. ⋄

Example 3. Transforming the rules of Example 1 leads to the following TRS:

abs(x | ⊥, y_{2})  → abs(x | [x ≥ 0, (x)], y_{2})
abs(x | y_{1}, ⊥)  → abs(x | y_{1}, [x < 0, (x)])
abs(y_{0} | [true, (x)], y_{2}) → x
abs(y_{0} | y_{1}, [true, (x)]) → −x

The following two theorems by Viry are of interest for the remaining paper.

Theorem 1. (Viry [36]) The transformation V is sound and complete for all conditional rewrite systems, i.e.,

1. for each derivation t →^{∗}_{ℜ} t′ there is a derivation t^{⊥} →^{∗}_{R_{V}} t^{′⊥} (completeness), 2. for each derivation t^{⊥} →^{∗}_{R_{V}} t′ there is a derivation t →^{∗}_{ℜ} t̄′

(soundness).

Note that, by defining soundness this way, it is implied that only a certain part of the target system R_{V} is relevant for simulating ℜ.^{6} If arbitrary terms of the target system are considered, soundness can not be ensured. For instance, in the system of Example 3, the term abs(x | [true, (x)], [true, (x)]) is contained in T (Σ_{R_{V}} , X). It is immediate to see that this term could cause problems in the context of the source system since it denotes that both x ≥ 0 and x < 0 could be evaluated to true. Therefore, we define the terms of interest:

Definition 12. (Terms of Interest, Bottom Term) Let R_{V} be the result of applying Viry’s transformation to a CTRS ℜ. Then the terms of interest T_{R_{V}} ⊂ T (Σ_{R_{V}} , X) are all terms with uninstantiated conditional positions (bottom terms) closed under

derivation: T_{R_{V}} := {u | ∃t ∈ T (Σ_{ℜ}, X) ∧ t^{⊥} →^{∗} u}. ⋄

It is easy to see that this definition excludes the example abs(x | [true, (x)], [true, (x)]) (unless in the semantics of the source system both x ≥ 0 and x < 0 can really be evaluated to true for some x).

The following proposition is important for the use of terms of interest:

Proposition 1. For each t ∈ T_{R_{V}} each subterm of t is also in T_{R_{V}} and for each substitution σ which replaces variables only with terms of interest, σ(t) is also in T_{R_{V}}.

An interesting question is the preservation of confluence, i.e., given a confluent ℜ, is R_{V} confluent, too? This cannot be ensured in general, as shown in the following example.

Example 4. Consider the confluent CTRS ℜ defined by the rules

\begin{aligned}f(g(x)) & → & x & if x →^{∗} 0 \\ g(g(x)) & → & g(x) \end{aligned}

The corresponding TRS R_{V} is

\begin{aligned}f(g(x) | ⊥) & → & f(g(x) | [x, (x)]) \\ f(y_{0} | [0, (x)]) & → & x \\ g(g(x)) & → & g(x) \end{aligned}

Note that g(x)^{X} = g(x) since no rule defining g is conditional. Now there is an R_{V}-derivation yielding two different normal forms (contracted redexes are underlined):

f(\underline{g(g(0))} | ⊥) → \underline{f(g(0) | ⊥)}

→ \underline{f(g(0) | [0, (0)])} → 0

\underline{f(g(g(0)) | ⊥)} → f(\underline{g(g(0))} | [g(0), (g(0))])

→ f(g(0) | [g(0), (g(0))])

Both derivations are attempts to simulate the ℜ-derivation f(g(g(0))) → f(g(0)) → 0 but the last step can be simulated only by the first R_{V}-derivation.

Viry suggests to solve the problem by restricting the possible derivations in R_{V}. By evaluating the conditional positions first, he wants to ensure confluence. In terms of [36], such a derivation is called conditional eager (cf. [36, Definition 4.1]). The second derivation of Example 4 is not conditional eager, as the term

6This is not an accidental property of Viry’s transformation but a consequence of the result that CTRSs are more compact than TRSs, as mentioned at the beginning of this section and shown in [9]. g(g(0)) is rewritten although the conditional positions are already instantiated.

Restricting the possible derivations in this way, Viry presents a theorem about preserving confluence:

Theorem 2. (⊥-Confluence [36]) If in R_{V} all terms derived from ⊥-terms by conditional eager derivations (i.e., proving conditions first) can be joined w.r.t. ¯ , then R_{V} is called ⊥-confluent. If ℜ is confluent, then R_{V} is ⊥-confluent.

Unfortunately, this theorem does not hold: Revisiting Example 4 but taking only the first step of the second derivation, i.e.,

\underline{f(g(g(0)) | ⊥)} → f(g(g(0)) | [g(0), (g(0))])

one can see that the derivation so far is trivially conditional eager (cf. [36, Definition 4.1]), because there is no remaining derivation which could rewrite an unconditional position of g(g(0)). But it is already too late: the resulting term cannot be joined with its counterpart f(g(0) | ⊥).

The main problem of the system in Example 4 is that the rules are not constructor-based. However, for functional logic programming, the class of considered systems can be further restricted since we are interested in the class of weakly orthogonal, constructor-based CTRSs.^{7} We want to show that a slightly modified transformation preserves confluence for this class. We first show that the target system of a constructor-based CTRS is also constructor-based.

Lemma 1. If ℜ is constructor-based, then R_{V} is constructorbased.

Proof. The signatures of ℜ and R_{V} differ only in the arity of the functions and a few new symbols without defining rules. In particular, ⊥ is a new constructor and the pair notation [u, (x⃗)] is only intended to ease reading. Instead of the m + k rules of ℜ

\begin{aligned}ρ_{f,i} : & f(l_{f,i_{1}}, …, l_{f,i_{n}}) & → r_{f,i} if u_{f,i} →^{∗} v_{f,i} \\ ρ_{f,j} : & f(l_{f,j_{1}}, …, l_{f,j_{n}}) & → r_{f,j}, \end{aligned}

where 1 ≤ i ≤ m and m < j ≤ m + k, we now have 2m + k rules of the form

ρ′_{f,i} :f(t_{1}^{X}, …, t_{n}^{X} | y_{1}, …, ⊥_{i}, …, y_{m})
→ f(t_{1}^{X}, …, t_{n}^{X} | y_{1}, …,[u_{f,i}^{⊥}, x⃗],…, y_{m})
ρ′′_{f,i} :f(z_{1}, …, z_{n} | y_{1}, …,[v_{f,i}^{X}, x⃗],…, y_{m})→ r_{f,i}^{⊥}
ρ′′_{f,j} :f(l_{f,j_{1}}^{X}, …, l_{f,j_{n}}^{X}| y_{1},  …,  y_{m})→ r_{f,j}^{⊥},

where 1 ≤ i ≤ m and m < j ≤ m+k. According to the definition of a constructor-based CTRS, the terms v_{f,i} are ground constructor terms (hence, v_{f,i}^{X} = v_{f,i}). As ⊥ is a constructor symbol, for every pattern l, the terms l^{X} and l^{⊥} are also patterns. Therefore, each left-hand side of R_{V} is a pattern.

It is easy to see that R_{V} is left linear if ℜ is left linear, since all the variables introduced by^{X} are fresh by definition. Now we will optimize the transformation to the case of interest of this paper. First we consider the variable vector x⃗. Saving the context in which a condition was instantiated is essential for the soundness of the transformation, as shown in Example 6 below. However, we will show that saving the context can be avoided if the source CTRS is constructor-based and left linear. Furthermore, some of the rules can be joined in a single one as defined by the following transformation. The latter improvement is crucial for our narrowing strategy.

7In [11] it is also shown that Viry’s transformation can be extended to preserve confluence in general. However, we omit this result since it is not needed in the context of this paper.

Definition 13. (Transformation J) Let ℜ be a constructorbased CTRS whose rules are either of the form

\begin{matrix}ρ_{f,i} : f(l_{1}, …, l_{n}) → r_{f,i} if u_{f,i} →^{∗} v_{f,i} or \\ ρ_{f,i} : f(l_{1}, …, l_{n}) → r_{f,i} \end{matrix}

We define R_{V}′ as the unconditional TRS that contains the following two rules for each conditional rule of the previous form, where m is the number of conditional rules for f in ℜ:

π_{f,i} :f(l_{1}, …, l_{n} | y_{1}, …, ⊥_{i}, …, y_{m})
→ f(l_{1}, …, l_{n}| y_{1}, …,u_{f,i}^{⊥},…, y_{m})
π′′_{f,i} :f(l_{1}, …, l_{n} | y_{1}, …,v_{f,i},…, y_{m})→ r_{f,i}^{⊥}.

For each unconditional rule of ℜ, R_{V}′ contains

π′′_{f,i} : f(l_{1}, …, l_{n} | y_{1}, …, y_{m}) → r_{f,i}^{⊥}.

The set of rules of R_{J} is defined by joining all π-rules of R_{V}′ with identical left-hand sides. Let I = {i_{1}, …, i_{k}} be the set of all rules in R_{V}′ of the form

π_{f,i_{1}} : f(l_{1}, …, l_{n} | …, ⊥_{i_{1}}, …, y_{i_{k}}, …)
→ f(l_{1}, …, l_{n} | …,u_{f,i_{1}},…, y_{i_{k}}, …)
⋮  ⋮  ⋮
π_{f,i_{k}} : f(l_{1}, …, l_{n} | …, y_{i_{1}}, …, ⊥_{i_{k}}, …)
→ f(l_{1}, …, l_{n} | …, y_{i_{1}}, …,u_{f,i_{k}},…).

Instead of these rules, R_{J} contains a single rule

\begin{matrix}π′_{f,I} : & f(l_{1}, …, l_{n} | …, & ⊥_{i_{1}}, & …, & ⊥_{i_{k}}, & …) \\ → f(l_{1}, …, l_{n} | …, & u_{f,i_{1}}, & …, & u_{f,i_{k}}, & …). \end{matrix}

The mappings t^{X}, t^{⊥} and \overline{t} as well as the notions of instantiating and reducing rule, bottom term, and the definition of the terms of interest carry over from R_{V} to R_{J} without difficulty. ⋄

Since the above definition applies to constructor-based CTRSs, by contrast to Definition 11 it is not necessary to transform the subterms in the left-hand sides of the source systems. For constructor terms, l_{i}^{X} = l_{i}.

Example 5. Applying transformation J to the rules of Example 1, we obtain the following system:

abs(x | ⊥, ⊥) → abs(x | x ≥ 0, x < 0)
abs(x | true, y_{2}) → x
abs(x | y_{1}, true) → −x

However, the transformation is not sound for arbitrary CTRSs.

Example 6. Consider the following (non-confluent) set of conditional rules:

\begin{matrix}f(g(x)) → & x & if x →^{∗} s(0) \\ g(s(x)) → & g(x) \end{matrix}

The system is transformed to

\begin{matrix}f(g(x) | ⊥) → & f(g(x) | x)) \\ f(g(x) | s(0)) → & x \\ g(s(x)) → & g(x). \end{matrix}

The derivation \underline{f(g(s(0)) | ⊥)} → f(\underline{g(s(0))} | s(0)) → \underline{f(g(0) | s(0))} → 0 is not sound, since, in the source system, f(g(s(0))) is reducible to both the normal forms s(0) and f(g(0)) but not to 0.

It is easy to see that the problem can not occur with Viry’s transformation. Using the variable vector x⃗, the last step would have been f(g(0) | [s(0), (s(0))]) → s(0). As mentioned above, we will prove that there is a simple reason why this system and the one of Example 4 are problematic: both systems are not constructorbased.

Theorem 3. For any constructor-based, left-linear CTRS ℜ the transformation J is complete and sound, i.e.,

1. for each derivation t →^{∗}_{ℜ} t′ there is a derivation t^{⊥} →^{∗}_{R_{J}} t^{′⊥} (completeness),

2. for each derivation t^{⊥} →^{∗}_{R_{J}} t′ there is a derivation t →^{∗}_{ℜ} t̄′ (soundness).

Proof. (Completeness) We show completeness by induction over the actual length 𝔏(t →^{∗} t′) of the derivations t →^{∗}_{ℜ} t′ which is defined as follows:

\begin{aligned}𝔏(t →_{l→r} t′) & = & 1 \\ 𝔏(t →_{l→r if u →^{∗} v} t′) & = & 1 + 𝔏(u →^{∗} v) \\ 𝔏(t_{0} → t_{1} → … → t_{n}) & = & ∑_{i=1}^{n} 𝔏(t_{i−1} → t_{i}) \end{aligned}

Base case (𝔏(t →^{∗} t′) = 0): The claim trivially holds for all derivations with an actual length of zero, since t = t′ implies t^{⊥} = t^{′⊥}

and, thus, t^{⊥} →^{∗} t^{′⊥}.

Inductive case: Suppose that the claim holds for all derivations of the actual length ≤ 𝔩. We have to show that it holds for all derivations with length 𝔩 + 1. Consider the derivation t →^{∗} s →_{ρ,p} t′. By the induction hypothesis, there exists a derivation t^{⊥} →^{∗} s^{⊥}. We now distinguish whether ρ is an unconditional or a conditional rule. For an unconditional rule ρ = f(l_{1} … l_{n}) → r ∈ ℜ, there exists a reducing rule ρ′′ : f(l_{1} … l_{n} | y_{1} … y_{m}) → r^{⊥} ∈ R_{J}. For this rule the reduction s^{⊥} →_{ρ′′,p} t^{′⊥} yields the last step we need.^{8} If ρ = f(l_{1}, …, l_{n}) → r if u →^{∗} v is the i-th conditional rule defining f in ℜ, then, by definition of 𝔏, the actual length of u →^{∗} v is ≤ 𝔩 and, by induction hypothesis, there exists a derivation α : u^{⊥} →^{∗}_{R_{J}} v(= v^{⊥}). Using the instantiating rule ρ′ and the reducing rule ρ′′ corresponding to ρ in R_{J}, we can construct

the derivation s^{⊥} →_{ρ′,p} s′ →^{∗}_{p·(n+i)·α} s′′ →_{ρ′′,p}→ t^{′⊥}, where

p · (n + i) · α means that the derivation α is inserted and performed at the position p · (n + i).

(Soundness) We define a mapping μ : T_{R_{J}} → T_{R_{V}} between the terms of interest of R_{J} and R_{V}:

μ(t) = \{ \begin{matrix}t & if t = \overline{t}^{⊥}, \\ f(μ(t_{1}), …, μ(t_{n}) | s′_{1}, …, s′_{m}) \\ if t = f(t_{1}, …, t_{n} | s_{1}, …, s_{m}), \end{matrix}

where s′_{i} = ⊥ if s_{i} = ⊥. Otherwise, s′_{i} = [μ(s_{i}), σ(x⃗)] where σ is the matching of the term f(t_{1}, …, t_{n} | ⊥, …, ⊥) and the lefthand side of the rule π′_{f,i} of R_{J}.^{9} We will prove that any derivation t^{⊥} →^{∗}_{R_{J}} t′ implies the existence of a derivation t^{⊥} →^{∗}_{R_{V}} μ(t′) by induction over the length l of the derivation t^{⊥} →^{∗}_{R_{J}} t′.

8Note that any position in t ∈ T (Σ_{ℜ}, X) is also a position in t^{⊥} since the new conditional positions are added after the original unconditional positions. 9This matching must (still) exist since in constructor-based and left-linear systems the matching cannot be destroyed by reductions below patterns.

\overbrace{f(g(s(0)) | s(0))}^{s}  →_{R_{J}}  \overbrace{f(g(0) | s(0))}^{t′}
↓ μ  ↓ μ
\underbrace{f(g(s(0)) | [s(0), (s(0))])}_{μ(s)} →_{R_{V}} \underbrace{f(g(0) | [s(0), (s(0))])}_{s′} ↛^{∗}_{R_{V}} \underbrace{f(g(0) | [s(0), (0)])}_{μ(t′)}

Figure 1: Sample derivations from Example 6

l = 0: The claim holds since μ(t^{⊥}) = t^{⊥}. Inductive case: Consider the last step of the derivation t^{⊥} →^{∗} s →_{p, π} t′.

a) If π is an instantiating rule π′, then μ(s) can be reduced to μ(t′) by applying all of the corresponding ρ′-rules of R_{V} joined in π′ in an arbitrary order.

b) The remaining case is that π is a reducing rule π′′. By construction of R_{J}, there is a corresponding rule ρ′′ in R_{V} which can be applied at a position p′ similar to p in μ(s).^{10} We consider the result s′ of the reduction μ(s) →_{p′, ρ′′} s′. How far can μ(t′) and s′ differ? The only possible difference is that the mapping μ might instantiate variables in the vectors x⃗ differently in s and t′. This causes only problems (i.e., leads to terms out of the terms of interest) if ℜ is not constructor-based, see, for example, the derivations in Figure 1. Since ℜ is constructor-based, any reduction at an unconditional position must be possible within the corresponding variable vectors as well, because the redexes copied when the vectors are instantiated cannot be destroyed.^{11} Therefore, the same rule π′′ can be applied below all the variables in the vector in arbitrary order, leading to

μ(s′) →^{∗} μ(t′).

Hence, we have shown that t^{⊥} →^{∗}_{R_{J}} t′ implies the existence of a derivation t^{⊥} →^{∗}_{R_{V}} μ(t′). By definition of μ, \overline{μ(t)} = \overline{t} holds for all t. The soundness of V implies the existence of a derivation t →^{∗}_{ℜ} \overline{t} and, thus, the transformation J is sound.

4. TRANSFORMATION OF FUNCTIONAL LOGIC PROGRAMS

As stated in Section 1, our main aim is to apply parallel narrowing to conditional TRSs. The remaining task to reach this aim is to examine under which circumstances the property of weak orthogonality of the target system can be guaranteed, since this is a basic requirement for the completeness of parallel narrowing. Therefore, we will extend the notion of (weak) orthogonality to CTRSs. The basic idea of orthogonality is as follows. If t is an arbitrary term that can be reduced to two terms t_{1}, t_{2}, then these reductions do not overlap. In the case of weak orthogonality, any two overlapping rules must reduce the terms in the same way, i.e., t_{1} = t_{2}.

For constructor-based TRSs, overlaps can only occur between rules defining the same operation and at root positions. Thus, it is sufficient to examine rules l_{i} → r_{i}, i = 1, 2 where l_{1} and l_{2} are unifiable.

10p and p′ differ slightly because terms of R_{V} contain variable vectors and terms of R_{J} do not. Thus, whenever a prefix pp of p denotes a conditional position with s|_{pp} = u, the corresponding pp′ has to denote the μ(u) in μ(s)|_{qq′} = [μ(u), (x⃗)] (where qq′ is directly above pp′). 11In the case of Example 6, the existence of a rule f(g(s(0)) | ⊥) → f(g(s(0)) | s(0)) in a constructor-based system R implies that there cannot be a rule in R rooted by the symbol g.

Considering constructor-based CTRSs, the left-hand sides of two different rules might unify but, nevertheless, there may not exist any term that is contracted by both rules. This can happen because the conditions of the two rules may not be satisfiable by a single term. Thus, we define (weak) orthogonality for conditional term rewriting systems as follows.

Definition 14. ((Weakly) Orthogonal CTRS) Let ℜ be a left-linear and constructor-based CTRS in which all unconditional rules l → r are considered to be of the form l → r if true →^{∗} true. ℜ is orthogonal if for all distinct conditional rules l_{i} → r_{i} if u_{i} →^{∗} v_{i}, i ∈ {1, 2}, chosen with no variables in common, and for all unifiers σ with σ(l_{1}) = σ(l_{2}) at most one derivation among σ(u_{1}) →^{∗} v_{1} and σ(u_{2}) →^{∗} v_{2} is possible. ℜ is weakly orthogonal if for all distinct rules l_{i} → r_{i} if u_{i} →^{∗} v_{i}, i ∈ {1, 2}, chosen with no variables in common, and for all unifiers σ with σ(l_{1}) = σ(l_{2}) it holds: either σ(r_{1}) = σ(r_{2}) or at most one derivation among σ(u_{1}) →^{∗} v_{1} and σ(u_{2}) →^{∗} v_{2} is possible. ⋄

This definition captures the idea of orthogonality, as described above. It generalizes a similar notion in [8] in which multiple rules with overlapping left-hand sides are not allowed. Various examples in this paper show that this generalization supports a more expressive programming style.

Note that there is an important difference between orthogonality for TRSs and the extended notion for CTRSs. Orthogonality for a TRS is effectively decidable by a simple analysis of the syntactic structure of the system. For CTRSs orthogonality is not decidable, since the definition considers a semantic property by testing the simultaneous satisfiability of the conditions. If in practical applications the property of (weak) orthogonality has to be effectively tested, e.g., by the compiler of a functional logic program, orthogonality can be syntactically approximated, see, for instance, [30].

Since orthogonality for CTRSs is a non-trivial semantic property and orthogonality for TRSs is a syntactic property, no computation can transform a (weakly) orthogonal CTRS into a (weakly) orthogonal TRS. The key idea is to limit the notion of orthogonality to that part of the target system R_{J} which represents the semantics of ℜ: the terms of interest T_{R_{J}}. It turns out that R_{J} is (weakly) orthogonal if ℜ is (weakly) orthogonal provided that we consider only the terms of interest T_{R_{J}}. To show this, we first define what orthogonality means when restricted to a set of terms:

Definition 15. ((Weak) Orthogonality for T ) Let R be a program and T a set of terms which is closed under →^{∗}_{R}. R is orthogonal for T if, for all distinct rules ρ_{1} and ρ_{2} in R, there exist no terms t, t_{1}, t_{2} ∈ T and a position p in t such that t →_{p, ρ_{1}} t_{1} and t →_{p, ρ_{2}} t_{2}. R is weakly orthogonal for T if, for all rules ρ_{1}, ρ_{2} in R, there exist no terms t, t_{1}, t_{2} ∈ T and a position p in t such that t →_{p, ρ_{1}} t_{1} and t →_{p, ρ_{2}} t_{2} and t_{1} ≠ t_{2}. ⋄ Analogously to the definition of ordinary orthogonality (Definition 10), we make use of the constructor discipline of the supposed system, since we consider overlapping at a same position only. Note that, if T = T (Σ, X), then (weak) orthogonality for T is equivalent to ordinary (weak) orthogonality.

We can now define the set of CTRSs on which our transformation J preserves orthogonality for the terms of interest:

Definition 16. (Conditional Program) We call a conditional program any constructor-based weakly orthogonal CTRS in which overlapping rules have identical left-hand sides. ⋄

Limiting conditional programs to overlapping rules with identical left-hand sides is not a restriction. We show by an example the idea of transforming every constructor-based left-linear CTRS into a form where all overlapping rules have identical left-hand sides. This is done by moving the pattern matching into the conditions and adding explicit rules for these matchings for the needed constructors. This example can be easily generalized to all constructorbased weakly orthogonal CTRSs. A formal proof can be found in [11].

Example 7. The system defined by the rules

fib(x)  → 1  if x < 2 →^{∗} true
fib(s(s(x))) → fib(s(x)) + fib(x)

can also be written as

fib(x) → 1  if x < 2 →^{∗} true
fib(x) → fib(s(select(x))) + fib(select(x))

if match(x) →^{∗} true

match(s(s(x))) → true
select(s(s(x))) → x

Operations select and match are specifically generated wherever needed. A compiler implementing this transformation would probably benefit from more general purpose operations, e.g., a select_{n} operation that selects the n-th argument of a constructor-rooted term. However, our specialized operations ease the understanding of the example. Note that it may be necessary to rename variables in other rules in order to get identical left-hand sides. Derivations in the new system will be longer because of the explicit matching and the selection steps, but it is easy to see that there exists a bisimulation between the two systems with respect to starting terms of the universe of the original system. The advantage of this transformation over similar approaches, like the “sequentialization” given in [2, section 4.3], is that it preserves (weak) orthogonality, which is crucial for our purpose.

From now on we will assume that overlapping rules in the given CTRSs have identical left-hand sides, as the only considered systems are constructor-based and left linear.

Theorem 4. Let ℜ be a conditional program. Then R_{J} is weakly orthogonal for the set of terms of interest T_{R_{J}}. Moreover, if ℜ is orthogonal, then R_{J} is orthogonal for the set of terms of interest T_{R_{J}}.

Proof. Suppose that there exists a t in T_{R_{J}} and two distinct rules ρ : l → r and ρ′ : l′ → r′ such that

t →_{Λ,ρ} w and t →_{Λ,ρ′} w′

Without loss of generality, we consider only root positions, since in the constructor-based setting one can always remove the context of a redex. Let π and π′ be the rules of the CTRS ℜ, from which ρ and ρ′ originate. The transformation replaces each conditional rule by two unconditional ones. The instantiating rule introduces the conditions by replacing ⊥ symbols. The reducing rule contracts the redex analogously to the unconditional part of the original rule. We do not have overlapping instantiating rules because they are joined by the transformation. Thus, all overlapping rules and, in particular, ρ and ρ′ must be reducing rules. Hence, because all overlapping rules have identical left-hand-sides, the two original rules of ℜ have

the form π : \overline{l} → \overline{r} if v →^{∗} u and π′ : \overline{l} → \overline{r′} if v′ →^{∗} u′.

Furthermore, the pattern l must match both terms \overline{t} and \overline{t′}. Since the transformation is sound, this implies the existence of the two reductions \overline{t} →_{Λ,π} \overline{w} and \overline{t} →_{Λ,π′} \overline{w′} and, therefore, ℜ cannot have been orthogonal. For weak orthogonality, we have to consider the additional case that w and w′ are different. Since the right-hand sides of the reducing rules ρ and ρ′ can only be different if the right-hand sides of their original rules, namely \overline{r} and \overline{r′}, differ, \overline{w} ≠ \overline{w′} implies that ℜ cannot have been weakly orthogonal as well.

In the next section we will show that for a conditional program ℜ the resulting system R_{J} can be evaluated with parallel narrowing if we limit ourselves to the terms of interest. For this it is crucial to see that the Parallel Moves Lemma (originally in [23], here according to the more general formulation [7, Lemma 6.4.4]) can be extended to the rewrite relation on T_{R_{J}}. For this the notion of a parallel rewriting step is required: t ⇉_{P} t′ if P = {p_{1}, …, p_{n}} is a set of pairwise disjoint positions of t such that and t →_{p_{1}} ⋯ →_{p_{n}} t′.

Lemma 2. Parallel Moves Lemma [7, Lemma 6.4.4] Let R be a TRS and l → r ∈ R a left-linear rule. If σ(l) ⇉_{P} t for a set of positions P and all elements of P are below variable positions of l, then there exists a substitution σ′ such that σ(r) ⇉ σ′(r) ← t.

The important point is that on the terms of interests T_{R_{J}} any parallel rewriting step meets the conditions of the Parallel Moves Lemma:

Lemma 3. Let ℜ be a conditional program and l → r a rule in R_{J}. If σ(l) ∈ T_{R_{J}} ⇉_{P} t for a set of (disjoint) positions P, then there exists a substitution σ′ such that σ(r) ⇉ σ′(r) ← t or σ(r) = σ′(r) = t.

Proof. By definition of a conditional program and construction of J, all rules of R_{J} are left linear. As conditional programs are also constructor-based, all positions in P are either below variable positions of l or P = {Λ}. In the first case, the Parallel Moves Lemma yields the result. In the second case, because R_{J} is weakly orthogonal for T_{R_{J}}, σ(r) must be equal to t no matter which rule was applied.

Analogously to the discussion in [7, p.152f], this leads to the proof that ⇉_{R_{J}} has the diamond property if it is restricted to the terms of interest:

Lemma 4. Let ℜ be a conditional program. Then for the terms of interest, ⇉ has the diamond property, i.e., for all s ∈ T_{R_{J}} with s ⇉_{P_{0}} t_{0} and s ⇉_{P_{1}} t_{1} there exists an s′ with t_{0} ⇉ s′ and t_{1} ⇉ s′.

Proof. (Analogously to the proof in [7, p.152]) We have to distinguish how the positions of the parallel reductions are relative to each other and partition the sets P_{0} and P_{1} accordingly:

P^{≰} := {p ∈ P_{i} | i ∈ {0, 1} ∧ ∀q ∈ P_{1−i} : q ≰ p}
P^{<} := {p ∈ P_{i} | i ∈ {0, 1} ∧ ∃q ∈ P_{1−i} : q < p}
P^{=} := P_{0} ∩ P_{1}

It is easy to see that we can obtain t_{0} and t_{1} from s by replacing all subterms of s at positions in P^{≰} ∪ P^{=} with the corresponding subterms of t_{i}: t_{i} = s[t_{i}|_{p}]_{p∈P^{≰}∪P^{=}}. As R_{J} is weakly orthogonal for T_{R_{J}}, t_{0}|_{p} = t_{1}|_{p} holds for all p ∈ P^{=}. Hence it suffices to construct, for each p ∈ P^{≰}, a term u_{p} such that t_{i}|_{p} ⇉ u_{p} (i = 1, 2). For each p ∈ P^{≰}, either t_{0} or t_{1} is rewritten at p. Calling this subterm t_{p}, there must exist a rule l → r in R_{J} and a substitution σ such that s|_{p} = σ(l) and t_{p} = σ(r). As s|_{p} ∈ T_{R_{J}}, our adapted Parallel Moves Lemma (Lemma 3) ensures the existence of a substitution σ′ with t_{i}|_{p} ⇉ σ′(r) or t_{i}|_{p} = σ′(r) and, thus, we define u_{p} := σ′(r).

These considerations enable us to draw some interesting conclusions. We use [7, Corollary 2.7.7] which states: If →_{1}⊆→_{2}⊆→^{∗}_{1} and →_{2} has the diamond property, then →_{1} is confluent. With →_{1}=→_{R_{J}} and →_{2}=⇉_{R_{J}}, both restricted to the terms of interest, we obtain:

Corollary 1. For any conditional program ℜ and the corresponding TRS R_{J}, the following properties hold:

• R_{J} is confluent for T_{R_{J}}.

• Each ⊥-term has at most one normal form.

• ℜ is confluent (by soundness of the transformation).

Note how the soundness of the transformation enables us to draw conclusions backwards, from the target to the source system. By using this method, results about classic TRSs can be extended to the conditional case. This result can be generalized to constructorbased weakly orthogonal CTRSs using the transformation that ensures that the left-hand sides of overlapping rules are identical, see Example 7.

5. NARROWING ON TRANSFORMED FUNCTIONAL LOGIC PROGRAMS

This paper is concerned with the use of CTRSs in declarative programming. Functional logic programs modeled by TRSs are usually executed by narrowing because narrowing amalgamates computational ideas from both functional and logic programming. Consequently, a pertinent question is the choice of a narrowing strategy appropriate to a given class of programs. The primary motivation of this work is the transformation of a CTRS into an ordinary TRS so that a wealth of existing results about narrowing strategies for ordinary TRSs can be applied to CTRSs.

In general, if we only consider the syntactic structure of the rules of R_{J}, we will not find any of the properties that support efficient, sound, and complete strategies, e.g., inductive sequentiality or weak orthogonality. However, we have shown that some strong properties are preserved for the rewrite relation over the set of the terms of interest T_{R_{J}}. These terms capture all and only the computations that one can perform with ℜ. Hence, there is no loss in restricting our attention to these terms and considering terms outside this set does not conform with the semantics of ℜ. Moreover, by construction, the set of terms of interest of R_{J} is closed under both substitution of bottom terms and rewriting. Consequently, it is closed under narrowing for bottom terms, too.

Weakly needed and parallel narrowing [4] are strategies defined for those TRSs R in which any operation defined in R has a parallel definitional tree [1]. For a defined operation f, the definitional tree for f is a data structure defined by the patterns, i.e., the lefthand sides, of the rules defining f in R. A parallel definitional tree may have so-called or-nodes in addition to those defined by pattern matching. These or-nodes allow the specification of overlapping rules and, thus, lead to parallel tests for pattern matching. This is necessary to cover the class of weakly orthogonal TRSs. A consequence of allowing overlapping rules is that the notion of a needed redex position, i.e., the position of a redex in a given term t which has to be reduced in order to yield a normal form for t, has to be generalized to a necessary set of redex positions. From this set the redex of at least one position has to be contracted to yield a normal form. This leads to the basic idea of weakly needed narrowing: (a) compute such a necessary set of positions for a given term using the parallel definitional trees for the defined operations of R; (b) non-deterministically choose some of the positions; (c) instantiate the terms at the chosen positions so that they become redexes and reduce them. In comparison to weakly needed narrowing, the strategy called parallel narrowing is more sophisticated: a minimal set of substitutions, i.e., the instantiations of variables, is computed by examining the whole necessary set of positions. For each substitution in this minimal set all resulting weakly needed redexes are reduced in parallel. Consequently, parallel narrowing is, in contrast to weakly needed narrowing, deterministic on ground terms since there is only the empty substitution in this case. Due to lack of space, we can not present all precise definitions but they are available in [4].

In order to apply weakly or parallel narrowing, we have to prove that any operation defined in R_{J} has a parallel definitional tree:

Lemma 5. Let R_{J} be a TRS obtained by transformation J from a conditional program ℜ. If f is a defined operation of R_{J}, there exists a parallel definitional tree for f.

Proof. If there is no left-hand side of a rule subsumed by the left-hand side of another rule in R_{J}, [1, Theorem 19] proves the existence of a parallel definitional tree. Note that [1, Theorem 19] is proved under the assumption that the TRS is weakly orthogonal, but the proof considers only the left-hand sides of the rules. Thus, the triviality of possible critical pairs is irrelevant. Now we prove that if the left-hand side of a rule is subsumed by some other left-hand side in R_{J}, then one of the rules is useless (see [1]) and can be discarded. By construction, subsuming left-hand sides of R_{J} may originate only from subsuming left-hand sides of ℜ. In the original program ℜ, the only case of subsumption of left-hand sides occurs when there are several conditional rules and possibly one unconditional rule, all with the same left-hand side. If there is one such unconditional rule, we can discard all the conditional rules with the same left-hand side. So, we are left only with conditional rules. In this case, the rules of R_{J} that originate from these conditional rules do not have subsuming left-hand sides according to the definition of the transformation J.

Example 8. The function abs of Example 5 has the following parallel definitional tree:

Or
abs(x_{1}|\underline{x_{2}}, x_{3}) abs(x_{1}|x_{2}, \underline{x_{3}})
abs(x_{1}|⊥, \underline{x_{3}}) abs(x_{1}|true, x_{3}) abs(x_{1}|x_{2}, true)
abs(x_{1}|⊥, ⊥)  x  −x

abs(x_{1}|x_{1} ≥ 0, x_{1} < 0)

Hence, one can apply both the weakly needed and parallel narrowing strategies to R_{J}. However, the narrowing relation computed by these strategies might not be complete for R_{J} w.r.t. arbitrary terms, because these strategies fire only one rule (after variable instantiation) when multiple overlapping rules can be applied to a same redex. This problem does not occur for the set of the terms of interest T_{R_{J}} obtained from a conditional program ℜ, because either a single rule can be fired for a redex (when ℜ is orthogonal and, hence, R_{J} is orthogonal for T_{R_{J}}) or the choice of multiple rules does not matter (when ℜ is weakly orthogonal and, hence, R_{J} is weakly orthogonal for T_{R_{J}}). This leads us to our main result:^{12}

Theorem 5. Let ℜ be a conditional program. Then both weakly needed narrowing and parallel narrowing are sound and complete with respect to the terms of interest T_{R_{J}}, i.e.:

1. For each t ∈ T_{R_{J}} and every constructor term s ∈ T (C, X) holds: If t ⇝_{σ_{1}} … ⇝_{σ_{n}} s (t ⇝ ⇝ _{σ_{1}} … ⇝ ⇝ _{σ_{n}}s) is a weakly needed (parallel) narrowing derivation, then σ_{n}(… σ_{1}(t) …) →^{∗} s (soundness).

2. For each term t ∈ T_{R_{J}} and each constructor substitution σ such that σ(t) is also in T_{R_{J}} and reduces to a constructor term s ∈ T (C, X), there exists a weakly needed (parallel) narrowing derivation t ⇝_{σ_{1}} … ⇝_{σ_{n}} s′ (t ⇝ ⇝ _{σ_{1}} … ⇝ ⇝ _{σ_{n}}s′) such that σ_{n} ∘ ⋯ ∘ σ_{1} is more general than σ and s is an instance of s′ (completeness).

Proof. Due to Lemma 5, both strategies can be applied to R_{J}. (Soundness) The soundness of both strategies is straightforward because a narrowing step is defined as an instantiation followed by a rewriting step. (Completeness) In [3] the completeness of weakly needed and parallel narrowing are proven using commutative diagrams. The existence and commutativity of these diagrams is ensured by confluence and the Parallel Moves Lemma. Consequently the proofs of completeness for weakly needed narrowing [3, Theorem 4] and parallel needed narrowing [3, Theorems 5] carry over without difficulty.

Weakly needed and parallel narrowing are relatively efficient for the class of systems we are discussing. The main advantage of using parallel narrowing for the class of transformed conditional programs is that, on ground terms, the computation is deterministic, i.e., at each computation step there are no don’t know choices. This ensures, among other advantages, that non-terminating evaluations of a condition do not preclude the application of other conditional rules. To see this, refer to the CTRS from Example 2 in Section 1. In that system the evaluation of the expression gmult(∞, 0) does not terminate if we try to apply the first rule for gmult. Similarly, gmult(0, ∞) does not terminate for the second rule and the third rule leads to an infinite computation for both terms. However, consider the system obtained by our transformation.

Example 9. Transforming the CTRS from Example 2, we obtain:

gmult(x, y | ⊥, ⊥, ⊥) →

gmult(x, y | g(x), g(y), g(x) > 0 ∧ g(y) > 0)

gmult(x, y | 0, y_{2}, y_{3}) → 0 gmult(x, y | y_{1}, 0, y_{3}) → 0 gmult(x, y | y_{1}, y_{2}, true) → g(x) ∗ g(y) g(0) → 0 g(∞) → g(∞)

12As usual in functional logic programming, we consider only constructor substitutions and constructor terms as the intended results of a computation, cf. [5] In this system both expressions gmult(∞, 0 | ⊥, ⊥, ⊥) and gmult(0, ∞ | ⊥, ⊥, ⊥) are evaluated with a finite number of parallel narrowing steps:

\underline{gmult(∞, 0|⊥, ⊥, ⊥)}
⇝ ⇝ gmult(∞, 0|\underline{g(∞)}, \underline{g(0)}, \underline{g(∞)} > 0 ∧ \underline{g(0)} > 0)
⇝ ⇝ \underline{gmult(∞, 0|g(∞), 0, g(∞) > 0 ∧ 0 > 0)}
⇝ ⇝ 0

and

\underline{gmult(0, ∞|⊥, ⊥, ⊥)} ⇝ ⇝ gmult(0, ∞|\underline{g(0)}, \underline{g(∞)}, \underline{g(0)} > 0 ∧ \underline{g(∞)} > 0)

⇝ ⇝ \underline{gmult(0, ∞|0, g(∞), 0 > 0 ∧ g(∞) > 0)}

⇝ ⇝ 0

6. CONCLUSIONS AND RELATED WORK

We have presented a new evaluation strategy for functional logic programs where functions are defined by conditional rewrite rules. In order to cover a large part of such programs, we consider weakly orthogonal constructor-based CTRSs, i.e., the overlaps are either trivial or the conditions of overlapping rules are exclusive. We have presented a transformation for this class of programs that maps such programs into unconditional TRSs. Although the resulting TRSs are not weakly orthogonal in general, they have this property for all terms of interest, i.e., terms obtained by this transformation. This property enables us to apply appropriate narrowing strategies for unconditional TRSs to evaluate such programs. In particular, both the non-strict evaluation strategies weakly needed and parallel narrowing can be applied to the transformed programs. Since parallel narrowing is deterministic on ground terms, our work offers the first known narrowing strategy that deterministically evaluates ground terms in weakly orthogonal constructor-based CTRSs.

We want to emphasize that our new strategy is a conservative extension of narrowing strategies known to be appropriate for functional logic programs. If the source program contains no conditional rules, our transformation is the identity. Thus, if the source program is inductively sequential, our strategy specializes to needed narrowing that is known to be optimal w.r.t. the length of successful computations and the number of computed solutions. Furthermore, if the left-hand sides of a conditional program ℜ are inductively sequential, then weakly needed narrowing as well as parallel narrowing computes a set of disjoint solutions [4, 5].

Our transformation is not an “unraveling” in the sense of [29]. By definition, an unraveling leaves the unconditional rules of a CTRS unchanged [29, Definition 3.1]. Furthermore, a “tidy” unraveling will transform every single conditional rule separately [29, p.109]. This leads to the idea to introduce a new function symbol for each conditional rule. In this case, one has to decide which rule must be applied before knowing which conditions are satisfiable. The key idea of Viry’s approach is to keep the information of testing all conditions in a single structure. This ensures that the correct rule can be chosen depending on the successful tests of all conditions. This has the immediate consequence that Viry’s transformation can be extended to preserve properties like termination and confluence (as shown in [11]) which unravelings principally cannot [29, p.120].

Transforming each conditional rule separately is also the approach of [33] so that it leads to the same problem as Marchiori’s unravelings. The interesting feature of the transformation presented in [33] is that it can deal with a certain form of extra variables. The extension of our transformation to the systems considered by Ohlebusch could be done by applying lambda-lifting [24] to eliminate this kind of variables.

An interesting topic for future work is the efficient implementation of this strategy. A useful starting point could be [6] where an implementation of weakly needed narrowing with a limited form of parallel reductions is proposed.

7. REFERENCES

[1] S. Antoy. Definitional trees. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pages 143–157. Springer LNCS 632, 1992.

[2] S. Antoy. Constructor-based conditional narrowing. In Proc. of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pages 199–206. ACM Press, 2001.

[3] S. Antoy, R. Echahed, and M. Hanus. A parallel narrowing strategy. Technical report tr 96-1, Portland State University, 1996.

[4] S. Antoy, R. Echahed, and M. Hanus. Parallel evaluation strategies for functional logic languages. In Proc. of the Fourteenth International Conference on Logic Programming (ICLP’97), pages 138–152. MIT Press, 1997.

[5] S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. Journal of the ACM, 47(4):776–822, 2000.

[6] S. Antoy, M. Hanus, B. Massey, and F. Steiner. An implementation of narrowing strategies. In Proc. of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pages 207–217. ACM Press, 2001.

[7] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[8] J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32(3):323–362, 1986.

[9] J.A. Bergstra and J.V. Tucker. Algebraic specifications of computable and semicomputable data types. Theoretical Computer Science, 75:111–138, 1987.

[10] D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proc. European Symposium on Programming, pages 119–132. Springer LNCS 213, 1986.

[11] B. Brassel. Conditional narrowing with lazy evaluation (in german). Master’s thesis, RWTH Aachen, 1999.

[12] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pages 243–320. Elsevier, 1990.

[13] N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.

[14] L. Fribourg. SLOG: A logic programming language interpreter based on clausal superposition and rewriting. In Proc. IEEE Internat. Symposium on Logic Programming, pages 172–184, Boston, 1985.

[15] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: A logic plus functional language. Journal of Computer and System Sciences, 42(2):139–185, 1991.

[16] E. Giovannetti and C. Moiso. Notes on the elimination of conditions. In Proc. CTRS’87, pages 91–97. Springer LNCS 308, 1987.

[17] M. Hanus. Compiling logic programs with equality. In Proc. of the 2nd Int. Workshop on Programming Language Implementation and Logic Programming, pages 387–401. Springer LNCS 456, 1990.

[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. Reduction strategies for declarative programming. In B. Gramlich and S. Lucas, editors, Electronic Notes in Theoretical Computer Science, volume 57. Elsevier Science Publishers, 2001.

[20] M. Hanus, S. Lucas, and A. Middeldorp. Strongly sequential and inductively sequential term rewriting systems. Information Processing Letters, 67(1):1–8, 1998.

[21] M. Hanus (ed.). Curry: An integrated functional logic language (vers. 0.8). Available at

http://www.informatik.uni-kiel.de/~curry,

2003.

[22] C. Hintermeier. How to transform canonical decreasing CTRSs into equivalent canonical TRSs. In Proc. of the 4th International Workshop on Conditional and Typed Rewriting Systems (CTRS’94), pages 186–205. Springer LNCS 968, 1994.

[23] G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 395–443. MIT Press, 1991.

[24] T. Johnsson. Lambda lifting: Transforming programs to recursive functions. In Functional Programming Languages and Computer Architecture, pages 190–203. Springer LNCS 201, 1985.

[25] J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.

[26] J. Lloyd. Programming in an integrated functional and logic language. Journal of Functional and Logic Programming, (3):1–49, 1999.

[27] R. Loogen, F. Lopez Fraguas, and M. Rodríguez Artalejo. A demand driven computation strategy for lazy narrowing. In Proc. of the 5th International Symposium on Programming Language Implementation and Logic Programming, pages 184–200. Springer LNCS 714, 1993.

[28] F. López-Fraguas and J. Sánchez-Hernández. TOY: A Multiparadigm Declarative System. In Proc. of RTA’99, pages 244–247. Springer LNCS 1631, 1999.

[29] M. Marchiori. Unravelings and ultra-properties. In 5th International Conference on Algebraic and Logic Programming (ALP’96), pages 107–121. Springer LNCS 1139, 1996.

[30] J.J. Moreno-Navarro, H. Kuchen, R. Loogen, and M. Rodríguez-Artalejo. Lazy narrowing in a graph machine. In Proc. Second International Conference on Algebraic and Logic Programming, pages 298–317. Springer LNCS 463, 1990.

[31] J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic programming with functions and predicates: The language BABEL. Journal of Logic Programming, 12:191–223, 1992.

[32] M.J. O’Donnell. Equational Logic as a Programming Language. MIT Press, 1985.

[33] E. Ohlebusch. Transforming conditional rewrite system with extra variables into unconditional systems. In Proc. of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR’99), pages 111–130. Springer LNCS 1705, 1999.

[34] G. Smolka. The Oz programming model. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, pages 324–343. Springer LNCS 1000, 1995.

[35] Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29(1-3):17–64, 1996.

[36] P. Viry. Elimination of conditions. Journal of Symbolic Computation, 28:381–400, 1999.