Efficient Strong Sequentiality Using Replacement Restrictions^{⋆}

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. Huet and Lévy defined the (orthogonal) strongly sequential term rewriting systems, for which index reduction, i.e., reduction of redexes placed at special positions called (strong) indices, is optimal and normalizing. Despite the fact that Huet and Lévy give an algorithm to compute indices for the general case, there are many proposals to define subclasses of strongly sequential rewrite systems for which this can be done more efficiently. In this paper, we show that sometimes it is possible to enlarge such classes by only introducing fixed replacement restrictions, without forcing any sensible modification of the corresponding index reduction strategy.

Keywords: functional programming, neededness, replacement restrictions, term rewriting.

1 Introduction

For orthogonal term rewriting systems (TRSs), Huet and Lévy gave a formal basis for the definition of efficient sequential strategies, i.e., reduction sequences in which only one needed redex is reduced in each step [2, 4]. The occurrences which is worthy to further explore to normalize a term are called (sequential) indices. Reduction of redexes placed at sequential indices (index reduction) is normalizing. In general, sequential indices are not computable, but Huet and Lévy define a class of orthogonal TRSs, the strongly sequential TRSs, for which this can be done. It is also decidable whether a TRS is strongly sequential.

The general algorithm to perform index reduction is rather complex, and several approximations have been developed in order to obtain more efficient, but less general methods [8, 9, 10]. A remarkable example are the left-normal TRSs (LN), a subclass of strongly sequential TRSs (SS), for which the leftmostoutermost strategy, an easily computable strategy, is indeed index reduction [8].

Context-sensitive rewriting (csr) [5] is rewriting with fixed restrictions on replacements which are completely determined by the symbols of the signature:

⋆ Work partially supported by Bancaixa (Bancaja-Europa grant) and CICYT (under grant TIC 95-0433-C03-03).

a mapping μ : Σ → P(IN) called the replacement map indicates the argument positions which can be replaced for each symbol f. The arguments of f indexed by μ(f) can be rewritten, and the others do not. The restrictions are lifted in the natural way from arguments of functions to arbitrary occurrences of terms.

Example 1.1 Let us consider the TRS R:

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

We define μ(s) = μ(::) = μ(from) = Ø and μ(first) = {1, 2}. We can perform the following context-sensitive derivation:

   first(\underline{zero}, from(0)) → \underline{first(0, from(0))} → [],

but the infinite derivation

   first(zero, \underline{from(0)}) → first(zero, 0 :: \underline{from(s(0))}) → · · ·

is avoided due to the restriction μ(::) = Ø.

In a computational system dealing with a certain subclass CL of SS, we have an index reduction strategy IF which is normalizing for the TRSs in CL. In this paper we give a general method to incorporate replacement restrictions into the TRSs of any class CL ⊆ SS. This can lead to an effective extension of the considered class CL. We show how to compute the corresponding index reduction (restricted) strategy IF^{μ} for each TRS by using the information in IF.

In Section 2, we give some preliminary definitions. In Section 3, we introduce csr. Section 4 reviews the main concepts and results about strong sequentiality. Section 5 studies the general relations between replacement restrictions and strong sequentiality. Section 6 explains how to adapt the strategies.

2 Preliminaries

We denote as V a countable set of variables and Σ denotes a signature: a set of function symbols {f, g, …}, each with a fixed arity given by a function ar : Σ → IN. By T (Σ, V), we denote the set of terms. Denote as t̃ a k-tuple t_{1}, …, t_{k} of terms where k will be clarified by the context. V ar(t) is the set of variables in t.

Terms are viewed as labelled trees in the usual way. Occurrences u, v, … are represented by chains of positive natural numbers used to address subterms of t. Occurrences are ordered by the standard prefix ordering: u ≤ v iff ∃v′ s.t. v = u.v′. Also, u ∥ v means u ≰ v and v ≰ u. We also use the total ordering ≤_{L} given by: ϵ ≤_{L} u and i.u ≤_{L} j.vv ⇔ i < j ∨ (i = j ∧ u ≤_{L} v). Denote as O(t) the set of occurrences of a term t. The occurrences of non-variable symbols in t are O_{Σ}(t), and O_{V} (t) are the variable occurrences. The subterm at occurrence u of t is t|_{u} and t[s]_{u} is the term t with the subterm at the occurrence u replaced with s. The symbol labelling the root of t is root(t) and Σ(t) = {f ∈ Σ | ∃u ∈ O(t).root(t|_{u}) = f} is the set of symbols from Σ appearing in t. We refer to any term C, which is the same as t everywhere except below u, i.e. there exists a term s such that C[s]_{u} = t (or just C[s]), 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). The left-hand side (lhs) of the rule is l and r is the right-hand side (rhs). A TRS is a pair R = (Σ, R) where R is a finite set of rewrite rules. Denote as L(R) the lhs’s of R. A TRS is left-linear if there are no multiple occurrences of a single variable in the lhs’s of the rules. Two rules l → r and l′ → r′ overlap, if there is a non-variable occurrence u ∈ O(l), a substitution σ such that σ(l|_{u}) = σ(l′). A TRS is non-ambiguous, if there are no overlapping lhs’s (trivial overlap in the same lhs is not considered). A leftlinear, non-ambiguous TRS is called orthogonal. An instance σ(l) of a lhs l of a rule is a redex. The set of redex occurrences in t is O_{R}(t) = {u ∈ O(t) | ∃l ∈ L(R) : t|_{u} = σ(l)}. We say that t rewrites to 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 ∈ R, u ∈ O(t) and substitution σ. A term t is in head-normal form (hnf) if there is no derivation t = t_{1} → t_{2} → ⋯ which reduces the root of a term t_{i} i ≥ 1.

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

3 Context-sensitive rewriting

Given a signature Σ, a mapping μ : Σ → P(IN) is a replacement map (or Σmap) if for all f ∈ Σ. μ(f) ⊆ IN_{ar(f)}^{+}. Hence, μ determines the argument positions which can be reduced for each symbol in the signature [5]. We define an ordering ⊑ on M_{Σ}, the set of all Σ-maps: μ ⊑ μ′ if for all f ∈ Σ, μ(f) ⊆ μ′(f). Then, (M_{Σ}, ⊑, μ_{⊥}, μ_{⊤}, ⊔, ⊓) is a lattice: for all f ∈ Σ, μ_{⊥}(f) = Ø, μ_{⊤}(f) = IN_{ar(f)}^{+}, (μ ⊔ μ′)(f) = μ(f) ∪ μ′(f) and (μ ⊓ μ′)(f) = μ(f) ∩ μ′(f). Hence, μ ⊑ μ′ means that μ considers less positions than μ′ for reduction.

The set of μ-replacing occurrences O^{μ}(t) is given by: O^{μ}(x) = {ϵ}, if x ∈ V and O^{μ}(f(t̃)) = {ϵ} ∪ ⋃_{i∈μ(f)} i.O^{μ}(t_{i}). The non-replacing occurrences are

Õ^{μ}(t) = O(t)\O^{μ}(t). In csr, we rewrite replacing occurrences: t μ-rewrites to s, written t ↪_{R(μ)} s (or simply ↪), if t →^{u}_{R} s and u ∈ O^{μ}(t). The set of replacing redexes is O_{R}^{μ}(t) = O_{R}(t) ∩ O^{μ}(t) and t is a μ-normal form, if O_{R}^{μ}(t) = Ø. The set of replacing variables is V ar^{μ}(t) = {x ∈ V ar(t) | ∃u ∈ O(t). t|_{u} = x}.

A term t ∈ T (Σ, V) is μ-compatible if every non variable occurrence of t is a replacing occurrence: O_{Σ}(t) ⊆ O^{μ}(t). Given a term t, the minimum Σ(t)-map μ_{t} ensuring that t is compatible is: 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 If t = first(0, x), then μ_{t}(first) = {1}. Since μ_{s(x)}(s) = Ø and μ_{y::z}(::) = Ø, for t′ = first(s(x), y :: z), we get μ_{t′}(s) = μ_{t′}(::) = Ø and μ_{t′}(first) = {1, 2}.

The canonical replacement map for R, μ_{R}^{com} = ⊔_{l∈L(R)}μ_{l}, is the minimum replacement map which makes the lhs’s of R compatible terms. For instance, μ in Example 1.1 is the canonical replacement map for the TRS R in the example.

4 Strong sequentiality

Indices point to unexplored parts of a term t which is worthy to further develop to normalize t. To represent unknown parts of t, a new constant symbol Ω is introduced. Terms in T (Σ ∪ {Ω}, V) are said Ω-terms. Denote as O_{Ω}(t) the set of occurrences of Ω in t: O_{Ω}(t) = {u ∈ O(t) | t|_{u} = Ω}. An ordering ≤ on Ω-terms is given: Ω ≤ t for all t, x ≤ x if x ∈ V, and f(t̃) ≤ f(s̃) if t_{i} ≤ s_{i} for all 1 ≤ i ≤ ar(f). Thus t ≤ s means ‘t is less defined than s’. An Ω-normal form t is s.t. O_{R}(t) = Ø and O_{Ω}(t) ≠ Ø. A redex scheme is a lhs in L(R) where all variables are replaced by Ω. Let L_{Ω}(R) be the set of redex scheme of R.

To calculate an index we use a function ω defined by means of a reduction relation →_{Ω} [4]: C[t] →_{Ω} C[Ω] if t ≠ Ω and there is l ∈ L_{Ω}(R) such that t ↑ l, i.e., there exists s ∈ T (Σ ∪ {Ω}, V), such that t ≤ s and l ≤ s. Then, →_{Ω} is confluent and terminating (see [2, 4]). Let ω(t) be the →_{Ω}-normal form of t.

Definition 4.1 ([4]) Let t ∈ T (Σ ∪ {Ω}, V) and u ∈ O_{Ω}(t). Let • be a fresh constant symbol, and t′ = t[•]_{u}. Then u is an index of t, iff ω(t′)|_{u} = •. Let us denote as I(t) the set of indices of t.

A term t is rigid if ω(t) = t, soft if ω(t) = Ω [3] and a strong hnf if ω(t) ≠ Ω.

Proposition 4.2 If t is a strong hnf, then t is a hnf.

Definition 4.3 ([3]) An orthogonal TRS is strongly sequential if every Ω-normal form has an index.

Any strategy which always reduces redexes pointed by indices is index reduction.

Theorem 4.4 ([2]) Index reduction is normalizing for orthogonal, strongly sequential TRSs.

5 Strong sequentiality and replacement restrictions

In this section, we analyze the relation between replacement restrictions given by a replacement map μ and indices of terms w.r.t. a TRS R. We consider replacing indices, I^{μ}(t) = I(t) ∩ O^{μ}(t), and non-replacing ones: Ĩ^{μ}(t) = I(t) ∩ Õ^{μ}(t).

Proposition 5.1 Let R be a TRS, and μ be such that μ_{R}^{com} ⊑ μ. Let t ∈ T (Σ ∪ {Ω}, V) be a soft term. Then Ĩ^{μ}(t) = Ø.

From Proposition 4.2, if t is not a hnf, then t is not a strong hnf. Hence t is soft. Thus, Proposition 5.1 entails that, in reductions leading to a hnf, only replacing redex occurrences must be considered, since there are no non-replacing indices.

Theorem 5.2 Let R be an orthogonal, strongly sequential TRS, and μ be such that μ_{R}^{com} ⊑ μ. Let t ∈ T (Σ ∪ {Ω}, V) be an Ω-normal form, such that O_{Ω}^{μ}(t) ≠ Ø. Then I^{μ}(t) ≠ Ø.

This result means that an index reduction strategy can be refined by including replacement restrictions without damage its index reduction nature.

5.1 The contractive transformation

Now, we connect strong sequentiality of a TRS R and strong sequentiality of a TRS R^{μ} obtained by means of a transformation called μ-contraction which we have introduced in a previous work [7]: The μ-contracted signature Σ^{μ} is defined as follows: f_{μ} ∈ Σ^{μ} ∧ ar(f_{μ}) = |μ(f)| ⇔ f ∈ Σ. Terms are related by means of a μ-contracting function τ_{μ} : T (Σ, V) → T (Σ^{μ}, V). This function drops the non-replacing immediate subterms of a term t and constructs a ‘μcontracted’ term by joining the (also transformed) replacing subterms below the corresponding operation of the μ-contracted signature: τ_{μ}(x) = x if x ∈ V, and τ_{μ}(f(t_{1}, …, t_{k})) = f_{μ}(τ_{μ}(t_{i_{1}}), …, τ_{μ}(t_{i_{p}})) if μ(f) = {i_{1}, …, i_{p}}. The i-th immediate (replacing) subterm of f in t = f(t̃) becomes the |IN_{i}^{+} ∩ μ(f)|-th immediate subterm of f_{μ} in τ_{μ}(t).

Example 5.3 Let R and μ = μ_{R}^{com} as given in Example 1.1.

Then t = first(s(x), y :: z) contracts to τ_{μ}(t) = first_{μ}(s_{μ},::_{μ}) and t′ = y :: first(x, z) contracts to τ_{μ}(t′) =::_{μ}.

Since τ_{μ} is surjective, we are allowed to consider any s ∈ T (Σ^{μ}, V) as the image by τ_{μ} of some t ∈ T (Σ, V). We write τ_{μ}(t) instead of s when s = τ_{μ}(t).

Replacing occurrences of t and occurrences of τ_{μ}(t) are related by ν_{μ,t} : O^{μ}(t) → O(τ_{μ}(t)): ν_{μ,t}(ϵ) = ϵ, and ν_{μ,f(t̃)}(i.u) = |IN_{i}^{+} ∩μ(f)|.ν_{μ,t_{i}}(u) if i ∈ μ(f). We write ν_{t} instead of ν_{μ,t} when μ is clear from the context. Note that ν_{μ,t} is a bijection, and ν_{μ,t}(O^{μ}(t)) = O(τ_{μ}(t)).

We use τ_{μ} to connect TRSs. Let R = (Σ, R) be a TRS. The μ-contraction of R is R^{μ} = (Σ^{μ}, R^{μ}), where R^{μ} = {τ_{μ}(l) → τ_{μ}(r) | l → r ∈ R}. We indicate as ρ_{μ}(l → r) the rule of R^{μ} which corresponds to a rule l → r of R. ρ_{μ} is surjective.

Example 5.4 By considering R and μ as in Example 1.1, R^{μ} is:

   zero_{μ} → 0_{μ}  first_{μ}(0_{μ}, x) → []_{μ}

from_{μ} →::_{μ}  first_{μ}(s_{μ},::_{μ}) →::_{μ}

The definition of R^{μ} only has complete sense if V ar^{μ}(r) ⊆ V ar^{μ}(l) for each l → r ∈ R. In this way, R^{μ} has no extra variables. For instance, in Example 5.4, we have obtained a valid TRS. However, if we define μ(::) = {1}, the new contraction does not yield a TRS, because we obtain extra variables. Nevertheless, concerning the results in this paper, we are independent from this circumstance.

5.2 Inducing strong sequentiality

In the following, we use J (t) to denote indices obtained using L_{Ω}(R^{μ}).

Proposition 5.5 Let R be a TRS and μ be such that μ_{R}^{com} ⊑ μ. Let t be an Ω-term. Then u ∈ I^{μ}(t) iff ν_{t}(u) ∈ J (τ_{μ}(t)), i.e., ν_{t}(I^{μ}(t)) = J (τ_{μ}(t)).

Strong sequentiality is independent from rhs’s of rules. Since τ_{μ} can introduce extra variables in the rhs’s, in order to formulate our results, we say that TRSs R = (Σ, R) and R′ = (Σ′, R′) are left-equivalent (R ∼_{l} R′) if they have the same lhs’s, i.e., R = {l_{i} → r_{i} | 1 ≤ i ≤ n} and R′ = {l_{i} → r′_{i} | 1 ≤ i ≤ n} [4].

Theorem 5.6 Let R be an orthogonal TRS. Let μ be such that μ_{R}^{com} ⊑ μ and R^{μ} is left equivalent to a strongly sequential TRS. Then R is strongly sequential.

To illustrate Theorem 5.6, we recall the notion of left-normal TRS [8, 10]: R is left-normal if, for all l ∈ L(R), the function symbols precede the variables according to ≤_{L}. Thus R in Example 1.1, is not left-normal. No easy syntactic characterization of strong sequentiality for R is available. However, R^{μ}, where μ = μ_{R}^{com}, in Example 5.4 is left-normal, hence strongly sequential. Therefore, Theorem 5.6 entails strong sequentiality of R. We give a further example.

Example 5.7 Let us consider the TRS R to manipulate prime numbers.

   from(x) → x :: from(s(x))
   primes → sieve(from(s(s(0))))
   sieve(x :: y) → x :: sieve(filter(x, y))
   filter(x, y :: z) → if(x|y, filter(x, z), y :: filter(x, z))

   sel(0, x :: y) → x          if(true, x, y) → x
   sel(s(x), y :: z) → sel(x, z) if(false, x, y) → y

Assume that | is a built-in predicate and x|y means x divides y. If we let μ = μ_{R}^{com}, then μ(s) = μ(::) = μ(from) = Ø, μ(sieve) = μ(if) = {1}, μ(filter) = {2}, μ(sel) = {1, 2}. R is not left-normal. Then R^{μ} is:

from_{μ} →::_{μ}

   primes_{μ} → sieve_{μ}(from_{μ})

sieve_{μ}(::_{μ}) →::_{μ}
filter_{μ}(::_{μ}) → if_{μ}(|_{μ})
sel_{μ}(0_{μ},::_{μ}) → x        if_{μ}(true_{μ}) → x
sel_{μ}(s_{μ},::_{μ}) → sel_{μ}(x, z) if_{μ}(false_{μ}) → y

R^{μ} is not a TRS (it has extra variables), but it is immediate to have a leftequivalent TRS S ∼_{l} R^{μ}. S must be a ground TRS (i.e., l, r ∈ T (Σ, Ø) for all rule l → r of S), since the lhs’s have no variable. Ground TRSs are left-normal, hence strongly sequential. Thus, R also is.

Theorem 5.8 Let R be an orthogonal, strongly sequential TRS. Let μ be such that μ_{R}^{com} ⊑ μ. Then, R^{μ} is left equivalent to a strongly sequential TRS.

Hence, Theorems 5.6 and 5.8 amount to saying that proving strong sequentiality in a TRS R or its μ-contraction R^{μ} is completely equivalent, whenever μ_{R}^{com} ⊑ μ.

6 Induced strategies

We have shown that it is possible to conclude strong sequentiality of R from strong sequentiality of (a TRS left-equivalent to) R^{μ}. In this section, we show how to obtain an index reduction strategy for R by using an index reduction strategy for R^{μ}.

A rewriting strategy for a TRS R = (Σ, R) is a function IF_{R} : T (Σ, V) → T (Σ, V) such that IF_{R}(t) = t if O_{R}(t) = Ø, i.e, t is a normal form, and t →_{R}^{+} IF_{R}(t) otherwise (t →_{R} IF_{R}(t) for sequential strategies) [3]. We drop the suffix R when no confusion arises. Also, we split IF into components IF = (IP, IR). The component IP : T (Σ, V) → P(IN_{>0}^{∗}) selects the redex occurrences to be reduced (a singleton for sequential strategies), and IR selects the rules which apply (see [1]). Since we only deal with orthogonal TRSs, the rule which applies to a redex is uniquely determined by the redex itself. Then, for a given IP, we get IR fixed. Hence, we do not pay more attention to IR. Then, IP and IF are related by:

IP(t) = Ø iff O_{R}(t) = Ø.

IP(t) = {u_{1}, …, u_{n}} ⊆ O_{R}(t) iff u_{i} ∥ u_{j} for 1 ≤ i < j ≤ n, t|_{u_{i}} = σ(l_{i}) for a single l_{i} → r_{i} ∈ R, 1 ≤ i ≤ n, and IF(t) = t[σ(r_{1})]_{u_{1}} ⋯ [σ(r_{n})]_{u_{n}}.

The notion of context-sensitive strategy or μ-strategy IF_{R(μ)} is analogous, but it uses ↪_{R(μ)} instead of →_{R} and O_{R}^{μ} instead of O_{R} (see [6]). However, note that, from μ-strategies, we only can expect to μ-normalize terms, rather than completely normalize them^{2}. Now, we introduce the notion of induced μ-strategy.

Definition 6.1 Let R = (Σ, R) be an orthogonal TRS and μ be such that μ_{R}^{com} ⊑ μ. Let IF = (IP, IR) be a rewriting strategy for S ∼_{l} R^{μ}. The μ-rewriting strategy IF^{μ} = (IP^{μ}, IR^{μ}) induced by IF is given by IP^{μ}(t) = ν_{t}^{−1}(IP(τ_{μ}(t))) for all t ∈ T (Σ, V). Since whenever μ_{R}^{com} ⊑ μ the μ-contraction preserves orthogonality, IR^{μ} is again fixed by IP^{μ}.

The definition of IP^{μ} should be obvious after Proposition 5.5. Now we prove that IF^{μ} in Definition 6.1 holds the expected property, i.e., it is an index reduction μstrategy for the TRS R, whenever IF is index reduction for (a TRS left-equivalent to) R^{μ}.

Theorem 6.2 Let S be an orthogonal strongly sequential TRS. Let IF be an index reduction strategy for S. Let R be a TRS and μ be such that μ_{R}^{com} ⊑ μ and R^{μ} ∼_{l} S. Then, IF^{μ} is an index reduction μ-strategy for R.

Sometimes, IP can be further decomposed as follows: IP = ÎP ∘ O_{R} where ÎP : P(IN_{>0}^{∗}) → P(IN_{>0}^{∗}) selects a set of occurrences from a non empty set of redex occurrences (ÎP(Ø) = Ø), and O_{R} : T (Σ, V) → P(IN_{>0}^{∗}) gives the redex occurrences of t. We also require ÎP(U) ⊆ U for all U ∈ P(IN_{>0}^{∗}). Some examples [3]: Leftmost-outermost (IF_{lo}): IP_{lo}(t) = {min_{≤_{L}}(minimal_{≤}(O_{R}(t)))} = {min_{≤_{L}}(O_{R}(t))}. Parallel-outermost (IF_{po}): IP_{po}(t) = minimal_{≤}(O_{R}(t)). Note that in these strategies, the question of which rule should be applied to a selected redex is left open: In orthogonal TRSs the redex fixes the rule.

The calculus of the IP^{μ} component of an induced strategy (Definition 6.1), for a given term t, proceeds by using τ_{μ} for moving to R^{μ}, next using the IP component of the original strategy and coming back to R by means of ν_{t}^{−1}. The decomposition IP = ÎP ∘ O_{R} can lead to a simplification of this procedure.

2 Nevertheless, it is easy to use μ-normalizing strategies to define normalizing procedures [6].

Proposition 6.3 Let R be an orthogonal TRS, and μ be s.t. μ_{R}^{com} ⊑ μ. Let IF = (IP, IR) be a rewriting strategy for S ∼_{l} R^{μ} and IF^{μ} = (IP^{μ}, IR^{μ}) be the induced μ-strategy for R. Let IP be such that IP = ÎP∘O_{R^{μ}}. If, for all t ∈ T (Σ, V) and U ⊆ O^{μ}(t), we have ν_{t}(ÎP(U)) = ÎP(ν_{t}(U)), then IP^{μ}(t) = ÎP(O_{R}^{μ}(t)).

The result on normalization by means of IF_{lo} can be given by showing that an orthogonal, left-normal TRS is strongly sequential and the leftmost-outermost redex occurrence min_{≤_{L}}(O_{R}(t)) of a term t is an index (O’Donnell, [8]).

We show that min_{≤_{L}} commutes with ν. This allows us to give a simpler expression of the induced leftmost-outermost strategy IF_{lo}^{μ}.

Proposition 6.4 Let t ∈ T (Σ, V). ∀U ⊆ O^{μ}(t), ν_{t}(min_{≤_{L}}(U)) = min_{≤_{L}}(ν_{t}(U)).

Therefore, from Proposition 6.4 and Proposition 6.3, the leftmost-outermost strategy IF_{lo} induces a μ-strategy IF_{lo}^{μ} for a given R and μ such that R^{μ} ∼_{l} S and S is left-normal. The calculus is nicely simple: IP_{lo}^{μ}(t) = min_{≤_{L}}(O_{R}^{μ}(t)).

Concerning Example 5.7 we have even better possibilies. Since in a ground, orthogonal TRS, every redex occurrence is an index, any strategy is index reduction. We can use ÎP = choose. Clearly, for all t, and U ⊆ O^{μ}(t), ν_{t}(choose(U)) = choose(ν_{t}(U)) (because of non-determinism). Hence IP^{μ} = choose(O_{R}^{μ}(t)).

References

1. S. Antoy and A. Middeldorp. A Sequential Reduction Strategy. Theoretical Computer Science 165:75-95, 1996.

2. G. Huet and J.J. Lévy. Computations in orthogonal term rewriting systems. In Computational logic: essays in honour of J. Alan Robinson, MIT Press, 1991.

3. J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume 3, pages 1-116. Oxford University Press, 1992.

4. J.W. Klop and A. Middeldorp. Sequentiality in Orthogonal Term Rewriting Systems. Journal of Symbolic Computation 12:161-195, 1991.

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

6. S. Lucas. Needed Reductions with Context-Sensitive Rewriting. In Proc. of ALP’97, LNCS to appear.

7. S. Lucas. Termination of Context-Sensitive Rewriting by Rewriting. In Proc. of ICALP’96, LNCS 1099:122-133, Springer-Verlag, 1996.

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

9. R.C. Sekar, S. Pawagi and I.V. Ramakrishnan. Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient Parallel Execution. In Proc. of RTA’89, LNCS 355:404-418, 1989.

10. Y. Toyama, S. Smetsers, M.C.J.D. van Eekelen and R. Plasmeijer. The Functional Strategy and Transitive Term Rewriting Systems. Term Graph Rewriting - Theory and Practice, pages 117-129, John Wiley & sons, 1993.