Minimal Relative Normalization in Orthogonal Expression Reduction Systems

John Glauert and Zurab Khasidashvili

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

Abstract. In previous papers, the authors studied normalization relative to desirable sets S of ‘partial results’, where it is shown that such sets must be stable. For example, the sets of normal forms, head-normal-forms, and weak head-normal-forms in the λ-calculus, are all stable. They showed that, for any stable S, S-needed reductions are S-normalizing. This paper continues the investigation into the theory of relative normalization. In particular, we prove existence of minimal normalizing reductions for regular stable sets of results. All the above mentioned sets are regular. We give a sufficient and necessary criterion for a normalizing reduction (w.r.t. a regular stable S) to be minimal. Finally, we establish a relationship between relative minimal and optimal reductions, revealing a conflict between minimality and optimality: for regular stable sets of results, a term need not possess a reduction that is minimal and optimal at the same time.

1 Introduction

The Normalization Theorem in the λ-calculus, due to Curry and Feys [CuFe58], states that contraction of leftmost-outermost redexes in a term t yields a normal form whenever t is normalizable, even if t has infinite reduction sequences.

Generalizing this fundamental theorem to a large class of Orthogonal Term Rewriting Systems (OTRSs), Huet and Lévy laid the foundations of a regular theory of ‘normalization by neededness’ in [HuLé91]. They proved that any term t not in normal form, in an OTRS, has a needed redex, and that contraction of needed redexes in a normalizable term results in a normal form. Here a redex u in t is needed if some residual of it is contracted in every normalizing reduction starting from t.

Barendregt et al. [BKKS87] applied the neededness notion to the λ-calculus, and studied neededness not only w.r.t. normal forms, but also w.r.t. head-normal forms. The authors proved correctness of the two needed strategies for computing corresponding normal forms. In [Mar92], Maranget also 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].

In [GlKh94], the present authors studied normalization with respect to any desired set of final terms, and found the sufficient and necessary properties, called

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

stability, that a set S of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. That is, they showed that, for any stable S, each S-normalizable term not yet in S (not in S-normal form) has at least one S-needed redex, and that repeated contraction of S-needed redexes in a term t will lead to an S-normal form of t whenever there is one. It is shown also that if a stable S is regular, i.e., if S-unneeded redexes cannot duplicate S-needed ones, then the S-needed strategy is hypernormalizing as well. This work was performed in the context of Orthogonal Expression Reduction Systems (OERSs) [Kha92], a form of higher-order rewriting which subsumes TRSs and the λ-calculus and is similar to Klop’s Combinatory Reduction systems (CRSs) [Klo80]. Most of these results were later generalized to an abstract framework of Deterministic Residual Structures [GlKh96].

Normalization theory has developed in other directions as well, of which we mention only a few. Boudol extended neededness theory to non-orthogonal TRSs [Bou85]. Khasidashvili defined a similar normalizing strategy, the essential strategy, in the λcalculus, OTRSs and OERSs [Kha88, Kha93, Kha94]. Kennaway and Sleep [KeSl89] generalized the needed strategy to Klop’s orthogonal CRSs [Klo80]. Sekar and Ramakrishnan [SeRa93] study a normalizing strategy which in each multi-step contracts a necessary set of redexes – a set at least one member of which is contracted in every normalizing reduction. A different approach to normalization in not-necessarily orthogonal rewrite systems is developed in Kennaway [Ken89] and Antoy&Middeldorp [AnMi94]. Antoy et al. [AEH94] designed a needed narrowing strategy. Gardner [Gar94] described a complete way of encoding neededness information using a type assignment system. Kennaway et al. [KKSV95] studied a needed strategy for infinitary OTRSs.

The contribution of this paper is to develop a theory of minimal reduction in the framework of relative normalization, and to establish a relationship between minimal and optimal [Lév78] reductions. 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 [Lév78] 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. However, we will show that standard reductions are not always minimal in the relative case, and a different concept of standard reduction is required.

The earliest 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.

In this paper, we restrict ourselves to finite reductions only. 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 Snormalizing reductions. We further give a sufficient and necessary criterion for an S-normalizing reduction to be S-minimal. We show also that S-minimal reductions need not exist if S is stable but is irregular.

It has been shown in [GlKh96] that complete S-needed family-reductions, which contract all members of a redex-family containing an S-needed redex in a multi-step, are optimal in the sense that they reach S in the least number of family-reduction steps. S-needed complete family reductions, though optimal, need not be S-minimal, because they may contract S-unneeded redexes that are S-essential. It is tempting to think that contracting only the S-needed redexes of S-needed families would 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. As a consequence, a term need not have a reduction that is both minimal and optimal at the same time.

The paper is organized as follows. In section 2, we introduce higher order rewriting through Expression Reduction Systems. In section 3, we review the theory of relative normalization. In section 4, we study S-minimal reductions for regular stable sets S, and in section 5, we relate relative optimal and minimal reductions. Conclusions appear in section 6. 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]. Several interesting formalisms have been introduced later [Kha92, 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θ. We call R simple if right-hand sides of R-rules are simple metaterms.

Our syntax is similar to that of Klop’s CRSs [Klo80], but is simpler and 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. We will indeed do so at least when giving TRS examples.

Notation 2.1 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 immediately from the definition of / that if P and Q are co-initial reductions in an OERS, then (P + P′)/Q ≈_{L} P/Q + P′/(Q/P) and P/(Q + Q′) ≈_{L} (P/Q)/Q′.

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

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

3 Relative Normalization

In this section, we review some notions and results concerning relative normalization from [GlKh94].

Definition 3.1 Let S be a set of terms in an OERS R. We call a redex u ⊆ t Sneeded, written NE_{S}(u, t), if at least one residual of it is contracted in any reduction from t to a term in S, and call it S-unneeded, written UN_{S}(u, t), otherwise.

Definition 3.2 (1) We call a set S of terms stable iff (a) S is closed under parallel moves: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e which 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. (2) We call a stable S regular iff S-unneeded redexes cannot duplicate S-needed ones.

Below S, resp. R, will denote a stable, resp. regular stable, set of terms in an OERS. t↓_{S} will denote that t is S-normalizable, i.e., reducible to a term in S, and similarly for t↓_{R}.

Lemma 3.1 (1) Residuals of S-unneeded redexes in a term t ∉ S are 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, NE_{S}(v, t), and v ≠ u. Then v has an S-needed residual in s.

Theorem 3.1 (Relative Normalization) Let S be a stable set of terms in an OERS R. Then any S-normalizable term t in R not in S-normal form contains an S-needed redex; and any S-needed reduction starting from t eventually terminates at a term in S. If S is moreover regular, then S-needed reductions starting from t eventually reach S even if finite sequences of consecutive S-unneeded steps are also allowed.

4 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 coinitial 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. Below we always consider reductions in OERSs.

Definition 4.1 (1) We call u ⊆ t persistently S-needed if all residuals of u are S-needed. (2) We call u ⊆ t S-erased if u doesn’t have a residual under any Snormalizing reduction. 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 4.1 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 4.1 Every persistently S-needed redex is S-erased, but an S-erased redex, even if S-needed, need not be persistently S-needed.

Proof. (⇒) Let u ⊆ t be persistently S-needed, and let P : t → → s be S-normalizing. If u/P was not empty, then every u′ ∈ u/P (the set of P -residuals of u) would be S-needed, which is not possible since s ∈ S. (⇐) From Example 4.1 (cases 1 and 3).

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

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

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

Proof. Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be an S-erased S-normalizing reduction, let

P_{i} : t_{0}→^{u_{0}} … → t_{i}, and let Q : t_{0} → → o ∈ S. By stability of S, Q_{i} = Q/P_{i} is

S-normalizing. Since u_{i} is S-erased and Q_{i} is S-normalizing, u_{i}/Q_{i} = ∅. Hence P/Q = ∅, i.e., P is S-minimal.

Definition 4.3 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 4.4 (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 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 4.2 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 3.1), we obtain the following proposition:

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

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

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 4.3 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 4.3 For any P : t → → s with t ∉ R, there is an R-needed Q, containing the same number of steps as that of R-needed steps in P, and an R-unneeded N, such that P ≈_{L} Q + N; and if P is R-normalizing or contains infinitely many R-needed steps, then N = ∅.

Proof. The lemma was proved in [Kha88, Kha93] for the case of essentiality in place of R-neededness. The same proof applies in this case.

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

Proof. Let P : t → → o, not necessarily an F_{ℜ}(t)-reduction. By Lemma 3.1.(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 → → s 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 4.3, 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 Lemma 3.1.(2) that there are R-needed u′′ and w′′ in the final term of P′ such that u′ and w′ are the only residuals of u′′ and w′′, respectively. Since u is R-unabsorbed, u′′ ∉ w′′. Hence u′′ has exactly one w′′-residual, say u^{∗}. By Theorem 2.1, w′′ + P′′/w′′ replicates u′′, since w′ replicates u′. Thus P′′/w′′ replicates u^{∗} – a contradiction, since P′′/w′′ is R-unneeded by Lemma 3.1.(1), and R is regular.

Note that if S is irregular, then an S-unabsorbed redex u ⊆ t need not be persistently S-needed or S-erased. Indeed, take R, S, and Q as in Example 4.3. 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 4.2 An R-normalizing reduction is R-minimal iff it is R-erased.

Proof. (⇐) From Lemma 4.2. (⇒) Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be R-minimal, and let Q : t_{0} → → o be R-unabsorbed, hence R-erased by Lemmas 4.4 and 4.1, R-normalizing reduction; Q exists by Proposition 4.1. 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 4.2. Since P is R-minimal too, u_{i}/Q_{i} = ∅ for every i. But for every R-normalizing reduction Q′_{i} : t_{i} → → o_{i}, it holds that Q_{i} ⊴ Q′_{i} (since Q_{i} is R-minimal). Hence u_{i}/Q′_{i} = ∅, i.e., u_{i} is R-erased, and P is R-erased too.

Remark 4.1 It can be shown that a redex u ⊆ t ∉ R is R-erased iff every residual of u (in particular, u itself) along any reductions starting from t is either R-needed or R-inessential. Here a subterm s ⊆ t is S-inessential iff there is no S-normalizing P starting from t such that s has a P -descendant. The latter notion is a refinement of that of residual, allowing tracing of contracted redexes – the descendant of a contracted redex is its contractum, while it does not have residuals [Kha92]. One can show also that a redex u ⊆ t ↓_{R}∉ R is R-inessential iff it is R-unneeded and R-erased. Note that the latter proposition can be taken as the definition of S- (in)essentiality, thus avoiding the use of the descendant concept, and the above characterization of R-erased redexes follows logically. See [GlKh94a] for details.

Now we are ready to prove the main result of the paper.

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

Proof. By Proposition 4.1, any t ↓_{R}∉ R has an R-unabsorbed redex, which is Rneeded and R-erased by Lemma 4.4 and Lemma 4.1. It remains to apply Theorem 3.1 and Proposition 4.2.

Remark 4.2 (Relative Standardization) Note that R-normalizing standard reductions (in the sense of [Bar84, 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. It is not difficult to see that R-unabsorbed R-normalizing reductions are then R-standard in the sense of [GLM92], and the left-to-right order of contraction of R-unabsorbed redexes can also be achieved by Klop’s standardization theorem [Klo80], which is valid for OERSs as well.

5 Relative optimal versus minimal reductions

Lévy introduced the notion of redex family in the λ-calculus, and showed that any multi-step reduction that in each multi-step contracts all redexes in a needed family (i.e., a family containing a needed redex) is optimal in the sense that it reaches a normal form (when it exists) in a minimal number of family-reduction steps [Lév78, Lév80]. This theory has been generalized to OTRSs, Interaction Systems, and higher-order rewrite systems [Mar91, AsLa93, Oos96], and to the case of relative normalization, to all Deterministic Family Structures [GlKh96]. The latter are abstract rewrite systems with axiomatized residual and family relations, and model family concepts in all orthogonal rewrite systems, OERSs among them. Redex families consist of ‘redexes with the same origin’, and here we only need to know that, in particular, all residuals of the same redex are in the same family.

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 such reductions R-needed semicomplete family-reductions. It follows from Proposition 4.2 that such a reduction is R-minimal as well iff every R-needed redex contracted in it is R-erased. For example, g(a) → f(a, a) → f(b, a) is both R-minimal and R-optimal semi-complete family-reduction in R = {g(x) → f(x, x), a → b}, where R is the set of terms not containing left-spine redexes. However, the following examples show that a term either in an OTRS or in the λ-calculus need not possess an R-minimal R-optimal family-reduction.

Example 5.1 Consider the OTRS R = {f(x) → g(x, x), g(b, x) → h(x, x), a → b}, and take for R the set of terms not containing left-spine redexes. One can show that R is regular. 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 Rneeded, but their contraction makes h(b, a) unreachable. Thus there is no R-minimal reduction that is R-optimal at the same time.

Example 5.2 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).

6 Conclusions and Future Work

We have studied minimal normalization relative to regular stable sets R of final terms, and have shown that R-normalizing reductions that are both minimal and optimal need not exist for an 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 context-sensitive conditional OERSs [KvO95], and therefore apply to numerous typed λ-calculi as well. We expect that the results remain valid for other systems of higher-order rewriting too.

Similar questions arise for infinite reductions. Stability and regularity of sets of finite and infinite reductions must be defined first, and we expect a strong connection between this concept and the concept of stability in interpretations [BeLé79].

As already mentioned in [GlKh94], it would be interesting to investigate strong sequentiality and strictness analyses for arbitrary stable sets of normal forms. Investigation of minimal relative normalization in an abstract setting seems also feasible and is useful.

Acknowledgments We thank J. R. Kennaway, J.-J. Lévy, L. Maranget, V. van Oostrom and F. van Raamsdonk for useful comments.

References

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

[AEH94] Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of 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. MSCS, 11:1-48, Cambridge University Press, 1993.

[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. Inf.& Comp., 75(3):191-231, 1987.

[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. Cambr. Univ. Press, 1985, p. 169-236.

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

[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. Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of 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 CAAP’96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180-195.

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: LICS’92, 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, 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 Int. Conference on Computer Logic COLOG’88, Tallinn 1988, Springer LNCS, v. 417, P. Martin-Löf and G. Mints, eds. 1990, p. 105-111.

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

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

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

[Mar91] Maranget L. Optimal derivations in weak λ-calculi and in orthogonal Term Rewriting Systems. In: Proc. POPL’91, p. 255-269.

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

[Nip93] Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of TLCA’93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds., 1993, p. 306-317.

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

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

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

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

[OR94] Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc. of LFCS’94, Springer LNCS, vol. 813, Narode A., Matiyasevich Yu. V. eds. St. Petersburg, 1994. p. 379-392.

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

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

This article was processed using the L^{A}TEX macro package with LLNCS style