Relative Normalization in Orthogonal Expression Reduction Systems

John Glauert and Zurab Khasidashvili

School of Information Systems, UEA Norwich NR4 7TJ England jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk ^{⋆}

Abstract. We study reductions in orthogonal (left-linear and non-am-biguous) Expression Reduction Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. To generalise the normalization theory of Huet and Lévy, we introduce the notion of neededness with respect to a set of reductions Π or a set of terms S so that each existing notion of neededness can be given by specifying Π or S. We imposed natural conditions on S, called stability, that are sufficient and necessary for each term not in S-normal form (i.e., not in S) to have at least one S-needed redex, and repeated contraction of S-needed redexes in a term t to lead to an S-normal form of t whenever there is one. Our relative neededness notion is based on tracing (open) components, which are occurrences of contexts not containing any bound variable, rather than tracing redexes or subterms.

1 Introduction

Since a normalizable term, in a rewriting system, may have an infinite reduction, it is important to have a normalizing strategy which enables one to construct reductions to normal form. It is well known that the leftmost-outermost strategy is normalizing in the λ-calculus. For Orthogonal Term Rewriting Systems (OTRSs), a general normalizing strategy, called the needed strategy, was found by Huet and Lévy in [HuLé91]. The needed strategy always contracts a needed redex – a redex whose residual is to be contracted in any reduction to normal form. Huet and Lévy showed that any term t not in normal form has a needed redex, and that repeated contraction of needed redexes in t leads to its normal form whenever there is one; we refer to it as the Normalization Theorem. They also defined the class of strongly sequential OTRSs where a needed redex can efficiently be found in any term.

Barendregt et al. [BKKS87] generalized the concept of neededness to the λcalculus. They studied neededness not only w.r.t. normal forms, but also w.r.t. head-normal forms – a redex is head-needed if its residuals are contracted in each reduction to a head-normal form. The authors proved correctness of the two

⋆ This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300

needed strategies for computing normal forms and head-normal forms, respectively. Khasidashvili defined a similar normalizing strategy, called the essential strategy, for the λ-calculus [Kha88] and OTRSs [Kha93]. The strategy contracts essential redexes – the redexes that have descendants under any reduction. The notion of descendant is a refinement of that of residual – the descendant of a contracted redex is its contractum, while it does not have residuals. This refined notion allows for much simpler proofs of correctness of the essential strategy in OTRSs and the λ-calculus, which generalize straightforwardly to all Orthogonal Expression Reduction Systems (OERSs). Kennaway and Sleep [KeSl89] used a generalization of Lévy’s labelling for the λ-calculus [Lév78] to adapt the proof from [BKKS87] to the case of Klop’s OCRSs [Klo80], which can also be applied to OERSs. Khasidashvili [Kha94] showed that in Persistent OERSs, where redex-creation is limited, one can find all needed redexes in any term. Gardner [Gar94] described a complete way of encoding neededness information using a type assignment system in the sense that using the principal type of a term one can find all the needed redexes in it (the principal type cannot be found efficiently, as one might expect). Antoy et al. [AEH94] designed a needed narrowing strategy.

In [Mar92], Maranget introduced a different notion of neededness, where a redex u is needed if it has a residual under any reduction that does not contract the residuals of u. This neededness notion makes sense also for terms that do not have a normal form, and coincides with the notion of essentiality [Kha93] (essentiality makes sense for all subterms, not only for redexes). In [Mar92], Maranget studied also a strategy that computes a (in fact, the ‘minimal’ in some sense) weak head-normal form of a term in an OTRS. Normalization w.r.t. another interesting set of ‘normal forms’, that of constructor head-normal forms in constructor OTRSs, is studied by Nöcker [Nök94].

A question arises naturally: what are the properties that a set of terms must possess in order for the neededness theory of Huet and Lévy still to make sense? The main contribution of this paper is to provide a solution to that question. We introduce the notion of neededness w.r.t. a set of reductions Π or a set of terms S so that each existing notion of neededness can be given by specifying Π or S. For example, Huet&Lévy-neededness is neededness w.r.t. the set of normal forms, Maranget-neededness is neededness w.r.t. all fair reductions, headneededness is neededness w.r.t. the set of head-normal forms, etc. We impose natural conditions on S, called stability, that are sufficient and necessary for each term not in S-normal form (i.e., not in S) to have at least one S-needed redex, and repeated contraction of S-needed redexes in a term t to lead to an S-normal form of t whenever there is one.

A set S of terms is stable if it is closed under permutation: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e, the final term of P/Q, the residual of P under Q, is in S; and is closed under unneeded expansion: for any e→^{u}o such that e ∉ S and o ∈ S, a residual of u is contracted in any reduction from e to a term in S. We present a counterexample to show that the S-needed strategy is not hypernormalizing for every stable S, i.e., an S-normalizable term may possess a reduction which never reaches a term in S even though S-needed redexes are contracted infinitely many times, but S-unneeded redexes are contracted as well. Therefore, multistep S-needed reductions need not be S-normalizing. This is because a ‘non-standard’ situation – when a component under an Sunneeded component is S-needed – may occur for some, call it irregular stable sets S. However, if S is a regular stable set, then the S-needed strategy is again hypernormalizing, and the multistep S-needed strategy is normalizing.

Our relative neededness notion is based on tracing (open) components, which are occurrences of contexts not containing any bound variable, rather than tracing redexes or subterms. We therefore introduce notions of descendant and residual for components that are invariant under Lévy-equivalence. A component of a term t ∉ S is called S-needed if at least one descendant of it is ‘involved’ in any S-normalizing reduction; a redex is S-needed if so is its pattern. Besides generality, this approach to defining the neededness notion via components is crucial from a technical point of view, because components of a term in an OERS enjoy the same ‘disjointness’ property that subterms of a term in an OTRS possesses: residuals of disjoint components of a term in an OERS remain disjoint, and this allows for simpler proofs.

The rest of the paper is organized as follows. In the next section, we review Expression Reduction Systems (ERS), a formalism for higher order rewriting that we use here [Kha90, Kha92]; define the descendant relation for components, and show that it is invariant under Lévy-equivalence. Section 3 establishes equivalence of Maranget’s neededness and our essentiality for OERSs. In section 4, we introduce the relative notion of neededness. In section 5, we sketch some properties of the labelling system of Kennaway&Sleep [KeSl89] for OERSs needed to define a family-relation among redexes. We prove correctness of the S-needed strategy for finding terms of S, for all stable S, in section 6. The conclusions appear in section 7.

2 Orthogonal Expression Reduction Systems

Klop introduced Combinatory Reduction Systems (CRSs) in [Klo80] to provide a uniform framework for reductions with substitutions (also referred to as higherorder rewriting) as in the λ-calculus [Bar84]. Restricted rewriting systems with substitutions were first studied in Pkhakadze [Pkh77] and Aczel [Acz78]. Several interesting formalisms have been introduced later [Nip93, Wol93, OR94]. We refer to Klop et al. [KOR93] and van Oostrom [Oos94] for a survey. Here we use a system of higher order rewriting, Expression Reduction Systems (ERSs), defined in Khasidashvili [Kha90, Kha92] (ERSs are called CRSs in [Kha92]); the present formulation is simpler.

Definition 2.1 Let Σ be an alphabet, comprising variables, denoted by x, y, z; function symbols, also called simple operators; and operator signs or quantifier signs. Each function symbol has an arity k ∈ N, and each operator sign σ has an arity (m, n) with m, n ≠ 0 such that, for any sequence x_{1}, …, x_{m} of pairwise distinct variables, σx_{1} … x_{m} is a compound operator or a quantifier with arity n. Occurrences of x_{1}, …, x_{m} in σx_{1} … x_{m} are called binding variables. Each quantifier σx_{1} … x_{m}, as well as the corresponding quantifier sign σ and binding variables x_{1} … x_{m}, has a scope indicator (k_{1}, …, k_{l}) to specify the arguments in which σx_{1} … x_{m} binds all free occurrences of x_{1}, …, x_{m}. Terms are constructed from variables using functions and quantifiers in the usual way.

Metaterms are constructed similarly from terms and metavariables A, B, …, which range over terms. In addition, metasubstitutions, expressions of the form (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, with t_{j} arbitrary metaterms, are allowed, where the scope of each x_{i} is t_{0}. Metaterms without metasubstitutions are simple metaterms. An assignment maps each metavariable to a term over Σ. If t is a metaterm and θ is an assignment, then the θ-instance tθ of t is the term obtained from t by replacing metavariables with their values under θ, and by replacing metasubstitutions (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, in right to left order, with the result of substitution of terms t_{1}, …, t_{n} for free occurrences of x_{1}, …, x_{n} in t_{0}.

For example, a β-redex in the λ-calculus appears as Ap(λx t, s), where Ap is a function symbol of arity 2, and λ is an operator sign of arity (1,1) and scope indicator (1). Integrals such as ∫_{s}^{t} f(x) dx can be represented as ∫x s t f(x) using an operator sign ∫ of arity (1,3) and scope indicator (3).

Definition 2.2 An Expression Reduction System (ERS) is a pair (Σ, R), where Σ is an alphabet, described in Definition 2.1, and R is a set of rewrite rules r : t → s, where t and s are closed metaterms (i.e., no free variables) such that t is a simple metaterm and is not a metavariable, and each metavariable that occurs in s occurs also in t.

Further, each rule r has a set of admissible assignments AA(r) which, in order to prevent undesirable confusion of variable bindings, must satisfy the condition that:

(a) for any assignment θ ∈ AA(r), any metavariable A occurring in t or s, and any variable x ∈ F V (Aθ), either every occurrence of A in r is in the scope of some binding occurrence of x in r, or no occurrence is.

For any θ ∈ AA(r), tθ is an r-redex or an R-redex, and sθ is the contractum of tθ. We call R simple if right-hand sides of R-rules are simple metaterms.

Our syntax is similar to that of Klop’s CRSs [Klo80], but is closer to the syntax of the λ-calculus and of First Order Logic. For example, the β-rule is written as Ap(λxA, B) → (B/x)A, where A and B can be instantiated by any terms; the η-rule is written as λx(Ax) → A which requires that an assignment θ is admissible iff x ∉ (Aθ), otherwise an x occurring in Aθ and therefore bound in λx(Aθx) would become free. A rule like f(A) → ∃x(A) is also allowed, but an assignment θ with x ∈ Aθ is not. The recursor rule from [AsLa93] is written as μ(λxA) → (μ(λxA)/x)A. ∃xA → (τx(A)/x)A and ∃!xA → ∃xA ∧ ∀x∀y(A ∧ (y/x)A ⇒ x = y) are rules corresponding to familiar definitions.

Below we restrict ourselves to the case of non-conditional ERSs, i.e., ERSs where an assignment is admissible iff the condition (a) of Definition 2.2 is satisfied. We ignore questions relating to renaming of bound variables. As usual, a rewrite step consists of replacement of a redex by its contractum. Note that the use of metavariables in rewrite rules is not really necessary – free variables can be used instead, as in TRSs. We will indeed do so at least when giving TRS examples.

To express substitution, we use the S-reduction rules

S^{n+1}x_{1} … x_{n}A_{1} … A_{n}A_{0} → (A_{1}/x_{1}, …, A_{n}/x_{n})A_{0}, n = 1, 2, …, where S^{n+1} is the operator sign of substitution with arity (n, n+1) and scope indicator (n+1), and x_{1}, …, x_{n} and A_{1}, …, A_{n}, A_{0} are pairwise distinct variables and metavariables. Thus S^{n+1} binds free variables only in the last argument. The difference with β-rules is that S-reductions can only perform β-developments of λ-terms [Kha92].

Notation 2.1 We use a, b, c, d for constants, t, s, e, o for terms and metaterms, u, v, w for redexes, and N, P, Q for reductions. We write s ⊆ t if s is a subterm of t. A one-step reduction in which a redex u ⊆ t is contracted is written as t →^{u} s or t → s or just u. We write P : t → → s or t → →^{P} s if P denotes a reduction of t to s. |P | denotes the length of P. P + Q denotes the concatenation of P and Q.

Let r : t → s be a rule in an ERS R and let θ ∈ AA(r). Subterms of a redex v = tθ that correspond to metavariables of t are the arguments of v, and the rest is the pattern of v. Subterms of v rooted in the pattern are called the pattern-subterms of v. If R is a simple ERS, then arguments, pattern, and pattern-subterms are defined analogously in the contractum sθ of v.

We now recall briefly the definition of descendant of subterms as introduced in [Kha88, Kha93, Kha92] for the λ-calculus, TRSs, and ERSs, respectively. First, we need to split an ERS R into a TRS-part R_{f} and the substitutionpart S. For any ERS R, which we assume does not contain symbols S^{n+1}, R_{f} is the ERS obtained from R by adding symbols S^{n+1} in the alphabet and by replacing in right-hand sides of the rules all metasubstitutions of the form (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0} by S^{n+1}x_{1} … x_{n}t_{1} … t_{n}t_{0}, respectively. For example, the β_{f} rule would be Ap(λxA, B) → S^{2}xBA. If R is simple, then R_{fS} =_{def} R_{f} =_{def} R. Otherwise R_{fS} =_{def} R_{f} ∪ S. For each step C[tθ] →^{u} C[sθ] in R there is a reduction P : C[tθ] →_{R_{f}} C[s′θ] → → _{S} C[sθ] in R_{fS}, where C[s′θ] → → _{S} C[sθ] is the rightmost innermost normalizing S-reduction. We call P the refinement of u. The notion of refinement generalizes to R-reductions with 0 or more steps.

Let t →^{u} s be an R_{f}-reduction step and let e be the contractum of u in s. For each argument o of u there are 0 or more arguments of e. We will call them udescendants of o. We refer to the i-th (from the left, i > 0) descendant of o also as the (u, i)-descendant of o. Correspondingly, subterms of o have 0 or more descendants. By definition, the descendant, referred to also as the (u, ∗)-descendant, of each pattern-subterm of u is e. It is clear what is to be meant by the descendant of a subterm s′ ⊆ t that is not in u. We call it also the (u, ∗)-descendant of s′.

In an S-reduction step C[S^{n+1}x_{1} … x_{n} t_{1} … t_{n}t_{0}]→^{u}C[(t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}], the

argument t_{i} and its subterms have the same number of descendants as the number of free occurrences of x_{i} in t_{0}; the i-th descendant is referred to as the (u, i)-descendant. Every subterm of t_{0} has exactly one descendant, the (u, 0)- descendent (in particular, the (u, 0)-descendants of free occurrences of x_{1}, …, x_{n} in t_{0} are the substituted subterms). The descendant or (u, ∗)-descendent of the contracted redex u itself is its contractum. The pairs (u, i) and (u, ∗) are called the indexes of corresponding descendants. The descendants of all redexes except the contracted one are called residuals.

The notions of descendant and residual extend by transitivity to arbitrary R_{fS}-reductions; indexes of descendants and residuals are sequences of indexes of immediate (i.e., under one step) descendants and residuals in the chain leading from the initial to the final subterm. If P is an R-reduction, then P descendants are defined to be the descendants under the refinement of P. The ancestor relation is the converse of the descendant relation.

We call a component an occurrence of a context that does not contain any bound variables; that is, neither variables bound from above in the term, nor variables for which the binder is in the component, belong to the component. Since we also consider occurrences of the empty context [ ], which has an arity 1, we will think of a component as a pair (context, path), where the path characterizes the position of the component in the term (usually, a position is a chain of natural numbers). Thus an empty component or empty occurrence is a pair ([ ], path). If terms are represented by trees, then the empty occurrence ([ ], path) can be seen as the connection at the top of the symbol at the position path.

Obviously, a component C can be considered as its corresponding subterm (the subterm rooted at the position of C), with some subterms (the arguments of C), removed. In particular, a subterm s with itself removed becomes the empty occurrence at the position of s. We say that an empty occurrence ([ ], path) in a term t is in a subterm or component e in t if path is a non-top position of e. We use C and the letters s, t, e, o used for terms to denote components as well. We write s ⊑ t if s is a component of t.

The concept of descendent can be extended to components in the following way:

Definition 2.3 Let R be an ERS, C be a component of a term t in R_{fS}, let s = C[s_{1}, …, s_{n}] be the corresponding subterm of C in t, let t→^{u}t′ in R_{fS}, and let o′ ⊆ t′ be the contractum of u. The pattern of u will be denoted by pat(u) and the pattern of the contractum by cpat(u). We define u-descendants of C by considering all relative positions of u and C.

(1) C ∩ u = ∅ (so if C is an empty component, C is not in u). Then the (u, ∗)-descendant of C is the (u, ∗)-descendant of s with the (u, ∗)-descendants of s_{j} removed. (If C is an empty occurrence ([ ], path), then its (u, ∗)-descendant is the same pair.)

(2) C is the empty occurrence at the top of an argument o of u. Then the (u, i)-descendant of C is the empty occurrence at the top-position of the (u, i)- descendant of o, if the latter exists; if o doesn’t have u-descendants, then C doesn’t have u-descendants either. (Thus, the (u, i)-descendant of C is the (u, i)- descendant of its corresponding subterm s = o with itself removed.)

(3) u is an R_{f}-redex and C is in an argument of u. Then the (u, i)-descendant of C is the (u, i)-descendant of s with the (u, i)-descendants of s_{j} removed (i ≥ 1).

(4) u is an S-redex and C is in an argument of u. Then the (u, i)-descendant of C is the (u, i)-descendant of s with the (u, i)-descendants of s_{j} removed (i ≥ 0).

(5) u is an R_{f}-redex and pat(u) is in C. Then the (u, ∗)-descendant of C is the (u, ∗)-descendant of s with the descendants of s_{j} removed (see Figure 1). In particular, if C is collapsed, i.e. pat(u) = C and cpat(u) = ∅, then the (u, ∗)- descendant of C is the empty occurrence at the position of o′.

Fig. 1.

(6) u is an S-redex, say with two arguments (for simplicity) u = S^{2}x e o, with the top in C, and let s = C′[s_{1}, …, S^{2}x C_{e}[s_{k}, …, s_{l}] C_{o}[s_{l+1}, …, s_{m}], …, s_{n}], with C = C′[…, S^{2}x C_{e}[ ] C_{o}[ ], …], e = C_{e}[s_{k}, …, s_{l}], and o = C_{o}[s_{l+1}, …, s_{m}]. Then, the (u, ∗)-descendants of C are the (u, ∗)-descendant of s with the descendants of the subterms s_{j} removed, and the descendants of C_{e}, as defined in (4) (see Figure 2, where k = l = 1 and l+1 = m = 2). Note that if C = P at(u) = S, then C_{e} and C_{o} are empty components, C is collapsed, and its descendants are the empty occurrences at the top positions of the descendants of u and its arguments.

Fig. 2.

(7) u is an R_{f}-redex, pat(u) and C partially overlap (i.e., neither contains another), and the top of u is (not necessarily strictly) below the top of C. Then the (u, ∗)-descendant of C is the (u, ∗)-descendant of s with the descendants of the arguments of u that do not overlap with C and the descendants of s_{i} that do not overlap with pat(u) removed (see Figure 3). In addition, if the top symbol of o′ doesn’t belong to the (above) (u, ∗)-descendant of C, then the empty component at the top of o′ is also a (u, ∗)-descendant of C.

Fig. 3.

(8) u is an R_{f}-redex, pat(u) and C partially overlap, and the top of C is below the top of u. Then the (u, ∗)-descendant of C is the (u, ∗)-descendant of s with the descendants of s_{i} that do not overlap with pat(u) and the descendants of the arguments of u that do not overlap with C removed (see Figure 4). In addition, if the top symbol of o′ doesn’t belong to the (above) (u, ∗)-descendant of C, then the empty component at the top of o′ is also a (u, ∗)-descendant of C.

Fig. 4.

(9) u is an R_{f}-redex and pat(u) contains C (C may be an empty component). Then the (u, ∗)-descendant of C is the contractum-pattern of u (the latter may also be empty) (see Figure 5).

Fig. 5.

The notion of descendant for components generalises by transitivity to all R_{fS} reductions and via refinements to all R-reductions.

In [Klo92], Klop also introduced a notion of descendant of (an occurrence of) a symbol for the case of TRSs. According to Klop’s definition, descendants of every symbol in the pattern of the contracted redex are all symbols in the contractum pattern. We extend this also to empty occurrences in the pattern of the contracted redex. If the rule is collapsing, i.e., the right-hand side is a variable, then Klop defines the descendant of pattern-symbols of the contracted redex to be the topmost symbol of the contractum. We define the descendant of the pattern-symbols in that case to be the empty occurrence at the position of the contractum. We can define the notion of descendant of a symbol in the same spirit for S-reduction steps by declaring that the descendants of the top S-symbol of a contracted S-redex u are the empty occurrences at the positions of the descendant of u and the descendants of its arguments. We define the descendants of other symbols, in particular of bound variables, to be the top-symbols of the descendants of the corresponding subterms. This gives us a definition of descendant for symbols for all ERSs. Now, it is not difficult to check that descendants of a component are composed of the ‘corresponding’ descendants of its symbols and occurrences, and similarly for the descendants of subterms. Note that, according to Klop’s definition, the descendants of a pattern-subterm o are all subterms rooted in the contractum-pattern, not just the contractum of the redex, as in our definition; so descendants of o need not be composed of descendants of the symbols in o, which is less natural.

Definition 2.4 Co-initial reductions P : t → → s and Q : t → → e are called Hindley-equivalent, written P ≈_{H} Q, if s = e and the residuals of a redex of t under P and Q are the same occurrences. We call P and Q respectively Klopequivalent, strictly equivalent [Kha92], or strictly* equivalent, written P ≈_{K} Q, P ≈_{st} Q, or P ≈_{st}^{∗} Q, if s = e and P -descendants and Q-descendants of respectively any symbol, subterm, or component of t are the same occurrences in s and e.

Definition 2.5 A rewrite rule t → s in an ERS R is left-linear if t is linear, i.e., no metavariable occurs more than once in t. R is left-linear if each rule in R is so. R = {r_{i} | i ∈ I} is non-ambiguous or non-overlapping if in no term redexpatterns can overlap, i.e., if r_{i}-redex u contains an r_{j}-redex u′ and i ≠ j, then u′ is in an argument of u, and the same holds if i = j and u′ is a proper subterm of u. R is orthogonal (OERS) if it is left-linear and non-overlapping.

As in the the λ-calculus [Bar84], for any co-initial reductions P and Q, one can define in OERSs the notion of residual of P under Q, written P/Q, due to Lévy [Lév80], via the notion of development of a set of redexes in a term. We write P ≤ Q if P/Q = ∅ (≤ is the Lévy-embedding relation); P and Q are called Lévy-equivalent or permutation-equivalent (written P ≈_{L} Q) if P ≤ Q and Q ≤ P. It follows immediately from the definition of / that if P and Q are co-initial reductions in an OERS, then (P + P′)/Q ≈_{L} P/Q + P′/(Q/P) and P/(Q + Q′) ≈_{L} (P/Q)/Q′.

Theorem 2.1 Let P and Q be co-initial reductions in an OERS R. Then: (1) (CR(res): Church-Rosser for residuals) P + Q/P ≈_{H} Q + P/Q.

(2) (CR(sub): Church-Rosser for subterms) P + Q/P ≈_{st} Q + P/Q.

(3) (CR(sym): Church-Rosser for symbols) P + Q/P ≈_{K} Q + P/Q.

(4) (CR(com): Church-Rosser for components) P + Q/P ≈_{st}^{∗} Q + P/Q.

Proof. (1) is proved in [Klo80]. (2) is obtained in [Kha92]. The proof of (3) is routine (it is enough to consider the case when |P | = |Q| = 1). (4) follows both from (3) and (2), since descendants of a component can be defined both via descendants of symbols and via descendants of subterms. (Note that (2) can also be derived from (3) for the same reason.)

3 Neededness, Essentiality and Unabsorbedness

In this section, we recall Huet&Lévy and Maranget’s notion of neededness, and relate them to the notion of essentiality, in OERSs. We also prove existence of an essential redex in any term, in an OERS, not in normal form.

Definition 3.1 A redex u in t is Huet&Lévy-needed [HuLé91, Lév80] if in each reduction of t to normal form (if any) at least one residual of u is contracted; u is Maranget-needed [Mar92] if u has at least one residual under any reduction starting from t that does not contract residuals of u.

Definition 3.2 A subterm s in t is essential (written ES(s, t)) if s has at least one descendant under any reduction starting from t and is inessential (written IE(s, t)) otherwise [Kha93, Kha88].

Definition 3.3 A subterm s of a term t is unabsorbed in a reduction P : t → → e if none of the descendants of s appear in redex-arguments of terms in P, and is absorbed in P otherwise; s is unabsorbed in t if it is unabsorbed in any reduction starting from t and absorbed in t otherwise [Kha93].

Remark 3.1 It is easy to see that a redex u ⊆ t is unabsorbed iff u is external [HuLé91] in t. Clearly, unabsorbedness implies essentiality, and Huet&Levy- and Maranget-neededness coincide for normalizable terms. □

Definition 3.4 Let P : t → → s and o be a subterm or a component in t. Then we say that P deletes o if o doesn’t have P -descendants.

Definition 3.5 (1) Let P : t → t_{1} → … and u ⊆ t_{i}. Then u is called erased in P if there is j > i such that u does not have residuals in t_{j}. P is fair if each redex in any t_{i} is erased in P [Klo92].

(2) We call a reduction P starting from t strictly cofinal if for any Q : t → → e there is an initial part P′ : t → → s of P, and a reduction Q′ : e → → s such that P′ ≈_{st} Q + Q′.

Lemma 3.1 Any strictly cofinal reduction P starting from t deletes all inessential subterms of t.

Proof. Immediate from Definitions 3.2 and 3.5.

For example, fair reductions are strictly cofinal: Klop’s proof of cofinality of fair reductions (Theorem 12.3 in [Klo80]) can be modified to a proof of strict cofinality of fair reductions by using CR(sub) (Theorem 2.1.(2)) instead of the CR theorem.

The following lemma from [Kha94] follows from CR(sub) (Theorem 2.1.(2)); the proofs are same as for OTRS [Kha93].

Lemma 3.2 (1) Let P : t → → t′ and s ⊆ t. Then IE(s, t) iff all P -descendants of s are inessential in t′.

(2) Let t→^{u}t′ and e ⊆ s ⊆ t. Then any u-descendant of e is contained in some u-descendant of s.

(3) Let e ⊆ s ⊆ t and ES(e, t). Then ES(s, t).

(4) Let s be a pattern-subterm of a redex u ⊆ t. Then ES(u, t) iff ES(s, t).

Notation We write t = (t_{1}//s_{1}, …, t_{n}//s_{n})s if s_{1}, …, s_{n} are disjoint subterms in s and t is obtained from s by replacing them with t_{1}, …, t_{n}, respectively.

Definition 3.6 Let t = (t_{1}//s_{1}, …, t_{n}//s_{n})s in an OERS R and let P : s = e_{0} →^{v_{0}} e_{1} →^{v_{1}} … be an R_{fS}-reduction. We define the reduction P ∥(t) : t = o_{0} →^{u_{0}} o_{1} →^{u_{1}} … as follows.

(1) If v_{0} is an R_{f}-redex and its pattern does not overlap with s_{1}, …, s_{n}, then u_{0} is the corresponding subterm of v_{0} in t = o_{0}.

(2) If v_{0} is an R_{f}-redex that is not inside the subterms s_{1}, …, s_{n} and its pattern does overlap with some of s_{1}, …, s_{n}, then u_{0} = ∅.

(3) If v_{0} is an S-redex that is outside the replaced subterms, then u_{0} is the corresponding S-redex in t_{0}.

(4) If v_{0} is in some of subterms s_{1}, …, s_{n}, then u_{0} = ∅.

In the first case, o_{1} is obtained from e_{1} by replacing the descendants of s_{1}, …, s_{n} with the corresponding descendants of t_{1}, …, t_{n}, respectively; in the second case, o_{1} is obtained from e_{1} by replacing the descendant of v_{0} by the descendant of its corresponding subterm in o_{0}, and by replacing the descendants of the subterms s_{i} that do not overlap with v_{0} by the corresponding descendants of t_{i}; in the third case, o_{1} is obtained from e_{1} by replacing outermost descendants of s_{1}, …, s_{n} with the corresponding descendants of t_{1}, …, t_{n}; in the fourth case, o_{1} is obtained from e_{1} by replacing the descendants of s_{1}, …, s_{n} with the corresponding descendants of t_{1}, …, t_{n}, respectively. Thus, in o_{1} we can choose the redex u_{1} analogously, and so on. (Note that P ∥(t) depends not only on P and t, but also on the choice of s_{1}, …, s_{k}, but the notation does not give rise to ambiguity.)

Lemma 3.3 Let s_{1}, …, s_{n} be inessential in s, in an OERS R, and let t = (t_{1}//s_{1}, …, t_{n}//s_{n})s. Then t_{1}, …, t_{n} are inessential in t.

Proof. We show by induction on |Q| that if an R_{fS}-reduction Q : s → → o deletes s_{1}, …, s_{n}, then Q∥(t) deletes t_{1}, …, t_{n}; such a Q exists by Lemma 3.1. Let Q = v + Q′, s→^{v}e, and s′_{1}, …, s′_{m} be all the v-descendants of s_{1}, …, s_{n}. By Lemma 3.2.(1), s′_{i} are inessential in e. By Definition 3.6, if v∥(t) : t → o, then o is obtained from e by replacing some inessential subterms that contain s′_{1}, …, s′_{m}, and all the descendants of t_{1}, …, t_{n} also are in the replaced subterms of o. By the induction assumption, the replaced subterms in o are inessential. Hence, by Lemma 3.2.(3), all the descendants of t_{1}, …, t_{n} in o are inessential and, by Lemma 3.2.(1), t_{1}, …, t_{n} are inessential in t.

It follows immediately from Definition 3.6 and the proof of Lemma 3.3 that replacement of inessential subterms in a term does not effect its normal form.

Corollary 3.1 Any term not in normal form, in an OERS, contains an essential redex.

Proof. If all redexes in t were inessential, their replacement by fresh variables would yield a term in normal form containing inessential subterms, a contradiction.

Existence of an unabsorbed redex in any term not in normal form can be proved exactly as in OTRSs [Kha93] (the proof does not use the proof of Corollary 3.1).

Proposition 3.1 Let t be a term in an OERS R and let u be a redex in t. Then u is essential in t iff it is Maranget-needed in t.

Proof. (⇐) Let IE(u, t). Further, let F V (u) = {x_{1}, …, x_{n}}, let f be a fresh n-ary function symbol that does not occur in the left-hand sides of rewrite rules (we can safely add such a symbol to the alphabet, if necessary), and let s = (f(x_{1}, …, x_{n})//u)t. By Lemma 3.3, IE(f(x_{1}, …, x_{n}), s), i.e., there is some reduction P starting from s such that f(x_{1}, …, x_{n}) does not have P -descendants. Let r : f(x_{1}, …, x_{n}) → u be a rule and Q : s → t be the r-reduction step. Obviously, R ∪ {r} is orthogonal. Hence P + Q/P ≈_{st} Q + P/Q and therefore u does not have P/Q-descendants. But P/Q does not contract the residuals of u. Thus u is not Maranget-needed. (⇒) From Definitions 3.2 and 3.1.

4 Relative Notions of Neededness

In this section, we introduce notions of neededness relative to a set of reductions Π and to a set of terms S. We show how all existing notions of neededness can be obtained by specifying Π or S; S-neededness is also a special case of Πneededness. We introduce stability of a set of terms, in an OERS, and show that if S is not stable, contraction of S-needed redexes in a term t need not terminate at a term in S even if t can be reduced to a term in S. It is the aim of the last section to show that if S is stable, then a S-needed strategy is S-normalizing.

Definition 4.1 (1) We call a reduction P starting from a term t in an OERS R external to a component e ⊑ t if there is no redex executed in P whose pattern overlaps with a descendant of e (e can be empty). We call P external to a redex u ⊆ t if P is external to pat(u), i.e., if P doesn’t contract the residuals of u.

(2) Let Π be a set of reductions. We call e ⊑ t Π-needed if there is no P ∈ Π starting from t that is external to e, and call it Π-unneeded otherwise.

(3) We call e ⊑ t P -(un)needed if it is ⟨P ⟩_{L}-(un)needed, where ⟨P ⟩_{L} is the set of all reductions Lévy-equivalent to P.

(4) Let S be a set of terms in R, and let Π_{S} be the set of S-normalizing reductions, i.e., reductions that end at a term in S. We call e ⊑ t S-(un)needed if it is Π_{S}-(un)needed.

(5) If o ⊆ t, then we call o (P, Π, S-)unneeded (needed) if so is Int(o), the component obtained from the subterm o by removing all bound variables. However, if not otherwise stated, we say that a redex u ⊆ t (which is a subterm) is (P, Π, S-)unneeded (needed) if so is its pattern.

(6) We say that P : t → → o S-suppresses e ⊑ t if P is S-normalizing and is external to e. We say that P S-suppresses u ⊆ t if it S-suppresses pat(u), i.e., is S-normalizing and is external to u. (Obviously, a redex or component is S-unneeded iff it is S-suppressed by some S-normalizing reduction.)

We write NE_{(P,Π,M)}(e, t) (UN(e, t)) if e is (P, Π, M)-needed (unneeded).

If o ⊑ t and P : t → → s is external to o, then we call the descendants of o also the residuals of o. A component that does overlap with the pattern of a contracted redex does not have residuals. Note that if u ⊆ t, then P : t → → s is external to pat(u) iff P does not contract the residuals of u, because orthogonality of the system implies that if the pattern pat(v) of a redex v contracted in P does overlap with a residual of pat(u), then pat(u) = pat(v). Hence u is S-needed iff at least one residual of it is contracted in each reduction from t to a term in S (the intended notion of neededness). Obviously, any redex in a term that is not S-normalizable is S-needed; we call such redexes trivially S-needed.

The following definition introduces the property of sets of terms for which it is possible to generalise the Normalization Theorem:

Definition 4.2 We call a set S of terms stable if:

(a) S is closed under permutation: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e, the final term of P/Q is in S; and

(b) S is closed under unneeded expansion: for any e→^{u}o such that e ∉ S and o ∈ S, u is S-needed.

Remark 4.1 Of course, a set closed under reduction is closed under permutation as well. But a set closed under permutation, even if closed under unneeded expansion, need not be closed under reduction. Indeed, consider R = {f(x) → g(x, x), a → b}, and take S = {g(a, a), g(b, b)}. The only one-step S-normalizing reductions are g(a, b) → g(b, b), g(b, a) → g(b, b), f(a) → g(a, a), and f(b) → g(b, b). Therefore, one can check that S is closed under unneeded expansion. Also, S is closed under permutation, since the right-bottom term g(b, b) in the diagram below, which is the only non-trivial diagram to be checked, is in S. However, S is not closed under reduction, since, e.g., g(a, a) → g(b, a), g(a, a) ∈ S, but g(b, a) ∉ S. Note that the second occurrence of a in g(a, a) is S-unneeded, but its residual in g(b, a) is S-needed.

f(a)  \overline{}g(a, a)
[figure]
g(a, b)  g(b, a)
[figure]
[figure: f(b); g(b, b)]
□

The most appealing examples of stable sets, for an OERS, are the set of normal forms [HuLé91], the set of head-normal forms [BKKS87], the set of weakhead-normal forms (a partial result is in [Mar92]), and the set of constructorhead-normal forms for constructor TRSs [Nök94]. The sets of terms having (resp. not having) (head-, constructor-head-) normal forms are stable as well. The graph G_{s} of a term s (which consists of terms to which s is reducible) is closed under reduction, but need not be closed under unneeded expansion. For example, the graph G_{I(x)} = {I(x), x} of I(x) is closed under reduction but is not closed under unneeded expansion: I(I(x)) can be reduced to I(x) by reducing either I-redex (according to the rule I(x) → x). Hence none of the redexes in I(I(x)) are S-needed. Thus the closure of S under unneeded expansion is a necessary condition for the normalization theorem.

We say that a set S of terms is closed under (S)-normalization if any reduct of every S-normalizable term is still S-normalizable. Obviously, sets closed under permutation are closed under normalization as well. Even if S is closed under unneeded expansion, closure of S under normalization is also necessary for the normalization theorem to be valid for S. Indeed, consider R = {f(x) → g(x, x), a → b}, take S = {g(a, b)}, and take t = f(a). Then t → g(a, a) → g(a, b) is an S-needed S-normalizing reduction, while after the S-needed step t → f(b), the term f(b) is not S-normalizable any more (the only redex in f(b) is only trivially S-needed). However, the following example shows that closure of S under normalization (even in combination with closure of S under unneeded expansion) is not enough; closure of S under permutation is necessary.

Example 4.1 Let R = {f(x) → g(x, x), a → b, b → a} and S = {g(a, b)}. Since the reduction preserves the height of a term and the property to be a ground term, only the terms in the following diagram are S-normalizable.

f(a)  \overline{}g(a, a)
[figure]
g(a, b)  g(b, a)
[figure]
[figure: f(b); g(b, b)]

Therefore, it is clear from the diagram that S is closed under normalization. It is easy to see that, in f(a) and f(b), all the redexes are S-needed; hence f(a) → f(b) → f(a) → … is an infinite S-needed reduction that never reaches S (there are many others). One can check that S is closed under unneeded expansion. Thus the reason for the failure of the normalization theorem is that, as it can be seen from the following diagram, S is not closed under permutation.

[figure: f(a); g(a, a); g(a, b); f(b); g(b, b); g(b, b)]

□

Proposition 4.1 A redex u ⊆ t is Maranget-needed iff it is needed w.r.t. the set of all fair reductions starting from t.

Proof. (⇒) Let u be Maranget-needed in t. Then any fair P starting from t should contract a residual of u (to erase it). (⇐) If u is not Maranget-needed, i.e., there is a reduction Q : t → → e in which u is erased and that does not contract the residuals of u, then there is a reduction Q′ such that Q^{∗} = Q + Q′ is fair and obviously u is not Q^{∗}-needed, a contradiction.

Proposition 4.2 A redex u ⊆ t is essential iff u (or pat(u)) is needed w.r.t. the set of all fair reduction starting from t.

Proof. An immediate corollary of Proposition 3.1 and Proposition 4.1.

Lemma 4.1 Let P : t → → s be external to e ⊑ t, and let o ⊆ t be the subterm corresponding to e. Then any descendant of o along P is the subterm corresponding to some P -descendant of e.

Proof. Immediate from Definition 2.3, since P is external to e.

Proposition 4.3 A subterm s ⊆ t is inessential iff there is a reduction that is external to Int(s) and deletes it.

Proof. (⇐) Immediate from Lemma 4.1. (⇒) Let x_{1}, …, x_{n} be the list of occurrences of bound variables in s from left to right, let f be a fresh n-ary function symbol not occurring in left-hand sides of rewrite rules, and let t^{∗} = (f(x_{1}, …, x_{n})//s)t. Since IE(s, t), there is Q starting from t that deletes s. Therefore, it follows from Definition 3.6 that P = ((Q∥t^{∗})∥t) is external to Int(s) and deletes it.

5 A Labelling for OERSs

In Kennaway&Sleep [KeSl89] a labelling is introduced for OCRSs, based on the labelling system of Klop [Klo80], which is in turn a generalization of the labelling system for the λ-calculus introduced by Lévy [Lév78]. Each label of Kennaway&Sleep [KeSl89] is a tuple of labels, built up from a set of base labels. For any OERS R, terms in the corresponding labelled OERS R^{L} are those of R where each subterm has one or more labels, represented as a string of labels. A labelling of a term is initial if all its subterms are labelled by different base labels. The signature of a labelled term is the tuple of all its labels, from left to right. Rules of R^{L} are those of R where pattern-symbols in left-hand sides are labelled by a string of labels except for the head-symbol, which has just one label (a string of length one). Each subterm (including metavariables) in the right-hand side of a rule bears the signature of the corresponding left-hand side. Further, a redex-index of a redex is the maximal depth of nesting in the labels of the corresponding left-hand side of the rule. The index Ind(P) of a reduction P is the maximal redex-index of redexes contracted in it.

The crucial properties of the labelling are given by the following propositions.

Proposition 5.1 [KeSl89] If a step t→^{u}s in an OERS R creates a redex v ⊆ s,

then, for any labelling t^{l} of t, the corresponding step t^{l}→^{u^{l′}}s^{l′′} in the corresponding labelled OERS R^{L} creates a redex v^{l^{∗}} whose label l^{∗} contains the label l′ of u. Thus Ind(u^{l′}) < Ind(v^{l^{∗}}). If w ⊆ s^{l′′} is a residual of a redex w′ ⊆ t^{l}, then w and w′ have the same labels, thus Ind(w) = Ind(w′).

Corollary 5.1 [KeSl89] Let P and Q be co-initial reductions such that P creates a redex u and Q does not contract residuals of any redex of t having a residual contracted in P. Then the redexes in u/(Q/P) are created by P/Q and Q/P is external to u.

Proposition 5.2 [Klo80, Lév78] Any reduction in which only redexes with a bounded redex-index are contracted is terminating.

Remark 5.1 The above propositions are obtained for OCRS, but it is straightforward to carry them over OERSs. □

Definition 5.1 (1) For any co-initial reductions P and Q, the redex Qv in the final term of Q (read as v with history Q) is called a copy of a redex P u if P ≤ Q, i.e., P + Q/P ≈_{L} Q, and v is a Q/P -residual of u; the zig-zag relation ≃_{z} is the symmetric and transitive closure of the copy relation [Lév80]. A family relation is an equivalence relation among redexes with histories containing the zig-zag relation.

(2) For any co-initial reductions P and Q, the redexes Qv and P u are in the same labelling-family if for any initial labelling of the initial term of P and Q, they bear the same labels.

Proposition 5.1 implies that the labelling-family relation is indeed a family relation. As pointed out in [AsLa93], for OERSs in general the zig-zag and labelling family relations do not coincide. Below by family we always mean the labelling-family.

6 The Relative Normalization Theorem

In this section, we present a uniform proof of correctness of the needed strategy that works for all stable sets of ‘normal forms’. Our proof is different from all known proofs because properties of needed and unneeded components are different in the general case (the main difference is that a component under an unneeded component may be needed). However, the termination argument we use is the same as in [KeSl89] and in [Mar92], and is based on Proposition 5.2. The main idea and a proof in the same spirit is already in [Lév80].

Below in this section S always denotes a stable set of terms.

Lemma 6.1 Let t→^{w}s, v ⊆ t, o ⊑ t, and let pat(v) ∩ o = ∅. Further, let v′ ⊆ s be a w-residual of v and o′ ⊑ s be a w-descendant of o. Then pat(v′) ∩ o′ = ∅.

Proof. Immediate from Definition 2.3.

Corollary 6.1 Let F be a set of redexes in t, and let every redex v ∈ F be external to s ⊑ t. Then any development of F is external to s.

Lemma 6.2 Let t→^{v}s, P : t → → o, e ⊑ t, and v be external to e. Then v/P is external to every P -descendant of e.

Proof. By Lemma 6.1, every P -residual of v is externa to each P -descendant of e, and the lemma follows from Corollary 6.1.

Lemma 6.3 (1) Let s_{1}, …, s_{n} ⊑ s be disjoint, let P : s → → e ≠ ∅ be external to s_{1}, …, s_{n}, let P^{∗} : s → → s^{∗}, let s_{1}^{∗}, …, s_{m}^{∗} be all P^{∗}-descendants of s_{1}, …, s_{n} in s^{∗}, and let Q = P/P^{∗} : s^{∗} → → e^{∗}. Then Q is external to s_{1}^{∗}, …, s_{m}^{∗}.

(2) If P S-suppresses s_{1}, …, s_{n}, then Q S-suppresses s_{1}^{∗}, …, s_{m}^{∗}.

Proof. (1) By induction on |P |. Let P = v + P′, let s′_{1}, …, s′_{l} be v-descendants of s_{1}, …, s_{n}, and let s_{1}^{′∗}, …, s_{k}^{′∗} be P^{∗}/v-descendants of s′_{1}, …, s′_{l}. By CR(com) (Theorem 2.1.(4)), s_{1}^{′∗}, …, s_{k}^{′∗} are v/P^{∗}-descendants of s_{1}^{∗}, …, s_{m}^{∗}. By the induction assumption, P′/(P^{∗}/v) is external to s_{1}^{′∗}, …, s_{k}^{′∗}. But by Lemma 6.2 v/P^{∗} is external to s_{1}^{∗}, …, s_{m}^{∗}; hence P/P^{∗} = v/P^{∗} + P′/(P^{∗}/v) is external to s_{1}^{∗}, …, s_{m}^{∗}.

[figure: s; v; P′; e; s^{∗}; P^{∗}; v/P^{∗}; P^{∗}/v; P′/(P^{∗}/v); e^{∗}; P^{∗}/P]

(2) By (1) and closure of S under permutation.

Corollary 6.2 (1) Descendants of S-unneeded redexes of t ∉ S remain Sunneeded.

(2) Residuals of S-unneeded redexes of t ∉ S remain S-unneeded.

Lemma 6.4 (1) Let t→^{u}t′ and e ⊑ s ⊑ t. Then any u-descendant of e is contained in some u-descendant of s.

(2) Let e ⊑ s ⊑ t and NE_{S}(e, t). Then NE_{S}(s, t).

(3) Let u ⊆ t and let s ⊑ pat(u). Then NE_{S}(u, t) iff NE_{S}(s, t).

Proof. (1) By Definition 2.3.

(2) By (1) and Definition 4.1.

(3) From Definition 4.1, since a reduction S-suppresses s iff it S-suppresses u (orthogonality of the system implies that any redex whose pattern contains a symbol from a residual of pat(u) coincides with pat(u) and hence contains a symbol from a residual of s as well).

Note that if a component s ⊑ t is below o ⊑ t, then UN_{S}(o, t) does not necessarily imply UN_{S}(s, t), although the inessentiality of the subterm corresponding to o implies that of the subterm corresponding to e (Lemma 3.2.(3)). Take for example R = {f(x) → g(x), a → b}, and take for S the set of terms not containing occurrences of a. Then S is stable, a is S-needed in f(a), but f(a) is not.

Lemma 6.5 Let t ∉ S, t→^{u}t′, UN_{S}(u, t), and let u′ ⊆ t′ be a u-new redex. Then UN_{S}(u′, t′).

Proof. UN_{S}(u, t) implies existence of P : t → → e that S-suppresses pat(u); thus P is external to u. By Corollary 5.1, P/u is external to u′. Also, P/u is Snormalizing since S is closed under permutation. Hence u′ is S-unneeded.

We call P : t_{0} → t_{1} → … S-needed if it contracts only S-needed redexes.

Theorem 6.1 (Relative Normalization) Let S be a stable set of terms in an OERS R.

(1) Any S-normalizable term t ∉ S in R contains an S-needed redex.

(2) If t ∉ S is S-normalizable, then any S-needed reduction starting from t eventually ends at a term in S.

Proof. (1) Let P : t → → s→^{u}e be an S-normalizing reduction that doesn’t contain terms in S except for e. By the stability of S, u is S-needed. By Corollary 6.2.(2) and Lemma 6.5, it is either created by or is a residual of an S-needed redex in s, and (1) follows by repeating the argument.

(2) Let P : t → → s be an S-normalizing reduction that doesn’t contain terms in S except for e, and let Q : t→^{u_{0}}t_{1}→^{u_{1}} … be an S-needed reduction. Further, let Q_{i} : t→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i} and P_{i} = P/Q_{i} (i ≥ 1). By Proposition 5.1, Ind(P_{i}) ≤ Ind(P). Since Q is S-needed and P_{i} is S-normalizing (by the closure of S under permutation), at least one residual of u_{i} is contracted in P_{i}. Therefore, again by Proposition 5.1, Ind(u_{i}) ≤ Ind(P_{i}). Hence Ind(Q) ≤ Ind(P) and Q is terminating by Proposition 5.2.

t  [figure: P] s

[figure: t_{i}; Q_{i}; P_{i}]

[figure: t_{i+1}; u_{i}; P_{i+1}]

[figure]

Lemma 6.6 Let t be S-normalizable, let t→^{u}s, e ⊑ t, NE_{S}(e, t), and pat(u)∩e = ∅. Then e has at least one S-needed u-residual in s. In particular, any S-needed redex v ⊆ t different from u has an S-needed residual.

Proof. Let P : s → → o be an S-needed S-normalizing reduction; there is one by Theorem 6.1. Then if all u-residuals of e were S-unneeded, P would S-suppress them, and u + P would S-suppress e, a contradiction.

We call a stable set S regular if S-unneeded redexes cannot duplicate Sneeded ones. One can show using Lemma 6.6 (e.g., as in [KeSl89] or in [Kha88]) that, for any regular stable S, the S-needed strategy is S-hypernormalizing. That is, a term is S-normalizing iff it does not have a reduction which contracts infinitely many S-needed redexes. However, this is not the case for some irregular stable S. Indeed, consider the OTRS R = {f(x) → h(f(x), f(x)), a → b} and take for S the set of terms not containing occurrences of a. Then the reduction f(a) → h(f(a), f(a)) → h(f(b), f(a)) → h(f(b), h(f(a), f(a))) → h(f(b), h(f(b), f(a))) → … contracts infinitely many S-needed redexes, while f(a) → f(b) is S-normalizing. This example shows also that multistep S-needed reductions need not be S-normalizing — just omit in the above reduction the initial step and group each pair of consecutive steps as a single multistep. Recall that multistep needed reductions are normalizing in the λ-calculus [Lév80]. The same holds for all regular stable S; this follows immediately from hypernormalization of the S-needed strategy for such S.

7 Conclusions and Future Work

We have introduced a relative notion of neededness and proved the Relative Normalization Theorem in OERSs. We expect that the same results can be proved for other higher-order rewriting systems too. Analogous questions arise for other strategies. For example, how can one construct reductions that avoid head-normal forms? Besides strong sequentiality for normal forms studied in Huet&Lévy [HuLé91], strong sequentiality is studied w.r.t. head-normal forms in Kennaway [Ken94]. Investigation of relative strong sequentiality and related to it strictness analysis (see e.g., [Nök94]) seems also as an interesting topic for future research.

Acknowledgements

We thank J. R. Kennaway, F. van Raamsdonk, and M. R. Sleep for useful discussions, and J.-J. Lévy, L. Maranget, and P.-A. Melliès for help in overcoming difficulties in an early version of the paper. The use of empty descendants in the definition of descendants of components was suggested by L. Maranget. Some of the diagrams were drawn using P. Taylor’s diagram package.

References

[Acz78] Aczel P. A general Church-Rosser theorem. Preprint, University of Manchester, 1978.

[AEH94] Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of the 21^{st} ACM Symposium on Principles of Programming Languages, POPL’94, Portland, Oregon, 1994.

[AsLa93] Asperti A., Laneve C. Interaction Systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, vol. 11, Cambridge University Press, 1993, p. 1-48.

[Bar84] Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.

[BKKS87] Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed Reduction and spine strategies for the lambda calculus. Information and Computation, v. 75, no. 3, 1987, p. 191-231.

[DeJo90] Dershowitz N., Jouannaud J.-P. Rewrite Systems. In: J. van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 6, vol. B, 1990, p. 243-320.

[Gar94] Gardner P. Discovering needed reductions using type theory. In: Proc. of the 2^{nd} International Symposium on Theoretical Aspects of Computer Software, TACS’94, Springer LNCS, v. 789, M. Hagiya, J. C. Mitchell, eds. Sendai, 1994, p. 555-574.

[HuLé91] Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In: Computational Logic, Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, eds. MIT Press, 1991.

[Ken94] Kennaway J. R. A conflict between call-by-need computation and parallelism. Workshop on conditional (and typed) term rewriting systems, Jerusalem, 1994.

[KeSl89] Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in regular combinatory reduction systems. Preprint, School of Information Systems, University of East Anglia, Norwich, 1989.

[Kha88] Khasidashvili Z. β-reductions and β-developments of λ-terms with the least number of steps. In: Proc. of the International Conference on Computer Logic COLOG’88, Tallinn 1988, Springer LNCS, v. 417, P. Martin-Löf and G. Mints, eds. 1990, p. 105–111.

[Kha90] Khasidashvili Z. Expression Reduction Systems. Proceedings of I. Vekua Institute of Applied Mathematics of Tbilisi State University, vol. 36, 1990, p. 200-220.

[Kha92] Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.

[Kha93] Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of the 5^{th} International Conference on Rewriting Techniques and Applications, RTA’93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.

[Kha94] Khasidashvili Z. On higher order recursive program schemes. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172-186.

[Klo80] Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980.

[Klo92] Klop J. W. Term Rewriting Systems. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1-116.

[KOR93] Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction systems: introduction and survey. In: To Corrado Böhm, J. of Theoretical Computer Science 121, 1993, p. 279-308.

[Lév78] Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de

l’Université de Paris VII, 1978. [Lév80] Lévy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry:

Essays on Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.

[Mar92] Maranget L. La stratégie paresseuse. Thèse de l’Université de Paris VII, 1992.

[Nip93] Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of the 1^{st} International Conference on Typed Lambda Calculus and Applications, TLCA’93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds. Utrecht, 1993, p. 306-317.

[Nök94] Nöcker E. Efficient Functional Programming. Compilation and Programming

Techniques. Ph. D. Thesis, Katholic University of Nijmegen, 1994.

[Oos94] Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph. D. Thesis, Free University of Amsterdam, 1994.

[OR94] Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc. of the 3^{rd} International Conference on Logical Foundations of Computer Science, ‘Logic at St. Petersburg’, LFCS’94, Springer LNCS, vol. 813, Narode A., Matiyasevich Yu. V. eds. St. Petersburg, 1994. p. 379-392.

[Pkh77] Pkhakadze Sh. Some problems of the Notation Theory (in Russian). Proceedings of I. Vekua Institute of Applied Mathematics of Tbilisi State University, Tbilisi, 1977.

[Wol93] Wolfram D.A. The Clausal Theory of Types. Cambridge Tracts in Theoretical Computer Science, vol. 21, Cambridge University Press, 1993.

This article was processed using the LaTEX macro package with LLNCS style