Stable Results and Relative Normalization

John Glauert School of Information Systems, UEA Norwich NR4 7TJ England J.Glauert@uea.ac.uk

Richard Kennaway School of Information Systems, UEA Norwich NR4 7TJ England R.Kennaway@uea.ac.uk

Zurab Khasidashvili Department of Mathematics and Computer Science Bar-Ilan University, Ramat-Gan 52900, Israel Khasidz@cs.biu.ac.il ^{∗}

Abstract

In orthogonal expression reduction systems, a common generalization of term rewriting and λ-calculus, we extend the concepts of normalization and needed reduction by considering, instead of the set of normal forms, a set S of “results”. When S satisfies some simple axioms, we prove the corresponding generalizations of some fundamental theorems: the existence of needed redexes, that needed reduction is normalizing, the existence of minimal normalizing reductions, and Lévy’s optimality theorem.

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

Normalization by Needed Reduction

For Orthogonal Term Rewriting Systems (OTRSs), a general normalizing strategy, called the needed strategy, was found by Huet and Lévy in [18]. The needed strategy always contracts a needed redex – a redex with at least one contracted residual in every reduction to normal form. Huet and Lévy show 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 this as the Normalization Theorem. They also define the class of strongly sequential OTRSs where a needed redex can be found efficiently in any term.

∗Work undertaken at UEA with the partial support of the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300.

Extending the concept of Neededness

Barendregt et al. [7] generalize the concept of neededness to the λ-calculus. They study 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 headnormal form. They prove correctness of the two needed strategies for computing normal forms and head-normal forms, respectively. Middeldorp [39] studies normalization w.r.t. root-stable terms (which are terms that cannot be rewritten to a redex). Normalization w.r.t. another interesting set of ‘normal forms’, that of constructor head-normal forms in constructor OTRSs, is studied by Nöcker [40].

The normalization by neededness theory has been extended in other directions too, of which we mention a few. Khasidashvili defined the essential strategy for the λ-calculus [22], OTRSs [25], and Expression Reduction Systems (OERSs) [26]. This strategy contracts essential redexes – the redexes that have descendants under every reduction. The notion of descendant is a refinement of residual – the descendant of a contracted redex is its contractum, while it does not have residuals.^{1} Essentiality makes sense for all subterms, not only redexes. In [35], Maranget introduces a different notion of neededness, where a redex u is needed if it has a residual under any reduction that does not contract residuals of u. This neededness notion makes sense even for terms that do not have a normal form, and coincides with the notion of essentiality.

Sekar and Ramakrishnan [42] study a normalizing strategy which proceeds by multisteps^{2}, each of which contracts a necessary set of redexes. Khasidashvili [26] shows that in Higher Order Recursive Program Schemes one can find all needed redexes in any term, implying decidability of weak and strong normalization. Khasidashvili and Piperno [28] designed an algorithm for statically finding all inessential subterms (i.e., the garbage) in simply typeable λ-terms. Gardner [11] 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. [2] designed a needed narrowing strategy. Kennaway et al. [20] studied needed strategies for infinitary OTRSs. Boudol [9] and Melliès [37] extended the needed strategy to non-orthogonal rewrite systems. A different approach to normalization is developed by Kennaway [19] and by Antoy and Middeldorp [3].

The concept of Relative Neededness

Since in the practice of Functional Programming one is interested in terms of different shapes (weak-head-normal forms, constructor head-normal forms, etc.) as the results of computation, 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.

1Note that descendants and residuals are sometimes treated as synonymous in the literature.

2A multistep contracts a set of redexes simultaneously.

We introduce the notion of neededness w.r.t. a set of reductions Π so that each existing notion of neededness can be given by specifying Π. Usually it is convenient to consider a set of terms S, and the induced set of reductions Π_{S} ending at a term in S. For example, Huet and Lévy-neededness [18] is neededness w.r.t. the set NF of normal forms, Maranget-neededness [35] is neededness w.r.t. all fair reductions, headneededness [7] is neededness w.r.t. the set of head-normal forms, root-neededness [39] is neededness w.r.t. the set of root-stable forms, etc.

We impose a natural condition on S, stability, which guarantees that each term not in S-normal form (i.e., not in S) has at least one S-needed redex, such that repeated contraction of S-needed redexes in a term t will lead to an S-normal form of t whenever there is one. A set S of terms is stable if it 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; and is closed under reduction: for any t → o where t ∈ S, then o ∈ S. ^{3}

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 contracting both S-needed and S-unneeded redexes which never reaches a term in S even though S-needed redexes are contracted infinitely many times. Therefore, multistep S-needed reductions, where every multistep contracts at least one S-needed redex, need not be S-normalizing. This is because a ‘non-standard’ situation may arise in what we will call irregular stable sets S, where S-unneeded redexes may contain S-needed ones. However, for regular stable sets S, the S-needed strategy is always hypernormalizing, and the multistep S-needed strategy is normalizing.

Although we claim that our definition of stability is the most natural that has been proposed, it is possible to weaken the conditions for stability and still retain the concept of relative neededness. For example, an alternative definition is explored in [13, 12] where a stable set S is closed under unneeded expansion and 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.

Minimal and Optimal Relative Normalization

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 a minimal S-normal form.

Minimal S-normal forms are useful to compute since any other S-normal form is accessible from the 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 [5] trees and Lévy-Longo [30, 33] (or lazy) trees, respectively. These trees represent the values of the term according to different semantics – Böhm semantics and 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.

3When the rewrite system is non-duplicating and non-erasing, our concept of stability coincides with the concept of stability in event structures [49].

Our research on minimal S-normalizing reductions was inspired by a result of Maranget [35], stating that standard reductions are minimal among reductions computing a ‘stable prefix’ of a given term. The earliest minimality result we are aware of was obtained by Berry and Lévy in [8], 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-external 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 S-erased 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 [32], developed for the λ-calculus. That is, we consider multistep reductions contracting a number of redexes in the same family in parallel, and consider optimality w.r.t. the number of such multisteps. This is chosen because Barendregt et al [6] showed that no one-step optimal recursive β-reduction strategy exists for the λ-calculus. We introduce a suitable labelling system, allowing us to define a family relation in OERSs. The generalization is then rather straightforward. We show that complete S-needed family-reductions, which contract all members of a family containing an S-needed redex in a multistep, are optimal.

It is easy to see that S-needed complete family reductions, though optimal, need not be S-minimal, because they may contract S-unneeded redexes that are not Serased. 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.

Overview

In the next section, we review Expression Reduction Systems [23, 24, 27]. In Section 3, we introduce the relative notion of neededness. In Section 4, we sketch some properties of our labelling system for OERSs needed to define a family relation among redexes. We prove correctness of the S-needed strategy for computing 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 concepts introduced in Section 3 build on [13], but here the definitions use only the residual concept while the earlier definitions were based on a concept of descendants for subterms and components. The stability concept is simpler, and hence slightly less general. The labelling system in Section 4 extends unpublished work by Kennaway and Sleep [21]. The proofs in Sections 5 and 6 simplify analogous proofs published as [13], and the remaining results are published in [14]. The results were first reported in [12].

The following section and Section 4 will be of less interest to those only interested in application to OTRS and the λ-calculus. Labelling systems due to Maranget and Lévy, respectively, are adequate for the later proofs.

2 Orthogonal Expression Reduction Systems

Klop introduced Combinatory Reduction Systems (CRSs) in [29] to provide a uniform framework for reductions with substitutions (also referred to as higher order rewriting) as in the λ-calculus [5] and its extensions. Restricted rewriting systems with substitutions were first studied in Pkhakadze [41] and Aczel [1]. Several interesting formalisms have been introduced later [24, 50, 36, 47]. We refer to van Raamsdonk [48] for a survey.

Expression Reduction Systems

Here we use Expression Reduction Systems (ERSs), defined in [24] (under the name of CRSs). The present formulation follows [27] and is simpler.

Definition 1 Let Σ be an alphabet comprising variables 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}, have 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 by using functions and quantifiers in the usual way: variables are terms, and if t_{1}, …, t_{n} are terms and δ is an n-ary (simple or compound) operator, then δ(t_{1}, …, t_{n}) is a term too.

Metaterms are constructed similarly from terms and metavariables A, B, … that range over terms, but with an extra operation: if t_{0}, …, t_{n} are metaterms, then so is (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, also called a metasubstitution, where the scope of each x_{i} is t_{0}. Metaterms without metasubstitutions are simple metaterms.

An assignment maps each metavariable to a term over Σ. If t is a metaterm and θ is an assignment, then the θ-instance tθ of t is the term obtained from t by replacing metavariables with their values under θ, and by replacing metasubstitutions (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, in right-to-left order, with the result of substitution of terms t_{1}, …, t_{n} for free occurrences of x_{1}, …, x_{n} in t_{0}. The substitution operation may involve a renaming of bound variables to avoid collision, and we assume that the set of variables in Σ comes equipped with an equivalence relation, called renaming, such that any equivalence class of variables is infinite. We also assume that any variable can be renamed by any other variable in the corresponding equivalence class.^{4} Unless otherwise specified, the default renaming relation is the total binary relation on variables (a partial renaming relation may be useful for conditional systems).

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 A Conditional Expression Reduction System (CERS) is a pair (Σ, R), where Σ is an alphabet described in Definition 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.

Furthermore, each rule r : t → s has a set of admissible assignments AA(r) which, in order to prevent undesirable confusion of variable bindings, must satisfy the following condition of being variable-capture-free:

[vcf] 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 so is any variant of tθ obtained from it by renaming of bound variables), and sθ is the contractum of tθ.

If for any rule r ∈ R, AA(r) is the maximal set of variable-capture free assignments, then the CERS is called an unconditional Expression Reduction System, or simply an Expression Reduction System (ERS).

For the sake of simplicity, we will restrict ourselves to variable-capture-free ERSs, which are ERSs in which all assignments are admissible for all rules. The results (and proofs) are valid for the much larger class of fully-extended context-sensitive CERSs [27]. Roughly, full extendedness means that an erasing step cannot turn a non-redex instance of a left-hand side of a rule into a redex. For example, the ληcalculus is not fully extended because an erasing beta step can create an η-redex above the contractum. It was first observed by van Oostrom that the full extendedness restriction is necessary for many important results in the theory of higher-order rewriting, and since then this restriction has been adopted in many recent works [48, 44, 17, 45, 46, 27]. It is no surprise that the restriction is needed here.

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.

4An equivalence class of variables can, for example, be the set of variables of the same type in a typed language.

Examples

Our syntax is similar to that of Klop’s CRSs [29], but has the attraction that it is closer to the syntax of the λ-calculus. For example, the β-rule is written as Ap(λxA, B) → (B/x)A, where A and B can be instantiated by any term; 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. ∃xA → (τx(A)/x)A and ∃!xA → ∃xA ∧ ∀x∀y(A ∧ (y/x)A ⇒ x = y) are rules corresponding to familiar definitions.

Notation 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. We write U ⊆ t if U is a set of redexes in t.

Orthogonality, Residuals, and Lévy-equivalence

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 [29]. The residual relation on redexes in ERSs is defined as a combination of the residual relations in TRSs and the λ-calculus, since any ERS step can be decomposed into a TRSs step followed by a number of substitution steps. Since the residual concept is familiar both in TRSs and the λ-calculus we do not reintroduce the concept here for ERSs, and instead refer to [24, 27] for more details. Developments of sets of redexes U ⊆ t are defined in ERSs as usual [5].

As in the case of the λ-calculus [5] or OCRSs, for co-initial reductions P and Q, one can define in OERSs the notion of residual of P under Q, written P/Q, using Klop’s method of commutative diagrams [29]. Klop’s method is equivalent to Lévy’s original definition of the residual relation in the λ-calculus [31, 32]; the latter is more ‘algebraic’ in nature and uses multisteps rather than complete developments.

We write P ⊴ Q if P/Q = ∅, where ⊴ is the Lévy-embedding relation. P and Q are called Lévy-equivalent^{5}, 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 = P/Q + P′/(Q/P) and P/(Q + Q′) = (P/Q)/Q′.

We will often be interested in residuals of single redexes written u/P where u is a single-step reduction contracting u, a redex in the initial term of P. For example, P ≈_{L} Q for finite P and Q implies that P and Q end at the same term and that u/P = u/Q for all redexes, u, in the initial term.

The Strong Church-Rosser (confluence) property is established for OERSs in [24, 27]; the Finite Developments Theorem [5, 29] is proved first, from which strong confluence follows by a standard argument. Strong confluence for other higher-order rewriting formats are obtained, among others, in [29, 47, 43, 37].

5or strongly-equivalent, or permutation-equivalent

Theorem 4 (Finite Developments) All complete developments of a set of redexes in a term t, in an OERS, end at the same term s, and the residuals in s of any redex in t along any complete development are the same.

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

3 Stability and 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 a special case of Π-neededness. We introduce stability of a set of terms in an OERS. It is the aim of the Section 5 to show that if S is stable, then a S-needed strategy is S-normalizing.

Relative Neededness

Definition 6 (1) P : t → → o is external to a redex u ⊆ t if P does not contract any residual of u.

(2) P : t → → o is external to a set of redexes U ⊆ t if P is external to all u ∈ U.

(3) P S-suppresses u if P is S-normalizing and is external to u.

(4) P erases u if u/P = ∅. Note that contracting a redex erases it.

(5) P discards u if P is external to u and erases it.

Definition 7 (1) Let Π be a set of reductions in an OERS R. We call a redex u ⊆ t Π-needed if in every reduction in Π starting from t at least one of its residuals is contracted (i.e., no reduction in Π is external to u) and call it Π-unneeded otherwise.

(2) Let S be a set of terms in an OERS R. Let Π_{S} be the set of all reductions that end at a term in S. These will be denoted S-normalizing reductions. A term t is denoted S-normalizing if some S-normalizing reduction starts at t. We call a redex u S-needed, written NE_{S}(u, t), if it is Π_{S}-needed, and call it S-unneeded, written UN_{S}(u, t), otherwise.

Thus Huet and 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 [35], 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 [12]. (Recall that a reduction is fair if all redexes in any of its terms are erased in it.) Obviously, any redex in a term that is not S-normalizable is S-needed; we call such redexes trivially S-needed.

Stability

Definition 8 A set S of terms is stable if:

(a) S is closed under reduction: if t ∈ S and t → s, then s ∈ 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 in an OERS are normal forms [18], head-normal forms [7], weak-head-normal forms, constructor-head-normal forms for constructor TRSs [40], and root-stable forms (terms that cannot be rewritten to a redex) [39].

Such sets are closed under reduction, which seems a natural condition for stability. Closure under unneeded expansion is less intuitive, but without it there will be Snormalizable terms with no S-needed redex. For example, consider R = {I(x) → x}, and S that contains I(t), but not I(I(t)), for some term t. There is no S-needed redex in I(I(t)) as it can be reduced to I(t) by reducing either I redex .

Weaker Stability Conditions

A weaker definition of stability is studied in [13] where a set S of terms is said to be stable if it is closed under unneeded expansion and is closed under parallel moves:

Definition 9 A set S is closed under parallel moves if for all t ∉ S, and P : t → → o ∈ S, then for any Q : t → → e that contains no term in S, the final term of P/Q is in S.

Clearly, closure under reduction implies closure under parallel moves. The S-needed strategy can also be proven to be S-normalizing under these weaker conditions. This rather technical definition ensures that if unneeded steps are taken when a normalizing needed reduction exists, it is still possible to reach a term in S by completing the residual of the normalizing reduction.

4 A Labelling for OERSs

We now introduce a labelling system for ERSs which will be used to establish termination of certain reductions and in section 9 to define the concept of a redex family. The labelling is a modification of one used by Klop [29] for CRSs.

Fix some OERS R. For technical reasons, we assume that R does not contain any rules whose left-hand side consists of just an operator applied to variables and metavariables. This is not a substantial restriction, since if the system includes a rule of the form f(x, y, z) → …, we can replace the symbol f(…) wherever it occurs by g(f(…)), where g is a new unary function symbol. The new system will behave in all essential respects like the old and will satisfy the restriction. A similar restriction is adopted in [29].

Let there be a set L_{0} of atomic labels, and two sets C and C′ of label constructors in 1−1 correspondence with the set of subterms of all the right-hand sides of the rules of the OERS, and in 1 − 1 correspondence with the rules of the OERS, respectively. The arity of each constructor in C′ is the number of nodes in the left hand side of the rule which it is associated with, excluding variable and metavariable nodes and the root. And the arity of each constructor in C is 1. The set L of labels is the set of terms freely generated by L_{0} and C ∪ C′. The height of a label is its height considered as a tree.

We add all members of L to the OERS as new unary function symbols. By a labelled term we mean any term which results from this extension of the signature. Every labelled term t determines an unlabelled term U(t) by simply dropping the labels — that is, by replacing every subterm of the form l(t′) by t′, where l is any label. A labelling of a term is initial if all its subterms are labelled by different atomic labels.

Although for technical reasons we have introduced labels as new function symbols, in writing terms down we shall indicate labels by superscripts. A term α(β(γ(t))) would be written t^{γβα}. This suggests an alternative way of looking at labels, closer to the way Lévy and Klop use them: the labels are considered to be annotations attached to the nodes of the syntax tree of the unlabelled term.

We now construct the set of labelled rules. Given any rule s → t of the unlabelled system, and labellings f of s and f′ of t, s^{f} → t^{f′} is a labelled rule provided that:

• f does not label the root of s, nor any occurrence of a metavariable.

• f′ attaches the label c(c′(l_{1}, …, l_{n})) to each subterm of t, other than metasubstitutions, where c is the label constructor corresponding to t, c′ is the constructor corresponding to the rule, and l_{1}, …, l_{n} are the labels present in f(s), listed in depth-first left-to-right order.

The choice of depth-first left-to-right ordering is not significant for the theory; it is merely a convenient standard choice. Note that f′ is completely determined by f, s, and t. All nodes of t^{f′} have distinct labels, and different labellings of s give different labellings of t. The reason for the restriction we made earlier is to ensure that every left-hand side has at least one place to attach a label to.

The set of labelled rules constitutes the system L(R). This is clearly an OERS. As an example, consider the beta rule of lambda calculus. In OERS notation, and

writing the application operator explicitly, it is:

Ap((λx(A)), B) → (B/x)A

An example of a redex is

Ap((λy(Ap(y, y))), (λz(z)))

A labelled version of this redex is:

(Ap((λy(Ap(y^{α}, y^{β}))^{γ})^{δ}, (λz(z)^{ϵ})^{ζ}))^{η}

This contains a redex of the labelled rule:

Ap((λx(A))^{δ}, B) → (B^{c(g(δ))}/x)A^{d(g(δ))}

where g is the label constructor for the β-rule) and it reduces to:

((Ap(((λz(z^{ϵ}))^{ζ})^{c(g(δ))}, ((λz(z^{ϵ}))^{ζ})^{c(g(δ))}))^{d(g(δ))})^{η}.

For a redex u in a labelled term, we define lab(u) to be c′(l_{1}, …, l_{n}), where c′ is the constructor for the rule for u and (l_{1}, …, l_{n}) is the tuple of labels in the left-hand side of the labelled rule for u. We call this the label of the redex. The index Ind(u) of u is the height of lab(u). The index Ind(P) of a reduction P is the maximal index of the redexes contracted in it.

This definition of labelling differs slightly from that of Klop [29]. Klop combines multiple labels on a single term into a single compound label, and thus for his definitions a term t^{α} is not a subterm of t^{α}^{β}, whereas for us the term t^{α} is a subterm of (t^{α})^{β}. He also represents compound labels as flat strings, instead of structured terms, using multiple underlining where we use multiple nesting. In addition, our use of label constructor symbols provides a greater generality which allows us simultaneously to treat several variants of labelled rewrite systems uniformly. (For example, in the case of the λ-calculus, there are two constructors in C corresponding to underlining and overlining [30, 31]. In the case of Interaction Systems [4] the constructors in C replace addresses in right-hand sides of rules. In the case of Klop’s labelling system [29], all constructors are ‘empty’. Redex-labels occurring as the arguments in right-hand sides of rewrite rules correspond to (constrained) labelled patterns in Maranget’s labelling system for TRSs [34]. And in his labelling system for HRSs, van Oostrom [44] uses numbers where we use constructors in C, and he uses rules where we use label constructors in C′.) However, our definitions are sufficiently close that Klop’s results for labelled systems carry over to the present setting.

The crucial properties of labelled reduction are given by the following propositions.

Proposition 10 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^{∗} strictly 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 the definition of labelling. Note that this is where we require the restriction on labelled OERSs, that each left-hand side contain more than one function symbol.

Corollary 11 In an OERS, let P and Q be co-initial reductions such that P creates a redex u and Q is external to every redex of t having a residual contracted in P. Then every member of u/(Q/P) is created by P/Q, and Q/P is external to u.

Proposition 12 In a labelled OERS, every reduction for which there is a bound on the indexes of the redexes it reduces is terminating.

Proof See [29, 37, 45].

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 differs from all known proofs because properties of needed and unneeded redexes are different when arbitrary stable sets are considered. The main difference is that S-unneeded redexes may replicate S-needed ones. However, the termination argument we use is the same as in [21] and in [35], and is based on Proposition 12. The main idea and a proof in the same spirit is already in [32]. As in most earlier 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.

In the rest of this section S always denotes a stable set of terms.

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

Q_{0} : t_{0} → → o_{0}. Then P′ = P/Q_{0} is external to U′ = U/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 U, we have for each i that v_{i} ∉ U/P_{i}. Therefore, v_{i}/Q_{i} ∩ U/(P_{i} + Q_{i}) = ∅ (since the residuals of different redexes are different). Thus, by Theorem 5, v_{i}/Q_{i} ∩ U/(Q_{0} + P′_{1} + … + P′_{i}) = ∅. Hence, P′_{i+1} is external to U′/(P′_{1} + … + P′_{i}). This means that P′ is external to U′. If P is S-normalizing, then so is P′, by the closure of S under reduction.

[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}; o_{n−1}; Q_{n−1}; P′_{n}; o_{n}; Q_{n}]

Corollary 14 For stable S, residuals of S-unneeded redexes are S-unneeded.

Lemma 15 Let t ∉ S, t→^{u}t′, UN_{S}(u, t), and let u′ ⊆ t′ be a created redex. Then UN_{S}(u′, t′). (Unneeded redexes cannot create needed redexes.)

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

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

Relative Normalization

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

(1) Every 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 14 and Lemma 15, either it is a residual of an S-needed redex in t, or it is created by an earlier step v of t → → s where v is S-needed. In the latter case the argument may be repeated.

(2) Let P : t → → e 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 10, Ind(P_{i}) ≤ Ind(P). Since Q is S-needed and P_{i} is S-normalizing (by the closure of S under reduction), at least one residual of u_{i} is contracted in P_{i}. Therefore, again by Proposition 10, Ind(u_{i}) ≤ Ind(P_{i}). Hence Ind(Q) ≤ Ind(P) and Q is terminating by Proposition 12.

t  [figure: P] s

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

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

[figure]

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

Lemma 17 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 16. 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 14, Lemma 15, and Lemma 17, in the following proposition.

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

(2) Let t ∉ S, t→^{u}t′, UN_{S}(u, t), and let u′ ⊆ t′ be a created 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 a practical point of view, as all the sets of results that have been used in practical programming languages are regular. Moreover, it allows for much simpler proofs. We do not need to consider termination of reductions with bounded index (Proposition 12), as the Finite Developments Theorem is enough. We do not use the Standardization Theorem [18, 29] either.

Failure of Relative Hypernormalization for some stable sets

For the case of normal forms, the needed strategy is hypernormalizing, that is, reductions starting from a normalizable term that contract finite sequences of unneeded steps in addition to needed redexes are still normalizing.

The following example shows that this need not be the case for all stable sets S:

Example 19 Consider R = {f(x) → h(x, f(x)), a → b} and take for S the set of terms not containing occurrences of a. Then the reduction f(a) → h(a, f(a)) → h(b, f(a)) → h(b, h(a, f(a))) → h(b, h(b, f(a))) → … contracts infinitely many Sneeded redexes, while the reduction f(a) → f(b) is S-normalizing. This example shows also that multistep S-needed reductions need not be S-normalizing: group each pair of consecutive steps in the reduction above as a multistep.

Regular Stable Sets

For some stable S, S-unneeded redexes may contain S-needed ones. Consider the simpler example R = {f(x) → g(x), a → b}, where S is the set of terms not containing occurrences of a: we observe that a is S-needed in f(a), but f(a) is not.

Nesting of S-needed redexes within S-unneeded ones need not cause problems; the failure of hypernormalization arises from duplication of S-needed redexes by Sunneeded ones. Hence we introduce the following definition:

Definition 20 We call a stable set R regular if, for any t ∉ R, R-unneeded redexes cannot duplicate R-needed ones.

Recall from [32] that multistep needed reductions are normalizing in the λ-calculus. The same holds for all regular stable R; this follows immediately from hypernormalization of the R-needed strategy, which we will prove in the rest of the section.

Canonical forms for Relative Reductions

The proof uses the ability to transform any reduction into an equivalent form where R-needed steps precede R-unneeded steps, while conserving the number of R-needed steps.

Definition 21 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_{N} + P_{U}, where P_{N} is S-needed and P_{U} is S-unneeded. In the latter case, we call P_{N} the S-needed part of P, and call P_{U} 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 22 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 will define a function K : Red → Red^{∗}. For any reduction P, with finite R-needed steps, we will denote the R-needed part K_{N}(P) and the R-unneeded part K_{U}(P) so that K(P) = K_{N}(P) + K_{U}(P). K is defined as follows:

(a) Let P be a finite reduction. K(P) is the R-semi-needed reduction obtained from P as follows: find in P the leftmost subreduction P_{1} : t→^{u}s→^{v}o such that UN_{R}(u, t) and NE_{R}(v, s). Let P = P_{0} + P_{1} + P_{2}. By Proposition 18.(2), v is a residual of a redex v′ ⊆ t, which is R-needed by Proposition 18.(1). Since R is regular, v is the only residual of v′, hence P_{1} and P′_{1} = v′ + u/v′ are both complete developments of the set u, v′ ⊆ t. Now replace P_{1} by P′_{1} 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. 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}, which 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} = K_{N}(P_{i}). Let |Q_{i}| = m_{i}. We define K(P) as the reduction whose prefix of length m_{i} is given by Q_{i} (i = 0, 1, …). It follows from (a)-(b) that if i < j, then Q_{i} is a prefix of Q_{j}, so K(P) is defined consistently. Obviously, K(P) is R-needed and hence K(P) ∈ Red^{∗}.

Lemma 23 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 K_{N}(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) follows immediately from Definition 22.

Lemma 24 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 23, t_{0} has an infinite R-needed reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} . . .. Let U_{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} ∉ U_{k} (otherwise there should be a number m such that t_{m}→^{u_{m}}t_{m+1} →^{u_{m+1}} … is an infinite U_{m}-development). By Proposition 18.(3), u_{k} ∉ U_{k} and NE_{R}(u_{k}, t_{k}) imply that u_{k} has at least one R-needed U_{k}-residual in s_{k}, i.e. u_{k}/U_{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 = U_{0}; u_{0}/U_{0}; s_{1}; U_{1}; u_{1}/U_{1}; s_{2}; U_{2}]

Relative Hypernormalization

Theorem 25 (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 24 Q/P is R-quasi-needed as well. By closure of R under reduction, Q/P is in R – a contradiction, since terms in R do not contain R-needed redexes. (⇐) By Theorem 16.(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

The theory of minimal reduction in the framework of relative normalization is based on reducing no more redexes than necessary when computing S-normal forms. A reduction P : t → → s with t ∉ S and s ∈ S is S-minimal if P ⊴Q for all S-normalizing Q : t → → e. Minimal S-normal forms, such as s above, are useful to compute since any other S-normal form is accessible from them.

We define S-external, persistently S-needed, and S-erased redexes. We show that each class is a strict subset of the next when S is regular, and use such redexes to build S-minimal reductions for regular S. We show that S-minimal reductions need not exist for irregular stable S.

Persistently S-needed and S-erased redexes

Definition 26 (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 27 Consider an OTRS R = {f(x) → g(x, h(x)), h(x) → c, a → b} and a term (redex) u = f(a):

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

Consider the following sets of terms in the reduction graph of u, in R: the set S_{1} = {g(b, c)} of normal forms; the set S_{2} = {g(b, h(a)),g(b, h(b)),g(b, c)} of terms not containing a redex on the left-spine, i.e. not containing a redex with its head symbol on the left-spine, when the term is considered as a tree; the set S_{3} = {f(b), g(b, h(b)), g(b, c)} of terms not containing occurrences of a; and the set S_{4} = {g(a, h(b)), g(a, c), f(b), g(b, h(b)), g(b, c)} of terms not containing a on the right-spine. Then 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. 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(a, h(a)) is S_{1}-unneeded. Nevertheless, 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. a is not S_{2}-erased as it 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.

Lemma 28 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. (⇐) ¿From Example 27 (cases 1 and 3).

Minimal Relative Reduction

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

It follows immediately from Definition 29 that if t ↓_{S} and t ∉ S, then t has no more than one 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 minimal S-normal forms cannot be taken as the definition, because in that case an S-normalizable term could have many 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 regular stable set S = {a, b}. The term t = f(a) has two S-normal forms, a and b, and each is accessible from the other. However, any reduction from t to b must contract the S-unneeded redex a and therefore no reduction from t to b can be considered as S-minimal.

Lemma 30 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.

Existence of Minimal S-normal forms

In the study of S-minimal reductions below , 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 31 Consider R = {f(x) → g(x, x), a → b}, with term t = f(a), and let S = {g(b, a), f(b), g(b, b)}, the set of terms not containing a on the left spine.

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

f(a)  \overline{}g(a, a)

[figure]

g(a, b)  g(b, a)

[figure]

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

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, but duplicates the innermost one which is S-needed.

There are three candidates for S-minimal reductions starting from t: P : f(a) → f(b) and 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 P and Q, but they clearly cannot be Sminimal. We have P ⋬ Q as P/Q = g(b, a) → g(b, b), Q⋬ P as Q/P = f(b) → g(b, b), and N ⋬ P as, again, N/P = f(b) → g(b, b). Hence none of the reductions is Sminimal.

S-external redexes

We go on to 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. However, S-erased reductions need not be S-needed, and hence need not be S-normalizing, and again for regular S, we show existence of S-external S-normalizing reductions, which are S-needed S-minimal reductions.

Definition 32 Let U ⊆ t. We call P an U-reduction if it contracts only residuals of redexes from U and created redexes; we call such redexes U-redexes. Below U(t) will denote the set of all redexes of t, and U_{S}(t) will denote the set of S-needed redexes of t.

Definition 33 (1) Let U ⊆ t. We call a redex u ⊆ t U-external (in t) if u ∈ U and, for any U-reduction P, none of the residuals of u along P appear in arguments of U-redexes.

(2) We call u ⊆ t external in t if it U(t)-external, and S-external if it is U_{S}(t)- external. (Thus any S-external redex is necessarily S-needed.) We call a reduction P S-external if each redex contracted in it is.

Example 34 Consider an OTRS R = {a → c, b → b′, f(c, x) → c′}, and take the term t = g(f(a, b), a). Both occurrences of a in t are external in t, while b is not external 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 U ⊆ t contains two redexes – the first occurrence of a in t and the redex b ⊆ t, then only the first a ⊆ t is U-external 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-external redex in t (it is the only S-needed redex too).

It is shown in [18, 25, 27] that any term t not in normal form contains an external redex (such redexes are called unabsorbed in [25, 13]). Now, if one ignores all redexes in t except those in U ⊆ t, it follows that, for any U ≠ ∅, U contains an U-external redex. And by taking U_{S}(t) for U (U_{S}(t) ≠ ∅ by Theorem 16), we obtain the following proposition:

Proposition 35 Every term t ∉ S contains an (S-needed) S-external redex.

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

Proof Let P : t → → o, not necessarily an U_{R}(t)-reduction. By Proposition 18.(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 23, 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 18.(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-external, u′′ ∉ w′′. Hence u′′ has exactly one w′′-residual, say u^{∗}. By Theorem 5, w′′ + P′′/w′′ replicates u′′, since w′ replicates u′. Thus P′′/w′′ replicates u^{∗} – a contradiction, since P′′/w′′ is R-unneeded by Proposition 18.(1), and R is regular.

Note that if S is irregular, then an S-external redex u ⊆ t need not be persistently S-needed or S-erased. Indeed, take R, S, and Q as in Example 31. Then a in t is Sneeded, 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-external, since the only U_{S}(t)-reduction is N : f(a) → f(b), and a is U_{S}(t)-external in N.

Characterizing R-minimal reductions

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

Proof (⇐) From Lemma 30. (⇒) Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be R-minimal, and let Q : t_{0} → → o be R-external, hence R-erased by Lemmas 36 and 28, R-normalizing reduction; Q exists by Proposition 35. 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 reduction. Hence Q_{i} is R-minimal by Lemma 30. 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.

Minimal Relative Normalization

Theorem 38 (Minimal Relative Normalization) Let R be a regular stable set of terms in an OERS, and let t ↓_{R} where t ∉ R. Then repeated contraction of Rneeded 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} where t ∉ R has an R-external R-minimal reduction, which is R-needed.

Proof By Proposition 35, any t ↓_{R} where t ∉ R has an R-external redex, which is R-needed and R-erased by Lemma 36 and Lemma 28. It remains to apply Theorem 16 and Proposition 37.

8 The Relative Standardization Theorem

Recall that a reduction is standard if redexes in it are contracted in left-to-right outside-in order [5, 18, 29]. Maranget proved in [35] that standard reductions are minimal among reductions computing a ‘stable prefix’ of a term, in an OTRS. Note that for regular R, in general, R-normalizing standard reductions need not be Rneeded, according to the definitions of [5, 18, 29], or according to [16], where left-to-right order of contracted redexes is not required.

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 and the final term is not a minimal R-normal form.

Therefore, we should require that relative standard reductions are R-minimal as in the following definition:

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

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

Relative Standardization

Theorem 40 (Relative Standardization) Let R be a regular stable set of terms in an OERS, and let t ↓_{R} where t ∉ R. Then t has an R-standard R-normalizing reduction. In particular, R-external 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 Section 4.

Definition 41 For 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 42 A multistep reduction P : t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} … → → t_{n} is called a familyreduction if each U_{i} is a set of redexes belonging to the same family (t_{i} → →^{U_{i}} t_{i+1} is the multistep corresponding to complete developments of U_{i}). ∥P ∥ will denote the number of multisteps in P. The family-reduction P is complete if each U_{i} is a maximal set of redexes of t_{i} belonging to the same family. A family-reduction P is called S-needed if each U_{i} contains at least one S-needed redex.

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

Lemma 43 Every family is contracted at most once in a complete family-reduction.

Proof Let P_{n} : t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} … → →^{U_{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 label of any new redex in t_{n} must contain lab(U_{n−1}). 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(U_{n−1}) ≠ lab(U_{i}), for all i < n − 1. Thus (b)_{n} is also valid.

Relative Optimality

Theorem 44 (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 [32]. Let P : t → → s be an S-normalizing family-reduction and Q : t → →^{U_{0}} t_{1}→^{U_{1}} … be an Sneeded complete family-reduction. Further, let Q_{i} : t → →^{U_{0}} t_{1}→^{U_{1}} … → → t_{i} and P_{i} = P/Q_{i}. By Proposition 10, FAM(P_{i}) ⊆ FAM(P). Since Q is S-needed, at least one residual of some u_{i} ∈ U_{i} is contracted in P_{i} (P_{i} is S-normalizing by the closure of S under reduction). Hence, again by Proposition 10, FAM(Q) ⊆ FAM(P). Hence, by Lemma 43, ∥Q∥ = Card(FAM(Q)) ≤ Card(FAM(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 Runneeded members, is still optimal. We will call this an R-needed semi-complete family-reduction. It follows from Proposition 37 that such a reduction is R-minimal as well iff every R-needed redex contracted in it is R-erased.

For example, consider R = {g(x) → f(x, x), a → b}, where R is the set of terms not containing left-spine redexes. Then g(a) → f(a, a) → f(b, a) is both R-minimal and a R-optimal semi-complete family-reduction, whereas complete family reductions would lead to f(b, b) which is not the minimal R-normal form.

However, the following example shows that a term in an OERS need not possess an R-minimal R-optimal semi-complete family-reduction:

Example 45 For the OERS R = {σxAB → δx(((A/x)B/x)A), f(A) → g(A, A)}, 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 does 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. That is, no R-unneeded redex can contain (or duplicate) a R-needed one.

Now let us consider the term t = σx(f(x), x). There are two R-needed semicomplete family-reductions 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 46 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 (e.g.

{h(b, a), h(b, b)}).

f(a)  \overline{}g(a, a)

[figure]

g(a, b)  g(b, a) \overline{}h(a, a)

[figure]

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

[figure]

h(b, b)

By the same argument as in Example 45, 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 47 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 when graph rewriting is concerned.

11 Conclusions

We have investigated properties which a set S of ‘final terms’ or ‘(partial) results’ should possess 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.

The abstract content of the relative normalization and optimality results has been analyzed by introducing stable Deterministic Residual Structures (SDRSs) and Deterministic Family Structures, respectively [15]. SDRSs axiomatize the residual relation in orthogonal systems, and DFSs are SDRSs with an axiomatized family relation. And our minimality results hold in such SDRSs where every set U of redexes in a term has an element that has at most one residual under any U-reduction (for example, U-external redexes in OERSs are such). Since this work was first presented, Melliès [38] has also established minimality results for his axiomatic rewrite systems.

Acknowledgments

We thank 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 referees provided valuable suggestions. The diagrams were drawn using P. Taylor’s diagram package.

References

[1] P. Aczel. A general Church-Rosser theorem. Technical report, University of Manchester, 1978.

[2] S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. In 21^{st} ACM Symposium on Principles of Programming Languages, POPL’94, pages 268–279. ACM, 1994.

[3] S. Antoy and A. Middeldorp. A sequential reduction strategy. Theoretical Computer Science, 165(1):75–95, 1996.

[4] A. Asperti and C. Laneve. Interaction Systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, 11:1–48, 1993.

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

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

[7] H. P. Barendregt, J. R. Kennaway, J. W. Klop, and M. R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information and Computation, 75(3):191–231, 1987.

[8] G. Berry and J.-J. Lévy. Minimal and optimal computations of recursive programs. Journal of the ACM, 26:148–175, 1979.

[9] G. Boudol. Computational semantics of term rewriting systems. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, pages 169–236. Cambridge University Press, 1985.

[10] H. B. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, 1958.

[11] P. Gardner. Discovering needed reductions using type theory. In M. Hagiya and J. C. Mitchell, editors, 2^{nd} International Symposium on Theoretical Aspects of Computer Software, TACS’94, volume 789 of LNCS, pages 555–574. Springer-Verlag, 1994.

[12] J. R. W. Glauert and Z. Khasidashvili. Minimal and optimal relative normalization in expression reduction systems. Technical Report SYS-C94-06, UEA, Norwich, UK, 1994.

[13] J. R. W. Glauert and Z. Khasidashvili. On relative normalization in orthogonal expression reduction systems. In N. Dershowitz and N. Lindenstrauss, editors, 4^{th} International Workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, volume 968 of LNCS, pages 144–165. Springer-Verlag, 1994.

[14] J. R. W. Glauert and Z. Khasidashvili. Minimal relative normalization in orthogonal expression reduction systems. In V. Chandru, editor, 16^{th} International Conference on Foundations of Software Technology and Theoretical Computer Science, FST&TCS’96, volume 1180 of LNCS, pages 238–249, 1996.

[15] J. R. W. Glauert and Z. Khasidashvili. Relative normalization in deterministic residual structures. In H. Kirchner, editor, 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’96, volume 1059 of LNCS, pages 180–195. Springer-Verlag, 1996.

[16] G. Gonthier, J.-J. Lévy, and P.-A. Melliès. An abstract standardisation theorem. In 7^{th} Annual IEEE Symposium on Logic in Computer Science, LICS’92, pages 72–81. The IEEE Computer Society Press, 1992.

[17] M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In H. Ganzinger, editor, 7^{th} International Conference on Rewriting Techniques and Applications, RTA’96, volume 1103 of LNCS, pages 138–152. Springer-Verlag, 1996.

[18] G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems. In J.-L. Lassez and G. Plotkin, editors, Computational Logic, Essays in Honor of Alan Robinson. MIT Press, 1991.

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

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

[21] J. R. Kennaway and M. R. Sleep. Neededness is hypernormalizing in regular combinatory reduction systems. Technical report, UEA, Norwich, UK, 1989.

[22] Z. Khasidashvili. β-reductions and β-developments of λ-terms with the least number of steps. In P. Martin-Löf and G. Mints, editors, International Conference on Computer Logic, COLOG’88, volume 417 of LNCS, pages 105–111. Springer-Verlag, 1990.

[23] Z. Khasidashvili. Expression reduction systems. In Proceedings of I. Vekua Institute of Applied Mathematics of Tbilisi State University, volume 36, pages 200–220, Tbilisi, 1990.

[24] Z. Khasidashvili. The Church-Rosser theorem in orthogonal combinatory reduction systems. Technical Report 1825, INRIA Rocquencourt, 1992.

[25] Z. Khasidashvili. Optimal normalization in orthogonal term rewriting systems. In C. Kirchner, editor, 5^{th} International Conference on Rewriting Techniques and Applications, RTA’93, Montreal, volume 690 of LNCS, pages 243–258. Springer-Verlag, 1993.

[26] Z. Khasidashvili. On higher order recursive program schemes. In S. Tison, editor, 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’94, Edinburgh, volume 787 of LNCS, pages 172–186. Springer-Verlag, 1994.

[27] Z. Khasidashvili, M. Ogawa, and V. van Oostrom. Perpetuality and uniform normalization in orthogonal rewrite systems. Information and Computation, To appear. Available from http://www.brl.ntt.co.jp/people/mizuhito/papers/TRS.html.

[28] Z. Khasidashvili and A. Piperno. Normalization of typeable terms by superdevelopments. In Proceedings of CSL’98, volume 1584 of LNCS, pages 260–282. Springer-Verlag, 1999.

[29] J. W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, Amsterdam, 1980.

[30] J.-J. Lévy. An algebraic interpretation of the λβK-calculus; and an application of a labelled lambda calculus. Theoretical Computer Science, 2:97–114, 1976.

[31] J.-J. Lévy. Réductions Correctes et Optimales dans le Lambda-Calcul. Thèse de l’Université de Paris VII, 1978.

[32] J.-J. Lévy. Optimal reductions in the lambda-calculus. In J. R. Hindley and J. P. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 159–192. Academic Press, 1980.

[33] G. Longo. Set theoretic models of lambda calculus: Theories, expansions and isomorphisms. Annals of Pure and Applied Logic, 24:53–188, 1983.

[34] L. Maranget. Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems. In 17^{th} ACM Symposium on Principles of Programming Languages, POPL’91, pages 255–269. ACM, 1991.

[35] L. Maranget. La Stratégie Paresseuse. Thèse de l’Université de Paris VII, 1992.

[36] R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.

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

[38] P. A. Melliès. A stability theorem for rewriting theory. In Proceedings of LICS’98, 1998.

[39] A. Middeldorp. Call by need computations to root-stable form. In 24^{th} ACM Symposium on Principles of Programming Languages, POPL’97, pages 94–105. ACM, 1997.

[40] E. Nöcker. Efficient Functional Programming: Compilation and Programming Techniques. PhD thesis, University of Nijmegen, 1994.

[41] Sh. Pkhakadze. Some problems of the notation theory (in Russian). In Proceedings of I. Vekua Institute of Applied Mathematics of Tbilisi State University, Tbilisi, 1977.

[42] R. C. Sekar and I. V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. Information and Computation, 104(1):78–109, 1993.

[43] V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Free University, Amsterdam, 1994.

[44] V. van Oostrom. Higher order families. In H. Ganzinger, editor, 7^{th} International Conference on Rewriting Techniques and Applications, RTA’96, volume 1103 of LNCS, pages 392–407. Springer-Verlag, 1996.

[45] V. van Oostrom. Finite family developments. In H. Common, editor, 8^{th} International Conference on Rewriting Techniques and Applications, RTA’97, volume 1232 of LNCS, pages 308–322. Springer-Verlag, 1997.

[46] V. van Oostrom. Normalisation in weakly orthogonal rewriting. In 10^{th} International Conference on Rewriting Techniques and Applications, RTA’99, volume 1631 of LNCS, pages 60–74. Springer-Verlag, 1999.

[47] V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies confluence: The higher-order case. In A. Narode and Yu. V. Matiyasevich, editors, 3^{rd} International Conference on Logical Foundations of Computer Science, LFCS’94, volume 813 of LNCS, pages 379–392. Springer-Verlag, 1994.

[48] F. van Raamsdonk. Confluence and Normalisation for Higher-Order Rewriting. PhD thesis, Free University, Amsterdam, 1996.

[49] G. Winskel. An introduction to event structures. In Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency, volume 354 of LNCS, pages 364–397. Springer-Verlag, 1989.

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