On the Correctness of the Factoring Transformation

Pascual Julián Iranzo^{1}

Departamento de Informática Universidad de Castilla–La Mancha Ciudad Real, Spain

                          pjulian@inf-cr.uclm.es

Abstract. Non-deterministic computations greatly enhance the expressive power of functional logic programs, but are often computationally expensive. Recently we analyzed a program transformation, called factoring transformation [4], that may save both execution time and memory occupation in a non-deterministic computation. In this paper we study the formal properties of our transformation, proving its correctness for constructor-based left linear rewriting systems, under some well established conditions. We also introduce some proof techniques that help us to reason with this kind of rewriting systems.

1 Introduction

The aim of functional logic programming is to integrate the best features of both functional and logic programming. Logic programming provides the use of predicates and logical formulas. Logic programs have a great expressive power thanks to the ability of logic languages of computing using logical variables, partial data structures and an operational mechanism that permits a non-deterministic search for answers. Functional programming is based on the concept of function. In a functional program functions are defined by means of equations. The deterministic evaluation of ground expressions increases the efficiency of functional programs. The concept of evaluation strategies, that also increase the efficiency of functional computations, relays on the existence and manipulation of nested terms. The combination of these features makes functional logic languages both more expressive than functional languages and more efficient than traditional logic languages.

Non-determinism is an essential feature of these integrated languages, since it allows problem solving using programs that are textually shorter, easier to

1 Supported by the Spanish Research Funding Agency (CICYT) TIC 2001-2705-C03-01, by Acción Integrada Hispano-Italiana HI2000-0161, by Acción Integrada Hispano-Alemana HA2001-0059, and the Valencian Research Council under grant GV01-424.

understand and maintain, and more declarative than their deterministic counterparts (see [2], [9] or [14] for several motivating examples).

In a functional logic programming language, non-deterministic computations are modeled by the defined operations of a constructor-based left linear rewrite system [2, 8]. The following emblematic example [8, Ex. 2] defines an operation, coin, that non-deterministically returns either zero or one.

\begin{matrix}coin → 0 \\ coin → s(0) \end{matrix}

Rewrite systems with operations such as coin are non-confluent. A computation in these rewrite systems may have distinct normal forms and/or does not terminate. Non-determinism abstracts the choice of one of several outcomes of a computation. The outcome of a non-deterministic computation is selected somewhat randomly. For example, for the operation coin defined above, each solution, 0 or s(0), is equally likely to be produced. There is no feasible means of deciding which replacement should be chosen at the time coin is evaluated. Therefore, evaluation under both replacements must be considered. In general, to ensure operational completeness, all the possible replacements of a non-deterministic computation must be executed fairly. In fact, if one replacement is executed only after the computation of another replacement is completed, the second replacement will never be executed if the computation originated by a first replacement does not terminate.

This approach, which we refer to as fair independent computations, captures the intended semantics, but clearly it is computationally costly. For example, consider the following operations, where “bigger” is a variant of coin:

add(0, Y) → Y

add(s(X), Y) → s(add(X, Y))
positive(0) → false
positive(s(X)) → true
bigger → s(0)
bigger → s(s(0))

The evaluation of the term positive(add(bigger, 0)) requires the evaluation of the subterm bigger. Therefore, one must compute fairly and independently both positive(add(s(0), 0)) and positive(add(s(s(0), 0)).

However, in a situation like the one just described, the cost of fair independent computations might be avoided by means of a programming technique that facilitates the use of deterministic choices. Our programming technique is based on the introduction of a new symbol, denoted by the infix operator “ ! ” and read as alternative, into the signature of the TRS modeling a functional logic program. We treat the new symbol as a polymorphic operation^{1}, defined by the rules [8, 14]:

\begin{matrix}ALT 1 : & X!Y → X \\ ALT 2 : & X!Y → Y \end{matrix}

1 The reader can see another different approach in [4], where we also consider the alternative symbol as an overloaded constructor.

The alternative operation allows us to give an equivalent definition of the oper-

ation bigger:

bigger → s(0!s0)

where a common context of the right-hand sides of the rules defining the operation bigger, in the original term rewriting system, has been “factored”. The advantage of this new definition of bigger with respect to the original one is that, using a needed strategy [2] or the constructor-based lazy narrowing of [9], only the factored portion of the two alternative right-hand sides of the rewrite rules of bigger is needed by a context and no fair independent computations are created. As it is shown by the following (needed) derivation:

positive(add(bigger, 0)) → positive(add(s(0!s(0)), 0)
→ positive(s(add(0!s(0)), 0))
→ true.

where two non-deterministic fair independent computations have been merged. Roughly speaking, if we “factor out” the common part of a set of non-deterministic choices, when it is possible, we can avoid the replication of the choice’s context obtaining a gain. For this example, the cost criteria developed in [4] reveal that our programming technique cuts the number of steps in half and reduces the memory consumption by 25% w.r.t. a computation performed using the original program. On the other hand, in cases where factoring the right-hand sides of two rewrite rules does not eliminate the need of fair independent computations, the run-time cost of factoring is a single additional rewrite step. For realistic programs, this cost is negligible. Hence, the factorization of right-hand sides is a source of potential improvement. In the best case, it saves computing time and/or storage for representing terms. In the worst case, it costs one extra step and very little additional memory (see [4] for some examples on larger benchmark programs, coded using the functional logic language Curry [11], that illustrate in more detail the impact on the efficiency produced by our factoring technique).

We can see all this process as a program transformation that starting from an original program produce a new and, in many cases, more efficient program. In this paper, we define our program transformation in a formal setting and we prove its correctness under precise conditions. That is, we prove that the original and the transformed program are semantically equivalent. In order to obtain this result it is convenient to introduce some proof techniques that help us to reason with non-confluent constructor-based rewrite systems, where the concept of descendants of a redex [12] is not well established.

The plan of the paper is as follows: Section 2 introduces some preparatory concepts that are used in the rest of the paper. Section 3 gives a formal definition of our transformation. Section 4 discusses the conditions under our transformation is sound and complete and we introduce some concepts to facilitate our proofs: namely, an embedding relation, that abstracts the intuitive notion of “containment” between terms with alternative symbols, and the concept of nonfactorized program, that defines a standard form of program. Finally, Section 5 contains our conclusions.

A full version with missing proofs can be found as a wed document at the

URL address http://www.inf-cr.uclm.es/www/pjulian.

2 Preliminaries

In this section we briefly summarize some well-known notations and concepts about term rewriting systems [5] and functional logic programming [10].

2.1 Terms, substitutions and positions.

Throughout this paper, X denotes a countably infinite set of variables and F denotes a set of function symbols (also called the signature), each of which has a fixed associated arity. We assume that the signature F is partitioned into two disjoint sets F = C⊎D. Symbols in C are called constructors and symbols in D are called defined functions. T (F, X) denotes the set of terms or expressions built from F and X. T (F) denotes the set of ground terms, while T (C, X) denotes the set of constructor terms. If t ∉ X, then Root(t) is the function symbol heading the term t, also called the root symbol of t. A term t is linear if t does not contain multiple occurrences of the same variable. Var(o) is the set of variables occurring in the syntactic object o.

A substitution is a mapping from the set of variables X to the set of terms T (F, X) such that its domain Dom(σ) = {x ∈ X | σ(x) ≠ x} is finite. We frequently identify a substitution σ with the set {x/σ(x) | x ∈ Dom(σ)}. We denote the identity substitution by id. We say that σ is a constructor substitution if σ(x) is constructor term for each x ∈ Dom(σ). We define the composition of two substitutions σ and θ, denoted σ ∘ θ as usual: σ ∘ θ(x) = σ̂(θ(x)), where σ̂ is the extension of σ to the domain of the terms T (F, X). We say that θ is more general than σ (in symbols θ ≤ σ) iff (∃γ) σ = γ ∘ θ. The restriction σ_{|V̀} of a substitution σ to a set V of variables is defined by σ_{|V̀}(x) = σ(x) if x ∈ V and σ_{|V̀}(x) = x if x ∉ V. We write σ = θ[V] iff σ_{|V̀} = θ_{|V̀}. A renaming is a substitution ρ such that there exists the inverse substitution ρ^{−1} and ρ ∘ ρ^{−1} = ρ^{−1} ∘ ρ = id. Given a set S of terms and a substitution σ, σ(S) = {σ(t) | t ∈ S}.

A term t is more general than s (or s is an instance of t), in symbols t ≤ s, if (∃σ) s = σ(t). Two terms t and t′ are variants if there exists a renaming ρ such that t′ = ρ(t). A unifier of a pair of terms ⟨t_{1}, t_{2}⟩ is a substitution σ such that σ(t_{1}) = σ(t_{2}). A unifier σ is called most general unifier (mgu) if σ ≤ σ′ for every other unifier σ′.

Positions of a term t (also called occurrences) are represented by sequences of natural numbers used to address subterms of t. The concatenation of the sequences p and w is denoted by p.w. We let Λ denote the empty sequence. Pos(t) and FPos(t) denote, respectively, the set of positions and the set of nonvariable positions of the term t. If p ∈ Pos(t), t|_{p} denotes the subterm of t at position p and t[s]_{p} denotes the result of replacing the subterm t|_{p} by the term s.

2.2 Term rewriting, classes of term rewrite systems and programs.

We limit the discussion to unconditional term rewriting systems. A rewrite rule is a pair l → r with l, r ∈ T (F, X), l ∉ X, and Var(r) ⊆ Var(l). l and r are called the left-hand side (lhs) and right-hand side (rhs) of the rewrite rule, respectively. A term rewriting system (TRS) R is a finite set of rewrite rules.

Rewrite rules in a TRS define a rewriting relation → between terms which can be defined as follows: t →_{p,l→r} s if there exists a position p ∈ Pos(t), a rewrite rule l → r, and a substitution σ with t|_{p} = σ(l) and s = t[σ(r)]_{p}. We say that s is reduced to t in a rewrite step, t →_{p,l→r} s and the subterm t|_{p} = σ(l) is a redex (reducible expression) of t. A sequence of (zero or more) rewriting steps is denoted by (t →^{∗} s) t →^{+} s. A term t is in normal form if t is a term without redexes. A term s has a normal form if there exists a reduction sequence s →^{∗} t, where t is a normal form.

A TRS is terminating or noetherian if there are no infinite reduction sequences. Since in this work we do not impose the requirement of terminating rules, normal forms may not exist.

A TRS is called confluent if, whenever a term s reduces to two terms t_{1} and t_{2}, both t_{1} and t_{2} reduce to the same term. Confluence is a decidable property for terminating TRSs. Confluent TRSs have unique normal forms, when they exist. The confluence property is lost when non convergent critical pairs appear. Given two rules l_{1} → r_{1} and l_{2} → r_{2} if there exists a position p ∈ FPos(l_{1}) such that l_{1}|_{p} and l_{2} unify with mgu σ, then the pair of terms ⟨σ(r_{1}), σ(l_{1})[σ(r_{2})]_{p}⟩ is a critical pair. If two rules have a critical pair, we say that they overlap. A special case of overlapping rules are, those what we call variant overlapping rules, that is, overlapping rules whose lhss are variants one of each other ^{2}. We call a TRS with overlapping rules overlapping TRS.

A TRS is said to be constructor-based (CB) if the “arguments” of the lhs of its rules are constructor terms or variables.

A TRS is said to be left-linear (resp. rigth-linear) if for each rule l → r in the TRS, the lhs l (resp. rhs r) is a linear term.

Since, in this paper, we are interested in non-determinism we are going to work with overlapping CB and left linear TRSs that we assimilate to programs. This is a suitable class of programs for integrating functional and logic languages and modeling a non-deterministic behavior [2, 8].

2.3 Functional Logic Programming.

Functional logic languages can be considered as an extension of functional languages with principles derived from logic programming. Most of this languages use TRSs as programs and (some variant) of narrowing as operational semantics. Narrowing generalizes the rewriting operational mechanism of functional

2 Rules of this kind are not unusual in practical programs. This is the only kind of overlapping allowed in overlapping inductively sequential rewrite systems, a class that supports both non-deterministic computations and optimal lazy evaluation [2].

languages. The narrowing relation induced by a TRS is defined as follows: a term t is reduced to the term s in a narrowing step, denoted t ⇝_{[p,R,σ]} s, if there exists a position p ∈ FPos(t), a variant program rule R = (l → r) and a unifier σ of the terms t|_{p} and l, such that s = σ(t[r]_{p}). We say that there exists a narrowing derivation from a term t to a term s, if there exists a sequence of narrowing steps t = t_{0} ⇝_{[p_{1},R_{1},σ_{1}]} t_{1} ⇝_{[p_{2},R_{2},σ_{2}]} … ⇝_{[p_{n},R_{n},σ_{n}]} t_{n} = s and we write t ⇝_{σ}^{∗} s, where σ = σ_{n} ∘ … ∘ σ_{2} ∘ σ_{1}. We say that the pair ⟨s, σ⟩ is the outcome of the derivation. Usually we say that the term s is the result of the derivation and the substitution σ is the computed answer. Mostly, we are interested in derivations to constructor terms, that we call values.

Intuitively, narrowing computes a suitable substitution, σ, which when it is applied to a term t, the term σ(t) can be reduced on a rewriting step σ(t) →_{p,R} s. Note that, usually, the substitution σ computed by a narrowing step is a most general unifier, i.e., σ = mgu({l = t|_{p}}). However we have relaxed this restriction to support narrowing strategies, such as needed narrowing [3] or INS [2], that may compute substitutions which are not most general unifiers.

Narrowing provides completeness in the sense of logic programming (computation of answers) and also in the sense of functional programming (computation of values or normal forms).

3 The Factoring Transformation

The aim of program transformation [6, 18] is to derive a program semantically equivalent to the original program. More accurately, given an initial program R, we want to derive a new program R′ which computes the same results and answers as R for any input term, but with a better behavior w.r.t. some determined properties (usually, we want the transformed program may be executed more efficiently than the initial one).

We are interested in the transformation of overlapping, CB and left linear TRSs modeling functional logic programs with a non-deterministic behavior [2, 9]. Beginning from this point, by abuse of language, and in order to lighten our discourse, we use the word “program” as a synonym of “overlapping, CB and left linear TRS”. In a program, variant overlapping rules can be “merged” and expressed in a more concise way by means of the introduction of the alternative operation “ ! ”. We consider the alternative operation “ ! ” as defined by the pair of variant overlapping rules introduced in Section 1. Also, we consider that this pair of rules is present in all our programs. This assumption is harmless, since the operation can be added to any program that does not already define it without changing the meaning of existing operations.

We formalize our transformation, intuitively introduced in Section 1, by means of the foollowing definitions.

Definition 1. [Term factoring] Let t, u and v be terms. We say that t is a product of u and v if and only if one of the following conditions hold:

1. t = u! v or t = v! u.

2. t = f(t_{1}, …, t_{n}), where f is a symbol of arity n and t_{1}, …, t_{n} are terms, u = f(u_{1}, …, u_{n}), v = f(v_{1}, …, v_{n}), where u_{1}, …, u_{n}, v_{1}, …, v_{n} are terms, and for all i ∈ {1, …, n}\{j}, with j ∈ {1, …, n}, t_{i} = u_{i} = v_{i} and t_{j} is a product of u_{j} and v_{j}.

Conversely we say that u and v are factors of t.

Observe that the last case of Definition 1 may apply when f is “ ! ”.

Example 1. Both s(0) ! s(s(0)) and s(0 ! s(0)) are products of the terms s(0) and s(s(0)). The term f(X, s(0 ! s(0))) is a product of the terms f(X, s(0)) and f(X, s(s(0))). Note also that, for the terms f(0, 0) and f(s(0), s(0)) it is impossible to construct a product other that the trivial f(0, 0) ! f(s(0), s(0)).

Intuitively, a product t is built by sharing a common context of u and v over a single common position of both u and v. In the simplest case the context is a vacuum context and the single common position is the top position of the factors.

Definition 2. [Program factoring] Let R be a program defining the alternative operation “ ! ”, and l_{1} → r_{1} and l_{2} → r_{2} are variant overlapping rules of R. Without loss of generality we assume that l_{1} = l_{2} (since renaming the variables of a rule does not change the rewrite relation). A program R′ factors R if and only if either R′ = R\{l_{1} → r_{1}, l_{2} → r_{2}} ∪ {l_{1} → r}, where r is a product of r_{1} and r_{2}, or R′ factors some program R′′ and R′′ factors R.

Informally, the factoring transformation can be seen as a process that starting with an overlapping, left linear and CB TRS (the original program) produce a new TRS (the transformed program) by application of a sequence of the following transformation steps:

1. merging step: we arbitrarily select two variant overlapping rules (different from ALT) l → u and l → v that are merged into a new single rule l → u ! v and the old rules are erased;

2. factoring step: if possible, we push the root alternative operator down the term by factoring some common part of the rhs.

This transformation process always terminates, provided that we work with finite programs and terms. Although we let unspecified both the starting program and the final program, it should be intuitively clear that the deeper the alternative operator can be pushed down the right-hand side, the more likely it will be to replace two fair independent computations by a single computation.

Example 2. Considering once more again the program R = {bigger → s(0), bigger → s(s(0))} (augmented with the ALT rules), the free application of the aforementioned transformation steps leads to the following residual programs:

R′_{1} = {bigger → s(0) ! s(s(0))} and R′_{2} = {bigger → s(0 ! s(0))}.

Both R′_{1} and R′_{2} factors R (according to Definition 2), but only R′_{2} can effectively produce a gain by merging two fair independent computations into a single computation. Finally, it is worthy to say that R′_{2} factors R′_{1} and R′_{2} cannot be further transformed.

Note that, since we introduce the ALT rules in the transformed program as well as in the original one, both programs derive the same signature and can be used to reduce the same kind of terms. Therefore, it is not necessary any kind of renaming transformation as it is the case of other more complex transformation techniques, e.g., the partial evaluation transformation of [1].

4 Correctness of the Factoring Transformation

From an operational semantics point of view, we say that a transformation is sound when, given a term, the results and answers computed by the transformed program are exactly the same as the ones computed by the original program for that term. The definition of completeness is the reverse of the last concept.

Definition 3. Let ℑ be a mapping from programs to programs. Let R and R′ be programs (with the same signature) such that R′ = ℑ(R). ℑ is complete if and only if for every term t and value v, t ⇝_{σ}^{∗} v in R implies t ⇝_{σ′}^{∗} v in R′ where σ = σ′[Var(t)]. ℑ is sound if and only if for every term t and value v, t ⇝_{σ′}^{∗} v in R′ implies t ⇝_{σ}^{∗} v in R where σ = σ′[Var(t)].

In this section we are interested in the study of the correctness properties of the factoring transformation given by Definition 2.

4.1 Embedding relation

For the class of programs we are working on there is not a notion of descendants [12] of a redex. Therefore, it is difficult to reason about the correctness properties of our transformation. To facilitate our proofs of correctness we introduce an intuitive notion of ordering, for terms with alternative symbols, in which a term that is “contained” inside another is smaller than the other.

Definition 4 (embedding relation). The embedding relation ⊴ on terms in T (F, X) is defined as the smallest relation satisfying: x ⊴ x for all x ∈ X, and s ⊴ t, if and only if:

1. if Root(s) ≠ ! and t = u ! v then s ⊴ u or s ⊴ v;

2. if s = f(s_{1}, …, s_{n}) and t = f(t_{1}, …, t_{n}) then s_{i} ⊴ t_{i} for all i = 1, …, n.

The strict embedding relation ⊲ is defined, in terms of the embedding relation ⊴, as follows: s ⊲ t, if and only if s ⊴ t and s ≠ t.

The above definition differs from the homeomorphic embedding relation of [7] or [16]. Note also that, for the second case, the operation symbol f may be an alternative symbol.

Example 3. These terms are in the embedding relation: 0 ⊴ 0 ! s(X); f(a) ⊴ a ! f(a ! b) and 0 ! f(X) ⊴ (0 ! s(0)) ! f(X).

The embedding relation ⊴ is a partial order over the set T (F, X). Clearly, the relation is reflexive, transitive, and antisymmetric.

Definition 5 (minimal element). Let t be a term, we call minimal element of t, a term u such that u ⊴ t and there no exists a term v ⊴ t such that v ⊲ u

The notion of minimal element can be extended to substitutions in a natural way: a substitution σ is minimal w.r.t. the substitution θ iff Dom(σ) = Dom(θ) and, for all x ∈ Dom(σ), σ(x) is a minimal element of θ(x).

Lemma 1. If s and t are terms such that s ⊴ t, then there exists a reduction sequence from t to s using only ALT rules.

Proof. By structural induction on t. We distinguish the following cases:

1. t ∈ X or t is a nullary symbol Then, by Definition 4, s = t and the claim follows by vacuity.

2. t = u ! v Assume Root(s) ≠ ! , otherwise we are in the third case of this proof. Now, by Definition 4, s ⊴ u or s ⊴ v. Assuming that s ⊴ u, by induction hypothesis u →_{ALT} … →_{ALT} s and we can built the reduction sequence:

t = u ! v →_{ALT_{1}} u →_{ALT} … →_{ALT} s

3. t = f(t_{1}, … t_{n})

Then s must be rooted by the symbol f, otherwise s would not be embedded in t. Hence, s = f(s_{1}, … s_{n}) and s_{i}⊴t_{i} for all i ∈ {1, …, n}. By the inductive hypothesis t_{i} →_{ALT} … →_{ALT} s_{i} for all i ∈ {1, …, n} and we can built the reduction sequence:

\begin{aligned}t = f(t_{1}, … t_{n}) & →_{ALT} … →_{ALT} f(s_{1}, … t_{n}) →_{ALT} … \\ & →_{ALT} … →_{ALT} f(s_{1}, … s_{n}) = s. \end{aligned}

Corollary 1. If u is a minimal element of t, then u is a normal form of t w.r.t. reduction sequences using only ALT rules.

Proof. Immediate by Definition 5 and Lemma 1.

4.2 Completeness

The following lemma establishes the precise relation between a step in the original program and a reduction sequence in the transformed one.

Lemma 2. Let R be a program, R′ be a program that factors R. If there exists a reduction step A = t → s in R then there exists a reduction sequence D′ = t →^{+} s in R′.

Proof. Assume that the step A is performed with the rule R = l → r over the position p and t|_{p} = θ(l), i.e., A = t →_{p,R} t[θ(r)]_{p}. We consider the following cases:

1. R is a rule that also belongs to R′. Then the claim immediately holds.

2. R was merged in a transformed rule R′ = l → r′ of R′, where r is a factor of r′. Then r ⊴ r and by Lemma 1 there exists the reduction sequence r′ →_{ALT} … →_{ALT} r. Therefore we can construct the following reduction sequence in R′

t →_{p,R′} t[θ(r′)]_{p} →_{ALT} … →_{ALT} t[θ(r)]_{p}

Now it is immediate to establish the equivalence between reduction sequences leading to a value in both the original and the transformed program.

Proposition 1 (pre-completeness). Let R be a program and R′ be a program that factors R. If there exists a reduction sequence D = t →^{∗} s in R, where s is a value then there exists a reduction sequence D′ = t →^{∗} s in R′.

Proof. By induction on the number n of steps of the reduction sequence D and Lemma 2.

Finally, the completeness of the transformation is an easy consequence of the correctness of narrowing.

Theorem 1. The factoring transformation is complete.

Proof. Let R be a program and R′ be a program that factors R. If there exists a derivation t ⇝_{σ}^{∗} s in R

⇒ σ(t) →^{∗} s in R  (by soundness of narrowing)
⇒ σ(t) →^{∗} s in R′  (by Proposition 1)
⇒ t ⇝_{σ′}^{∗} s in R′ with σ′ = σ[Var(t)] (by completeness of narrowing).

Note that it was not necessary to impose additional requirements to the programs (such as right linearity) or to use a special semantics (see Section 4.4) in order to obtain the completeness result.

4.3 Soundness

As we are going to see, our transformation does not preserve the soundness property in all cases. The following example points out this drawback and permit us to understand the kind of restrictions that are necessary to introduce to preserve this property.

Example 4. Given the initial program R

\begin{matrix}R_{1} : & double(X) → X + X \\ R_{2} : & f → double(0) R_{3} : & f → double(s(0)) \end{matrix}

extended with the usual rules for the addition, and the input term f, only the following results are possible: {0, s(s(0))}. On the other hand, the factored version of R, namely R′, is

\begin{matrix}R_{1} : & double(X) → X + X \\ R_{23} : & f → double(0 ! s(0)) \end{matrix}

and it can compute the additional result s(0) (twice) for the input term f.

This example reveals that, in general, our transformation is unsound, because there exists derivations in R′ that cannot be reproduced in R. At the first sight, a possible solution for this drawback might be to restrict the kind of operations that can be used in the transformation. Note that, the operation double, defined by rule R_{1}, is not right linear and this is the main source of our problem: the subterm at position 1 of double(0 ! s(0)) is duplicate, introducing new alternatives that are not produced when the reduction of f is done using the original program R. Therefore, the solution might be to impose as a restriction that only operations defined by right linear rules should be part of a context containing a product. Unfortunately, a stronger restriction, namely the right linearity of the program, must be imposed. Suppose that we change the rule R_{1}, in R, by this right linear rule

R_{1} : double(X) → s(s(0)) × X,

we also introduce in our program the suitable rules for the operation × and we transform the resulting program to obtain a new factored version of it. Then when we proceed with the computation of f, due to the lack of right linearity of one of the rules defining the operation ×, the same problem is reproduced again (the original program computes the results {0, s(s(0))} whereas the transformed program computes the results {0, s(0), s(s(0))}).

For the class of programs we use, the concept of right linearity must be revised, considering that the variables occurring in different alternatives of a rhs of a variant overlapping rule are completely independent. Certainly, since this kind of rules are the result of merging several rules whose lhss are variants [2], this distintion corresponds with the intended semantics of the original program.

Example 5. Given the program

R_{1} : f(X) → g(X) R_{2} : f(X) → h(X)

it can be transformed in this other program

R_{12} : f(X) → g(X) ! h(X)

The variables of the rules R_{1} and R_{2} of the original program are independent and, indeed, we have to select a variant of these rules when they are applied to perform a computation step. Therefore, it is meaningless to consider the variable X of the rule R_{12} as the same variable for both alternatives.

On the other hand, the situation illustrated by Example 5 does not lead to the unsoundness problem as we have been discussing above. Although the rule R_{12} of Example 5 is not right linear, at most one of both alternatives of the function f is needed in a computation to a value. Therefore, we assume that the apparition of this kind of rules in the transformed program doesn’t break the good properties provided by the right linearity of the original program. Certainly, this kind of rules preserve an important compositional property that we are going to establish in Lemma 5.

In order to prove the soundness of our transformation we need the following auxiliary lemmas. The first lemma points out the existence of a compositional property between the minimal elements of a linear term t, the minimal substitutions w.r.t. a substitution σ and the minimal elements of the term σ(t).

Lemma 3. Let t be a linear term and σ a substitution. Let M be the set of all minimal elements of t and ⋃_{i=1}^{n}{σ_{i}} be the set of all minimal substitutions w.r.t. σ. Then, ⋃_{i=1}^{n}σ_{i}(M) is the set of all minimal elements of the term σ(t).

Proof. By structural induction on t. We distinguish the following cases:

1. t ∈ X In this case t is a minimal element of itself and, by definition of minimal substitution, each σ_{i}(x), i ∈ {1, …, n} is a minimal element of σ(x). Therefore, ⋃_{i=1}^{n}{σ_{i}(x)} is the set of all minimal elements of the term σ(t).

2. t is a nullary symbol Then, the claim trivially follows, since t is the single minimal element of itself, σ(t) = t and σ_{i}(t) = t, for all i ∈ {1, …, n}.

3. t = f(t_{1}, … t_{m})

Since t is linear, each subterm t_{j} is also linear. Assume M_{j} is the set of all minimal elements of t_{j}, j ∈ {1, …, m}. By the inductive hypothesis, ⋃_{i=1}^{n}σ_{i}(M_{j}) is the set of all minimal elements of the term σ(t_{j}). Now consider the term s = f(s_{1}, … s_{m}) where s_{j} ∈ M_{j}, j ∈ {1, …, m}. By construction s is one of the minimal elements of t and, by Definition 4 and the inductive hypothesis,

σ_{i}(s) = f(σ_{i}(s_{1}), … σ_{i}(s_{m})) ⊴ f(σ(t_{1}), … σ(t_{m})) = σ(t)

that is, σ_{i}(s) is a minimal element of σ(t). Therefore, the claim of this lemma immediately follows.

The intuitive idea behind Lemma 3 is to avoid problems like the one illustrated in the following example:

Example 6. Suppose the non-linear term t = X + X (possibly a rhs of a rule) and a substitution σ = {X/(0 ! s(0))}. Then, t is minimal, {{X/0}, {X/s(0)}} is the set of minimal substitutions w.r.t. σ, but {{X/0}(t), {X/s(0)}(t)} = {0 + 0, s(0) + s(0)} is not the set of all minimal elements of σ(t).

Lemma 3 can be extended to a product where each factor is linear, although some of these factors may share some variables in common.

Lemma 4. Let t = u ! v be a product where u and v are linear terms such that Var(u) ∩ Var(v) ≠ ∅. Let U and V be the set of all minimal elements of u and v respectively. Let σ be a substitution and ⋃_{i=1}^{n}{σ_{i}} be the set of all minimal substitutions w.r.t. σ. Then, (⋃_{i=1}^{n} σ_{i}(U))∪(⋃_{i=1}^{n_{i}} σ_{i}(V)) is the set of all minimal elements of the term σ(t).

Proof. Since u is a linear term, by Lemma 3, M_{u}^{σ} = ⋃_{i=1}^{n}σ_{i}(U) is the set of all minimal elements of the term σ(u) and M_{v}^{σ} = ⋃_{i=1}^{n}σ_{i}(V) is the set of all minimal elements of the term σ(v). Now, consider a term s ∈ U, by Definition 4,

σ_{i}(s) ⊴ σ(u) ⊴ σ(u) ! σ(v) = σ(t),

and, by Corollary 1, σ_{i}(s) is a minimal element of σ(t). Therefore, each element of M_{u}^{σ} is a minimal element of σ(t). Similarly, each element of M_{v}^{σ} is a minimal element of σ(t). Hence, M_{u}^{σ} ∪ M_{v}^{σ} is the set of all minimal elements of the term σ(t).

Note that, in Lemma 4, the only requirement for the subterms u and v is linearity and, therefore, they can contain occurrences of the alternative symbol. The following lemma is a generalization of Lemma 4.

Lemma 5. Let t = t_{1} ! , …, ! t_{m} be a product where each factor t_{j}, j ∈ {1, …, m}, is a linear term such that ⋂_{j=1}^{m} Var(t_{j}) ≠ ∅. Let M_{j} be the set of all minimal elements of t_{j}, j ∈ {1, …, m}. Let σ be a substitution and ⋃_{i=1}^{n}{σ_{i}} be the set of all minimal substitutions w.r.t. σ. Then, ⋃_{i=1}^{n}_{j=1}^{m}σ_{i}(M_{j}) is the set of all minimal elements of the term σ(t).

Proof. By induction on the number of alternative symbols in t and Lemma 4.

Note that our transformation produce, mostly, transformed rules whose rhss fulfills the conditions of Lemma 5. Therefore, the last result can be use to obtain all minimal elements of a rhs σ′(r′) applying the minimal substitutions σ w.r.t. σ′ to the minimal elements r of r′. This is one of the keys to prove Lemma 6. But, we first need the introduction of a new concept.

As we said, Definition 2 lets unspecified the shape of the original program as well as the way the transformation steps are applied. Managing this great freedom in the use of our transformation when we try to prove its soundness can increase unnecessarily the difficulty of the proof without produce, as we are going to reason, a real gain. Therefore, in order to maintain the proof as simple as possible, we first assume that the original program is in a “non-factorized” form and we prove some auxiliary results that are extended to arbitrary programs later.

Definition 6 (non-factorized program). A non-factorized program is a program where the rhs of its rules don’t contain occurrences of the alternative symbol.

That is, a non-factorized program is a program where the variant overlapping rules are in the simplest possible form and none factoring transformation was previously applied.

Example 7. The program {bigger → s(0), bigger → s(s(0))} is a non-factorized version of bigger whereas {bigger → s(0) ! s(s(0))} or {bigger → s(0 ! s(0))} are not.

It is clear that the non-factorized form of a program is unique, since the factoring transformation does not erase factors and it can be undone following this sequence of steps: i) given a rule R = l → r, where r contains the alternative operator, find the set {r_{1}, …, r_{n}} of minimal elements of r (w.r.t. embedding relation); ii) replace the rule R by the set of rules {l → r_{1}, …, l → r_{n}}.

Now, we are ready to prove the following auxiliary lemmas.

Lemma 6. Let R be a non-factorized and right linear program and R′ be a program that factors R. If there exists a reduction step t′ → u′ in R′ then, for any minimal element u of u′ there exists a minimal element t of t′ and a reduction step t → u in R or t = u.

Proof. By structural induction on t′. We distinguish the following cases:

1. t′ ∈ X or t′ is a nullary constant symbol The claim follows by vacuity, since t′ is a normal form which is a minimal element of itself.

2. t′ is a nullary function symbol In this case, t′ is a minimal element of itself and there must be a rule R′ = t′ → u′ in R′ (the step is performed over the top position Λ using the identity substitution id). By Definition 2 and since R is a non-factorized program, for each minimal element u of u′ there must be a rule R = t′ → u in R. Thus, the claim follows trivially.

3. t′ = t′_{1} ! t′_{2}

(a) The step is performed over the top position Λ. Then the step is performed with an ALT rule. Assume that t′ →_{ALT_{1}} t′_{1} is the performed reduction step and that u is a minimal element of t′_{1}. Then, by Corollary 1, we can construct the reduction sequence t′ →_{ALT_{1}} t′_{1} →^{∗} u ↛_{ALT}. Therefore, u is also a minimal element of t′ and the claim follows trivially since t = u.

(b) The step is performed over a position p ≠ Λ. Assume p = 1.q (i.e., p belongs to t′_{1}) and the step is t′ → u′_{1} ! t′_{2}. Then there exists a step t′_{1} → u′_{1} in R′ and, by the inductive hypothesis, for any minimal element u of u′_{1} there exists a minimal element t of t′_{1} and a reduction step t → u in R. Now, the claim follows by Definition 5 and the transitive property of the embedding relation. On the other hand, note that, for each minimal element u of t′_{2} the claim follows trivially, since then u is also a minimal element of t′, that is, t = u.

4. t′ = f(t′_{1}, … t′_{n})

(a) The step is performed over the top position Λ. In this case there must be a rule R′ = l → r′ in R′ such that l = f(C_{1}[x_{11}, …, x_{1m_{1}}], …, C_{n}[x_{n1}, …, x_{nm_{n}}]), where each C_{i}[ ] is (a possibly empty) constructor context and t′_{i} = C_{i}[s_{i1}, …, s_{nm_{i}}]. Therefore there exists a substitution σ′ such that it is possible the reduction step t′ = σ′(l) → σ′(r′). By definition of factoring transformation and since R is a non-factorized program, for each minimal element r of r′ there exists a rule R = l → r in R. Now consider a minimal substitution σ w.r.t. σ′, it is possible the following rewriting step t = σ(l) → σ(r) = u in R. By Lemma 5 u is a minimal element of u′ and, clearly, t is a minimal element of t′. Also, by Lemma 5 all minimal elements of u′ can be obtained applaying the minimal substitutions σ w.r.t. σ′ to the minimal elements r of r′.

(b) The step is performed over a position p ≠ Λ. Assume p = i.q (i.e., p belongs to t′_{i}) and the step is t′ → f(t′_{1}, …, u′_{i}, …, t′_{n}). Then there exists a step t′_{i} → u′_{i} in R′ and, by the inductive hypothesis, for any minimal element u_{i} of u′_{i} there exists a minimal element t_{i} of t′_{i} and a reduction step t_{i} → u_{i} in R. Now, the claim follows by Definition 4 and the replacement property of rewriting: for any minimal element t_{j} of t′_{j} (with j ≠ i), u = f(t_{1}, …, u_{i}, …, t_{n}) is a minimal element of u′, there exits a step t = f(t_{1}, …, t_{i}, …, t_{n}) → f(t_{1}, …, u_{i}, …, t_{n}) = u in R and t is a minimal element of t′.

Lemma 7. Let R be a non-factorized and right linear program and R′ be a program that factors R. If there exists a reduction sequence t′ →^{∗} u′ in R′ then, for any minimal element u of u′ there exists a minimal element t of t′ and a reduction sequence t →^{∗} u in R

Proof. Immediate, by induction on the number of steps n of the reduction sequence in R′ and Lemma 6.

The following lemma establishes the relation between the reduction sequences leading to a value in both the transformed and the original program.

Lemma 8. Let R be a non-factorized and right linear program and R′ be a program that factors R. If there exists a reduction sequence t →^{∗} s in R′, where s is a value then there exists a reduction sequence t →^{∗} s in R

Proof. By Lemma 7 there exists a reduction sequence u →^{∗} v in R, where u is a minimal element of t and v a minimal element of s. Since u ⊴ t, by Lemma 1, there exists a reduction sequence t →_{ALT} … →_{ALT} u. On the other hand, if s is a value and v ⊴ s, then v = s. Therefore, we can construct the following reduction sequence in R: t →_{ALT} … →_{ALT} u →^{∗} v = s.

Now, we lift the last result to arbitrary right linear programs.

Proposition 2 (pre-soundness). Let R be a right linear program and R′ be a program that factors R. If there exists a reduction sequence t →^{∗} s in R′, where s is a value then there exists a reduction sequence t →^{∗} s in R

Proof. Assume R′′ is the non-factorized program such that R factors R′′. By definition of the factoring transformation it is clear that R′′ exists and R′ factors R′′. Also note that, being R right linear, R′′ must be right linear. Now, by Lemma 8, if there exists a reduction sequence t →^{∗} s in R′, then there exists a reduction sequence t →^{∗} s in R′′ and therefore, by Proposition 1, there exists a reduction sequence t →^{∗} s in R.

The soundness of the transformation is an easy consequence of the correctness of narrowing and Proposition 2

Theorem 2. The factoring transformation is sound for right linear programs.

Proof. Let R be a right linear program and R′ be a program that factors R. If there exists a derivation t ⇝_{σ}^{∗} s in R′

⇒ σ′(t) →^{∗} s in R′  (by soundness of narrowing)
⇒ σ′(t) →^{∗} s in R  (by Proposition 2)
⇒ t ⇝_{σ}^{∗} s in R with σ = σ′[Var(t)] (by completeness of narrowing).

4.4 Discussion

As we have seen, factoring is generally unsound, but soundness can be recovered in some cases of practical interest. In the following discussion, the notions of descendant of a redex is informal, as this notion has been rigorously defined only for orthogonal rewrite systems [12]. The unsoundness of factoring originates from computations in which some redex r generates several descendants, and distinct descendants are reduced to different terms. Thus, two simple independent solutions to the unsoundness problem are to avoid distinct descendants of a redex or to ensure that all the descendants of a redex are contracted using the same rewrite rule.

The first condition holds, as we have just proved, for right-linear rewrite systems. But the restriction to right linear systems is unacceptable from a programming point of view.

The second condition is ensured by the use of a call-time choice semantics or sharing. These solutions were proposed to manage similar but distinct issues in the context of overlapping TRSs by Hussmann [14]. Informally, the call-time choice semantics consists of “committing” to the value of an argument of a symbol (either operation or constructor) at the time of the symbol’s application. The value of the argument does not need to be computed at application time: thus, the laziness of computations is not jeopardized. This semantics is the most appropriate for some computations, but it fails to capture the intuitive meaning of others. Nevertheless, there are formalisms, such as [9], and languages, like Toy [17] (based on the aforementioned formalism) and Curry [11], that adopt the call-time choice as the only semantics of non-deterministic computations. On the other hand, sharing is a technique where all occurrences of the same variable in a rhs of a rule are shared, i.e. all these occurrences are replaced by a pointer to the same subterm after a rewriting step. Sharing is effectively implemented using term graphs.

Hence, both approaches, call-time choice semantics or sharing, are useful to resolve the problems discussed w.r.t. Example 4: they avoid the strong syntactic restriction of right linearity while keep the factoring transformation sound.

5 Conclusions

Non-deterministic computations are an essential feature of functional logic programming languages but its implementation may be very costly, since, usually it is necessary to compute a set of fair independent computations whose results are used, and possibly discarded, by a context.

In this paper, we have defined a program transformation, called factoring transformation, that can be fully automated or used as a programming technique. The factoring transformation is based on the introduction of a new symbol, called alternative, into the signature of a program. The alternative symbol is a polymorphic defined operation. This symbol allows a program to factor a common portion of the non-deterministic replacements of a redex. This transformation may improve the efficiency of a computation by reducing the number of computation steps or the memory used in representing terms. Savings are obtained when fair independent computations are avoided because only the factored portion of non-deterministic replacements is needed.

We have studied the formal properties of the factoring transformation, proving its correctness for right linear programs. Afterwards, we have discussed how this impractical syntactic restriction can be overcome if sharing or call-time choice semantics is used as an implementation device of the functional logic language. Therefore, our transformation can be applied safely to the Constructorbased (conditional) ReWriting Logic (CRWL) programs of [9] as well as to Curry programs [11], since they adopt the call-time choice semantics for nondeterministic functions.

Also, in order to prove our results we have introduced an embedding relation that have shown its usefulness to reason with non-confluent constructor-based TRSs, where the notion of descendants of a redex [12] is not well established.

Finally note that, although the process of factoring a program can remind, in some aspects, the full laziness transformation of Functional Programming [13, 15], at the best of our knowledge, it is a novel transformation that can be applied to a high programming language as well as to a core language, producing an effective improvement of the efficiency of the programs.

Acknowledgments

I wish to thank Sergio Antoy the discussion of technical aspects of this paper that greatly improve it. Part of this research was done while the author was visiting the Department of Computer Science at Portland State University. The author gratefully acknowledges the hospitality of that department.

References

1. M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Specialization of Lazy Functional Logic Programs. In Proc. of PEPM’97, volume 32, 12 of Sigplan Notices, pages 151–162, New York, 1997. ACM Press.

2. S. Antoy. Optimal non-deterministic functional logic computations. In Proc. of ALP’97, pages 16–30. Springer LNCS 1298, 1997.

3. S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. Journal of the ACM, 47(4):776–822, July 2000.

4. S. Antoy, P. Julián Iranzo, and B. Massey. Improving the efficiency of nondeterministic computations. Electronic Notes in Theoretical Computer Science,

    64:22, 2002. URL: http://www.elsevier.nl/locate/entcs/volume64.html.

5. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

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

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

8. J.C. González-Moreno, M.T. Hortalá-González, F.J. López-Fraguas, and M. Rodríguez-Artalejo. A rewriting logic for declarative programming. In Proc. ESOP’96, pages 156–172. Springer LNCS 1058, 1996.

9. J.C. González-Moreno, F.J. López-Fraguas, M.T. Hortalá-González, and M. Rodríguez-Artalejo. An approach to declarative programming based on a rewriting logic. The Journal of Logic Programming, 40:47–87, 1999.

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

11. M. Hanus (ed.). Curry: An Integrated Functional Logic Language (Ver. 0.71). Web

document http://www.informatik.uni-kiel.de/~mh/curry/report.html, 2000.

12. G. Huet and J.-J. Lévy. Computations in orthogonal term rewriting systems. In J.-L. Lassez and G. Plotkin, editors, Computational logic: essays in honour of Alan Robinson. MIT Press, Cambridge, MA, 1991.

13. R. Hughes. The Design and Implementation of Programming Languages. PhD thesis, University of Oxford, 1984., 1984.

14. H. Hussmann. Nondeterministic Algebraic Specifications and nonconfluent term rewriting. Journal of Logic Programming, 12:237–255, 1992.

15. S. L. Peyton Jones and D. Lester. A modular fully-lazy lambda lifter in HASKELL. Software, Practice and Experience, 21(5):479–506, 1991.

16. M. Leuschel and B. Martens. Global Control for Partial Deduction through Characteristic Atoms and Global Trees. In Proc. of the 1996 Dagstuhl Seminar on Partial Evaluation, pages 263–283. Springer LNCS 1110, 1996.

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

18. A. Pettorossi and M. Proietti. A Comparative Revisitation of Some Program Transformation Techniques. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, Int’l Seminar, Dagstuhl Castle, Germany, pages 355–385. Springer LNCS 1110, 1996.