Minimal and Optimal Relative Normalization in Orthogonal Expression Reduction Systems

John Glauert and Zurab Khasidashvili School of Information Systems, UEA Norwich NR4 7TJ England

Abstract

We study normalization relative to desirable sets S of ‘results’ 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 – 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 higher-order rewriting subsuming term rewriting and the λ-calculus, similar to Klop’s Combinatory Reduction Systems. The results apply to numerous typed λ-calculi as well.

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. In [Mar92], Maranget studied 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]. Middeldorp [Mid97] studies normalization w.r.t. root-stable terms (which are terms that cannot be rewritten to a redex).

The normalization by neededness theory has been extended to other directions too, of which we mention a few (we do not discuss work on strong sequentiality here). Khasidashvili defined a similar normalizing strategy, called the essential strategy, for the λ-calculus [Kha88], OTRSs [Kha93], and Expression Reduction Systems (OERSs) [Kha94]. 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. 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).

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 Combinatory Reduction Systems (OCRSs) [Klo80]. Sekar and Ramakrishnan [SeRa93] study a normalizing strategy which in each multistep contracts a necessary set of redexes. Khasidashvili [Kha94] showed that in (Higher Order) Recursive Program Schemes one can find all needed redexes in any term, implying decidability of weak and strong normalization. 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. Kennaway et al. [KKSV95] studied needed strategies for infinitary OTRSs. Boudol [Bou85] and Melliès [Mel96] extended the needed strategy to non-orthogonal rewrite systems. A different approach to normalization is developed in Kennaway [Ken89] and in Antoy and Middeldorp [AnMi94].

Since, in the practice of Functional Programming, one is interested in terms of different shapes (normal forms, head-normal forms, etc.) as the results, it is natural to ask what properties a set of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. Here we provide a comprehensive 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 [HuLé91] is neededness w.r.t. the set NF of normal forms, Maranget-neededness [Mar92] is neededness w.r.t. all fair reductions, headneededness [BKKS87] is neededness w.r.t. the set of head-normal forms, root-neededness [Mid97] is neededness w.r.t. the set of root-stable forms, etc. We impose a natural condition on S, called stability, which is 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 (where every multi-step contracts at least one S-needed redex) 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.

Here 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 show that an S-normalizing reduction is S-minimal iff it contracts Serased redexes, i.e., the redexes that do not have residuals under any S-normalizing reduction. We show also that S-minimal reductions need not exist if S is stable but is not regular.

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. That is, we consider multi-step reductions contracting a number of redexes in the same family in parallel, and consider optimality w.r.t. the number of such multi-steps. This is because Barendregt et al [BBKV76] showed that there does not exist a one-step optimal recursive β-reduction strategy 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.

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 not S-erased. 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.

In the next section, we review Expression Reduction Systems, a formalism for higher order rewriting that we use here [Kha90, Kha92]. In section 3, we introduce the relative notion of neededness. In section 4, 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 5, and prove hypernormalization of the S-needed strategy w.r.t. regular stable sets S in section 6. In section 7, we study S-minimal reductions for regular stable sets S. In section 8 we establish a Relative Standardization Theorem. In section 9, we prove the Relative Optimality theorem. Finally, in section 10, we relate relative optimal and minimal reductions. The conclusions appear in section 11. The results in Sections 3 – 6 are published as [GlKh94], and the rest in [GlKh96a]. More details can be found in [GlKh94a].

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 [Kha92, Wol93, Nip93, OR94]. We refer to van Raamsdonk [Raa96] for a survey. Here we use a system of higher order rewriting, Expression Reduction Systems (ERSs), defined in [Kha92] (under the name of CRSs); the present formulation follows [GlKh94] and 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} as 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) in our notation, 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θ.

Our syntax is similar to that of Klop’s CRSs [Klo80], but is simpler in that it 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. Note that the use of metavariables in rewrite rules of ERSs is not really necessary – free variables can be used instead, as in TRSs (since (free) variables in TRS rules play the role of metavariables in ERS rules). We will indeed do so at least when giving TRS examples.

Notation 2.3 We use a, b, c, d for constants, t, s, e, o for terms, 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 contracting a redex u ⊆ t 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 + Q denotes the concatenation of P and Q.

The definition of orthogonality in ERSs is similar to the case of CRSs: all the rules are left-linear and in no term redex-patterns can overlap [Klo80]. As in the case of 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]. 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 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′.

The following strong Church-Rosser (confluence) property is proved for ERSs in [Kha92]; the same result for other higher-order rewriting formats are obtained, among others, in [Klo80, Nip93, KOR93, OR94, Oos94, KvO95, Raa96, Mel96].

Theorem 2.4 (Strong Church-Rosser) For any co-initial reductions P and Q in an OERS, P + Q/P ≈_{L} Q + P/Q.

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

Definition 3.1 (1) We call P : t → → o external to a redex u ⊆ t if P does not 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 3.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 Sunneeded, written UN_{S}(u, t), otherwise. (Thus u is S-(un)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.)

Thus Huet-Lévy neededness coincides with neededness w.r.t. the set of normal forms. It is easy to see that Maranget’s notion of neededness [Mar92] (where a redex is needed if it has a residual along any reduction external to it) coincides with neededness w.r.t. the set of fair reductions. (Recall that a reduction is fair if any redex in any of its terms is erased in it.) 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 3.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 does not 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.

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]), the set of constructor-head-normal forms for constructor TRSs [Nök94], and the set of root-stable forms (which are terms that cannot be rewritten to a redex) [Mid97]. All these sets are closed under reduction, which implies closure under parallel moves.

The graph G_{s} of any 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.

Note that 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)]

Actually, a stable set need not be closed under reduction even if the rewrite system is nonduplicating (i.e., has a non-duplicating residual relation). For example, take R = {a → b, b → a}, and take S = {a}. Then S is closed under unneeded expansion: the only step entering S is b → a, which is S-needed; and is trivially closed under parallel moves, but S is not closed under reduction.

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 3.4 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 (i.e., variable-free) 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)]

4 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 4.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 4.2 [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 4.3 [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 (see [Klo80, Mel96, Oos96a]. (Actually, it is shown in [Oos96a] that the structure of labels is not really essential – natural numbers can be used as labels to obtain the same result.)

5 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 Sunneeded redexes may replicate S-needed ones). However, the termination argument we use is the same as in [KeSl89] and in [Mar92], and is based on Proposition 4.3. The main idea and a proof in the same spirit is already in [Lév80]. As the most of known proofs, we use the fact that residuals of unneeded redexes remain unneeded, and that unneeded steps cannot create needed redexes. However, in order to prove that every needed redex has at least one needed residual after contacting any other redex, we need first to show the existence of a needed normalizing reduction.

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

Definition 5.1 We call P external to a set of redexes F ⊆ t if P does not contract residuals of redexes in F.

Lemma 5.2 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 the figure below).

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

[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}]

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

Lemma 5.4 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 4.2, 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 5.5 (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 does not contain terms in S except for e. By the stability of S, u is S-needed. By Corollary 5.3 and Lemma 5.4, 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 does not 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 (see the figure). 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 4.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 4.1, Ind(u_{i}) ≤ Ind(P_{i}). Hence Ind(Q) ≤ Ind(P) and Q is terminating by Proposition 4.3.

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 5.6 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 5.5. 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 conclude this section by summarizing the neededness properties of residuals and created redexes, established in Corollary 5.3, Lemma 5.4, and Lemma 5.6, in the following proposition.

Proposition 5.7 (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.

6 The Relative Hypernormalization Theorem

In this section, we prove the Relative Hypernormalization Theorem for all regular stable sets of final terms, in OERSs, and demonstrate that the theorem fails for some irregular stable sets. Thus this theorem refines the Relative Normalization Theorem, but is less general as it is restricted to regular stable sets of results only. However, regularity is not a restriction from practical point of view, as all the sets of results that have been used in the practise of programming are regular. Moreover, it allows for much simpler proofs. We do not use termination of reductions with bounded index any more (Proposition 4.3) – the Finite Developments Theorem is enough. We do not use the Standardization Theorem [HuLé91, Klo80] either.

As mentioned above, for some stable 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.1 We call a stable set S regular if, for any t ∉ S, S-unneeded redexes cannot duplicate S-needed ones.

For the case of normal forms, the needed strategy is hypernormalizing, that is, reductions starting from a normalizable term that besides needed redexes contract a finite number of unneeded steps are still normalizing. The following example shows that this need not be the case for irregular stable sets.

Example 6.2 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, which we are going to prove next.

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 5.7.(2), v is a residual of a redex v′ ⊆ t, which is R-needed by Proposition 5.7.(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), and K(P) ∈ Red^{∗}.

(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) ∈ Red^{∗} 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.5 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.6 Let t_{0} have an R-quasi-needed reduction and t_{0}→^{u}s_{0}. Then s_{0} also has an R-quasi-needed reduction. Proof By Lemma 6.5, 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 below. It follows from 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 5.7.(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.

[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}]

Theorem 6.7 (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.6 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.6 that infinitely many of them contain R-needed redexes – a contradiction, since terms in R do not contain Rneeded redexes. (⇐) By Theorem 5.5.(1), one can repeatedly contract R-needed redexes in t, unless a term in R is reached; the latter is inevitable since t does not have an infinite R-needed reduction.

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, hence need not be S-normalizing, 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 does not have a residual under any S-normalizing reduction.

(3) We call a reduction S-erased if it only contracts S-erased redexes.

Note that S-erased redexes need not be S-needed (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 OTRS.

Example 7.2 Consider an OTRS 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.3 Every persistently S-needed redex is S-erased, but an S-erased redex, even if Sneeded, 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. (⇐) From Example 7.2 (cases 1 and 3).

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

It follows immediately from Definition 7.4 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.5 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.

Definition 7.6 Let F be 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. Below F ⊆ t will denote that F is a set of redexes in a term t, and F (t) will denote the set of all redexes of t.

Definition 7.7

(1) Let F ⊆ t. We call a redex u ⊆ t F -unabsorbed (in t) if u ∈ F and, for any F -reduction P, none of the residuals of u along P appear in arguments of F -redexes; we call u F -absorbed in t if u ∈ F and it is not F -unabsorbed.

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

Example 7.8 Consider an OTRS R = {a → c, b → b′, f(c, x) → c′}, and take a term t = g(f(a, b), a). Then both occurrences of a in t are F (t)-unabsorbed in t, while b is F (t)-absorbed in t: we have t → g(f(c, b), a) = s, and the residual of b in s is in an argument of the created redex f(c, b). If F ⊆ t contains two redexes – the first occurrence of a in t and the redex b ⊆ t, then only the first a ⊆ t is F -unabsorbed in t. If the set of terms not having a left-spine redex is taken for S, then the first a is the only S-unabsorbed redex in t (it is the only S-needed redex too).

It is shown in [HuLé91, Kha93, GlKh94] that any term t not in normal form contains an F (t)- unabsorbed redex (such redexes are called external in [HuLé91]). Now, if one ignores all redexes in t except those in F ⊆ t, it follows that, for any F ≠ ∅, F contains an F -unabsorbed redex. And by taking F_{S}(t) for F (F_{S}(t) ≠ ∅ by Theorem 5.5), we obtain the following proposition:

Proposition 7.9 Every term t ∉ S contains an (S-needed) S-unabsorbed redex.

1We prefer to use minimal rather than least or smallest.

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.10 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 S-normalizing reductions starting from t : P : f(a) → f(b); Q : f(a) → g(a, a) → g(b, a), and N : f(a) → g(a, a) → g(a, b) → g(b, b). (There are two more reductions that continue Q and P, 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.11 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_{ℜ}(t)-reduction. By Proposition 5.7.(3), it is enough to show that if a residual u′ of u can appear inside an R-needed redex w′ ≠ u′, 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 → → o such that a residual u′ of u is inside an R-needed redex w′ such that w′ replicates 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.5, 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 5.7.(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.4, w′′ + P′′/w′′ replicates u′′, since w′ replicates u′. Thus P′′/w′′ replicates u^{∗} – a contradiction, since P′′/w′′ is R-unneeded by Proposition 5.7.(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.10. 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}(t)-reduction is N : f(a) → f(b), and a is F_{S}(t)-unabsorbed in N.

Proposition 7.12 An R-normalizing reduction is R-minimal iff it is R-erased. Proof (⇐) From Lemma 7.5. (⇒) 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.11 and 7.3, R-normalizing reduction; Q exists by Proposition 7.9. Further, let P_{i} : t_{0}→^{u_{0}} … → t_{i} and let Q_{i} = Q/P_{i}. 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.5. 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 Minimal Relative Normalization Theorem.

Theorem 7.13 (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.9, any t ↓_{R}∉ R has an R-unabsorbed redex, which is R-needed and R-erased by Lemma 7.11 and Lemma 7.3. It remains to apply Theorem 5.5 and Proposition 7.12.

8 The Relative Standardization Theorem

Recall that a reduction is standard if redexes in it are contracted in left-to-right outside-in order [Bar84, HuLé91, Klo80]. Maranget proved in [Mar92] that standard reductions are minimal among reductions computing a ‘stable prefix’ of a term, in an OTRS. Note that, in general for any regular R, R-normalizing standard reductions (in the sense of [Bar84, HuLé91, Klo80], or in the sense of [GLM92], where left-to-right order of contracted redexes is not required) need not be R-needed. 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 regular, f(a) → g(a, a) → g(b, a) → g(b, b) is standard and R-normalizing, but the second step is R-unneeded. Therefore, we should take standard R-minimal reductions for the R-standard R-normalizing reductions.

Definition 8.1 We call an R-normalizing reduction R-standard if it is outside-in and R-minimal.

It is not difficult to check that R-unabsorbed R-normalizing reductions are then R-standard (see [GlKh94a]), and the left-to-right order of contraction of R-unabsorbed redexes can also be arranged. Hence we have the following Relative Standardization Theorem:

Theorem 8.2 (Relative Standardization) 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. In particular, R-unabsorbed R-normalizing reductions are R-standard.

9 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. The family concept we use is based on the labelling system of Kennaway&Sleep described in section 4. Recent results on the optimality theory for orthogonal (first and higher order) rewrite systems can be found in [Mar92, AsLa93, Oos96].

Definition 9.1 For any co-initial reductions P : t → → s and Q : t → → o, redexes u ∈ s and v ∈ o with histories P and Q, written P u and Qv, are in the same (labelling-)family if for any initial labelling of t, they bear the same labels.

Definition 9.2 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 9.3 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 9.4 (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 familyreduction. Further, let Q_{i} : t → →^{F_{0}} t_{1}→^{F_{1}} … → → t_{i} and P_{i} = P/Q_{i}. By Proposition 4.1, 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 Proposition 4.1, F AM(Q) ⊆ F AM(P). Hence, by Lemma 9.3, ∥Q∥ = Card(F AM(Q)) ≤ Card(F AM(P)) ≤ ∥P ∥.

10 Relative optimal versus minimal reductions

It is easy to see that any R-needed family-reduction that in each step contracts all the R-needed 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.12 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 familyreduction 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 10.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 10.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 10.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 semi-complete 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 10.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.

11 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 R-normalizable 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 and for contextsensitive conditional orthogonal ERSs [KvO95], and therefore apply to numerous typed λ-calculi as well. Actually, the normalization and optimality results have already been generalized to abstract orthogonal rewrite systems with axiomatized residual relation, more precisely, to stable Deterministic Residual Structures (SDRSs) and to Deterministic Family Structures, respectively [GlKh96]; the latter structure is a refinement of the former in that it formalizes the concept of redex-family. And the above minimality results hold in such SDRSs where every set F of redexes in a term has a non-duplicable element – one that has at most one residual under any F -reduction (for example, F -unabsorbed redexes in OERSs are non-duplicable w.r.t. F).

Study of minimal and optimal relative normalization makes also sense for infinite reductions. The starting point here is the work by Lévy and Berry [Lév78, BeLé79]. In [BeLé79], minimality and optimality of outermost complete family-reductions is shown to coincide for Recursive Program Schemes. 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 coinitial 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, V. van Oostrom, 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. Information and Computation, 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.

[AnMi94] Antoy S. and Middeldorp A. A Sequential Reduction Strategy. In Proc. of ALP’94, Springer LNCS, vol. 850, p. 168-185, 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.

[BBKV76] Barendregt H.P., Bergstra J., Klop J.W., Volken H. Degrees, reductions and representability in the λ-calculus. Report 22, University of Utrecht, 1976.

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

[Bou85] Boudol G. Computational semantics of term rewriting systems. In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds. Cambridge Univ. Press, 1985, p. 169-236.

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

[Gar94] Gardner P. Discovering needed reductions using type theory. In: Proc. of TACS’94, Springer LNCS, v. 789, M. Hagiya, J. C. Mitchell, eds. Sendai, 1994, p. 555-574.

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

[GlKh94a] Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in Expression Reduction Systems. Report SYS-C94-06, UEA, Norwich, 1994.

[GlKh96] Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180-195.

[GlKh96a] J. R. W. Glauert, Z. Khasidashvili. Minimal relative normalization in orthogonal expression reduction systems. In Proc. of the 16^{th} International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’96, Springer LNCS, to appear.

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

[Ken89] Kennaway J.R. Sequential evaluation strategy for parallel-or and related reduction systems. Annals of Pure and Applied Logic, 43:31-56, 1989.

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

[KKSV95] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Transfinite reductions in orthogonal term rewriting. Information and Computation, 119(1):18-38, 1995.

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

[KvO95] Khasidashvili Z., van Oostrom V. Context-sensitive conditional expression reduction systems. Electronic Notes in Theoretical Computer Science, vol. 2, A. Corradini, U. Montanari, eds. Elsevier, 1995, p. 141-150.

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

[Mel96] Melliès P.-A. Description Abstraite des Systèmes de Réécriture. Thèse de l’Université Paris 7, 1996.

[Mid97] Middeldorp A. Call by need computations to root-stable form. In Proc. of the 24^{th} ACM Symposium on Principles of Programming Languages, POPL’97, Paris, 1997.

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

[Oos96] Van Oostrom V. Higher order families. In proc. of RTA’96, Springer LNCS, vol. 1103, Ganzinger, H., ed., 1996, p. 392–407.

[Oos96a] Van Oostrom V. Finite family developments. To appear.

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

[Raa96] Van Raamsdonk F. Confluence and normalisation for higher-order rewriting. Ph.D. Thesis, Free University, Amsterdam, 1996.

[SeRa93] Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond Strong Sequentiality. Information and Computation, 104(1):78-109, 1993.

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