Minimal and Optimal Relative Normalization in Orthogonal Expression Reduction Systems

J. Glauert and Z. Khasidashvili

Technical Report SYS-C94-06

UEA Norwich, UK

Minimal and Optimal Relative Normalization in Orthogonal Expression Reduction Systems

John Glauert and Zurab Khasidashvili ^{1} jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk School of Information Systems University of East Anglia Norwich NR4 7TJ, UK

Technical Report SYS-C94-06

Abstract

We study normalization relative to desirable sets S of ‘normal forms’ by generalizing Huet&Lévy theory of ‘normalization by neededness’. 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. Further, we prove existence of minimal normalizing reductions for regular stable sets of normal forms. For example, the sets of normal forms, head-normal-forms, and weak head-normal-forms, in the λ-calculus, are all stable and regular. Finally, we generalize Lévy’s Optimality theorem to the case of all stable sets of normal forms, and establish a relationship between relative minimal and optimal reductions, revealing a conflict between minimality and optimality of a reduction – for regular stable sets of normal forms, a term need not posses a reduction that is minimal and optimal at the same time.

All this results are obtained in the framework of orthogonal (left-linear and non-ambiguous) Expression Reduction Systems, a formalism for Term Rewriting Systems with bound variables and substitutions.

\begin{matrix}c \\ ◯ \end{matrix} J. Glauert & Z. Khasidashvili, UEA Norwich, 1994

1Supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300

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 [CuFe58]. 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 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) [Kha90] and Klop’s Orthogonal Combinatory Reduction Systems (OCRSs) [Klo80]. 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, 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, for the case of the λ-calculus, 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. 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 (essentiality makes sense for all subterms, not only for redexes). In [Mar92], Maranget studied also a strategy that computes a 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 NF of normal forms, Maranget-neededness is neededness w.r.t. all fair reductions, head-neededness 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 parallel moves: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e not containing terms in S, 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 S-unneeded redexes may contain S-needed ones – 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.

We further develop a theory of minimal and optimal reduction in the framework of relative normalization, and establish a relationship between them. While normal forms are unique in an OERS, a term may have many S-normal forms. A reduction P : t → → s with t ∉ S and s ∈ S is said to be S-minimal if it does no more work than any other S-normalizing reduction Q : t → → e, i.e., the residual P/Q of P under Q is empty. The final term in the S-minimal reduction is said to be an S-minimal S-normal form.

S-minimal S-normal forms are useful to compute since any other S-normal form is accessible from the S-minimal one. Further, strategies computing partial results (such as head-normal-forms (hnfs) and weak hnfs, in the λ-calculus) usually compute minimal reductions, and it is natural to ask whether optimality can be achieved while retaining minimality. The prime example is the leftmost outermost strategy computing the so called ‘principal’ hnf and whnf of a λ-term, and used in constructions of Böhm [Bar84] and Lévy-Longo [Lév76, Lon83] (also called lazy [AbOn93]) trees, respectively. These trees represent the values of the term according to different semantics – Böhm semantics and Lévy- or lazy semantics, respectively. Clearly this property of minimality is not useful for full normal forms, but full normal forms are rarely used in the practice of functional programming.

Our research on minimal S-normalizing reductions was inspired by a result of Maranget [Mar92], stating that standard reductions are minimal among reductions computing a ‘stable prefix’ of a given term. The earliest (to our knowledge) minimality result was obtained by Berry and Lévy in [BeLé79], where existence of minimal reductions was shown for any (finite or infinite) approximation of a possibly infinite value of a term, for Recursive Program Schemes. Minimal reductions were used to design optimal reductions, both finite and infinite, and minimality and optimality of outermost complete family-reductions were shown. Minimal and optimal reductions were studied also in arbitrary interpretations, not only for term (or Herbrand) models.

In this paper, we restrict ourselves to finite reductions only, and study only syntactic properties. We show that, for any stable and regular S, any S-normalizable term not yet in S possesses an S-needed S-unabsorbed redex, and repeated contraction of such redexes gives S-minimal S-normalizing reductions. These redexes play the role of standard redexes w.r.t. S, since they are S-needed and cannot be duplicated. We further give a sufficient and necessary criterion for an S-normalizing reduction to be S-minimal. We show also that S-minimal reductions need not exist if S is stable but is not regular.

To give the characterization of S-minimal reductions, we introduce a relative notion of essentiality. A subterm s ⊆ t is said to be S-essential if it has a descendant under at least one S-normalizing reduction of t. Essentiality [Kha93, Kha88] of subterms in normalizable terms coincides with NF -essentiality, i.e. essentiality w.r.t. the set of normal forms. NF -essentiality of redexes in normalizable terms coincides with both Huet&Lévy and Maranget’s concepts of neededness, while in the general case, for stable S, the two concepts are different. All S-needed redexes are S-essential. S-unneeded redexes may be S-essential, in which case they contribute to the minimal S-normal form, or can be S-inessential in which case they will be erased under any reduction to S-normal form. Inessentiality is related to the notion of garbage – an inessential subterm may be replaced by any term without affecting the normal form. However, for certain stable and even regular S, replacing an S-inessential subterm by another term may lead to an S-essential subterm at the same position, and the S-normal form of the term can change.

We show that an S-normalizing reduction is S-minimal iff it contracts S-erased redexes, i.e., the redexes that do not have residuals under any S-normalizing reduction. Further, we show that a redex u in t is S-erased iff every one of its residuals is either S-needed or S-inessential.

Our study of optimal normalization w.r.t. stable sets S is a generalization of Lévy’s optimality theory [Lév80], developed for the λ-calculus. The generalization is rather straightforward, since a suitable labelling system allowing us to define a family relation in OERSs, due to Kennaway&Sleep [KeSl89], is available. We show that complete S-needed family-reductions, which contract all members of a family containing an S-needed redex in a multi-step, are optimal in the sense that they reach S in the least number of family-reduction steps.

It is easy to see that S-needed complete family reductions, though optimal, need not be Sminimal, because they may contract S-unneeded redexes that are S-essential. It is tempting to think that contracting only the S-needed redexes of S-needed families could yield S-optimal reductions that are S-minimal at the same time. We show however that this is not the case either in the λ-calculus or in OTRSs.

The rest of the paper is organized as follows. In the next section, we review Expression Reduction Systems, a formalism for higher order rewriting that we use here [Kha90, Kha92]. 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. In section 7, we study S-minimal reductions for regular stable sets S. In section 8, we study the relative notion of essentiality, and in section 9, reductions standard w.r.t. regular stable sets. In section 10, we prove the Relative Optimality theorem. Finally, in section 11, we relate relative optimal and minimal reductions. The conclusions appear in section 12. The results in Sections 3 – 6 are published as [GlKh94], there we in addition study relative neededness and essentiality properties of components of terms in OERSs, which are occurrences of contexts. This requires introduction of notions of descendants and residuals for components.

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 higher-order rewriting) as in the λ-calculus [Bar84] and its extensions. Restricted rewriting systems with substitutions were first studied in Pkhakadze [Pkh77] and Aczel [Acz78]. Several interesting formalisms have been introduced later [Kha90, 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 sign σ, as well as any corresponding quantifier σx_{1} … x_{m} 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 the left to right 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 is written as μ(λxA) → (μ(λxA)/x)A.

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. Subterms of a redex corresponding to metavariables are arguments of the redex, and the rest is its pattern; patterns and arguments are defined similarly for the contractum of the redex if the right-hand side of the rule is a simple metaterm. Note that the use of metavariables in rewrite rules of ERSs 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]. Therefore, S-redexes are similar to simultaneous let-expressions.

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 if P denotes a reduction of t to s. |P | denotes the length of P. P +Q denotes the concatenation of P and Q. F V (t) denotes the set of free variables of t.

We now give a brief but complete definition of descendants of subterms as introduced in [Kha88, Kha93, Kha92] for the λ-calculus, TRSs, and ERSs, respectively. ^{2} First, we need to split an ERS R into a TRS-part R_{f} and the substitution-part S. For any ERS R, which we assume does not contain symbols S^{n+1}, we define R_{fS} =_{def} R_{f} =_{def} R if R is simple. Otherwise, we define R_{fS} =_{def} R_{f} ∪ S, where 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 β_{f} : Ap(λxA, B) → S^{2}xBA. Obviously, an R-step can be refined into an R_{f}-step, followed by a number of S-steps, evaluated say in right to left order. For example, the refinement of the β-step Ap(λxt, s) →_{β} (s/x)t would be Ap(λxt, s) →_{β_{f}} S^{2}xst →_{S} (s/x)t. The notion of refinement generalizes to R-reductions with 0 or more steps.

Definition 2.3 Let t →^{u} s be an R_{f}-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 call them (u-)descendants of o. Correspondingly, subterms of o have 0 or more descendants. The descendant of each patternsubterm (i.e., a subterm rooted within the pattern) of u is e. It is clear what is to be meant by descendants of a subterm of t that is not in u.

2Klop [Klo92] gives a slightly different notion of descendant for TRSs.

Technical Report SYS-C94-06 UEA Norwich, UK

For example, in the step t = f(g(a)) → b = s according to the rule f(g(x)) → b, the descendant of both pattern-subterms f(g(a)) and g(a) of t in s is b, and a doesn’t have a descendant in s.

Definition 2.4 Let t = 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}] = s be an S-step.

Then the descendants of an argument t_{i} of u are the substituted occurrences of t_{i} in s; so t_{i} has the same number of descendants as the number of free occurrences of x_{i} in t_{0}. Subterms of t_{i} have the same number of descendants, which are the corresponding subterms occurring in the descendants of t_{i}. All subterms of t_{0} have exactly one descendant (the descendants of the free occurrences of x_{1}, …, x_{n} in t_{0} are the substituted subterms). The descendant of the contracted redex u itself is its contractum. It is clear what is to be meant by descendants of a subterm of t rooted within C[ ].

For example, in the step o = Sxaf(x) → f(a) = e, the descendant of a ⊆ o, as well as of the bound occurrence of x in f(x), is the occurrence of a in e. The descendant of f(x), as well as of o itself, is e.

The notion of descendant extends by transitivity to arbitrary R_{fS}-reductions. If P is an Rreduction, then P -descendants are defined to be the descendants under the refinement of P. The ancestor relation is converse to that of descendant. If t →^{u} s in R, then the descendants of any redex v ≠ u are called residuals of v; a redex in s is called a new redex or a created redex if it is not a residual of a redex of t. The notion of residual extends by transitivity to arbitrary R-reductions.

Recall that P : t → → s and Q : t → → e are Hindley-equivalent, written P ≈_{H} Q, if s = e and the residuals of any redex of t under P and under Q are the same redexes in s; and are strictly equivalent, written P ≈_{st} Q, if s = e and the descendants of any subterm of t under P and under Q are the same subterms in s [Kha88].

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 redex-patterns 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 case of OTRSs [HuLé91] and 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év78]. P ⊔Q abbreviates P +Q/P. We write P ⊴ Q if P/Q = ∅ (⊴ is the Lévy-embedding relation); P and Q are called Lévy-equivalent, strongly-equivalent, or permutation-equivalent (written P ≈_{L} Q) if P ⊴ Q and Q ⊴ P. It follows immediately from the definition of / that if P, P′, Q 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′. This is all well known, and we do not give more details here.

Below, we use the following strong and strict Church-Rosser properties:

Theorem 2.1 (1) [Klo80] (Strong Church-Rosser) For any co-initial reductions P and Q in an OERS, P + Q/P ≈_{L} Q + P/Q; and if P ≈_{L} Q, then P ≈_{H} Q.

(2) [Kha92] (Strict Church-Rosser) Let P ≈_{L} Q, in an OERS. Then P ≈_{st} Q.

3 Neededness, Essentiality and Unabsorbedness

In this section, we recall Huet&Lévy and Maranget’s notions of neededness, and relate them to the notion of essentiality, in OERSs. We also prove existence of an unabsorbed, hence 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 it 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 its descendants 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].

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 (1) Let P : t → t_{1} → … and u ⊆ t_{i}. Then u is erased in P if u does not have residuals in t_{j} for some j > i. P is fair if each redex in any t_{i} is erased in P [Klo92].

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

(3) We say that P : t → t_{1} → … deletes o ⊆ t_{i} if o doesn’t have descendants in t_{j} for some j > i.

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

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 Theorem 2.1.(2) instead of the CR theorem.

The following lemma follows from Theorem 2.1.(2); proofs are the 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).

Proof (1) (⇒) Let IE(s, t). Then some Q : t → → e deletes s. Then, by Theorem 2.1.(2), Q/P deletes all P -descendants of s. (⇐) If all P -descendants of s are inessential in t′, there is an N : t′ → → s′ that deletes them, and P + N deletes s, i.e., IE(s, t). (2) is immediate from the definition of descendant relation. (3) follows from (2). The contractum of u is the unique descendant of u, as well as of s. Hence (4) follows from (1).

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.5 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}; obviously, u_{0} is an R_{f}-redex too.

(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 one of the 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 contractum 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.5 and Lemma 3.2, 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.5 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 t 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.

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.

We now proof existence of an unabsorbed redex in any term not in normal form, in an OERS; the proof is exactly as in OTRSs [Kha93] (it does not use the proof of Corollary 3.1).

Lemma 3.4 Let P : t_{0} →^{u_{0}} t_{1} →^{u_{1}} … → t_{n}. Then for any outermost redex v ⊆ t_{n} there is an unabsorbed in P redex w ⊆ t_{0} that has a descendant s ⊆ t_{n} containing a pattern-subterm e of v.

Proof By induction on |P |. If |P | = 0, then the lemma is obvious. So suppose P :

t_{0} → →^{P′} t_{n−1} →^{u_{n−1}}t_{n}.

(a) Let v be a residual of a redex v′ of t_{n−1}. Further, let v^{∗} = v′ if v′ ⊈ u_{n−1} and v^{∗} = u_{n−1} otherwise. Since v is outermost, v^{∗} is outermost as well. By the induction assumption, a descendant s′ ⊆ t_{n−1} of w ⊆ t_{0} contains a pattern-subterm of v^{∗} (s′ is the only descendant of w since w is unabsorbed in P′ by the induction assumption). Therefore, by Lemma 3.2.(2), s′, and hence also w, have a descendant that contains a pattern-subterm of v, and w is unabsorbed in P.

(b) Assume now that v is created by u_{n−1}. Then u_{n−1} is outermost and, by the induction assumption, a pattern-subterm e′ of u_{n−1} is contained in a descendant s′ of w (the only one). Let e be the maximal common subterm of v and the contractum of u_{n−1}. Then e is a patternsubterm of v. Since e′ is a pattern-subterm of u_{n−1}, its descendant is the contractum of u_{n−1} and hence contains e. By Lemma 3.2.(2), s′, and hence also w, have a descendant s that contains the pattern-subterm e of v. So w is unabsorbed in P as well.

Lemma 3.5 For any reduction P : t → → s starting from a term t not in normal form there is an outermost redex u in t that is unabsorbed in P.

Proof If |P | = 0 or |P | > 0 and s is not in normal form, then the lemma follows immediately from Lemma 3.4. Otherwise, let P : t → → s′ →^{v} s. By Lemma 3.4 there is an unabsorbed in t → → s′ redex u ⊆ t whose only descendant contains a pattern-subterm of v. Thus u has a descendant in s that is not in a redex-argument, since s is in normal form. Hence, u is unabsorbed in P.

Lemma 3.6 Let u be absorbed in P : t → → s and let Q : t → → e. Then u is absorbed in Q⊔P.

Proof It suffices to prove the lemma for |Q| = 1, i.e., Q = w for a redex w in t. The rest follows by induction on |Q|. Furthermore, we can assume that u is absorbed in the last step of P, i.e., there is a redex v created in the last step of P and containing the only descendant o of u in its argument. If o does not have a w/P -descendant, then, by Theorem 2.1.(2), u does not have (w ⊔ P)−descendants, so u is absorbed in w ⊔ P (otherwise its descendants cannot be deleted). If o has a w/P -descendant o′, then, by Lemma 3.2.(2), v also has a w/P -descendant that contains o′. Since in w/P only residuals of w are contracted and v is a new redex, v has a residual v′ that contains o′. But, by Theorem 2.1.(2), o′ also is a (w ⊔ P)−descendant of u. Hence, u is absorbed in w ⊔ P.

Proposition 3.2 Let t be a term not in normal form in an OERS. Then there is an unabsorbed outermost — hence essential — redex in t.

Proof If, for any outermost redex u_{i} of t, there is a reduction P_{i} that absorbs u_{i} (i = 1, …, k), then, by Lemma 3.6, P_{1} ⊔ … ⊔ P_{k} absorbs all redexes u_{i}, contrary to Lemma 3.5.

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 Section 6 to show that if S is stable, then a S-needed strategy is S-normalizing.

Definition 4.1 (1) We call P : t → → o external to a redex u ⊆ t if P doesn’t contract the residuals of u.

(2) We say that P S-suppresses u if P is S-normalizing and is external to u.

(3) We say that P discards u if P is external to u and u/P = ∅.

Definition 4.2 (1) Let Π be a set of reductions in an OERS R. We call a redex u ⊆ t Πneeded if at least one residual of it is contracted in every reduction in Π starting from t, and call Π-unneeded otherwise.

(2) Let S be a set of terms in an OERS R. We call a redex u ⊆ t S-needed, written NE_{S}(u, t), if at least one residual of it is contracted in any reduction from t to a term in S, and call it S-unneeded, written UN_{S}(u, t), otherwise. (Thus u is S-needed iff it is Π_{S}-(un)needed, where Π_{S} be the set of all S-normalizing reductions, i.e., reductions that end at a term in S.)

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.3 We call a set S of terms stable if:

(a) S is closed under parallel moves: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e that doesn’t contain terms in S, 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 parallel moves as well. But a set closed under parallel moves, 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 parallel moves, 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 weak-head-normal forms (a partial result is in [Mar92]), and the set of constructor-head-normal forms for constructor TRSs [Nök94]. 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 any Snormalizable term is still S-normalizable. Obviously, sets closed under parallel moves 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 parallel moves 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 parallel moves.

[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 Π_{f} 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 that discards u, then there is a reduction Q′ such that Q^{∗} = Q + Q′ is fair, and obviously Q^{∗} is external to u, i.e., u is not Π_{f}-needed.

Proposition 4.2 A redex u ⊆ t is essential iff 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.

5 A Labelling for OERSs

In Kennaway&Sleep [KeSl89] a labelling is introduced for OCRSs, based on Klop’s labelling system [Klo80], which is in turn a generalization of Lévy’s original labelling system for the λ-calculus [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′).

Proof Easy from definition of the labelling.

Corollary 5.1 [KeSl89] Let P and Q be co-initial reductions, in an OERS R, 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 a labelled OERS R^{L}, in which only redexes with a bounded redex-index are contracted is terminating.

Proof Same as in the case of OCRSs [Klo80].

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 labellingfamily 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 S of ‘normal forms’. Our proof is different from all known proofs because properties of needed and unneeded redexes are different in the general case (the main difference is that S-unneeded redexes may contain S-needed ones). However, the termination argument [figure: t_{0}; v_{0} = P_{1}; t_{1}; t_{n−1}; v_{n−1}; t_{n}; o_{0}; Q_{0}; P′_{1}; o_{1}; Q_{1}; t_{n−1}; Q_{n−1}; P′_{n}; o_{n}; Q_{n}]

Figure 1: Preservation of External Reductions

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

Further, we also prove a Relative Hypernormalization theorem for all regular stable sets of final terms, in OERSs, and demonstrate that the theorem fails for some irregular stable sets.

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

Definition 6.1 We call P external to a set of redexes F ⊆ t if P doesn’t contract residuals of redexes in F.

Lemma 6.1 Let P : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{n} be external to F = {u_{1}, …, u_{n}} ⊆ t_{0}, and let Q_{0} :

t_{0} → → o_{0}. Then P′ = P/Q_{0} is external to F′ = F/Q_{0}. If P is S-normalizing, then so is P′.

Proof Let P_{i} : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{i}, Q_{i} = Q_{0}/P_{i}, and P′_{i+1} = v_{i}/Q_{i}, 0 ≤ i < n (see Figure 1).

Since P is external to F, we have for each i that v_{i} ∉ F/P_{i}. Therefore, v_{i}/Q_{i} ∩ F/(P_{i} + Q_{i}) = ∅ (since the residuals of different redexes are different). Thus, by Theorem 2.1, v_{i}/Q_{i} ∩ F/(Q_{0} + P′_{1} + … + P′_{i}) = ∅. Hence, P′_{i+1} is external to F′/(P′_{1} + … + P′_{i}). This means that P′ is external to F′. If P is S-normalizing, then so is P′, by the closure of S under parallel moves.

Corollary 6.1 For any stable S, residuals of S-unneeded redexes of a term t under any reduction starting from t remain S-unneeded.

Lemma 6.2 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 u; thus P is external to u. By Corollary 5.1, P/u is external to u′. Also, P/u is S-normalizing since S is closed under parallel moves. Hence u′ is S-unneeded.

We call P : t_{0} → t_{1} → … S-(un)needed if it contracts only S-(un)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 reaches 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.1 and Lemma 6.2, 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). Let R^{L} be the corresponding labelled OERS of R, let t have an initial labelling, and assume that P and Q are reductions in R^{L}. 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 parallel moves), 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]

Notation Below t↓_{S} will denote that t is S-normalizable, i.e., reducible to a term in S.

Lemma 6.3 Let t ↓_{S} and let t→^{u}s. Then 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 v were S-unneeded, P would S-suppress them, and u + P would S-suppress v, a contradiction.

We summarize the neededness properties of residuals and created redexes, established in Corollary 6.1, Lemma 6.2, and Lemma 6.3, in the following proposition.

Proposition 6.1 (1) Residuals of S-unneeded redexes in a term t ∉ S remain S-unneeded.

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

(3) Let t↓_{S}, t→^{u}s, v ⊆ t be S-needed, and v ≠ u. Then v has an S-needed residual in s.

As mentioned above, for some S, S-unneeded redexes may contain S-needed ones. 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. Hence the following definition is justified.

Definition 6.2 We call a stable set S regular if S-unneeded redexes cannot duplicate S-needed ones.

Definition 6.3 We call P S-quasi-needed if NE_{S}|P | = ∞, where NE_{S}|P | denotes the number of S-needed steps in P. We call P S-semi-needed if it can be expressed as P = P_{1} + P_{2}, where P_{1} is S-needed and P_{2} is S-unneeded. In the latter case, we call P_{1} the S-needed part of P, and call P_{2} the S-unneeded part of P.

In the following definition, we describe an algorithm that, for a regular stable R in an OERS, transforms any finite reduction P into an R-semi-needed reduction Lévy-equivalent to P, and any R-quasi-needed reduction Q into an infinite R-needed reduction. The regularity of R is essential for termination of the transformation process, and for preservation of R-quasi-neededness of the reduction under transformation. The latter property is crucial for our method of proving the Relative Hypernormalization theorem.

Definition 6.4 Let Red be the set of all reductions in an OERS R, let R be a regular stable set of terms in R, and let Red^{∗} be the set of R-semi-needed reductions. We define a function K : Red → Red^{∗} as follows:

(a) Let P be a finite reduction. K(P) is an R-semi-needed reduction obtained from P in the following way: find in P the first from the left subreduction P_{0} : t→^{u}s→^{v}o such that UN_{R}(u, t) and NE_{R}(v, s). Let P = P_{1} + P_{0} + P_{2}. By Proposition 6.1.(2), v is a residual of a redex v′ ⊆ t, which is R-needed by Proposition 6.1.(1). Since R is regular, v is the only residual of v′, hence P_{0} and P′_{0} = v′ + u/v′ are both complete developments of the set u, v′ ⊆ t. Now replace P_{0} by P′_{0} in P. Transform the obtained reduction P′ in the same way, and so on, as long as possible. Obviously, the number of R-unneeded steps in P′ preceding v′ is less than the number preceding v in P, and the number of R-needed steps in P and P′ coincide. Therefore, the procedure terminates eventually. The result is K(P). Obviously, P ≈_{L} K(P).

(b) Let NE_{R}|P | < ∞ (|P | = ∞ is possible). P can be expressed as P = P_{1} + P_{2}, where P_{2} is R-unneeded and the last step in P_{1} is R-needed. Then we take K(P) = K(P_{1}) + P_{2} (this is possible since P_{1} ≈_{L} K(P_{1})). Obviously, K(P) ∈ N^{∗} and P ≈_{L} K(P).

(c) Let NE_{R}|P | = ∞. Suppose that P_{i} is the initial part of P with a length i and Q_{i} is the R-needed part of K(P_{i}). Let |Q_{i}| = m_{i}. By definition, K(P) is the reduction whose initial part of the length m_{i} coincides with Q_{i} (i = 0, 1, …). It follows from (a)-(b) that if i < j, then Q_{i} is an initial part of Q_{j}, so K(P) is defined correctly. Obviously, K(P) is R-needed and hence K(P) ∈ Red^{∗}.

Lemma 6.4 Let P be a finite or infinite reduction in an OERS, and let R be regular.

(1) If P ends at a term in R, then the R-needed part of K(P) ends at a term in R as well.

(2) If NE_{R}|P | = ∞, then K(P) is R-needed, and is infinite.

Proof (1) follows from the stability of R — K(P) is R-semi-needed, it ends at R, and the step of K(P) entering R is R-needed. (2) follow immediately from Definition 6.4.

Lemma 6.5 Let t_{0} have an R-quasi-needed reduction and t_{0}→^{u}s_{0}. Then s_{0} also has an Rquasi-needed reduction.

Proof By Lemma 6.4, t_{0} has an infinite R-needed reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} . . .. Let F_{i} = u/(u_{0} + … + u_{i−1}), i = 0, 1, . . .. We can construct the diagram in Figure 2. It follows from [figure: t_{0}; u_{0}; t_{1}; u_{1}; t_{2}; s_{0}; u = F_{0}; u_{0}/F_{0}; s_{1}; F_{1}; u_{1}/F_{1}; s_{2}; F_{2}]

Figure 2: Preservation of Quasi-needed Reductions

finiteness of developments that there are infinitely many numbers k such that u_{k} ∉ F_{k} (otherwise there should be a number m such that t_{m}→^{u_{m}}t_{m+1} →^{u_{m+1}} … is an infinite F_{m}-development). By Proposition 6.1.(3), u_{k} ∉ F_{k} and NE_{R}(u_{k}, t_{k}) imply that u_{k} has at least one R-needed F_{k}- residual in s_{k}, i.e. u_{k}/F_{k} contains at least one R-needed step. Hence P/u is R-quasi-needed.

Theorem 6.2 (Relative Hypernormalization) Let R be a regular stable set of terms in an OERS R, and let t ∉ R be a term in R. Then t has an R-normal form iff it does not possess a reduction in which infinitely many times R-needed redexes are contracted.

Proof (⇒) Let t → →^{P} s ∈ R. Suppose on the contrary that there is an R-quasi-needed Q starting from t. Then by Lemma 6.5 Q/P is R-quasi-needed as well. By closure of R under parallel moves, infinitely many terms of Q/P are in R, and it follows from the proof of Lemma 6.5 that infinitely many of them contain R-needed redexes – a contradiction, since terms in R do not contain R-needed redexes. (⇐) By Theorem 6.1.(1), one can repeatedly contract R-needed redexes in t, unless a term in R is reached; the latter is inevitable since t doesn’t have an infinite R-needed reduction.

The following example shows that the above Hypernormalization Theorem fails for irregular stable sets.

Example 6.1 Consider 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 R; this follows immediately from hypernormalization of the R-needed strategy.

7 Minimal Relative Normalization

In this section, we define S-unabsorbed, persistently S-needed, and S-erased redexes, and show that each class is a strict subset of the next when S is regular. Further, we define S-minimal reductions as minimal w.r.t. Lévy-embedding ⊴ among co-initial S-normalizing reductions, and show that, when S is regular, an S-normalizing reduction is S-minimal iff it is S-erased, i.e., contracts only S-erased redexes. But S-erased reductions need not be S-needed, and again for regular S, we show existence of S-unabsorbed S-normalizing reductions, which are S-needed S-minimal reductions. We show that S-minimal reductions need not exist for irregular stable S.

Definition 7.1 (1) We call u ⊆ t persistently S-needed if all residuals of u are S-needed.

(2) We call u ⊆ t S-erased if u doesn’t have a residual under any S-normalizing reduction (it may have descendants). We call a reduction S-erased if it only contracts S-erased redexes.

Note that every persistently S-needed redex is S-needed, but S-erased redexes need not be (e.g., when S is the set of normal forms and the OERS has an erasing rule, say f(x) → a). The following example illustrates the introduced concepts using a simple TRS.

Example 7.1 Consider an orthogonal TRS R = {f(x) → g(x, h(x)), h(x) → c, a → b}, consider a term (redex) u = f(a), and the following sets of terms in R: the set S_{1} of normal forms; the set S_{2} of terms not containing a redex on the left-spine (i.e., not containing a redex with the top symbol on the left-spine, when the term is considered as a tree); the set S_{3} of terms not containing occurrences of a; and the set S_{4} of terms not containing a on the right-spine. Then, for the two redexes u and a in u = f(a), we have the following:

1. u is S_{1}-needed, persistently S_{1}-needed, and S_{1}-erased. a ⊆ u is S_{1}-needed but not persistently S_{1}-needed (since the second residual of a in g(x, h(a)) is S_{1}-unneeded); still, a is S_{1}-erased.

2. u is S_{2}-needed, persistently S_{2}-needed, and S_{2}-erased. a ⊆ u is S_{2}-needed but not persistently S_{2}-needed; and a is not S_{2}-erased – a has a residual along the S_{2}-normalizing reduction u → g(a, h(a)) → g(b, h(a)).

3. u is neither (persistently) S_{3}-needed nor S_{3}-erased. a ⊆ u is S_{3}-needed but not persistently S_{3}-needed (since the second residual of a in g(a, h(a)) is S_{3}-unneeded); still, a is S_{3}-erased.

4. both u and a are neither (persistently) S_{4}-needed nor S_{4}-erased.

Note that S_{1} and S_{2} are regular stable sets; S_{3} is stable but not regular, since S_{3}-unneeded redex u duplicates the S_{3}-needed redex a; and S_{4} is not stable (therefore, u does not contain an S_{4}-needed redex).

Lemma 7.1 Every persistently S-needed redex is S-erased, but an S-erased redex, even if S-needed, need not be persistently S-needed.

Proof (⇒) Let u ⊆ t be persistently S-needed, and let P : t → → s be S-normalizing. If u/P was not empty, then every u′ ∈ u/P (the set of P -residuals of u) would be S-needed, which is not possible since s ∈ S. (⇐) Take R = {f(x) → g(x, x), g(x, y) → x, a → b}, take for S the set of terms not containing left-spine redexes, and consider P : f(a) → g(a, a) → a → b. Then a in f(a) is S-needed, so is the first a in g(a, a), but the second a in g(a, a) is S-unneeded (and S-erased), and therefore a in f(a) is not persistently S-needed.

Definition 7.2 We call P : t → → s S-minimal if it is S-normalizing and P ⊴ Q for any S-normalizing Q : t → → o. When P is S-minimal, we call s an S-minimal S-normal form of t.

It follows immediately from Definition 7.2 that if t ↓_{S}∉ S (i.e., t ↓_{S} and t ∉ S), then t has no more than one S-minimal S-normal form s. For any other S-normal form e of t, it holds that s → → e. Note that the latter property of S-minimal S-normal forms cannot be taken as the definition, because in that case an S-normalizable term could have many S-minimal S-normal forms, due for example to a cycle in S, and some of them may require more reduction to be reached than others. For example, take R = {a → b, b → a, f(x) → x} and S = {a, b}. Then S is stable and regular, t = f(a) has two S-normal forms from which any other one is accessible – a and b, but any reduction from t to b should contract the S-unneeded redex a in t; therefore, no reduction from t to b can be considered as S-minimal.

Lemma 7.2 Every S-erased S-normalizing reduction is S-minimal.

Proof Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be an S-erased S-normalizing reduction, let P_{i} : t_{0}→^{u_{0}} … → t_{i}, and let Q : t_{0} → → o ∈ S. By stability of S, Q_{i} = Q/P_{i} is S-normalizing. Since u_{i} is S-erased and Q_{i} is S-normalizing, u_{i}/Q_{i} = ∅. Hence P/Q = ∅, i.e., P is S-minimal.

t_{0}  [figure: Q] o
[figure: t_{i}; P_{i}; Q_{i}]

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

Definition 7.3 Let F ⊆ t (i.e., F is a set of redexes in t). We call P an F -reduction if it contracts only residuals of redexes from F and created redexes; we call such redexes F -redexes.

Definition 7.4 (1) Let F ⊆ t. We call a redex u ⊆ t F -unabsorbed in an F -reduction P : t → → e if u ∈ F and none of the descendants of u along P appear in arguments of F -redexes; we call u F -absorbed in P otherwise. We call u F -unabsorbed in t if it is F -unabsorbed in any F -reduction and F -absorbed in t otherwise.

(2) We call u ⊆ t S-(un)absorbed if it is F_{S}^{n}(t)-(un)absorbed, where F_{S}^{n}(t) is the set of S-needed redexes of t. We call a reduction P S-unabsorbed if each redex contracted in it is.

Obviously, a redex u ⊆ t is unabsorbed in t, according to Definition 3.3, iff it is F (t)-unabsorbed, where F (t) is the set of all redexes in t. By Proposition 3.2, any term t not in normal form contains an unabsorbed redex. Now, if one ignores all redexes in t except those in F, it follows that:

Lemma 7.3 Let F ≠ ∅ be a set of redexes in a term t. Then F contains an F -unabsorbed redex.

Proposition 7.1 Every term t not in S-normal form contains an (S-needed) S-unabsorbed redex.

Proof It is enough to take F_{S}^{n}(t) for F in Lemma 7.3; F_{S}^{n}(t) ≠ ∅ by Theorem 6.1. Note that any S-unabsorbed redex is necessarily S-needed.

Below, in the study of S-minimal reductions, we will restrict ourselves to regular stable S. The reason is that, as shown by the following example, an S-normalizable term need not have an S-minimal reduction when S is irregular.

Example 7.2 Consider R = {f(x) → g(x, x), a → b}, take for S the set of terms not containing a as the leftmost innermost node, and take t = f(a). Obviously, S is closed under unneeded expansion, because the only S-needed redex in a term s ∉ S is the leftmost occurrence of a in it, and S is closed under reduction. S is not regular, because the outermost redex in t is S-unneeded, while the innermost one is S-needed. Further, there are three Snormalizing reductions starting from t : P : t → f(b); Q : t → g(a, a) → g(b, a), and N : t → g(a, a) → g(a, b) → g(b, b). (There are two more reductions that continue Q and N, but we do not need to consider them because they cannot be S-minimal.) We have P ⋬ Q, Q ⋬ P, and N ⋬ P. Hence none of the reductions is S-minimal.

Lemma 7.4 If a redex u ⊆ t is R-unabsorbed, then it need not be unabsorbed in t, but it cannot be replicated and is persistently R-needed.

Proof Let P : t → → o, not necessarily an F_{ℜ}^{n}-reduction. By Proposition 6.1.(3), it is enough to show that if a residual u′ of u can be absorbed inside an R-needed redex w′, then w′ cannot replicate u′; therefore u has at most one residual in any term of P. Suppose, on the contrary, that there is P : t → → s such that a residual u′ of u is absorbed inside an R-needed redex w′ such that w′ can replicate u′; and assume that P is a shortest such a reduction, i.e., u has exactly one residual in every term in P. By Lemma 6.4, there are R-needed P′ and R-unneeded P′′ such that P ≈_{L} P′ + P′′. Since u′ and w′ are R-needed and P′′ is R-unneeded, it follows from Proposition 6.1.(2) that there are R-needed u′′ and w′′ in the final term of P′ such that u′ and w′ are the only residuals of u′′ and w′′, respectively. Since u is R-unabsorbed, u′′ ∉ w′′. Hence u′′ has exactly one w′′-residual, say u^{∗}. By Theorem 2.1.(1), w′′ + P′′/w′′ replicates u′′, since w′ replicates u′. Thus P′′/w′′ replicates u^{∗} – a contradiction, since P′′/w′′ is R-unneeded by Proposition 6.1.(1), and R is regular.

Note that if S is irregular, then an S-unabsorbed redex u ⊆ t need not be persistently S-needed or S-erased. Indeed, take R, S, and Q as in Example 7.2. Then a in t is S-needed, so is its leftmost residual in g(a, a), but the rightmost residual is S-unneeded, and a/Q ≠ ∅. Hence a ⊆ t is not persistently S-needed or S-erased. But a ⊆ t is S-unabsorbed, since the only F_{S}^{n}(t)-reduction is N : f(a) → f(b), and a is F_{S}^{n}(t)-unabsorbed in N.

Proposition 7.2 An R-normalizing reduction is R-minimal iff it is R-erased.

Proof (⇐) From Lemma 7.2. (⇒) Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be R-minimal, and let Q : t_{0} → → o be R-unabsorbed, hence R-erased by Lemmas 7.4 and 7.1, R-normalizing reduction; Q exists by Proposition 7.1. Further, let P_{i} : t_{0}→^{u_{0}} … → t_{i} and let Q_{i} = Q/P_{i} (see figure for Lemma 7.2). Since Q is R-erased, so is Q_{i}, and Q_{i} is R-normalizing by the closure of R under parallel moves. Hence Q_{i} is R-minimal by Lemma 7.2. Since P is R-minimal too, u_{i}/Q_{i} = ∅ for every i. But for every R-normalizing reduction Q′_{i} : t_{i} → → o_{i}, it holds that Q_{i} ⊴ Q′_{i} (since Q_{i} is R-minimal). Hence u_{i}/Q′_{i} = ∅, i.e., u_{i} is R-erased, and P is R-erased too.

Now we are ready to prove the main result of this section.

Theorem 7.1 (Minimal Relative Normalization) Let R be a regular stable set of terms in an OERS, and let t ↓_{R}∉ R. Then repeated contraction of R-needed R-erased redexes in t yields an R-minimal R-normalizing reduction, even if a finite number of R-unneeded R-erased, and only such, redexes are also contracted. In particular, any t ↓_{R}∉ R has an R-unabsorbed R-minimal reduction, which is R-needed.

Proof By Proposition 7.1, any t ↓_{R}∉ R has an R-unabsorbed redex, which is R-needed and R-erased by Lemma 7.4 and Lemma 7.1. It remains to apply Theorem 6.1 and Proposition 7.2.

8 Relative Essentiality

In this section, we introduce the relative notion of essentiality, relate it to relative neededness, and give a characterization of R-erased redexes in terms of relative neededness and essentiality.

First we generalize some properties of essential subterms [Kha93, GlKh94] to the relative case.

Definition 8.1 We call s ⊆ t S-essential, written ES_{S}(s, t), if it has a P -descendant for at least one S-normalizing P starting from t, and call it S-inessential, written IE_{S}(s, t), otherwise.

Lemma 8.1 (1) Let e ⊆ s ⊆ t and ES_{S}(e, t). Then ES_{S}(s, t).

(2) Let s be a pattern-subterm of a redex u ⊆ t. Then ES_{S}(u, t) iff ES_{S}(s, t).

Proof From the definition of the descendant relation for subterms and Definition 8.1.

Lemma 8.2 Let P : t → → o be S-minimal. Then ES_{S}(s, t) iff s has a P -descendant.

Proof (⇒) Since ES_{S}(s, t), s has a Q-descendant for some Q : t → → o ∈ S. Since P is Sminimal, we have P ⊴ Q, and hence Q ≈_{L} P + P′ for some P′. Therefore, by Theorem 2.1.(2), Q ≈_{st} P + P′, and s has a P -descendant as well. (⇐) is immediate.

Lemma 8.3 Let N : s → → t, P : s → → s′, and P′ = P/N. Then

(1) If P is R-minimal, then so is P′.

(2) If P′ is R-minimal and N is R-inessential, then P is R-minimal as well.

Proof (1) By Proposition 7.2, P is R-erased. Hence, so is P′, and again by Proposition 7.2, P′ is R-minimal.

(2) We can construct the following diagram, where Q and Q′ are R-normalizing:

t [figure: P′] t′
[figure: N]
s [figure: P] Q′  s′

[figure: o; o′]
[figure]
[figure: e; Q; e′]

We have to show that P ⊴ Q. We have that N/Q = N/P = ∅, since N is R-inessential and R is closed under parallel moves. Hence P/Q = (P +N/P)/Q ≈_{L} (N +P′)/Q ≈_{L} N/Q+P′/Q′ = P′/Q′ = ∅, where Q′ = Q/N. Hence P is R-minimal.

Lemma 8.4 (1) Descendants of R-inessential subterms of any s↓_{R}∉ R remain R-inessential.

(2) Let N : s → → o be R-inessential and let ES_{ℜ}(s′, s). Then s′ has exactly one N-descendant o′ ⊆ o, which is R-essential; the R-minimal R-normal forms of s and o coincide.

Proof (1) Let IE_{ℜ}(s′, s), let P : s → → e be R-minimal, let N : s → → o, and let o′ be an N-descendant of s′. By Lemma 8.3.(1), P/N is R-minimal. By Lemma 8.2, s′ does not have P -descendants. Further, P + N/P ≈_{st} N + P/N by Theorem 2.1.(2). Hence o′ does not have P/N-descendants, and IE_{ℜ}(o′, o) by Lemma 8.2.

(2) Let P : s → → e be R-minimal. Then by Lemma 8.2, s′ has a P -descendant. Since N is R-inessential, we have that N/P = ∅, and hence P ≈_{st} N + P/N by Theorem 2.1.(2). Further, s′ has exactly one N-descendant o′ by Lemma 8.1.(1), and o′ has P/N-descendant since o has a P -descendant. By Lemma 8.3.(1), P/N is R-minimal. Hence o′ is R-essential by Lemma 8.2. The R-minimal R-normal forms of s and o coincide because N/P = ∅.

As shown above (Lemma 3.3), if s_{1}, …, s_{n} are inessential in s and t is obtained from s by replacing them with t_{1}, …, t_{n}, then t_{1}, …, t_{n} are inessential in t. The following example shows that, surprisingly, this is not the case for every stable, even regular, set.

Example 8.1 Consider the OERS R = {f(x) → a} with the alphabet Σ = {f, a, x, y, …}, and take R = {t ∥ t = a or t contains a variable}. Then any R-normalizable term not in Rnormal form has the shape f(… (f(a)) …), only the outermost f-redexes are R-needed, and their contraction yield the R-normal form a. Thus R is regular and stable. Now take s = f(a) and t = f(x). Then a is R-inessential in s – it does not have descendants in the only R-normal form a of s; but x is R-essential in t, since t ∈ R.

Next we establish the relationship between relative neededness and essentiality and prove a characterization of R-erased redexes. We need two lemmas first.

Lemma 8.5 Every R-unabsorbed redex u ⊆ t↓_{R} is R-essential.

Proof Let P : t → → e be R-unabsorbed R-minimal reduction, which exists by Theorem 7.1. Since u is R-unabsorbed, it has (exactly one) P -descendant by Definition 7.4. Hence u is R-essential by Lemma 8.2.

Lemma 8.6 Let P : t → → s ∈ R be R-unabsorbed. Then IE_{R}(u, t) iff P discards u.

Proof First note that, by Theorem 7.1, P is R-minimal. (⇒) By Lemma 8.5, P is R-essential. By Lemma 8.4.(1), all descendants of u along P remain R-inessential. Hence P is external to u, and every descendant of u along P is its residual. Since IE_{R}(u, t), u does not have P - descendants by Lemma 8.2. Hence u/P = ∅, and P discards u. (⇐) If P discards u, then u does not have P -descendants, hence is R-inessential by Lemma 8.2.

Proposition 8.1 A redex u ⊆ t↓_{R}∉ R is R-inessential iff it is R-unneeded and R-erased.

Proof (⇒) From Lemma 8.6. (⇐) Let P : t → → s ∈ R be R-unabsorbed; P exists by Theorem 7.1. Since UN_{R}(u, t), P is external to u by Proposition 6.1.(1), and since u is Rerased, u/P = ∅. Thus P discards u. Now it remains to apply Lemma 8.6.

Proposition 8.2 A redex u ⊆ t ∉ R is R-erased iff (α): every residual of u (in particular, u itself) along any reductions starting from t is either R-needed or R-inessential.

Proof (⇒) Let u be R-erased, and suppose on the contrary that u doesn’t satisfy (α), i.e., there are P′ : t → → s and a residual u′ ∈ u/P′ such that u′ is R-unneeded and R-essential. Let P′′ : s → → o ∈ R be an R-needed R-minimal reduction; P′′ exists by Theorem 7.1. Then P′′ is external to u′ by Proposition 6.1.(1), and u′/P′′ ≠ ∅ by Lemma 8.2, since every descendant of u′ along P′′ is its residual (P′′ is external to u′). (Alternatively, u′/P′′ ≠ ∅ can be shown as follows. Since u′ is R-unneeded and R-essential, it is not R-erased by Proposition 8.1, and since P′′ is R-minimal, u′/P′′ ≠ ∅.) Thus, u/(P′ + P′′) = (u/P′)/P′′ ⊇ u′/P′′ ≠ ∅, i.e., u is not R-erased in t – a contradiction. (⇐) We show that u/P = ∅ for any R-normalizing reduction P by induction on |P |. Indeed, let P = v + P′. Since u satisfies (α), so does every v-residual of it (by the property (α) itself). By the induction assumption, (u/v)/P′ = ∅. Hence u/P = ∅.

9 Relative Standardization Theorem

In this section, we define R-standard R-normalizing reductions, and show that R-unabsorbed R-normalizing reductions are R-standard.

In [HuLé91], for any reduction P : t → → s, external and outermost redexes of P are defined; we call them P -external and P -outermost, respectively. (The Huet&Lévy concept of a P -external redex must not be confused with our earlier concept of a reduction being external to a redex, as in Definition 4.1.) It is easy to see that u is P -external iff a residual of u is contracted in P and no descendant of u is absorbed in a redex contracted in P (i.e., no descendant of u appears in an argument of a redex contracted in P); and u is P -outermost iff a residual of u is contracted in P and no residual of u is absorbed in a redex contracted in P.

In [GLM92], a reduction P is called standard if P = ∅ or P = u + P′, where u is Q-outermost for any Q ≈_{L} P, and P′ is standard. The following Standardization Theorem is proved: For any finite P, there is a standard Q such that Q ≈_{L} P. This result is obtained for Abstract Reduction Systems in which the residual relation satisfy several axioms. It is not difficult to check that the standardization theorem applies to OERSs as well (and similarly to OCRSs, as suggested already in [GLM92]).

The following lemma, relating the above concepts, was proved in [HuLé91] for OTRSs, but the proofs remain valid for OERSs too.

Lemma 9.1 ([HuLé91]) Let P : t → → s. A redex u ⊆ t is P -external iff it is Q-outermost for any Q ≈_{L} P, and the latter holds iff u is N-outermost for a standard N ≈_{L} P. Therefore, u is P -external iff it is Q-external for any Q ≈_{L} P.

Hence a reduction P is standard if P = ∅ or P = u + P′, where u is P -external and P′ is standard. Thus a normalizing reduction is standard iff it contracts unabsorbed redexes. One of the most important properties of a standard reduction, not difficult to prove, is that it is (persistently) needed w.r.t. the class of reductions Lévy-equivalent to it. Since R-normalizing reductions need not be Lévy-equivalent, R-normalizing standard reductions need not be Rneeded. Indeed, take for example R = {f(x) → g(x, x), a → b}, and take for R the set of terms not containing a redex on the right-spine; then R is stable and regular, f(a) → g(a, a) → g(b, a) → g(b, b) is a standard R-normalizing reduction, but the second step is R-unneeded. Therefore, we should take standard R-minimal reductions for the R-standard R-normalizing reductions. Corollary 9.2 below justifies our choice.

Definition 9.1 We call an R-normalizing reduction R-standard if it is standard and Rminimal.

Now, we have from Theorem 7.1 and the Standardization Theorem [GLM92] the following corollary:

Corollary 9.1 (Relative Standardization Theorem) Let R be a regular stable set of terms in an OERS, and let t↓_{R}∉ R. Then t has an R-standard R-normalizing reduction.

Lemma 9.2 Let P : t → → s be R-minimal and u ⊆ t be P -external and R-erased. Then NE_{R}(u, t).

Proof Obviously, u has a P -descendant, hence is R-essential by Lemma 8.2. Therefore, by Proposition 8.2, u is R-needed.

Lemma 9.3 Let u ⊆ t ↓_{R} be R-unabsorbed and P : t → → s be R-minimal. Then u is P - external.

Proof Suppose on the contrary that u is not P -external. By Lemma 9.1, u is not N-outermost for a standard N ≈_{L} P, i.e., there is a decomposition N = N′ +v +N′′ such that a residual of u is in an argument of v. Since N is R-erased by Proposition 7.2, it is R-needed by Lemma 9.2, hence an F_{R}^{n}-reduction – a contradiction, since u is R-unabsorbed.

Corollary 9.2 R-unabsorbed R-normalizing reductions are R-standard.

10 The Relative Optimality Theorem

In this section, we generalize Lévy’s Optimality theorem to the case of all stable sets of normal forms, in OERSs.

Definition 10.1 A multistep reduction P : t_{0} → →^{F_{0}} t_{1} → →^{F_{1}} … → → t_{n} is called a family-reduction if each F_{i} is a set of redexes belonging to the same family (t_{i} → →^{F_{i}} t_{i+1} is a complete development of F_{i}). ∥P ∥ will denote the number of multisteps in P. The family-reduction P is complete if each F_{i} is a complete development of a maximal set of redexes of t_{i} belonging to the same family. A family-reduction P is called S-needed if each F_{i} contains at least one S-needed redex.

Notation Below F AM(P) will denote the set of families (whose member redexes are) contracted in P. Card(F AM(P)) will denote the number of families in F AM(P).

Lemma 10.1 Every family is contracted at most once in any complete family-reduction.

Proof Let P_{n} : t_{0} → →^{F_{0}} t_{1} → →^{F_{1}} … → →^{F_{n−1}} t_{n} be a complete family-reduction. We show by induction on n = ∥P ∥ that (a)_{n}: all families contracted in P_{n} are different; and (b)_{n}: there is no redex in t_{n} whose family has been contracted in P_{n}. So let us assume that P_{n} is a labelled reduction with t_{0} having an initial labelling. The case n = 0 is clear. Further, (a)_{n} follows immediately from (a)_{n−1} and (b)_{n−1}. Again by (a)_{n−1} and (b)_{n−1}, and by completeness of P_{n}, all redexes in t_{n} that are residuals of redexes of t_{n−1} are in families that have not been contracted before. The labels of new redexes in t_{n} contain the label lab(F_{n−1}) of (redexes in the family) F_{n−1}; more precisely, the label of a new redex in t_{n} is a tuple that has lab(F_{n−1}) as a component. A redex with the same label cannot occur in t_{0}, …, t_{n−1} since t_{0} has an initial labelling and, by the induction assumption, lab(F_{n−1}) ≠ lab(F_{i}), for all i < n − 1. Thus (b)_{n} is also valid.

Theorem 10.1 (Relative Optimality) Let S be a stable set of terms in an OERS R, and let t↓_{S}. Then any S-needed complete family-reduction starting from t is S-optimal in the sense that it reaches an S-normal form of t in a minimal number of family-reduction steps.

Proof Similar to the proof of the optimality theorem for the λ-calculus in [Lév80]. Let P : t → → s be an S-normalizing family-reduction and Q : t → →^{F_{0}} t_{1}→^{F_{1}} … be an S-needed complete family-reduction. Further, let Q_{i} : t → →^{F_{0}} t_{1}→^{F_{1}} … → → t_{i} and P_{i} = P/Q_{i}. Since ≃_{z}⊆≃, we have F AM(P_{i}) ⊆ F AM(P). Since Q is S-needed, at least one residual of some u_{i} ∈ F_{i} is contracted in P_{i} (P_{i} is S-normalizing by the closure of S under parallel moves). Hence, again by ≃_{z}⊆≃, F AM(Q) ⊆ F AM(P). Hence, by Lemma 10.1, ∥Q∥ = Card(F AM(Q)) ≤ Card(F AM(P)) ≤ ∥P ∥.

11 Relative optimal versus minimal reductions

It is easy to see that any R-needed family-reduction that in each step contracts all the Rneeded redexes of some family, but does not necessarily contract its R-unneeded members, is still optimal. We will call this an R-needed semi-complete family-reduction. It follows from Proposition 7.2 that such a reduction is R-minimal as well iff every R-needed redex contracted in it is R-erased. For example, g(a) → f(a, a) → f(b, a) is both R-minimal and R-optimal semi-complete family-reduction in R = {g(x) → f(x, x), a → b}, where R is the set of terms not containing left-spine redexes. However, the following example shows that a term in an OERS need not possess an R-minimal R-optimal family-reduction.

Example 11.1 Consider the OERS R = {σxAB → δx(((A/x)B/x)A), f(A) → g(A, A)}, and let R be the set of terms not containing left-spine redexes. Then R is closed under unneeded expansion because for any t ∉ R such that t→^{u}s ∈ R, u must be the outermost left-spine redex. Also, R is closed under reduction – no redex can be created or put on the left-spine without contracting a left-spine redex, which do not exist in terms from R. Thus R is stable. R is moreover regular, since if there is u such that UN_{R}(u, t), then the reduction P : t → → s ∈ R that contracts outermost left-spine redexes is R-needed, and is external to u, and each residual of u along P that is placed on the left-spine is discarded by contraction of a left-spine redex above it. But so do the residuals of redexes that are in u, and hence they cannot be R-needed.

Now let us consider the term t = σx(f(x), x). There are two R-needed semi-complete familyreductions starting from t: P : t → δx(f(f(x))) → → δx(g(g(x, x), g(x, x))) (since both occurrences of f in δx(f(f(x))) are R-needed) and Q : t → σx(g(x, x), x) → δx(g(g(x, x), g(x, x))), but neither reaches the R-minimal R-normal form δx(g(g(x, x), f(x))) of t, obtainable by the reduction t → δx(f(f(x))) → δx(g(f(x), f(x))) → δx(g(g(x, x), f(x))).

The reason why the above counterexample works is that redexes of the same family are nested. However the following examples show that, even if there is a ‘hierarchy’ of nesting of redexes of different families, the term still need not have R-minimal R-optimal family-reductions.

Example 11.2 Consider the OTRS R = {f(x) → g(x, x), g(b, x) → h(x, x), a → b}, and again take for R the set of terms not containing left-spine redexes. By the same argument as in Example 11.1, we can show that R is a regular stable set. Now P : f(a) → g(a, a) → g(b, a) → h(a, a) → h(b, a) is an R-minimal reduction, but h(b, a) is not reachable by an R-needed semicomplete family reduction. If the first step reduces a then we reach the R-normal form h(b, b) which is not R-minimal. Hence, in order to reduce f(a) to h(b, a), one should delay contraction of the R-needed occurrences of a (which all belong to the same family). So f(a) → g(a, a) must be the first step. In g(a, a), both occurrences of a are R-needed, but their contraction makes h(b, a) unreachable. Thus there is no R-minimal reduction that is R-optimal at the same time.

Example 11.3 Take for R the set of λ-terms in head-normal form, which is regular, and take t = (λx.xx)u, where u = (λy.λz.zvz)w, and y, z, v and w are different variables. Then P : t → uu → (λz.zvz)u → uvu → (λz.zvz)vu → vvvu = e is an R-minimal reduction. In order to reach e from t by a semi-complete R-needed family reduction, one should delay contraction of R-needed redexes in the family of u. So the outermost redex in t must be contracted first. In the obtained term o = uu, both occurrences of u are R-needed, and their contraction would make e unreachable – there is no occurrence of w in (λz.zvz)(λz.zvz).

Obviously, if reductions are non-duplicating, then every R-optimal reduction is R-minimal too, and every R-needed R-normalizing reduction is both R-minimal and R-optimal at the same time. This suggests that there may not be conflict between minimality and optimality then graph rewriting is concerned. But this goes beyond the scope of this paper.

12 Conclusions and Future Work

We have investigated properties which a set S of ‘final terms’ or ‘(partial) results’ should posses in order for the normalization-by-neededness theory still to make sense. We introduced appropriate notions of neededness, defined stability and regularity of sets of terms, and proved a Normalization Theorem relative to stable sets of ‘normal forms’, and a Hypernormalization Theorem relative to regular stable sets of ‘normal forms’. We have also studied minimal and optimal normalization relative to regular stable sets R of final terms, and have showed that R-normalizing reductions that are both minimal and optimal need not exist for any Rnormalizable term t, despite the fact that t possesses minimal as well as optimal R-normalizing reductions. These results were obtained for orthogonal ERSs, but are valid for Klop’s CRSs as well, and we expect that they remain valid for other systems of higher-order rewriting 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 by Huet&Lévy in [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.

Study of minimal and optimal relative normalization makes also sense for infinite reductions. The starting point here is the work [BeLé79] by Berry and Lévy, where minimality and optimality of outermost complete family-reductions is shown to coincide. An infinite complete family-reduction P computing an infinite tree T is called optimal if every family contracted in P is contracted in any complete family-reduction computing T (and co-initial with P). Minimality is defined w.r.t. ⊴ again. For the general case, stability and regularity of sets of finite and infinite reductions must be defined first.

Acknowledgements

We thank J. R. Kennaway, J.-J. Lévy, L. Maranget, P.-A. Melliès, F. van Raamsdonk, and M. R. Sleep for useful comments and discussions. The diagrams were drawn using P. Taylor’s diagram package.

References

[AbOn93] Abramsky S., Ong C.-H. L. Full abstraction in the lazy lambda calculus. Inf.& Comp., 105:159-267, 1993.

[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 Univ. 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.

[BeLé79] Berry G., Lévy J.-J. Minimal and optimal computations of recursive programs. JACM 26, 1979, p. 148-175.

[CuFe58] Curry H. B., Feys R. Combinatory Logic. vol. 1, North-Holland, 1958.

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

[GlKh94] Glauert J.R.W., Khasidashvili Z. On Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of the 4^{th} International workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, Springer LNCS, vol. 968, N. Dershowitz, N. Lindenstrauss, eds. Jerusalem, 1994, p. 144-165.

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

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. of the 7^{th} Annual IEEE Symposium on Logic in Computer Science, LICS’92, Santa Cruz, California, IEEE Computer Society Press, 1992, p. 72-81.

[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, CTRS’94, Springer LNCS, vol. 968, N. Dershowitz, ed. Jerusalem, 1994, p. 247-261.

[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 Univ. 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év76] Lévy J.-J. An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus. TCS 2(1):97-114, 1976.

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

[Lon83] Longo G. Set theoretic models of lambda calculus: theories, expansions and isomorphisms. Annals of pure and applied logic, 24:153-188, 1983.

[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 higherorder 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.