Root-neededness and approximations of neededness^{∗}

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

When dealing with reduction strategies for term rewriting systems, needed reduction is only adequate for defining normalizing strategies. However, Middeldorp has shown that root-needed reduction provides a suitable basis for the definition of root-normalizing, normalizing, and infinitary normalizing strategies. Since neededness and root-neededness are undecidable, some notion of approximation is necessary. In this paper, we investigate whether it is possible to approximate rootneededness by using well-known decidable approximations to neededness and sequentiality (such as strong, NV, NVNF, shallow, and growing approximations). We show that NV-sequentiality (hence strong sequentiality, a particular case of NV-sequentiality) is the most general approximation to root-neededness. We also demonstrate that NVNF-sequentiality only approximates root-neededness in terms that have a normal form. Shallow and growing approximations do not approximate root-neededness in general. As a consequence, only NV-sequentiality seems to provide a suitable general basis for the definition of infinitary normalizing strategies.

Keywords: neededness, root-neededness, sequentiality, strategies, term rewriting.

1 Introduction

Huet and Lévy’s theory of needed reductions provides a basis for the definition of normalizing strategies for orthogonal term rewriting systems (TRSs) [4]: every term which is not a normal form has a needed redex. A needed redex is a redex which is contracted (either itself or one of its descendants) in every rewrite sequence leading to a normal form. Needed reduction (the repeated contraction of needed redexes) is normalizing. However, needed reduction fails in infinitary normalization, because, by definition, every redex of a term which does not have a (finite) normal form is needed.

Example 1.1 Let us consider the TRS R [10]:

    f(x) → g(f(x))
    a → a

The term f(a) has no finite normal form. Thus, the redex a is needed; however, repeated reductions of this redex:

    f(\underline{a}) → f(\underline{a}) → · · ·

do not yield the infinite normal form g(g(g(…))). Moreover, it is not able to produce a root-stable form

of f(a) such as g(f(a)).

A root-stable term (also called a head-normal form) is a term which cannot be reduced to a redex. A term is root-normalizing if it rewrites to a root-stable term. Example 1.1 shows that needed reduction is not adequate for achieving root-normalization. A redex in a term is root-needed if the redex (itself or one of its descendants) is reduced in each rewriting sequence leading to a root-stable term. Example 1.1 shows that needed redexes do not need to be root-needed. For orthogonal TRSs, reduction of root-needed redexes is root-normalizing [10]. The notion of root-stable term and that of root-needed reduction both provide a suitable formal framework for the definition of rootnormalizing, normalizing, and infinitary normalizing reduction sequences [10].

Neededness is undecidable and it must be approximated. In order to use a given approximation in practice, it is necessary to (1) provide a method to decide whether a redex is needed and to (2) identify the class of TRSs ensuring that every reducible term has a redex for which the previous method succeeds [3]. Decidable approximations to neededness (and the related notion of sequentiality) have been extensively explored [2, 3, 4, 5, 9, 11, 12, 13]. Since rootneeededness is also undecidable [10], this paper investigates whether the previous approximations can also be used to approximate root-needednes for almost orthogonal TRSs. We demonstrate that NV-sequentiality [12] (hence strong sequentiality [4, 9, 13], a particular case of NV-sequentiality) is the most general approximation to root-neededness. We also show that NVNFsequentiality [11] safely approximates root-neededness for terms having a normal form. We show that shallowsequentiality [2] (hence growing sequentiality [5] which is a wider class) in general does not approximate rootneededness.

∗Work partially supported by Spanish CICYT (under grant TIC 95-0433-C03-03).

In Section 2, we give some preliminary definitions. In Section 3, we review the theory of root-neededness. In Section 4, we review the notion of neededness and approximation which we use in the paper. Section 5 establishes the approximations which are safe for rootneededness. Section 6 addresses the problem of defining root-normalizing and infinitary normalizing strategies. Section 7 concludes.

2 Preliminaries

Throughout the paper (full definitions in [1, 3, 8, 10]), 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 and T (Σ) is the set of ground terms, i.e., terms without occurrences of variables. If terms t, s are identical, we write t ≡ s. V ar(t) is the set of variables in t. A term is linear if it has no multiple occurrences of a single variable. A substitution is a function σ : V → T (Σ, V) which extends to terms as follows σ(f(t_{1} …, t_{k})) = f(σ(t_{1}), …, σ(t_{k})) for all f(t_{1} …, t_{k}) ∈ T (Σ, V). The set Dom(σ) = {x ∈ V | σ(x) ≢ x} is called the domain of σ. Whenever Dom(σ) ∩ Dom(σ′) = Ø, for substitutions σ, σ′, we denote by σ ∪ σ′, a substitution such that (σ ∪ σ′)(x) = σ(x) if x ∈ Dom(σ) and (σ ∪ σ′)(x) = σ′(x) if x ∈ Dom(σ′). Terms t, s unify if there is a substitution σ (called a unifier of t, s) s.t. σ(t) ≡ σ(s). A unifier σ of t, s is called a most general unifier if for each unifier σ′ of t, s, ∃σ′′ s.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. By ϵ, we denote the empty chain. Occurrences are ordered by the prefix ordering: u ≤ v iff ∃v′ s.t. v = u.v′. Also, u ∥ v means u ≰ v and v ≰ u. The set of occurrences of a term t is denoted by O(t). The subterm at occurrence u of t is denoted by t|_{u} and t[s]_{u} is the term t with t|_{u} replaced with s. The depth of a subterm t|_{u} is the length |u| of the occurrence which addresses the subterm. By O_{s}(t), we denote the set of occurrences of s in t, i.e., u ∈ O_{s}(t) iff t|_{u} = s.

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 set of rewrite rules. L(R) denotes the lhs’s of R. An instance σ(l) of a lhs l of a rule is a redex. The set of redex occurrences in t is O_{R}(t). A TRS R = (Σ, R) is (right-) left-linear if for all l → r ∈ R, (r) l is linear. A TRS is shallow if for every rewrite rule l → r, the variables in V ar(l) ∩ V ar(r) occur at depth 1 in l and at depth 0 or 1 in r. A TRS is growing if for every rewrite rule l → r, the variables in V ar(l)∩V ar(r) occur at depth 1 in l. Two (possibly renamed) rules l → r and l′ → r′ overlap, if there is a non-variable occurrence u ∈ O(l) and a most-general unifier σ such that σ(l|_{u}) = σ(l′). The pair ⟨σ(l)[σ(r′)]_{u}, σ(r)⟩ is called a critical pair and is also called an overlay if u = ϵ. A critical pair ⟨t, s⟩ is trivial if t ≡ s. A left-linear TRS without critical pairs is called orthogonal. It is called almost orthogonal if its critical pairs are trivial overlays. If it only has trivial critical pairs it is called weakly orthogonal. A term t rewrites to s (at the occurrence u), written t →^{u}_{R} s (or just t →^{u} s or t → s), if t|_{u} = σ(l) and s = t[σ(r)]_{u}, for some rule l → r ∈ R, u ∈ O(t) and substitution σ : V ar(l → r) → T (Σ, V). The one-step rewrite relation for R is →. The transitive, reflexive closure of → is →^{∗}. If t →^{∗} s, then s is a reduct of t. The inner reduction relation is →^{>ϵ} =→\→^{ϵ}. A term t is rootstable if it cannot be rewritten to a redex. A term is root-normalizing if it has a root-stable reduct. A term t is a normal form if O_{R}(t) = Ø. To emphasize, when necessary, that t is a normal form with respect to a TRS R, we will say that t is an R-normal form.

A rewriting strategy for a TRS R is a function S that assigns to every term t a set of non-empty finite rewrite sequences each beginning with t. We assume that S(t) = Ø if and only if t is a normal form. S is one-step if, for all t, every member of S(t) has length 1. We write t →_{S} s if t →^{∗} s ∈ S(t). An S-sequence is a reduction sequence of the form t_{1} →_{S} t_{2} →_{S} · · ·. S is root-normalizing if for all rootnormalizing terms t, every possible infinite S-rewrite sequence starting from t contains a root-stable term. S is normalizing if, for all terms t that have a normal form, there is no infinite S-rewrite sequence starting from t. Let quasi-S be the strategy defined by quasi-S(t) = {t →_{R}^{∗} t′ →_{S} s | t′ ∈ T (Σ, V)}, i.e., S diluted with arbitrary (finitely many) reduction steps. A strategy S is hypernormalizing if quasi-S is normalizing. S is hyper root-normalizing if quasi-S is rootnormalizing. When dealing with ground terms, we do not further develop these definitions which adapt to this particular setting in the obvious way.

3 Root-neededness

A redex Δ in a term t is root-needed, if Δ (itself or one of its descendants) is contracted in every rewrite sequence from t to a root-stable term [10]. For orthogonal TRSs, every non-root-stable term has a root-needed redex. Root-stable terms have no root-needed redex, and redexes in terms having no root-stable reduct are trivially root-needed. Root-needed redexes in maximal non-root-stable subterms are needed. However, rootneeded redexes are not necessarily outermost.

Example 3.1 Let us consider the following TRS R

g(a,x) → x
b → a

The root-normalizing derivations for g(a,b) are:

1. g(a,\underline{b}) → \underline{g(a,a)} → a, and

2. \underline{g(a,b)} → \underline{b} → a

The nonoutermost redex b is root-needed in g(a,b).

A root-necessary set of redexes is a set of redexes such that, at least one of the redexes in the set, or one of its descendants, must always be reduced in each rootnormalizing derivation.

Theorem 3.2 [10] There are no parallel rewrite sequences starting from a root-normalizing term that contain infinitely many root-necessary steps.

Example 3.3 The reduction step

\underline{f(a)} → g(f(a))

(w.r.t. R in Example 1.1) contracts a root-needed redex f(a) yielding a root-stable term g(f(a)).

4 Neededness

We follow Durand and Middeldorp’s approach [3]. In this section we consider TRSs which may have rules l → r that do not satisfy V ar(r) ⊆ V ar(l). In the remainder of the paper, we assume the existence of a constant • not appearing in Σ. We let Σ_{•} = Σ∪{•} and we view each TRS R as a TRS R = (Σ_{•}, R) over this extended signature. NF_{R} is the set of ground normal forms in T (Σ_{•}). Given a TRS R = (Σ_{•}, R), we let R_{•} = (Σ_{•}, R ∪ {• → •}). Thus, NF_{R_{•}} = NF_{R} ∩ T (Σ).

Definition 4.1 ([3]) Let R = (Σ_{•}, R) be a TRS. We say that redex Δ in C[Δ] ∈ T (Σ) is R-needed if there is no term t ∈ NF_{R_{•}} such that C[•] →_{R}^{∗} t.

For orthogonal TRSs, this notion of neededness is equivalent to the usual one (see [4]). Since neededness is not computable, it is necessary to approximate it: given TRSs R and S over the same signature, we say that S approximates R if →_{R}^{∗}⊆→_{S}^{∗} and NF_{R} = NF_{S}. S-needed redexes are R-needed. Given a TRS R, we consider four approximations: R_{s}, R_{nv}, R_{sh}, and R_{g} [3]: R_{s} is obtained by replacing the rhs of every rewrite rule in R by a variable that does not occur in the corresponding lhs. R_{nv} is obtained by replacing the variables in the rhs of every rule by pairwise distinct variables that do not occur in the corresponding lhs. R_{sh} is any right-linear shallow TRS that is obtained from R by replacing variables in the rhs of every rule by variables that do not occur in the corresponding lhs. R_{g} is any right-linear growing TRS that is obtained from R by replacing variables in the rhs of every rules by variables that do not occur in the corresponding lhs.

The class of TRSs R on a signature Σ such that every reducible term in T (Σ) has an R_{α}-needed redex is denoted by CBN-NF_{α}. For instance, CBN-NF_{s} corresponds to strongly sequential TRSs.

4.1 Sequentiality

The notion of sequentiality has also been used to define optimal rewriting strategies. We refer to [3] for a discussion on neededness versus sequentiality.

Let Ω be a new constant symbol. Terms in T (Σ ∪ {Ω}) are called Ω-terms. We let ≤ be the least ordering which satisfies Ω ≤ t for all t ∈ T (Σ) and f(t_{1}, …, t_{k}) ≤ f(t_{1}, …, t_{k}) if t_{i} ≤ s_{i} for all 1 ≤ i ≤ k. We say that t, t′ ∈ T (Σ ∪ {Ω}) are compatible (written t ↑ t′) if ∃s ∈ T (Σ ∪ {Ω}) such that t ≤ s and t′ ≤ s. Given t ∈ T (Σ, V), t_{Ω} denotes the Ω-term obtained from t by replacing all variables in t by Ω’s. Given a TRS R, t is an Ω-normal form if O_{R}(t) = Ø and O_{Ω}(t) ≠ Ø.

Sequentiality is based on the notion of index. An Ωoccurrence u ∈ O_{Ω}(t) of an Ω-term t is an index with respect to a predicate P on Ω-terms if, for every Ω-term t′ with t′ ≥ t, P (t′) implies t′|_{u} ≠ Ω. The set of indices of t with respect to P is denoted I_{P} (t). A monotonic predicate^{1} P is sequential if ∀t ∈ T (Σ∪{Ω}), whenever P (t) does not hold and there exists s such that s ≥ t and P (s) holds, it follows that I_{P} (t) ≠ Ø. A TRS R is sequential if the predicate nf_{R}(t) (which holds if and only if t has a R-normal form in T (Σ)) is sequential. The sequentiality of TRSs is undecidable and several decidable approximations have been investigated. R is strongly sequential [4, 9, 13] if R_{s} is sequential. Strong sequentiality is equivalent to R_{s}-neededness (see [3]). Strong indices can be computed by using Ω-reduction [9, 13]: t →_{Ω} s if t|_{u} ↑ l_{Ω}, t|_{u} ≠ Ω, l ∈ L(R), and s = t[Ω]_{u}. The →_{Ω}-normal form of t is denoted by ω(t). We have u ∈ I_{s}(t[Ω]_{u}) iff ω(t[•]_{u})|_{u} = •. NVNF, shallow and growing sequentiality of R correspond to R_{nv}, R_{sh}, and R_{g}-sequentiality, respectively. NVsequentiality [12] is not equivalent to R_{nv}-sequentiality or R_{nv}-neededness (see [3]) and we elaborate on it in some detail to develop our results.

1We consider False ≤ True for booleans.

Given a TRS R = (Σ, R), we write t →_{nv} s if and only if there exist u ∈ O(t) and l → r ∈ R such that t|_{u} ≥ l_{Ω} and s = t[r′]_{u} for some r′ such that r′ ≥ r_{Ω}. For left-linear TRSs, we have →_{nv}⊇→. The predicate term is defined as follows: term(t) holds if and only if there exists^{2} s ∈ T (Σ) such that t →_{nv}^{∗} s (i.e., →_{nv} succeeds in removing the Ω-occurrences from t). The set of indices in a term with respect to term is written I_{nv}(t). A TRS R is said to be NV-sequential if and only if term is sequential at every Ω-normal form [12].

Lemma 4.2 [12] Let t ∈ T (Σ ∪ {Ω}), and let u, v ∈ O(t), where u ∥ v. If u ∈ I_{nv}(t[Ω]_{v}), then u ∈ I_{nv}(t).

Lemma 4.3 [12] If u.v ∈ I_{nv}(t), then v ∈ I_{nv}(t|_{u}).

We write C[t]_{u} →_{ω} C[r_{Ω}]_{u} if t ≠ Ω and there exists l → r in R such that t ↑ l_{Ω}.

Lemma 4.4 [12] Let t ∈ T (Σ ∪ {Ω}) and u ∈ O_{Ω}(t). Then u ∉ I_{nv}(t) if and only if there exist v ∈ O(t), where v < u, and s ∈ T (Σ ∪ {Ω})\{Ω} such that t[•]_{u}|_{v} →_{ω}^{∗} s and s ↑ l_{Ω} for some l ∈ L(R).

Lemma 4.5 [12] Let t →_{nv} t′ and s ≤ t where t, t′, s ∈ T (Σ ∪ {Ω}). Then either s ≤ t′ or there exists s′ ∈ T (Σ ∪ {Ω}) such that s →_{ω} s′ and s′ ≤ t′. (This implies that ∃s′ such that s →_{ω}^{∗} s′ and s′ ≤ t′.)

Strong and NV-sequentiality are related: If u ∈ I_{s}(t[Ω]_{u}), then u ∈ I_{nv}(t[Ω]_{u}). Strongly sequential TRSs are NV-sequential. A nv-strategy is any strategy that only reduces redexes addressed by nv-indices.

5 Approximations of neededness and root-neededness

Almost orthogonal TRSs have the following property: descendants of a redex are redexes (of the same lhs) [10]. We apply this property to a specific case as follows.

Lemma 5.1 Let R be an almost orthogonal TRS and t be a term such that t = σ(l) for some l ∈ L(R). If u ∈ O_{R}(t)\{ϵ}, then, for all s, there exists σ′ such that t[s]_{u} = σ′(l).

Almost orthogonal TRSs have another interesting property: nv-indices are outermost.

Lemma 5.2 Let R be an almost orthogonal TRS and t be a term. Let u, v ∈ O_{R}(t) such that u ≠ v. If u ∈ I_{nv}(t[Ω]_{u}), then v ≰ u.

Proof. Assume v ≤ u. Since u ≠ v, we have v < u. Since t|_{v} = σ(l) for some l ∈ L(R), by Lemma 5.1, t|_{v}[•]_{u} = t[•]_{u}|_{v} = σ′(l) Therefore, t[•]_{u}|_{v} ↑ l_{Ω}. By Lemma 4.4, u ∉ I_{nv}(t[Ω]_{u}), a contradiction. □

Lemma 5.2 does not hold for weakly orthogonal TRSs.

Example 5.3 Let the weakly orthogonal TRS R be:

                                                   pred(succ(x)) → x
                                                   succ(pred(x)) → x
                                               For t = pred(succ(pred(0))) we have O_{R}(t) =

{ϵ, 1}. The outermost redex is addressed by a strong index of t[Ω]_{ϵ} (as ω(•) = •), hence by a nv-index. The nonoutermost occurrence 1 is a nv-index of t[Ω]_{1} as pred(•) is not compatible with pred(succ(Ω)).

A similar result is given for the nv-approximation R_{nv}.

Lemma 5.4 Let R = (Σ, R) be an almost orthogonal TRS and t ∈ T (Σ) be R_{nv}-normalizing. Let u, v ∈ O_{R}(t) such that u ≠ v. If t|_{u} is R_{nv}-needed, then v ≰ u.

Proof. Since t is R_{nv}-normalizing, then t →_{R_{nv}}^{∗} s for some R_{nv}-normal form s ∈ T (Σ). We proceed by induction on the length n > 0 of this derivation.

If n = 1, the only way to have such a one-step normalizing derivation is that v ≤ u and t →^{v}_{R_{nv}} s with t|_{v} = σ(l) for some l → r in R_{nv} and s = t[σ(r)]_{v}. Since V ar(l) ∩ V ar(r) = Ø (by definition of R_{nv}), we let σ = σ_{l} ∪ σ_{r} with Dom(σ_{l}) = V ar(l) and Dom(σ_{r}) = V ar(r). By Lemma 5.1, t[•]_{u}|_{v} = σ′(l) for some σ′. Without losing generality, we let σ′ = σ′_{l} ∪σ_{r}, i.e., the bindings for variables of r are the same as given by σ. Therefore, σ′(l) →_{R_{nv}} σ(r), hence t[•]_{u} = t[σ′(l)]_{v} →_{R_{nv}} t[σ(r)]_{v} = s, i.e., t|_{u} is not R_{nv}-needed, a contradiction.

2The original definition was given with respect to arbitrary terms (with variables) [12]. Since variables of input terms can also be seen as constant symbols, for uniformity, we take the usual ‘ground’ approach everywhere as it does not inccur loss of generality (see [2]).

If n > 1, we write t →^{w}_{R_{nv}} t′ →_{R_{nv}}^{∗} s. Note that t′ is R_{nv}-normalizing too. We consider the different cases for the occurrence w. The case w < u is not possible due to the same reasoning as in the base case. Let us consider u ∥ w or u < w. Then t′|_{u} is R_{nv}-needed (in t′). Otherwise, since t[•]_{u} →_{R_{nv}} t′[•]_{u} (for the first case) or t[•]_{u} = t′[•]_{u} (for the second one), it follows that t|_{u} is not R_{nv}-needed. If v ∈ O(t′), then, by I.H., v ≰ u. If v ∉ O(t′), then the reduction step t →^{w}_{R_{nv}} t′ has (re)moved the redex t|_{v}. This is only possible when w ≤ v. Since we have either u ∥ w or u < w, we also have u ∥ v or u < v, i.e., v ≰ u. □

Lemma 5.5 Let R be an almost orthogonal TRS and t ∈ T (Σ) be R-normalizing. Let u, v ∈ O_{R}(t) such that u ≠ v. If t|_{u} is R_{nv}-needed, then v ≰ u.

Proof. Since →_{R}^{∗}⊆→_{R_{nv}}^{∗} and NF_{R} = NF_{R_{nv}}, t is R_{nv}-normalizing and Lemma 5.4 applies. □

Given an almost orthogonal TRS R = (Σ, R), a reduction step A : t →^{v} s, for some l → r ∈ R, and an outermost redex occurrence u ∈ O_{R}(t), the set u\A of descendants of redex t|_{u} by A is: u\A = Ø if v = u, and u\A = {u} if u ∥ v or u < v. Now, we are ready to prove our main result.

Theorem 5.6 Let R = (Σ, R) be an almost orthogonal TRS, t ∈ T (Σ) be a non-root-stable term, and u ∈ O_{R}(t). If u ∈ I_{nv}(t[Ω]_{u}), then t|_{u} is root-needed.

Proof. If u = ϵ, then it is immediate, since almost orthogonality of R ensures that reductions strictly below the root of the redex t cannot root-normalize t: such reducts of t are still redexes. Therefore, in order to root-normalize t, some reduction step at occurrence ϵ is needed. Thus, redex t|_{ϵ} is root-needed.

If u > ϵ, since t is not root-stable, we can assume that it has a root-stable reduct s. Otherwise, t has no root-stable reduct and every redex in t is rootneeded. Then, we write the derivation t →^{∗} s as t⟶^{>ϵ}^{∗}σ(l) →^{∗} s, for some rewrite rule l → r ∈ R (see [10]). Now we proceed by contradiction. If t|_{u} is not root-needed, we can assume that it is not contracted (neither itself nor any of its descendants) in the previous derivation to a root-stable form. We formalize this fact by replacing the redex occurrence t|_{u} by the constant •. We show, by induction on the length n of the derivation t⟶^{>ϵ}^{∗}σ(l), that there exists a derivation t[•]_{u}⟶^{>ϵ}^{∗}σ′(l) for some substitution σ′. Note that t is not a redex because otherwise u > ϵ is not a nvindex (Lemma 5.2). Therefore, the base case is n = 1.

Let t →^{v} σ(l), where v > ϵ is the occurrence of a redex σ′′(l′) for some rule l′ → r′ ∈ R. We have that t[σ′′(r′)]_{v} = σ(l). By Lemma 5.1, σ(l)[•]_{u} = σ′(l) for some substitution σ′. Since u ∈ I(t[Ω]_{u}), by Lemma 5.2, we only have two cases: u ∥ v and u < v. In the first case, t[•]_{u} = t[σ′′(l′)]_{v}[•]_{u} = t[•]_{u}[σ′′(l′)]_{v}, i.e., t[•]_{u} →^{v} σ′(l). In the second case (u < v), t[•]_{u} = t[σ′′(l′)]_{v}[•]_{u} = t[σ′′(r′)]_{v}[•]_{u} = σ(l)[•]_{u} = σ′(l). Therefore, we get t[•]_{u}⟶^{>ϵ}^{∗}σ′(l) and the conclusion follows.

If n > 1, we write t →^{v} t′⟶^{>ϵ}^{∗}σ(l). Again, we have either u ∥ v or u < v. In both cases, the residual of u ∈ O_{R}(t) is the same redex occurrence u ∈ O_{R}(t′). By I.H., t′[•]_{u} →^{∗} σ′(l). If u ∥ v, then t′ = t[σ′′(r′)]_{v} and t[•]_{u} →^{v} t′[•]_{u}. If u < v, then t[•]_{u} = t′[•]_{u}. In both cases, the conclusion follows.

Then, we obtain a reduction t[•]_{u}⟶^{>ϵ}^{∗}σ′(l) for some substitution σ′. Therefore root(t[•]_{u}) = root(σ′(l)) = f. If we let t[•]_{u} = f(t_{1}, …, t_{k}) and l = f(l_{1}, …, l_{k}), then t_{i} →^{∗} σ′(l_{i}), for 1 ≤ i ≤ k. Since →⊆→_{nv}, we have t_{i} →_{nv}^{∗} σ′(l_{i}). By Lemma 4.5, for each l_{i}, 1 ≤ i ≤ k, there exists s_{i} such that s_{i} ≤ σ′(l_{i}) and t_{i} →_{ω}^{∗} s_{i}. Clearly, t[•]_{u} = f(t_{1}, …, t_{k}) →_{ω}^{∗} f(s_{1}, …, s_{k}) = s and s ≤ σ′(l). Since σ′(l) ↑ l_{Ω}, we have s ↑ l_{Ω}. Since s ≠ Ω, by Lemma 4.4, u ∉ I_{nv}(t[Ω]_{u}), a contradiction. □

In Theorem 5.6, the restriction to non-root-stable terms cannot be dropped, as root-stable terms have no root-needed redexes. As expected from the undecidability of root-neededness, nv-indices do not cover all occurrences of root-needed redexes. We cannot extend Theorem 5.6 to weakly orthogonal TRSs.

Example 5.7 Consider the TRS R in Example 5.3. We have the following root-normalizing derivations for

                                               t = pred(succ(pred(0))):
                                                   \underline{pred(succ(pred(0)))} → pred(0)

and

                                                   pred(\underline{succ(pred(0))}) → pred(0)

The former derivation shows that t is not root-stable. As shown in Example 5.3, ϵ and 1 are nv-indices. However, neither t|_{ϵ} nor t|_{1} are root-needed.

For orthogonal TRSs, every non-root-stable term has a root-needed redex [10]. Middeldorp did not extend this result to almost orthogonal TRSs, and he gave the following example [10]:

Example 5.8 Let the almost orthogonal TRS R be:

                                                   T or x → T

                                                   x or T → T

The term (T or T) or (T or T) is not root-stable. However, neither occurrence 1 nor occurrence 2 of redex T or T is root-needed.

Note that R in Example 5.8 is not NV-sequential: the Ω-normal form Ω or Ω in t has no nv-index. Theorem 5.6 allows us to complement Middeldorp’s results.

Theorem 5.9 Let R be an almost orthogonal, NVsequential TRS. Every non-root-stable ground term t has a root-needed redex.

Proof. Let s be the Ω-normal form which results from changing the redex occurrences of t for Ω’s. By NV-sequentiality, s has a nv-index u. By a repeated application of Lemma 4.2, we get u ∈ I_{nv}(t[Ω]_{u}). By Theorem 5.6, t|_{u} is root-needed. □

TRS in Example 5.3 is strongly sequential (see [13]), hence NV-sequential.

Remark 5.10 Definition 4.1 implies that every redex in t ∈ T (Σ) having no R-normal form is R-needed. This is because if t has no R-normal form, t[•]_{u} does not have an R_{•}-normal form. Otherwise, if s ∈ T (Σ) is an R_{•}-normal form of t (R_{•}-normal forms have no occurrence of •), it would be possible to build an Rreduction sequence leading from t to an R-normal form s of t by just taking the same reduction steps issued in R_{•} to normalize t. Similar considerations can be made for sequentiality (based on the predicate nf_{R}).

Example 5.11 The nv-approximation R_{nv} of R in Example 1.1 is

    f(x) → g(f(y))

    a → a

The term f(a) has no R_{nv}-normal form (hence it has no R-normal form). Therefore, the redex a is R_{nv}- needed. However, it is not root-needed.

Theorem 5.12 Let R = (Σ, R) be an almost orthogonal TRS, t ∈ T (Σ) be a non-root-stable, R-normalizing term, and u ∈ O_{R}(t). If t|_{u} is R_{nv}-needed, then t|_{u} is root-needed.

Proof. If u = ϵ, we reason as in the proof of Theorem 5.6. For the case when u > ϵ we also proceed analogously by writing t⟶^{>ϵ}^{∗}σ(l) →^{∗} s, for some rewrite rule l → r ∈ R and (unique) R-normal form s ∈ T (Σ) of t. Confluence of R ensures that this derivation exists. By using Lemma 5.5, and by proceeding as done in the proof of Theorem 5.6, we conclude that t[•]_{u}⟶^{>ϵ}^{∗}σ′(l) for some substitution σ′. Since →_{R}^{∗}⊆→_{R_{nv}}^{∗}, we have t[•]_{u} →_{R_{nv}}^{∗} σ′(l). We can assume that σ′ = σ′_{l} ∪ σ_{r} where σ_{r}(x_{v}) = σ(x) if x_{v} ∈ V ar(r′) is the fresh variable which corresponds, in the rule l → r′ of R_{nv}, to occurrence v of variable x ∈ V ar(r): r|_{v} = x iff r′|_{v} = x_{v}. Then we write σ′(l) →_{R_{nv}}^{∗} s, i.e., t[•]_{u} →_{R_{nv}}^{∗} s. Therefore, t|_{u} is not R_{nv}-needed. □

We conjecture that Theorem 5.12 can be improved by requiring that t is R_{nv}-normalizing rather than Rnormalizing. Since every R-normalizing term is R_{α}- normalizing for every approximation R_{α} of R, this is a weaker restriction which is indeed true for R_{s}: as every term has an R_{s}-normal form, this conjecture is actually verified by Theorem 5.6.

Theorem 5.13 Let R ∈ CBN-NF_{nv} be an almost orthogonal TRS. Every non-root-stable, R-normalizing ground term t has a root-needed redex.

Proof. Since R ∈ CBN-NF_{nv}, t has an R_{nv}-needed redex. By Theorem 5.12 the conclusion follows. □

Corollary 5.14 Let R ∈ CBN-NF_{nv} be an almost orthogonal, weakly normalizing TRS. Every non-root-stable, ground term has a root-needed redex.

We give an example of application of Theorem 5.13.

Example 5.15 The (terminating) TRS R [3]:

                                                   f(a,b,x) → a

                                                   f(b,x,a) → b
                                                   f(x,a,b) → c

is not NV-sequential (the term f(Ω,Ω,Ω) has no index). However, it belongs to CBN-NF_{nv} (see [3]).

CBN-NF_{nv} includes NVNF-sequential TRSs. Thus, the results concerning CBN-NF_{nv} also hold for NVNFsequential TRSs. However, TRS in Example 1.1 is NVNF-sequential. Thus, Theorem 5.6 does not hold for NVNF-sequential TRSs (see Example 5.11).

As needed redexes could not be root-needed, we cannot hope that each approximation to neededness approximates root-neededness as well.

Example 5.16 Let the (terminating) TRS R be:

                                                   f(x,b) → g(x)

                                                   a → b
                                                   c → b

and t = f(a,c). This term has a normal form

                                                   f(a,\underline{c}) → \underline{f(a,b)} → g(\underline{a}) → g(b)

Since R is right-linear and shallow, R = R_{sh}. The outermost redex a is R_{sh}-needed, hence R-needed. However, a is not root-needed.

Example 5.16 shows that the shallow and growing approximations R_{sh} and R_{g} cannot generally be used to approximate root-neededness. In fact, the example concerns the original shallow sequential approximation (strictly included in CBN-NF_{sh}) as defined by H. Comon [2]. This is a more precise negative result.

6 Root-normalization and infinitary normalization

Theorem 6.1 Let R be an almost orthogonal TRS and t be a root-normalizing ground term. Let t = t_{1} → t_{2} → ⋯ be an infinite reduction sequence such that,

∀i ≥ 1, ∃j ≥ i such that t_{j} →^{u} t_{j+1} and u ∈ I_{nv}(t_{j}[Ω]_{u}).

There is p ≥ 1 such that t_{p} is root-stable.

Proof. If there exists no p such that t_{p} is root-stable, by Theorem 5.6, the reduction sequence contains an infinite number of root-needed reduction steps, hence an infinite number of root-necessary reduction steps. This contradicts Theorem 3.2. □

This theorem has an immediate consequence.

Theorem 6.2 Every nv-strategy is hyper root-norm-alizing for almost orthogonal, NV-sequential TRSs.

Theorem 6.2 justifies the derivation of Example 3.3. We reduce a nv-index which serves to root-normalize the term since it corresponds to a root-needed redex.

We follow Middeldorp’s approach to infinitary normalization [10]. An infinite rewrite sequence t_{1} → t_{2} → ⋯ is strongly converging if for all d ≥ 0, there is i ≥ 1 such that ∀j ≥ i, t_{j} →^{u} t_{j+1} implies |u| ≥ d. Also all finite rewrite sequences are strongly converging.

Definition 6.3 [10] A rewrite sequence is called infinitary normalizing if it strongly converges to a (possibly infinite) normal form.

An infinite rewrite sequence that is not infinitary normalizing is called perpetual. A term is infinitary normalizing if it admits an infinitary normalizing rewrite sequence. A strategy S for a TRS is called infinitary normalizing if there are no perpetual S-rewrite sequences starting from infinitary normalizing terms.

An infinite rewrite sequence t_{1} → t_{2} → ⋯ is called fair if, ∀i ≥ 1 and every maximal non-root-stable subterm s of t_{i} that has a root-stable reduct, there is a j ≥ i such that the position of the redex contracted in the step t_{j} → t_{j+1} is below the position of s in t_{i}. A reduction strategy S for a TRS is called infinitary fair-normalizing if there are no perpetual fair S-rewrite sequences starting from infinitary normalizing terms.

A one-step strategy S is context-free if, for all rootstable term t = f(t_{1}, …, t_{i}, …, t_{k}) and i ∈ {1, …, k}, such that t →_{S} f(t_{1}, …, t′_{i}, …, t_{k}), we have t_{i} →_{S} t′_{i}. General nv-strategies do not need to be context-free.

Example 6.4 Let S be the nv-strategy that selects the leftmost redex addressed by an nv-index if n = |O_{R}(t)| is odd, and the rightmost one if n is even. For TRS

                                                   f(b,c) → d
                                                   a → d

and the root-stable term t = f(f(a,a),a) we have

                                                   f(f(\underline{a},a),a) →_{S} f(f(d,a),a)

but

                                                   f(a,\underline{a}) →_{S} f(a,d)

which means that S is not context-free.

Middeldorp showed that, for confluent TRSs, contextfree root-normalizing one-step strategies are infinitary fair-normalizing. We prove a similar result for nvstrategies without requiring context-freeness.

Proposition 6.5 Let R be an almost orthogonal TRS and t be an infinitary normalizing ground term. Every fair reduction sequence that only contracts nv-indices is infinitary normalizing.

Proof. Let A : t = t_{1} → t_{2} → ⋯ be a fair reduction sequence that only contracts nv-indices. We prove that, for every depth d ≥ 0, there is p ≥ 1 such that

∀j ≥ p, if t_{j} →^{u} t_{j+1}, then |u| ≥ d and ∀w ∈ O(t_{j}), s.t.

|w| < d, we have that t_{j}|_{w} is root-stable.

By induction on d. If d = 0, it is immediate. Let d > 0. Since t is infinitary normalizing, it has a rootstable reduct, s, such that t →^{∗} s. By Theorem 6.1, we can assume that this is an initial subsequence of A, i.e., there exists m such that s = t_{m}. Let s = C[s_{1}, …, s_{n}], such that s_{1}, …, s_{n} are the maximal non-root-stable subterms of s and s_{i} = s|_{u_{i}} for 1 ≤ i ≤ n. Since R is almost orthogonal, it is confluent. By confluence, each s_{i} is infinitary normalizing for 1 ≤ i ≤ n.

For 1 ≤ i ≤ n, let A_{i} : s_{i} = s_{i}^{1} →^{v_{i}^{1}} s_{i}^{2} →^{v_{i}^{2}} ⋯ be

the (finite or infinite) rewrite sequence extracted from

the tail of A which starts in s: each step s_{i}^{k} →^{v_{i}^{k}} s_{i}^{k+1}

in A_{i} corresponds to a step t_{p(i,k)} →^{u_{p(i,k)}} t_{p(i,k)+1} in

A in such a way that u_{p(i,k)} = u_{i}.v_{i}^{k} and the relative order of reductions in A is preserved in the corresponding A_{i} (we do not further formalize this connection). Since A is fair, and each s_{i} is a maximal non-root-stable term in s, each A_{i} is non-empty and fair for 1 ≤ i ≤ n. Since u_{p(i,k)} ∈ I_{nv}(t_{p(i,k)}[Ω]_{u_{p(i,k)}}), by Lemma 4.3, v_{i}^{k} ∈ I_{nv}(s_{i}^{k}[Ω]_{v_{i}^{k}}) for 1 ≤ i ≤ n and k ≥ 0, i.e., each A_{i} is a fair reduction sequence that only contracts nv-indices. Since C[ ] is not empty (as s is root-stable), |u_{i}| > 0 for 1 ≤ i ≤ n. We can apply the induction hypothesis to each d_{i} = d − |u_{i}|, 1 ≤ i ≤ n. Thus, there exist p_{1}, …, p_{n} such that ∀k_{i} ≥ p_{i}, if

s_{i}^{k_{i}} →^{v_{i}^{k_{i}}} s_{i}^{k_{i}+1}, then |v_{i}^{k_{i}}| ≥ d_{i} and ∀w_{i} ∈ O(s_{i}^{k_{i}}), s.t.

|w_{i}| < d_{i}, we have that s_{i}^{k_{i}}|_{w_{i}} is root-stable. Let p = max({p(i, p_{i}) | 1 ≤ i ≤ n}). Then, ∀j ≥ p, if t_{j} →^{u} t_{j+1}, then |u| ≥ d and since every part of C[ ] is root-stable, then, for all w ∈ O(t_{j}), s.t. |w| < d, t_{j}|_{w} also is root-stable. Clearly, it is a strongly converging sequence leading to a normal form. □

Theorem 6.6 Every nv-strategy is infinitary fairnormalizing for almost orthogonal, NV-sequential TRSs.

Proof. Let t be an infinitary normalizing term and A : t = t_{1} →_{S} t_{2} →_{S} ⋯ be an infinite S-rewrite sequence starting from t. If A is not fair, it is immediate. If A is fair, by Proposition 6.5, it is infinitary normalizing, hence it is not perpetual. Thus, the conclusion follows. □

Theorem 6.6 proves that S in Example 6.4 is infinitary fair-normalizing. This cannot be obtained from Middeldorp’s results.

As remarked in [10], without the fairness requirement for the strategy, we only ensure that an infinite stable part (rather than an infinite normal form) is obtained. For instance, leftmost-outermost strategy is a nv-strategy for almost orthogonal, left-normal TRSs (see [13]), hence infinitary fair-normalizing (Theorem 6.6), but it is not fair (see [10]).

Example 6.7 The reduction sequence

    \underline{f(a)} → g(\underline{f(a)}) → g(g(\underline{f(a)})) → · · ·

(w.r.t. R in Example 1.1) contracts nv-indices. It is trivially fair, and it converges now to an infinite normal form g(g(g(…))).

Approximations R_{nv}, R_{sh}, and R_{g} are not adequate for infinitary normalization, as the first one only approximates root-neededness for normalizing terms and the other ones do not approximate root-neededness.

7 Conclusions

Decidable approximations to root-neededness have already been attempted [3, 7]. Kennaway proposed strongly root-neededness as an approximation to rootneededness [7]. Since root-stability itself is not decidable, Kennaway formulated his approximation with respect to the (decidable) notion of strongly root-stable term (also known as strong head-normal form, [4, 9]). Occurrences of strongly root-needed redexes are also called indices by Kennaway. However, Kennaway’s indices do not coincide with nv or strong indices. Moreover, Durand and Middeldorp have pointed out some inconsistencies in Kennaway’s approximation to rootneededness [3]. In [3], Durand and Middeldorp also try to simultaneously deal with the undecidability of both root-stability and root-neededness. However (as remarked by a referee), if we consider an approximation of root-stability (like strong root-stability), we do not have the property that in a non strongly-root-stable term, every strongly root-needed redex is root-needed as non-strong-root stability does not imply non-root-stability. Thus, this does not provide decidable callby-need computations to root-stable form.

We have isolated the problem of decidability of rootneededness from the decidability of root-stability. We do not provide a completely decidable approach to root-neededness as the notion of non-root-stable term remains undecidable. Nevertheless, we think that our work clarifies the connections between neededness and root-neededness in a novel unexplored way.

Acknowledgements

I would like to thank the anonymous referees for their suggestions and clarifying remarks.

References

[1] H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer, and M.R. Sleep. Term Graph Rewriting. In Proc. of PARLE’87, LNCS 259:141-158, Springer-Verlag, 1987.

[2] H. Comon. Sequentiality, Second Order Monadic Logic and Tree Automata. In Proc. of LICS’95, pages 508-517, IEEE Press, 1995.

[3] I. Durand and A. Middeldorp. Decidable Call by Need Computations in Term Rewriting (Extended Abstract). In Proc. of CADE’97, LNAI 1249:4-18, Springer-Verlag, 1997.

[4] 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.

[5] F. Jacquemard. Decidable approximations to Term Rewriting Systems. In Proc. of RTA’96, LNCS 1103:362-376, Springer-Verlag, 1996.

[6] J.P. Jouannaud and W. Sadfi. Strong Sequentiality of Left-Linear Overlapping Rewrite Systems. In Proc. of CTRS’94, LNCS 968:235-246, Springer-Verlag, 1994.

[7] R. Kennaway. A Conflict Between Call-By-Need Computation and Parallelism. In Proc. of CTRS’94, LNCS 968:247-261, Springer-Verlag, 1994.

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

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

[10] A. Middeldorp. Call by Need Computations to Root-Stable Form. In Proc. of POPL’97, pages 94-105, ACM Press, 1997.

[11] T. Nagaya, M. Sakai, and Y. Toyama. NVNF-Sequentiality of Left-Linear Term Rewriting Systems. RIMS Technical Report 918, pages 109-117, University of Kyoto, 1995.

[12] M. Oyamaguchi. NV-Sequentiality: a decidable condition for call-by-need computations in termrewriting systems. SIAM Journal of Computing, 22(1):114-135, 1993.

[13] Y. Toyama. Strong Sequentiality of Left-Linear Overlapping Rewrite Systems. In Proc. of LICS’92, pages 274-284, IEEE Press, 1992.