Transformations for Efficient Evaluations in Functional Programming^{⋆}

Salvador Lucas

Departamento de Sistemas Informáticos y Computación Universidad Politécnica de Valencia Camino de Vera s/n, E-46071 Valencia, Spain.

                        e.mail: slucas@dsic.upv.es
            URL: http://www.dsic.upv.es/users/elp/slucas.html

Abstract. Rewriting is a suitable mechanism to implement functional programming languages. The definition of efficient evaluation strategies is a natural concern in this setting. Recently we have shown that, by imposing some simple restrictions on the replacements which are allowed for the arguments of functions, we can obtain efficient head-evaluations of terms in a certain class of programs. We are also able to completely evaluate terms, but in this case, the efficiency of computation can be compromised. This paper concerns the definition of program transformations that enable efficient but still complete evaluation of function calls.

Keywords: evaluation, functional programming, program transformation, term rewriting.

1 Introduction

Functional languages which allow the definition of functions by means of patterns (e.g. Haskell, Hope or Miranda), are well suited to use term rewriting [4] as execution principle. Computing involves reduction of (input) terms to a normal form [9]. Any effective execution procedure must include a normalizing rewriting strategy able to compute the normal form of the input term if it exists. Such a reduction strategy is expected to be efficient both in performing only useful reductions and in its implementation [8]. For orthogonal term rewriting systems (TRSs), the Huet and Levy’s notion of needed reduction [2] formalizes what we mean by a useful reduction. Needed reduction is any strategy which only selects needed redexes. A redex of a term t is needed if it is reduced (itself or some of its residuals) in every reduction sequence leading t to a normal form. Reduction of needed redexes is normalizing and, moreover, each step do actually contributes to normalization. Computing such needed redexes is not possible in the general case, but some approximations have been defined in the literature [2, 8].

Using strongly replacing-independent TRSs [7], it is possible to define a needed reduction strategy by only considering syntactic replacement restrictions: a mapping μ : Σ → P(IN) (called the replacement map) indicates the fixed argument

⋆ This work has been partially supported by CICYT under grant TIC 95-0433-C03-03.

positions μ(f) ⊆ {1, …, k} of each k-ary function f for which we enable replacements. The restrictions on arguments are lifted to occurrences and the resulting restriction on rewriting is said context-sensitive rewriting (csr) [5, 6]. Given an orthogonal TRS R, we are able to define a canonical replacement map μ_{R}^{com} under which csr is able to compute head-normal forms [5]. An orthogonal, strongly replacing-independent TRS makes this by only reducing needed redexes [7]. The computation of such redexes is very easy, since we can take any replacing redex occurrence. This is to say that the replacement restrictions themselves are able to capture only needed redexes. Therefore, the implementation of a head-normalizing strategy for orthogonal strongly replacing-independent TRSs is nicely simple. For this reason, in this paper we analyze the problem of transforming an arbitrary TRS into an equivalent strongly replacing-independent TRS. This is always possible. However, orthogonality is not always preserved. Therefore, we have some limits in obtaining the desired benefits.

Computing head-normal forms is not completely satisfactory in functional programming. Our final goal is to evaluate a term t, i.e., to obtain the constructor term δ (the value of t) which expresses the meaning of t. csr is also able to compute values by using a less restrictive replacement map μ_{R}^{B} [5]. However, when dealing with orthogonal strongly replacing-independent TRSs, if we use μ_{R}^{B} instead of μ_{R}^{com} (and μ_{R}^{com} ≠ μ_{R}^{B}) we loose the nice correspondence between replacing redexes and needed redexes. Now we have replacing redexes which are not needed. To solve this problem, we introduce a new transformation which is able to combine the requirement of achieving complete evaluations by only reducing the needed redexes which can be computed by means of replacement restrictions.

In Section 2, we give some preliminary definitions. In Section 3, we recall the main definitions concerning csr. Section 4 gives the transformations to obtain a strongly replacing-independent TRS from a given TRS. In Section 5, we define a program transformation which raises the good properties of csr concerning head-evaluations to complete evaluations. Section 6 compares with some related work and concludes.

2 Preliminaries

Let us first introduce the main notations used in the paper [1, 4]. V denotes a countable set of variables and Σ denotes a set of function symbols {f, g, …}, each of which has a fixed arity given by a function ar : Σ → IN. By T (Σ, V) we denote the set of terms. t̃ denotes a k-tuple t_{1}, …, t_{k} of terms, where k will be clarified from the context. V ar(t) is the set of variables in a term t. Terms are viewed as labelled trees in the usual way. Occurrences u, v, … are chains of positive natural numbers used to address subterms of t. If W is a set of occurrences, u.W is the set {u.v | v ∈ W }. Occurrences are ordered by the standard prefix ordering: u ≤ v iff ∃w v = u.w. O(t) denotes the set of occurrences of a term t. Given a subset U ⊆ O(t), U↓ is the set U↓= {v ∈ O(t) | u ∈ U ∧ v ≤ u}. t|_{u} is the subterm at occurrence u of t. t[s]_{u} is the term t with the subterm at the occurrence u replaced with s. root(t) is the symbol labelling the root of t. Σ(t) = {f ∈ Σ | ∃u ∈ O(t).root(t|_{u}) = f} is the set of symbols from Σ appearing in t. Given a T ⊆ T (Σ, V), Σ(T) = ∪_{t∈T} Σ(t). O_{Σ}(t) = {u ∈ O(t) | root(t|_{u}) ∈ Σ} is the set of nonvariable occurrences in a term t. O_{V} (t) = O(t)\O_{Σ}(t) is the set of variable occurrences. We refer to any term C, which is the same as t everywhere except below u, i.e., ∃s. C[s]_{u} = t, as the context within the replacement occurs.

A rewrite rule is an ordered pair (l, r), written l → r, with l, r ∈ T (Σ, V), l ∉ V and V ar(r) ⊆ V ar(l). l is the left-hand side (lhs) of the rule and r is the right-hand side (rhs). A TRS is a pair R = (Σ, R) where R is a set of rewrite rules. L(R) is the set of lhs’s of R. An instance σ(l) of a lhs l ∈ L(R) is a redex. O_{R}(t) = {u ∈ O(t) | ∃l ∈ L(R) : t|_{u} = σ(l)} is the set of redex occurrences in a term t. Given a TRS R = (Σ, R), we consider Σ as the disjoint union Σ = C ⊎F of symbols c ∈ C, called constructors, having no associated rule and symbols f ∈ F, called defined functions or operations, which are defined by some program rule f(l̃) → r ∈ R: F = {f ∈ Σ | f(l̃) → r ∈ R} and C = Σ\F. Constructor terms (i.e., values) are denoted δ ∈ T (C, V).

For a given TRS R = (Σ, R), a term t rewrites to a term s (at the occurrence u), written t →^{u}_{R} s (or just t → s), if t|_{u} = σ(l) and s = t[σ(r)]_{u}, for some rule l → r in R, occurrence u in t and substitution σ. →_{R} is the one-step rewrite relation for R. A term t is in head-normal form if there is no derivation t = t_{1} → t_{2} → ⋯ starting from t which reduces the root of a term t_{i}, i ≥ 1.

IN_{k}^{+} is an initial segment {1, 2, … k} of the set of positive natural numbers IN^{+}, where IN_{0}^{+} = Ø. P(IN) is the powerset of natural numbers.

3 Context-sensitive rewriting

A mapping μ : Σ → P(IN) is a replacement map (or Σ-map) for the signature Σ iff for all f ∈ Σ. μ(f) ⊆ IN_{ar(f)}^{+}. A Σ-map μ determines the argument positions which can be reduced for each symbol in Σ [5, 6]. If we assume an arbitrary ordering in the signature^{2} Σ = {f_{1}, …, f_{n}}, then we express a Σ-map as μ = ⟨I_{1}, …, I_{n}⟩, where I_{j} = μ(f_{j}) for 1 ≤ j ≤ n. Given Δ ⊆ Σ, μ↓_{Δ} is the Δ-map given by: μ↓_{Δ} (f) = μ(f) for all f ∈ Δ.

The ordering ⊆ on P(IN) extends pointwise to an ordering ⊑ on M_{Σ}, the set of all Σ-maps: μ ⊑ μ′ if for all f ∈ Σ, μ(f) ⊆ μ′(f). (M_{Σ}, ⊑, μ_{⊥}, μ_{⊤}, ⊔, ⊓) is a complete lattice: for all f ∈ Σ, μ_{⊥}(f) = Ø, μ_{⊤}(f) = IN_{ar(f)}^{+}, (μ ⊔ μ′)(f) = μ(f)∪μ′(f) and (μ⊓μ′)(f) = μ(f)∩μ′(f). Thus, μ ⊑ μ′ means that μ considers less positions than μ′ for reduction.

The set of μ-replacing occurrences is given by: O^{μ}(x) = {ϵ} if x ∈ V, O^{μ}(f(t_{1}, …, t_{k})) = {ϵ} ∪ ⋃_{i∈μ(f)} i.O^{μ}(t_{i}). In csr, we only rewrite on replacing occurrences: t μ-rewrites to s, written t ↪_{R(μ)} s, if t →^{u}_{R} s and u ∈ O^{μ}(t). The set of replacing redexes is O_{R}^{μ}(t) = O_{R}(t) ∩ O^{μ}(t). The set of non-replacing occurrences is Õ^{μ}(t) = O(t)\O^{μ}(t). We also have O_{Σ}^{μ}(t) = O_{Σ}(t) ∩ O^{μ}(t) and O_{V}^{μ} (t) = O_{V} (t) ∩ O^{μ}(t).

A term t is μ-compatible (comp_{μ}(t)) if its non-replacing occurrences are variables: comp_{μ}(t) iff Õ^{μ}(t) ⊆ O_{V} (t). Equivalently, comp_{μ}(t) holds iff O_{Σ}(t) ⊆

2 Usually, the order in which the symbols are written.

O^{μ}(t). There exists a minimum Σ(t)-map μ_{t} ensuring compatibility: if t = x, then μ_{t}(f) = Ø for all f ∈ Σ. If t = f(t_{1}, …, t_{k}), then μ_{t} = μ_{t}^{ϵ} ⊔ μ_{t_{1}} ⊔ ⋯ ⊔ μ_{t_{k}}, where μ_{t}^{ϵ} is μ_{t}^{ϵ}(f) = {i | t_{i} ∉ V } and μ_{t}^{ϵ}(g) = Ø for all g ≠ f.

Example 3.1 Given t = first(0, x), Σ(t) = {0, first}, and we have:

μ_{first(0,x)} = μ_{first(0,x)}^{ϵ} ⊔ μ_{0} ⊔ μ_{x} = ⟨Ø, {1}⟩ ⊔ ⟨Ø, Ø⟩ ⊔ ⟨Ø, Ø⟩ = ⟨Ø, {1}⟩. For t′ = first(s(x), y :: z), Σ(t′) = {s,::, first}, and we get μ_{first(s(x),y::z)} = μ_{first(s(x),y::z)}^{ϵ}⊔μ_{s(x)}⊔μ_{y::z} = ⟨Ø, Ø, {1, 2}⟩⊔⟨Ø, Ø, Ø⟩⊔⟨Ø, Ø, Ø⟩ = ⟨Ø, Ø, {1, 2}⟩.

Analogously, for a set of terms T, we define μ_{T} = ⊔_{t∈T} μ_{t}. These replacement maps characterize compatibility: comp_{μ}(t) ⇔ μ_{t} ⊑ μ and comp_{μ}(T) ⇔ μ_{T} ⊑ μ.

Given a TRS R = (Σ, R), its canonical replacement map μ_{R}^{com} is μ_{R}^{com} = ⊔_{l∈L(R)}μ_{l}, where L(R) is the set of lhs’s of the TRS. μ_{R}^{com} is the minimum replacement map which makes the lhs’s of the TRS compatible terms.

Example 3.2 Consider the following program R which defines some functions on lists of natural numbers:

dbl(0) → 0               dbls([]) → []

   dbl(s(x)) → s(s(dbl(x))) dbls(x :: y) → dbl(x) :: dbls(y)

sel(0, x :: y) → x          indx([], x) → []

   sel(s(x), y :: z) → sel(x, z) indx(x :: y, z) → sel(x, z) :: indx(y, z)

   from(x) → x :: from(s(x))

The canonical replacement map for R is: μ_{R}^{com}(f) = Ø for all f ∈ {0, s, [],::, from}, μ_{R}^{com}(dbl) = μ_{R}^{com}(dbls) = μ_{R}^{com}(indx) = {1} and μ_{R}^{com}(sel) = {1, 2}.

Theorem 3.3 ([5]) Let R = (Σ, R) = (C ⊎ F, R) be a left-linear TRS and μ be a Σ-map such that μ_{R}^{com} ⊑ μ. Let t be a term and s = c(s̃) for some c ∈ C. If t →^{∗} s, there exists s′ = c(s̃′) s.t. t ↪^{∗} s′, and s′ →^{∗} s.

Theorem 3.4 ([5]) Let R = (Σ, R) be an orthogonal TRS and μ be a Σ-map such that μ_{R}^{com} ⊑ μ. Let t be a term and s = f(s̃) be a head-normal form. If t →^{∗} s, there exists a head-normal form s′ = f(s̃′) s.t. t ↪_{R(μ)}^{∗} s′, and s′ →^{∗} s.

Hence, from Theorem 3.3, for left-linear TRSs, we have completeness in headevaluations (i.e., reductions leading to a constructor head-normal form). For orthogonal TRSs, we have completeness in head-normalization (Theorem 3.4).

Example 3.5 For R in Example 3.2, we get the following head-evaluation using μ_{R}^{com} (redexes underlined; we mark some steps for further discussion):

   sel(s(0), dbls(\underline{from(0)}))

↪ sel(s(0), \underline{dbls(0 :: from(s(0)))})  (∗)
↪ \underline{sel(s(0), dbl(0) :: dbls(from(s(0))))}  (∗∗)

       ↪ sel(0, dbls(\underline{from(s(0))}))

↪ sel(0, \underline{dbls(s(0) :: from(s(s(0))))})  (∗)

       ↪ \underline{sel(0, dbl(s(0)) :: dbls(from(s(s(0))))}
       ↪ \underline{dbl(s(0))}

↪ s(s(dbl(0)))

4 Strongly replacing-independent TRSs

In this section, we introduce the strongly replacing-independent TRSs, for which we have proven that any context-sensitive reduction is needed [7]. A term t is strongly μ-compatible (scomp_{μ}(t)) if Õ^{μ}(t) = O_{V} (t). Alternatively scomp_{μ}(t) holds if O_{Σ}(t) = O^{μ}(t). Clearly scomp_{μ}(t) ⇒ comp_{μ}(t). A set of terms T ⊆ T (Σ, V) is said to be weakly compatible (wcomp(T)), if, for all t ∈ T, scomp_{μ_{t}}(t). T is strongly μ-compatible (scomp_{μ}(T)), if, for all t ∈ T, scomp_{μ}(t).

Some terms have no replacement map μ which satisfies scomp_{μ}(t). For instance, there is no replacement map which makes the term f(f(x, a), y) strongly compatible. When such a Σ(t)-map exists, it only can be μ_{t}. The Σ(T)-map μ which makes a set T strongly μ-compatible must be μ = μ_{T}. However, the replacement restrictions for symbols in Σ\Σ(T) can be freely established without damaging the strong compatibility of T. We assume this fact in the remainder of our exposition with no explicit mention. A weakly compatible set of terms is not, in general, strongly compatible.

Example 4.1 Both t = first(0, x) and t′ = first(s(x), y :: z) terms are strongly compatible w.r.t. μ_{t} and μ_{t′}, respectively. Thus, the set T = {t, t′} is weakly compatible. However, the set T is not strongly compatible w.r.t. μ_{t} ⊔ μ_{t′}.

Weak compatibility is a modular property (i.e., given T, S ⊆ T (Σ, V), wcomp(T ∪ S) ⇔ wcomp(T) ∧ wcomp(T)), but scomp is not. We also have the following:

Proposition 4.2 Let T ⊆ T (Σ, V) and μ_{T} = ⊔_{t∈T} μ_{t}. Then scomp_{μ_{T}} (T) iff wcomp(T) and for all t, t′ ∈ T μ_{t}↓_{Δ}= μ_{t′}↓_{Δ} where Δ = Σ(t) ∩ Σ(t′).

This proposition gives us a criterion to know whether a weakly compatible set of terms is strongly compatible. Note that, in Example 4.1, μ_{t}↓_{Δ}≠ μ_{t′}↓_{Δ}, where Δ = Σ(t) ∩ Σ(t′) = {first}, because μ_{t}(first) = {1} and μ_{t′}(first) = {1, 2}.

Definition 4.3 (Weakly and strongly replacing-independent TRSs) Let R = (Σ, R) be a TRS. R is weakly (strongly) replacing-independent if L(R) is a weakly (strongly) compatible set of terms.

If R is strongly replacing-independent, it is so w.r.t. μ_{R}^{com}. This is the intended replacement map when dealing with strongly replacing-independent TRSs. The TRS in Example 3.2 is strongly replacing-independent.

Theorem 4.4 ([7]) Let R be an orthogonal, strongly replacing-independent TRS. Let t be a term. Then O_{R}^{μ_{R}^{com}}(t) is a set of needed redexes.

This theorem motivates our interest in strongly replacing-independent TRSs: we can only perform needed μ_{R}^{com}-reductions when we work with this class of TRSs.

To transfom a TRS into a strongly replacing-independent TRS, first we obtain a weakly replacing-independent TRS (transformation W). From this one, we obtain a strongly replacing-independent TRS (transformation S).

4.1 From TRSs to weakly replacing-independent TRSs

If t is not strongly compatible, there is a μ_{t}-replacing variable occurrence v.i ∈ O_{V}^{μ_{t}}(t) which is the i-th argument of a function symbol f ∈ Σ(t). By definition of μ_{t}, there exists a replacing argument of f which is not a variable at an occurrence u.i ∈ O_{Σ}^{μ_{t}}(t). We say that u.i is a disagreeing occurrence in t. Denote as D_{t} the set of disagreeing occurrences of subterms in a term t: D_{t} = {u.i ∈ O_{Σ}^{μ_{t}}(t) | t = C[f(t̃)]_{u} ∧ (∃v.i ∈ O_{V}^{μ_{t}}(t). t = C′[f(s̃)]_{v})}. To eliminate i from μ_{t}(f), we need to remove such disagreeing occurrences. Let C_{D}^{t} be the occurrences of strongly compatible subterms in t: C_{D}^{t} = {u ∈ O(t) | t|_{u} is strongly compatible}. We remove strongly compatible (proper) subterms containing disagreeing occurrences: U_{D}^{t} is the set of occurrences of maximal strongly compatible subterms in a term t which contain the disagreeing occurrences. U_{D}^{t} = (maximal(D_{t})↓ ∩ minimal(C_{D}^{t}))\{ϵ}. Note that, if t is strongly compatible, then minimal(C_{D}^{t}) = {ϵ} and therefore U_{D}^{t} = Ø.

If t is a lhs of a rule of a TRS, this elimination will change the matchings in the rewriting process. In order to keep the semantics of the TRS, new function symbols match gather the removed subterms to complete the delayed matching.

Definition 4.5 (Transformation W) Let R = (Σ, R) be a TRS. The TRS W(R) = (Σ ⊎ M, R′) is: R′ = ∪_{l→r∈R}w(l → r), where

w(l → r) =

       if U_{D}^{l} = Ø then {l → r} else

let u_{D} ∈ U_{D}^{l}

           X ∉ V ar(l) be a fresh variable

{y_{1}, …, y_{p}} = V ar(l[ ]_{u_{D}}), and

           match ∈ M be a new p + 1-ary function symbol

in {match(l|_{u_{D}}, y_{1}, …, y_{p}) → r} ∪ w(l[X]_{u_{D}} → match(X, y_{1}, …, y_{p}))

Example 4.6 Let us consider the following TRS R:

f(c(d(x)), d(c(y))) → x f(c(x), f(y, c(b))) → y

We apply w to each rule. For l = f(c(d(x)), d(c(x))), we have D_{l} = {1.1, 2.1}, minimal(C_{D}^{l}) = {1, 2} and U_{D}^{l} = {1, 2}. We choose u_{D} = 1 and we get:

   f(X, d(c(y))) → match(X, y) match(c(d(x)), y) → x

Each lhs is strongly compatible now. For l′ = f(c(x), f(y, c(b))), we have: D_{l′} = {1, 2.2.1}, minimal(C_{D}^{l′}) = {1, 2} and U_{D}^{l′} = {1, 2}. Choosing u_{D} = 1, we get

   f(X, f(y, c(b))) → match′(X, y) match′(c(x), y) → y

Theorem 4.7 Let R be a TRS. Then W(R) is a weakly replacing-independent TRS. If R is weakly replacing-independent, then W(R) = R.

Theorem 4.8 (Correctness and completeness) Let R = (Σ, R) be a TRS, and W(R) = (Σ ⊎ M, R′). Let t, s ∈ T (Σ, V). Then, t →_{R}^{∗} s iff t →_{W(R)}^{∗} s.

In general, W does not preserve orthogonality or confluence of the original TRS but only left-linearity. For instance, W(R) in Example 4.6 is orthogonal. However, in the second step of Example 4.6, we could choose u_{D} = 2 instead of u_{D} = 1. Thus we obtain the following non-orthogonal weakly replacingindependent TRS:

   f(X, d(c(y))) → match(X, y) match(c(d(x)), y) → x
   f(c(x), X) → match′(X, x)  match′(f(y, c(b)), x) → y

Therefore, we must check for confluence of W(R) (by using the standard methods) in order to make a practic use of the transformation.

4.2 From weakly to strongly replacing independent TRSs

W solves disagreements inside each lhs. In order to make a TRS strongly replacingindependent, we need to eliminate disagreements among lhs’s of different rules.

Example 4.9 Let us consider the weakly replacing-independent TRS R:

   first(0, x) → []
   first(s(x), y :: z) → y :: first(x, z)

The lhs’s l = first(0, x) and l′ = first(s(x), y :: z) of R do not conform a strongly compatible set of terms (see Example 4.1). By Proposition 4.2, this is because of μ_{l}(first) = {1} and μ_{l′}(first) = {1, 2}. In order to convert {l, l′} into a strongly compatible set of terms, we must eliminate the subterm y :: z from l′ and to replace it by a fresh variable X. In this way, we obtain {first(0, x), first(s(x), X)} which is a strongly compatible set.

We need to keep the semantics of the original TRS unchanged. We add a new symbol match which is intended to perform the matching of the second argument with the pattern x :: y. We obtain the strongly replacing-independent TRS R′:

   first(0, x) → []  match(y :: z, x) → y :: first(x, z)

   first(s(x), X) → match(X, x)

We generalize this procedure. Let us consider a TRS R = (Σ, R), and l ∈ L(R) in the following definitions:

– D_{l} = {l′ ∈ L(R) | μ_{l}↓_{Δ}≠ μ_{l′}↓_{Δ} where Δ = Σ(l) ∩ Σ(l′)}

– Σ_{D}(l) = {f ∈ Σ(l) | ∃l′ ∈ D_{l}.f ∈ Σ(l′) ∧ μ_{l}(f) ≠ μ_{l′}(f)}

– For all f ∈ Σ(l), D_{l}^{f} = {l′ ∈ D_{l} | f ∈ Σ(l′)}

– For all f ∈ Σ_{D}(l), μ_{D}^{l}(f) = ∪_{l′∈D_{l}^{f}} μ_{l}(f)\μ_{l′}(f)

– U_{D}^{l} = {u.i ∈ O_{Σ}^{μ_{l}}(l) | l = C[f(t̃)]_{u} ∧ f ∈ Σ_{D}(l) ∧ i ∈ μ_{D}^{l}(f)}

– U_{D}^{R} = {U_{D}^{l} | l → r ∈ R}

Roughly speaking, U_{D}^{l} is the set of occurrences of subterms in l which should be removed from l in order to eliminate all disagreements introduced by l in L(R). They are said positive disagreements of l, because by removing subterms from l itself, we can eliminate them.

Definition 4.10 (Transformation S) Let R = (Σ, R) be a weakly replacingindependent TRS. The TRS S(R) = (Σ ∪ M, R′) is: R′ = S_{0}(R, U_{D}^{R}) where S_{0}(Ø, X) = Ø, S_{0}({l → r} ∪ R, {U_{D}^{l}} ∪ U_{D}^{R}) = s(l → r, U_{D}^{l}) ∪ S_{0}(R, U_{D}^{R}) and

s(l → r, U_{D}^{l}) =

       if U_{D}^{l} = Ø then {l → r} else

let W = maximal(U_{D}^{l}) = {v_{1}, …, v_{m}}

           X_{1}, . . . , X_{m} be fresh, distinct variables

Y = {y_{1}, …, y_{p}} = V ar(l[ ]_{v_{1}} ⋯ [ ]_{v_{m}}), and

           match ∈ M be a new m + p-ary function symbol

in {match(l|_{v_{1}}, …, l|_{v_{m}}, y_{1}, …, y_{p}) → r} ∪ s(l[X_{1}]_{v_{1}} ⋯ [X_{m}]_{v_{m}} → match(X_{1}, …, X_{m}, y_{1}, …, y_{p}), U_{D}^{l}\ W)

Example 4.11 Let us consider the following weakly replacing-independent TRS: g(a, x, f(a, b)) → b f(x, g(x, c, d)) → a

As we can see, l = g(a, x, f(a, b)) has a positive (g-)disagreement and (f-)disagreement with l′ = f(x, g(x, c, d)) and l′ has a positive (g)-disagreement with l. We have:

D_{l} = {l′}, Σ_{D}(l) = {f, g}, μ_{D}^{l} = μ_{l}\μ_{l′} = ⟨{1, 2}, {1, 3}⟩\⟨{2}, {2, 3}⟩ = ⟨{1}, {1}⟩, U_{D}^{l} = {1, 3.1}.

Also D_{l′} = {l}, Σ_{D}^{l′} = {f, g}, μ_{D}^{l′} = μ_{l′}\μ_{l} = ⟨{2}, {2, 3}⟩\⟨{1, 2}, {1, 3}⟩ = ⟨Ø, {2}⟩, U_{D}^{l′} = {2.2}. Thus for l, we get W = U_{D}^{l}, Y = {x}, match is a 3-ary symbol, and

s(l, U_{D}^{l}) = {g(X, x, f(Y, b)) → match(X, Y, x), match(a, a, x) → b}. For l′, W = U_{D}^{l′}, Y = {x}, match′ is a 2-ary symbol, and

s(l′, U_{D}^{l′}) = {f(x, g(x, X, d)) → match′(X, x), match′(c, x) → a}. Thus, S(R) is:

   g(X, x, f(Y, b)) → match(X, Y, x) match(a, a, x) → b
   f(x, g(x, X, d)) → match′(X, x)  match′(c, x) → a

Theorem 4.12 If R is a weakly replacing-independent TRS, then S(R) is strongly replacing-independent. If R is strongly replacing-independent, then S(R) = R.

S can fail if the input TRS is not weakly replacing-independent.

Example 4.13 Let us consider R in Example 4.6. Note that Δ = Σ(l)∩Σ(l′) = {c, f} and μ_{l}↓_{Δ}= ⟨{1}, {1, 2}⟩ = μ_{l′}↓_{Δ}. Therefore, D_{l} = D_{l′} = Ø, hence U_{D}^{l} = U_{D}^{l′} = Ø and S(R) = R, but R is not strongly replacing-independent.

Theorem 4.14 (Correctness and completeness) Let R = (Σ, R) be a weakly replacing-independent TRS, and S(R) = (Σ ⊎ M, R′). Let t, s ∈ T (Σ, V). Then, t →_{R}^{∗} s iff t →_{S(R)}^{∗} s.

S preserves left-linearity. S preserved non-overlaps in Examples 4.9 and 4.11. Unfortunately, in general, S does not preserve either orthogonality or confluence.

Example 4.15 The orthogonal, weakly replacing-independent TRS R:

   h(x, b, c) → x ; h(a, x, b) → x ; h(b, c, x) → x

is transformed into S(R):

   h(x, X, Y) → match(X, Y, x)  match(b, c, x) → x
   h(X, x, Y) → match′(X, Y, x)  match′(a, b, x) → x
   h(X, Y, x) → match′′(X, Y, x) match′′(b, c, x) → x

which is not orthogonal. It is not confluent, since h(a, b, c) →_{S(R)}^{∗} a, but also h(a, b, c) →_{S(R)}^{∗} match′(a, c, b) and h(a, b, c) →_{S(R)}^{∗} match′′(a, b, c).

Therefore, we should also test confluence of S(R) (using any standard method) to safely use it. W and S could be combined: Let R be as in Example 4.6. S(W(R)) is:

f(X, d(Y)) → match′′(Y, X)  f(X, f(y, c(Y))) → match′′′(Y, X, y)

   match(c(X), y) → match^{iv}(X, y) match′(c(x), y) → y
   match′′(c(y), X) → match(X, y)  match′′′(b, X, y) → match′(X, y)
   match^{iv}(d(x), y) → x

which is an orthogonal TRS. Therefore, the previous results ensure that S(W(R)) is equivalent to R, but we can perform optimal reductions by using the canonical replacement map because it is a strongly replacing-independent TRS.

5 Program transformation for complete evaluations

Regarding normalization of terms, if we restrict ourselves to values, csr is powerful enough to compute them. Given a set B ⊆ C, the replacement map μ_{R}^{B} is μ_{R}^{B} = μ_{R}^{com} ⊔ μ_{B}, where μ_{B}(c) = IN_{ar(c)}^{+} for all c ∈ B and μ_{B}(f) = Ø if f ∉ B.

Theorem 5.1 ([5]) Let R = (Σ, R) = (C ⊎ F, R) be a left-linear TRS, B ⊆ C and μ be a Σ-map such that μ_{R}^{B} ⊑ μ. Let t ∈ T (Σ, V), and δ ∈ T (B, V). Then t →^{∗} δ iff t ↪^{∗} δ.

By taking μ_{R}^{com} as given in Example 3.2, and B = {0, s}, then μ_{R}^{B}(s) = {1} (recall that μ_{R}^{com}(s) = Ø). We continue the head-evaluation of Example 3.5,

s(s(\underline{dbl(0)})) ↪ s(s(0)) to get the complete evaluation. The non-terminating or useless computations which could start in the steps (∗) and (∗∗) in Example 3.5 are still avoided, because μ_{R}^{B}(::) = Ø. Moreover, by using the results in [12] we can prove that R is μ_{R}^{B}-terminating. Unfortunately, we cannot ensure optimality of the μ_{R}^{B}- derivation, since μ_{R}^{com} ⊏ μ_{R}^{B} and Theorem 4.4 does not apply. More problematic situations arise.

Example 5.2 Let us consider t = indx(s(0) :: [], dbls(from(0))). By using R in Example 3.2, we can head-evaluate t under μ_{R}^{com}:

   indx(s(0) :: [], dbls(from(0)))
       ↪ sel(s(0), dbls(from(0))) :: indx([], dbls(from(0)))

If we want to compute the value of t, we take B = {0, s, [],::}. Hence, μ_{R}^{B}(s) = {1} and μ_{R}^{B}(::) = {1, 2}. This allows us to continue until the end:

   sel(s(0), dbls(from(0))) :: \underline{indx([], dbls(from(0)))}
       ↪ sel(s(0), dbls(\underline{from(0)})) :: []

↪ sel(s(0), \underline{dbls(0 :: from(s(0)))}) :: []  (∗)
↪ \underline{sel(s(0), dbl(0) :: dbls(from(s(0))))} :: []  (∗∗)

       ↪ sel(0, dbls(\underline{from(s(0))})) :: []

↪ sel(0, \underline{dbls(s(0) :: from(s(s(0))))}) :: []  (∗)
↪ \underline{sel(0, dbl(s(0)) :: dbls(from(s(s(0)))))} :: []
↪ \underline{dbl(s(0))} :: []
↪ s(s(\underline{dbl(0)})) :: []
↪ s(s(0)) :: []

However, R is not μ_{R}^{B}-terminating now: Since μ_{R}^{B}(::) = {1, 2}, the repeated application of a from-rule in the (∗) terms goes into a loop. Optimality of derivations is also compromised: we could perform an unbound number of (useless) reductions for the redex double(0) in (∗∗) which are not needed.

The unpleasant situation sketched in Example 5.2 is solved by giving a new program transformation.

5.1 The transformation V

If we deal with typed TRSs, Theorem 5.1 is very easy to use, since, given a term t = f(t̃), we are able to establish the maximal set of constructors B ⊆ C which should be considered. In this section we assume the existence of some valid type system [9]. Basic types are denoted as nat, bool, etc. Symbols f ∈ Σ are typed by: f : τ_{1} × … × τ_{k} → τ. The type of f is type(f) = τ. Types of arguments of f are gathered in typearg(f) = {τ_{1}, …, τ_{k}}. Variables x ∈ V also have a type, type(x). We also assume that all terms are well typed everywhere. The type of a term t is the type of its outermost symbol.

We need to isolate the replacement restrictions which are needed to perform the head-evaluation of an operation rooted term t = f(t̃) for some f ∈ F from the restrictions which are needed to allow them within a constructor context C[ ] ∈ T (B, V) for some B ⊆ C. Below the outermost defined symbols, reductions should be performed only up to head-evaluation. To deal with this task, we introduce the following notations:

– outer_{F}(t) = {root(t|_{u}) ∈ F | ∀ v < u. root(t|_{v}) ∉ F} is the set of outermost defined symbols in t.

– V ar_{B}(t) = {x ∈ V ar(t) | ∃u ∈ O(t). t|_{u} = x ∧ ∀ v < u. root(t|_{v}) ∈ B} is the set of B-variables, i.e., variables of t having a maximal proper prefix which only points to symbols in B. We also define B_{τ} = {c ∈ B | type(c) = τ}.

– The set of possible types for outermost defined functions arising by instantiation of a variable x is T ype_{B}(type(x)) where

T ype_{B}(τ) = \{τ\} ∪ ⋃ \begin{matrix}c ∈ B_{τ} \\ τ′ ∈ typearg(c) \end{matrix} T ype_{B}(τ′)

– Vouter_{B}(t) = ⋃_{x∈V ar_{B}(t)}{f ∈ F | type(f) ∈ T ype_{B}(type(x))} are the defined symbols which can become outermost by instantiating B-variables of t.

Example 5.3 Let us consider the TRS in Example 3.2. We calculate Vouter_{B}(x). Let type(x) = nat and B = {0, s}. Since T ype_{B}(type(x)) = {nat}∪T ype_{B}(nat) = {nat}, we have V outer_{B}(x) = {dbl, sel}.

Given a TRS R = (Σ, R) = (F ⊎ C, R), B ⊆ C and f ∈ F, outrhs_{R}(f) ⊆ F contains the outermost defined symbols in rhs’s of the f-rules: outrhs_{R}(f) = ∪_{f(l̃)→r∈R}outer_{F}(r). Now Vrhs(f) ⊆ F is the set of outermost defined symbols which can appear by instantiation of B-variables in rhs’s of the f-rules: Vrhs(f) = ∪_{f(l̃)→r∈R}V outer_{B}(r). If F_{R} : P(F) → P(F) is:

F_{R}(F) = F ∪ ⋃_{g∈F} F_{R}(outrhs_{R}(g)) ∪ ⋃_{g∈F} F_{R}(Vrhs(g)).

the set F_{R}^{f} = F_{R}({f}) contains the defined symbols which can turn outermost when a f-rooted (well typed) term f(t̃) is rewritten.

Example 5.4 Given R in Example 3.2, let us obtain F_{R}^{sel} and F_{R}^{indx}.

– We have that outrhs_{R}(sel) = {sel} and Vrhs(sel) = {sel, dbl}. Thus, F_{R}^{sel} = F_{R}({sel}) = {sel} ∪ F_{R}({sel}) ∪ F_{R}({dbl}) = {sel, dbl}.

– outrhs_{R}(indx) = {sel, indx} and Vrhs(indx) = Ø. Thus,

   F_{R}^{indx} = F_{R}({indx}) = {indx} ∪ F_{R}({sel}) = {indx, sel, dbl}.

The formal treatment of the transformation which we are going to introduce becomes simpler, if we do not look for the least increment of the number of rules of the TRS. For instance, by introducing new rules f′(l̃) → r′ to deal with each defined symbol f′ which stands for the outermost version of a symbol f ∈ F, the definition of the transformation would be easier, but we also get undesirable consequences. For example, in the evaluation of t = indx(s(0) :: [], dbls(from(0))) as given in Example 5.2, the symbol from does not become outermost. Thus, we do not need the rule:

from′(x) → T̄(x) ::′ from′(s(x)) (the meaning of T̄ is explained below) which introduces non-termination, because we need that ::′ (the ‘outermost’ version of ::) be replacing in both its first and second arguments in order to obtain completeness in evaluations. However, this rule does not add computational power to the transformation, because from′ will never arise in the evaluation. For this reason, we perform a more accurated analysis of the required additional rules. We define now the program transformation. First, we give the new signature.

Definition 5.5 Given a TRS R = (Σ, R) = (C ⊎ F, R), f ∈ F and B ⊆ C, Σ_{B}^{f} = Σ ⊎ F′ ⊎ B′, where: c′ ∈ B′ ⇔ c ∈ B ∧ ar(c′) = ar(c) and g′ ∈ F′ ⇔ g ∈ F_{R}^{f} ∧ ar(g′) = ar(g). c′ represents the constructors above the outermost applications of defined symbols. g′ represents outermost applications of g ∈ F_{R}^{f}.

The (partial) function τ_{B}^{f} transforms terms in T (Σ, V) into terms in T (Σ_{B}^{f}, V): τ_{B}^{f}(x) = x, τ_{B}^{f}(g(t̃)) = g′(t̃) if g ∈ F_{R}^{f}. Finally, τ_{B}^{f}(c(t̃)) = c′(τ_{B}^{f}(t̃)) if c ∈ B. τ_{B}^{f} is only defined on a subset ev_{B}^{f}(Σ, V) of terms which is given as follows:

V ⊆ ev_{B}^{f}(Σ, V), g(t̃) ∈ ev_{B}^{f}(Σ, V) if g ∈ F_{R}^{f} and c(t̃) ∈ ev_{B}^{f}(Σ, V) if c ∈ B and t_{1}, …, t_{ar(c)} ∈ ev_{B}^{f}(Σ, V). If we do not require V ⊆ ev_{B}^{f}(Σ, V), then we are defining the set gev_{B}^{f}(Σ, V). Note that, if t can be evaluated to a value δ ∈ T (B, V) (δ ∈ T (B)), then t ∈ ev_{B}^{f}(Σ, V) (t ∈ gev_{B}^{f}(Σ, V)).

The transformation introduces rules to deal with our differentiation of symbols. Rules for outermost defined symbols f′ ∈ F′ introduce new outermost constructors c′ ∈ B′ and outermost defined symbols f′ ∈ F′. Rules for inner defined symbols f ∈ F are exactly the original ones of the TRS.

Definition 5.6 (Transformation V) Let R = (Σ, R) = (C ⊎ F, R) be a TRS, f ∈ F and B ⊆ C. Then V_{B}^{f}(R) = (Σ_{B}^{f} ⊎ {T̄}, R ∪ S_{B} ∪ T_{B}), where:

– T̄ with ar(T̄) = 1 is a fresh, defined symbol whose rules perform the renaming of external constructors c ∈ B to constructors c′ ∈ B′ and outermost application of g ∈ F_{B}^{f} to outermost applications of the corresponding g′ ∈ F′.

– S_{B} = {g′(l̃) → κ_{B}^{f}(r) | g(l̃) → r ∈ R ∧ g ∈ F_{R}^{f} ∧ r ∈ ev_{B}^{f}(Σ, V)}, where

κ_{B}^{f}(x) = T̄(x), κ_{B}^{f}(g(t̃)) = g′(t̃) if g ∈ F_{R}^{f}, and κ_{B}^{f}(c(t̃)) = c′(κ_{B}^{f}(t̃)) if c ∈ B.

\begin{aligned}T_{B} = & \{T̄(c(x_{1}, …, x_{k})) → c′(T̄(x_{1}), …, T̄(x_{k})) | c ∈ B\} ∪ \\ & \{T̄(g(x_{1}, …, x_{k})) → g′(x_{1}, …, x_{k}) | g ∈ F_{R}^{f}\} \end{aligned}

To simplify the notation, we usually write V instead of V_{B}^{f}, when f and B are clear from the context. The following examples illustrate our transformation.

Example 5.7 If we take f = sel and B = {0, s} ⊆ {0, s, [],::} = C, the additional rules for the evaluation of t = sel(Num, ListNum) are:

   dbl′(0) → 0′  sel′(0, x :: y) → x

dbl′(s(x)) → s′(s′(dbl′(x))) sel′(s(x), y :: z) → sel′(x, z)

   T̄(0) → 0′  T̄(dbl(x)) → dbl′(x)

T̄(s(x)) → s′(T̄(x))  T̄(sel(x, y)) → sel′(x, y)

Example 5.8 If we take f = indx and B = {0, s, [],::} = C, the additional rules for the evaluation of t = indx(ListNum, ListNum) are:

dbl′(0) → 0′  indx′([], x) → []′
dbl′(s(x)) → s′(s′(dbl′(x))) indx′(x :: y, z) → sel′(x, z) ::′ indx′(y, z)

   sel′(0, x :: y) → x

sel′(s(x), y :: z) → sel′(x, z)

   T̄(0) → 0′  T̄(dbl(x)) → dbl′(x)

T̄(s(x)) → s′(T̄(x))  T̄(indx(x, y)) → indx′(x, y)
T̄([]) → []′  T̄(sel(x, y)) → sel′(x, y)

T̄(x :: y) → T̄(x) ::′ T̄(y)

Given a Σ-map μ, we define the replacement map μ′ which is used in the transformed TRS V(R) to obtain complete evaluations (leading to values) provided that μ is complete for head-evaluations. To obtain it we use a function.

Definition 5.9 Let R = (Σ, R) = (C ⊎ F, R) be a TRS, f ∈ F, and B ⊆ C. Let μ be a Σ-map. The function rmap_{B}^{f} : M_{Σ} → M_{Σ_{B}^{f}⊎{T̄}} is given by: rmap_{B}^{f}(μ) =

μ ⊔ μ′ ⊔ μ_{B′}, where μ′(g′) = μ(g) for all g ∈ F_{R}^{f} and μ′(g) = Ø for any other symbol. μ_{B′}(c′) = IN_{ar(c′)}^{+} for all c′ ∈ B′, and μ_{B′}(g) = Ø for any other symbol.

Note that, if μ′ = rmap_{B}^{f}(μ), then μ′(T̄) = Ø.

Example 5.10 Let us consider the TRS R in Example 3.2. If f = indx, B = {0, s, [],::}, and μ′ = rmap_{B}^{f}(μ_{R}^{com}), then μ′(s) = μ′(::) = μ′(from) = μ′(T̄) = Ø, μ′(s′) = μ′(dbl) = μ′(dbl′) = μ′(dbls) = μ′(indx) = μ′(indx′) = {1}, μ′(::′) = μ′(sel) = μ′(sel′) = {1, 2}.

We have that μ-replacing redex occurrences of t are exactly the same than rmap_{B}^{f}(μ)-replacing redex occurrences (w.r.t. V(R)) of τ_{B}^{f}(t). Thus, rmap_{B}^{f}(μ) computes below an outermost defined symbol exactly in the same degree than μ does. Thus, we avoid useless computations.

Proposition 5.11 Let R = (Σ, R) = (F ⊎ C, R) be a TRS, f ∈ F and B ⊆ C. Let t = C[t_{1}, …, t_{n}] ∈ T (Σ, V), u_{1}, …, u_{n} ∈ O(t) be such that C[x_{1}, …, x_{n}] ∈ T (B, V) and root(t_{i}) ∈ F_{R}^{f}, t_{i} = t|_{u_{i}} for 1 ≤ i ≤ n. Let μ be a Σ-map and μ′ = rmap_{B}^{f}(μ). Then, O_{V(R)}^{μ′}(τ_{B}^{f}(t)) = ∪_{1≤i≤n}u_{i}.O_{R}^{μ}(t_{i}).

If R is an orthogonal strongly replacing-independent TRS, computations in V(R) using rmap_{B}^{f}(μ_{R}^{com}) are needed as long as computations in R using μ_{R}^{com} are.

To utilize V(R) in evaluating a term f(t̃), we can directly evaluate T̄(f(t̃)). V preserves confluence of R (but not orthogonality) when evaluating a term t = f(t̃) for which V was defined. Thus, we can apply the rules careless: no undesired reduction sequence will arise.

Example 5.12 Let us consider the TRS R in Example 3.2. Let f = indx and B = {0, s, [],::}. Let μ′ = rmap_{B}^{f}(μ_{R}^{com}) (see Example 5.10). By using V(R) (see Example 5.8) and μ′, we have:

   T̄(indx(s(0) :: [], dbls(from(0))))
       ↪ \underline{indx′(s(0) :: [], dbls(from(0)))}

       ↪ sel′(s(0), dbls(from(0))) ::′ \underline{indx′([], dbls(from(0)))}

↪ sel′(s(0), dbls(\underline{from(0)})) ::′ []′
↪ sel′(s(0), \underline{dbls(0 :: from(s(0)))}) ::′ []′  (∗)
↪ \underline{sel′(s(0), dbl(0) :: dbls(from(s(0))))} ::′ []′  (∗∗)
↪ sel′(0, dbls(\underline{from(s(0))})) ::′ []′
↪ sel′(0, \underline{dbls(s(0) :: from(s(s(0))))}) ::′ []′  (∗)
↪ \underline{sel′(0, dbl(s(0)) :: dbls(from(s(s(0)))))} ::′ []′
↪ \underline{T̄(dbl(s(0)))} ::′ []′
↪ \underline{dbl′(s(0))} ::′ []′
↪ s′(s′(\underline{dbl′(0)})) ::′ []′
↪ s′(s′(0′)) ::′ []′

Note that, from (∗) and (∗∗), no harmful or wasteful computations can be initiated. The cs-derivation does really behave as being essentially guided by μ_{R}^{com} (Proposition 5.11). Thus, neededness of computations is preserved.

Theorem 5.13 (Correctness and completeness) Let R = (Σ, R) = (C ⊎ F, R) be a left-linear TRS. Let f ∈ F, B ⊆ C, t = f(t̃) ∈ T (Σ, V), and δ ∈ T (B). Let R′ = V(R). Let μ be a Σ-map such that μ_{R}^{com} ⊑ μ, and μ′ = rmap_{B}^{f}(μ). Then t →_{R}^{∗} δ iff τ_{B}^{f}(t) ↪_{R′(μ′)}^{∗} τ_{B}^{f}(δ).

6 Conclusions and future work

We have introduced the class of weakly replacing-independent TRSs, a superclass of strongly replacing-independent TRSs which covers many usual functional programs. The transformation W yields a weakly replacing-independent TRS from an arbitrary TRS. S produces a strongly replacing-independent TRS from a weakly replacing-independent TRS. This allows us to eventually obtain benefit from the nice properties of strongly replacing-independent TRSs. In particular, neededness of computations when using orthogonal strongly replacingindependent TRSs. The transformations have been proven both correct and complete, but orthogonality is not preserved, in general.

We have also defined a program transformation V which allows us to raise the good properties of csr concerning head-evaluations to complete evaluations. In [3] we found a transformation to achieve lazy evaluations in a transformed TRS by using eager rewriting. This transformation is more complex than our V transformation. In the worst case for that transformation, it adds 3+n r+n 2^{l} + 2 s rules to the original TRS R = (Σ, R) (see [3]), where n is the number of rules in R, s is the number of symbols in Σ, r is the maximal number of nonvariable nonreplacing occurrences in the rhs’s of the TRS, and l is the maximal number of nonvariable nonreplacing occurrences^{3} in the lhs’s in R. The transformation V only introduces n + s new rules in the worst case. This is because we obtain advantages in compiling to csr instead of rewriting as in [3]. However, a more detailed comparison of time complexity (to obtain the transformed TRS) would be required for a fair comparison.

Strongly replacing-independent TRSs have some links with the path sequential TRSs of Sekar et al. in [10]. The strict prefix sprefix_{t}(u) of an occurrence u in a term t is the chain of symbols laying in occurrences v < u. Roughly speaking, a constructor-based TRS R is path sequential if, for all l, l′ ∈ L(R), and u ∈ O(l) ∩ O(l′) such that sprefix_{l}(u) = sprefix_{l′}(u), u ∈ O_{Σ}(l) iff u ∈ O_{Σ}(l′). Path sequential TRSs are a particular class of strongly sequential TRSs [2, 10]. It is not difficult to see that constructor-based strongly replacing-independent TRSs are path sequential. However, computations with strongly replacing-independent TRSs are simpler. In [10], a method to transform a constructor-based strongly sequential TRS into a path sequential TRS is given. Our transformations W and

3 There is an easy correspondence between the predicate Λ which is used in [3] to specify replacement restrictions and our replacement map μ. Nevertheless, lazy rewriting which is defined from Λ is quite different from csr.

S are simpler and they apply to any TRS. An interesting topic is using W and S to connect strongly sequential and strongly replacing-independent TRSs. Since our transformations do not preserve orthogonality, we are interested in giving conditions to ensure its preservation, or even to modify them to obtain this behavior. Nevertheless, after [11], orthogonality is not required to have strong sequentiality, hence normalizing strategies. Thus, the topic is also an interesting subject for further research, even for the current version of the transformations.

References

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

2. 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 J. Alan Robinson, pages 395-414 and 415-443. The MIT Press, Cambridge, MA, 1991.

3. J.F.Th. Kamperman and H.R. Walters. Lazy Rewriting and Eager Machinery. In J. Hsiang, editor, Proc. of 6th International Conference on Rewriting Techniques and Applications, RTA’95, LNCS 914:147-162, Springer-Verlag, Berlin, 1995.

4. J.W. Klop. Term Rewriting Systems. In S. Abramsky, D.M. Gabbay and T.S.E. Maibaum. Handbook of Logic in Computer Science, volume 3, pages 1-116. Oxford University Press, 1992.

5. S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1997, to appear.

6. S. Lucas. Fundamentals of context-sensitive rewriting. In M. Bartǒsek, J. Staudek and J. Wiedermann, editors, Proc. of XXII Seminar on Current Trends in Theory and Practice of Informatics, SOFSEM’95, LNCS 1012:405-412, Springer-Verlag, Berlin, 1995.

7. S. Lucas. Needed Reductions with Context-Sensitive Rewriting. In M. Hanus and K. Meinke, editors, Proc. of 6th International Conference on Algebraic and Logic Programming, ALP’97, LNCS to appear.

8. M.J. O’Donnell. Equational Logic as a Programming Language. The MIT Press, Cambridge, Massachusetts, 1985.

9. C. Reade. Elements of Functional Programming. Addison-Wesley Publishing Company, 1993.

10. R.C. Sekar, S. Pawagi and I.V. Ramakrishnan. Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient Parallel Execution. In N. Dershowitz, editor, Proc. of 3rd International Conference on Rewriting Techniques and Applications, RTA’89, LNCS 355:404-418, Springer-Verlag, Berlin, 1989.

11. Y. Toyama. Strong Sequentiality of Left-Linear Overlapping Rewrite Systems. In Proc. of 7th IEEE Symposium on Logic in Computer Science, Santa Cruz, CA, pages 274-284, 1992.

12. H. Zantema. Termination of Context-Sensitive Rewriting. In H. Comon, editor, Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97, LNCS 1232:172-186, Springer-Verlag, Berlin, 1997.

This article was processed using the L^{A}TEX macro package with LLNCS style