Minimal and Optimal Relative Normalization in Orthogonal Expression Reduction Systems

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

Submitted to PLILP 95

Abstract

This paper continues an investigation into the theory of normalization relative to desirable sets S of ‘normal forms’, started in [GlKh94], where it is shown that such sets must be stable. In particular, we prove existence of minimal normalizing reductions for regular stable sets of normal forms, and give a sufficient and necessary criterion for a normalizing (w.r.t. a regular stable S) reduction to be minimal. The sets of normal forms, head-normal-forms, weak head-normal-forms, etc. are all regular stable sets. As a corollary, we obtain the Relative Standardization theorem. Further, we generalize Lévy’s Optimality theorem to the case of all stable sets of normal forms, and establish a relationship between relative minimal and optimal reductions, revealing a conflict between minimality and optimality of a reduction – for regular stable sets of normal forms, a term need not posses a reduction that is minimal and optimal at the same time. We also introduce and study a relative notion of essentiality and relate it to the relative notion of neededness. This study gives a clearer picture of the character of redexes that are contracted in minimal S-normalizing reductions.

Correspondence Address

John Glauert School of Information Systems University of East Anglia Norwich NR4 7TJ England

Email: jrwg@sys.uea.ac.uk Tel: +44 1603 592671 Fax: +44 1603 593344

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

1 Introduction

A normalizable term, in a rewriting system, may have an infinite reduction, so it is important to have a normalizing strategy which enables one to construct reductions to normal form. It is well known that the leftmost-outermost strategy is normalizing in the λ-calculus.

For Orthogonal Term Rewriting Systems (OTRSs), a general normalizing strategy, called the needed strategy, was found by Huet and Lévy in [HuLé91]. The needed strategy always contracts a needed redex – a redex whose residual is to be contracted in any reduction to normal form. Huet and Lévy showed that any term t not in normal form has a needed redex, and that repeated contraction of needed redexes in t leads to its normal form whenever there is one.

Barendregt et al. [BKKS87] generalized the concept of neededness to the λ-calculus. They studied neededness not only w.r.t. normal forms, but also w.r.t. head-normal forms – a redex is head-needed if its residuals are contracted in each reduction to a head-normal form. The authors proved correctness of the two needed strategies for computing normal forms and head-normal forms, respectively. In [Mar92], Maranget studied also a strategy that computes a weak head-normal form of a term in an OTRS. Normalization w.r.t. another interesting set of ‘normal forms’, that of constructor head-normal forms in constructor OTRSs, is studied by Nöcker [Nök94].

In [GlKh94], the present authors address the question of normalization with respect to a desired set of final terms, considering the properties that a set of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. They introduce the notion of neededness w.r.t. a set of reductions Π or a set of terms S so that each existing notion of neededness can be given by specifying Π or S. For example, Huet&Lévy-neededness is neededness w.r.t. the set of normal forms, Maranget-neededness is neededness w.r.t. all fair reductions, head-neededness is neededness w.r.t. the set of head-normal forms, etc. This work was performed in the context of Orthogonal Expression Reduction Systems (OERSs) [Kha90, Kha92], a form of higher-order rewriting which subsumes TRSs and the λ-calculus.

Natural conditions are imposed on S, called stability, that are sufficient and necessary so that each S-normalizable term not yet in S (not in S-normal form) has at least one S-needed redex, and so 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.

The contribution of this paper is to develop a theory of minimal and optimal reduction in the framework of relative normalization, and to 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 [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. 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. Clearly this concept of minimality is not useful for full normal forms.

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 M-minimal Snormalizing reductions. These redexes play the role of standard redexes w.r.t. S, since they are S-needed and cannot be duplicated. We further give a sufficient and necessary criterion for an S-normalizing reduction to be S-minimal. We show also that S-minimal reductions need not exist if S is stable but is irregular.

To give the characterization of S-minimal reductions, we introduce a relative notion of essentiality. A subterm s ⊆ t is said to be S-essential if it has a descendant under at least one S-normalizing reduction of t. The notion of descendant is a refinement of that of residual – the descendant of a contracted redex is its contractum, while it does not have residuals. The notion of essentiality (i.e., w.r.t. normal forms) was introduced in [Kha93, Kha88], where the essential strategy was shown to be normalizing for OTRSs and the λ-calculus (the strategy works for OERSs as well [GlKh94]).

For the case of normal forms, essentiality coincides with Maranget’s concept of neededness, while in the general case, for stable S, the two concepts are different. All S-needed redexes are S-essential. S-unneeded redexes may be S-essential, in which case they contribute to the minimal S-normal form, or can be S-inessential in which case they will be erased under any reduction to S-normal form. Inessentiality is related to the notion of garbage – an inessential subterm may be replaced by any term without affecting the normal form. However, for certain stable and even regular S, replacing an S-inessential subterm by another term may lead to an S-essential subterm at the same position, and the S-normal form of the term may be changed.

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

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

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

In section 2, we introduce higher order rewriting through Expression Reduction Systems. In section 3, we review the theory of relative normalization [GlKh94]. In section 4, we study S-minimal reductions for regular stable sets S. In section 5, we study the relative notion of essentiality, and in section 6, reductions standard w.r.t. regular stable sets. In section 7, we prove the Relative Optimality theorem. Finally, in section 8, we relate relative optimal and minimal reductions.

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 [Nip93, OR94]. We refer to Klop et al. [KOR93] for a survey. Here we use a system of higher order rewriting, Expression Reduction Systems (ERSs), as defined in [GlKh94].

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

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

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

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

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

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

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

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

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

To express substitution, we use the S-reduction rules

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

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

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

Let t →^{u} s be an R_{f}-reduction step and let e be the contractum of u in s. For each argument o of u there are 0 or more arguments of e. We call them (u-)descendants of o. Correspondingly, subterms of o have 0 or more descendants. The descendant of each pattern-subterm (i.e., a subterm rooted within the pattern) of u is e. It is clear what is to be meant by descendants of a subterm that is

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

t_{i} and subterms in t_{i} have the same number of descendants as the number of free occurrences of x_{i} in t_{0}. All subterms of t_{0} have exactly one descendant (the descendants of the free occurrences of x_{1}, …, x_{n} in t_{0} are the substituted subterms). The descendant of the contracted redex u itself is its contractum. The notion of descendant extends by transitivity to arbitrary R_{fS}-reductions. If P is an R-reduction, then P -descendants are defined to be the descendants under the refinement of P. The ancestor relation is converse to that of descendant. Descendants of all redexes except the contracted redex are residuals. If t →^{u} s in R, then a redex in s is called a new redex or a created redex if it is not a residual of a redex of t.

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

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, P′, Q and Q′ are coinitial reductions in an OERS, then (P +P′)/Q ≈_{L} P/Q+P′/(Q/P) and P/(Q+Q′) ≈_{L} (P/Q)/Q′. Below, we use the following strong and strict Church-Rosser properties:

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

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

3 Relative Normalization

In this section, we review some notions and results concerning relative normalization from [GlKh94]. Below we always consider reductions in OERSs.

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

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

Definition 3.2 (1) We call a set S of terms stable iff (a) S is closed under permutation: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e, the final term of P/Q is in S; and (b) S is closed under unneeded expansion: for any e→^{u}o such that e ∉ S and o ∈ S, u is S-needed.

(2) We call a stable S regular iff S-unneeded redexes cannot duplicate S-needed ones.

The prime examples of stable sets are the set of normal forms [HuLé91], the set of head-normal forms [BKKS87], the set of weak-head-normal forms [Mar92], and the set of constructor-head-normal forms for constructor TRSs [Nök94]. All the above sets are closed under reduction, which implies that they are closed under permutation.

Theorem 3.1 (Relative Normalization [GlKh94]) 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 a finite number of S-unneeded are also contracted.

Below S, resp. R, will always 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. We call any reduction P : t → → s with t ∉ S an S-reduction. t↓_{R} and an R-reduction are defined similarly.

Lemma 3.1 (1) Residuals of S-unneeded redexes under any S-reduction remain S-unneeded. (2) Let t ∉ S, t→^{u}t′, UN_{S}(u, t), and let u′ ⊆ t′ be a u-new redex. Then UN_{S}(u′, t′).

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

4 Minimal Relative Normalization

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

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

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

Note that every persistently S-needed redex is S-needed, but S-secured redexes need not be (e.g., when S is the set of normal forms and the OERS has an erasing rule, say f(x) → a).

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

Definition 4.2 We call P : t → → s S-minimal if it is S-normalizing and P ≤ Q for any Snormalizing Q : t → → o. 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, then t has no more than one Sminimal 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-secured S-normalizing reduction is S-minimal. Proof Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be an S-secured 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-secured and Q_{i} is S-normalizing, u_{i}/Q_{i} = ∅. Hence P/Q = ∅, i.e., P is S-minimal.

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

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

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

Definition 4.4 (1) ([Kha93, GlKh94]) We call a subterm s of a term t unabsorbed in a reduction P : t → → e if none of the descendants of s along P appear in redex-arguments, and call it absorbed in P otherwise. We call s unabsorbed in t if it is unabsorbed in any reduction starting from t and absorbed in t otherwise.

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

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

A redex u ⊆ t is unabsorbed in t iff it is F (t)-unabsorbed, where F (t) is the set of all redexes in t; the latter holds iff u is external [HuLé91] in t. It is shown in [HuLé91, Kha93, GlKh94] that any term t not in normal form contains an unabsorbed redex. Now, if one ignores all redexes in t except those in F, it follows that:

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

Proposition 4.1 Every term t not in S-normal form contains an S-needed S-unabsorbed redex. Proof It is enough to take F_{S}^{n}(t) for F in Lemma 4.3; F_{S}^{n}(t) ≠ ∅ by Theorem 3.1. Note that any S-unabsorbed redex is necessarily S-needed.

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

Example 4.1 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 : t → f(b); Q : t → g(a, a) → g(b, a), and N : t → g(a, a) → g(a, b) → g(b, b). (There are two more reductions that continue Q and N, but we do not need to consider them because they cannot be S-minimal.) We have P ≰Q, Q ≰P, and N ≰P. Hence none of the reductions is S-minimal.

Lemma 4.4 For any R-reduction P 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 essential and inessential reductions in place of R-needed and R-unneeded ones. The same proof applies in this case.

Lemma 4.5 If a redex u ⊆ t is R-unabsorbed, then it need not be unabsorbed in t, but it cannot be replicated and is persistently R-needed. Proof Let P : t → → o, not necessarily an F_{ℜ}^{n}-reduction. By Lemma 3.1.(3), it is enough to show that if a residual u′ of u can be absorbed inside an R-needed redex w′, then w′ cannot replicate u′; therefore u has at most one residual in any term of P. Suppose, on the contrary, that there is P : t → → s such that a residual u′ of u is absorbed inside an R-needed redex w′ such that w′ can replicate u′; and assume that P is a shortest such a reduction, i.e., u has exactly one residual in every term in P. By Lemma 4.4, there are R-needed P′ and R-unneeded P′′ such that P ≈_{L} P′ + P′′. Since u′ and w′ are R-needed and P′′ is R-unneeded, it follows from 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.(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-secured. Indeed, take R, S, and Q as in Example 4.1. 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-secured. But a ⊆ t is S-unabsorbed, since the only F_{S}^{n}(t)-reduction is N : f(a) → f(b), and a is F_{S}^{n}(t)-unabsorbed in N.

Proposition 4.2 An R-normalizing reduction is R-minimal iff it is R-secured. 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-secured by Lemmas 4.5 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} (see figure for Lemma 4.2). Since Q is R-secured, so is Q_{i}, and Q_{i} is R-normalizing by the closure of R under permutation. 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-secured, and P is R-secured too.

Lemma 4.1 justifies the following definition (see also Proposition 5.2):

Definition 4.5 We call u ⊆ t quasi-persistently S-needed if u is S-needed and S-secured.

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

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 quasi-persistently R-needed redexes in t yields an R-minimal R-normalizing reduction, even if a finite number of R-unneeded R-secured, and only such, redexes are also contracted. In particular, any t ↓_{R}∉ R has an R-unabsorbed R-minimal reduction, which is R-needed. Proof By Proposition 4.1, any t ↓_{R}∉ R has an R-unabsorbed redex, which is quasi-persistently R-needed by Lemma 4.5 and Lemma 4.1. It remains to apply Theorem 3.1 and Proposition 4.2.

5 Relative Essentiality

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

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

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

Lemma 5.1 (1) [GlKh94] Let t→^{u}t′ and e ⊆ s ⊆ t. Then any u-descendant of e is contained in some u-descendant of s.

(2) Let e ⊆ s ⊆ t and ES_{S}(e, t). Then ES_{S}(s, t).

(3) Let s be a pattern-subterm of a redex u ⊆ t. Then ES_{S}(u, t) iff ES_{S}(s, t). Proof From the definition of the descendant relation for subterms and Definition 5.1.

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

Lemma 5.3 Let N : s → → t, P : s → → e, and P′ = P/N. Then (1) If P is R-minimal, then so is P′.

(2) If P′ is R-minimal and N is R-inessential, then P is R-minimal as well. Proof (1) By Proposition 4.2, P is R-secured. Hence, so is P′, and again by Proposition 4.2, P′ is R-minimal.

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

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

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

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

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

(2) Let N : s → → o be R-inessential and let ES_{ℜ}(s′, s). Then s′ has exactly one N-descendant o′ ⊆ o, which is R-essential; the R-minimal R-normal forms of s and o coincide. Proof (1) Let IE_{ℜ}(s′, s), let P : s → → e be R-minimal, let N : s → → o, and let o′ be an Ndescendant of s′. By Lemma 5.3.(1), P/N is R-minimal. By Lemma 5.2, s′ does not have P - descendants. Further, P + N/P ≈_{st} N + P/N by Theorem 2.1.(2). Hence o′ does not have P/N-descendants, and IE_{ℜ}(o′, o) by Lemma 5.2.

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

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

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

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

Lemma 5.5 Every R-unabsorbed redex u ⊆ t↓_{R} is R-essential. Proof Let P : t → → e be R-unabsorbed R-minimal reduction, which exists by Theorem 4.1. Since u is R-unabsorbed, it has (exactly one) P -descendant by Definition 4.4. Hence u is R-essential by Lemma 5.2.

Definition 5.2 We call P : t → → s external to u ⊆ t if it does not contract residuals of u [GlKh94]. We say that P discards u if P is external to u and u/P = ∅.

Lemma 5.6 Let P : t → → s ∈ R be R-unabsorbed. Then IE_{R}(u, t) iff P discards u. Proof (⇒) By Lemma 5.5, P is R-essential. By Lemma 5.4.(1), all descendants of u along P remain R-inessential. Hence P is external to u, and every descendant of u along P is its residual. Since IE_{R}(u, t), u does not have P -descendants by Lemma 5.2. Hence u/P = ∅, and P discards u. (⇐) If P discards u, then u does not have P -descendants, hence is R-inessential by Lemma 5.2.

Proposition 5.1 A redex u ⊆ t↓_{R}∉ R is R-inessential iff it is R-unneeded and R-secured. Proof (⇒) From Lemma 5.6. (⇐) Let P : t → → s ∈ R be R-unabsorbed. Since UN_{R}(u, t), P is external to u by Lemma 3.1, and since u is R-secured, u/P = ∅. Thus P discards u. Now it remains to apply Lemma 5.6.

Proposition 5.2 A redex u ⊆ t ∉ R is R-secured iff (α): every residual of u (in particular, u itself) along any reductions starting from t is either R-needed or R-inessential. Proof (⇒) Let u be R-secured, and suppose on the contrary that u doesn’t satisfy (α), i.e., there are P′ : t → → s and a residual u′ ∈ u/P′ such that u′ is R-unneeded and R-essential. Let P′′ : s → → o ∈ R be an R-needed R-minimal reduction; P′′ exists by Theorem 4.1. Then P′′ is external to u′ by Lemma 3.1.(1), and u′/P′′ ≠ ∅ by Lemma 5.2, since every descendant of u′ along P′′ is its residual (P′′ is external to u′). Thus, u/(P′ + P′′) = (u/P′)/P′′ ⊇ u′/P′′ ≠ ∅, i.e., u is not R-secured in t – a contradiction. (⇐) We show that u/P = ∅ for any R-normalizing reduction P by induction on |P |. Indeed, let P = v + P′. Since u satisfies (α), so does every v-residual of it (by the property (α) itself). By the induction assumption, (u/v)/P′ = ∅. Hence u/P = ∅.

6 Relative Standardization Theorem

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

In [HuLé91], for any reduction P : t → → s, external and outermost redexes of P are defined; we call them P -external and P -outermost, respectively. The Huet&Lévy concept of a P -external redex must not be confused with our earlier concept of a reduction being external to a redex, as in Definition 5.2. It is easy to see that u is P -external iff a residual of u is contracted in P and no descendant of u is absorbed in a redex contracted in P (i.e., no descendant of u appears in an argument of a redex contracted in P); and u is P -outermost iff a residual of u is contracted in P and no residual of u is absorbed in a redex contracted in P. A reduction P is called standard (in the sense of [GLM92]) if P = ∅ or P = u + P′, where u is Q-outermost for any Q ≈_{L} P, and P′ is standard.

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

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

Hence a reduction P is standard if P = ∅ or P = u + P′, where u is P -external and P′ is standard. Thus a normalizing reduction is standard iff it contracts unabsorbed redexes. One of the most important properties of a standard reduction, not difficult to prove, is that it is (persistently) needed w.r.t. the class of reductions Lévy-equivalent to it. Since R-normalizing reductions need not be Lévy-equivalent, R-normalizing standard reductions need not be 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 stable and regular, f(a) → g(a, a) → g(b, a) → g(b, b) is a standard R-normalizing reduction, but the second step is R-unneeded. Therefore, we should take standard R-minimal reductions for the R-standard R-normalizing reductions. Corollary 6.2 justifies our choice. Hence, we have from Theorem 4.1 and the Standardization Theorem [GLM92] the following corollary:

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

Lemma 6.2 Let P : t → → s be R-minimal and u ⊆ t be P -external and R-secured. Then NE_{R}(u, t). Proof Obviously, u has a P -descendant, hence is R-essential by Lemma 5.2. Therefore, by Proposition 5.2, u is R-needed.

Lemma 6.3 Let u ⊆ t↓_{R} be R-unabsorbed and P : t → → s be R-minimal. Then u is P -external. Proof Suppose on the contrary that u is not P -external. By Lemma 6.1, u is not N-outermost for a standard N ≈_{L} P, i.e., there is a decomposition N = N′ + v + N′′ such that a residual of u is in an argument of v. Since N is R-secured by Proposition 4.2, it is R-needed by Lemma 6.2, hence an F_{R}^{n}-reduction – a contradiction, since u is R-unabsorbed.

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

7 The Relative Optimality Theorem

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

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

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

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

(2) For any P : t → → s and Q : t → → e, the redexes Qv and P u are in the same labelling-family if for any initial labelling of t, they bear the same labels.

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

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

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

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

Theorem 7.1 (Relative Optimality) Let S be a stable set of terms in an OERS R, and let t ↓_{S}. Then any S-needed complete family-reduction starting from t is S-optimal in the sense that it reaches an S-normal form of t in a minimal number of family-reduction steps. Proof Similar to the proof of the optimality theorem for the λ-calculus in [Lév80]. Let P : t → → s be an S-normalizing family-reduction and Q : t → →^{F_{0}} t_{1}→^{F_{1}} … be an S-needed complete familyreduction. Further, let Q_{i} : t → →^{F_{0}} t_{1}→^{F_{1}} … → → t_{i} and P_{i} = P/Q_{i}. Since ≃_{z}⊆≃, we have F AM(P_{i}) ⊆ F AM(P). Since Q is S-needed, at least one residual of some u_{i} ∈ F_{i} is contracted in P_{i} (P_{i} is Snormalizing by the closure of S under permutation). Hence, again by ≃_{z}⊆≃, F AM(Q) ⊆ F AM(P). Hence, by Lemma 7.1, ∥Q∥ = Card(F AM(Q)) ≤ Card(F AM(P)) ≤ ∥P ∥.

8 Relative optimal versus minimal reductions

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

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

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

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

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

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

9 Conclusions and Future Work

We have 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 Rnormalizing reductions. These results were obtained for ERSs, but are valid for Klop’s CRSs as well, and we expect that they remain valid for other systems of higher-order rewriting too.

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

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

References

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

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

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

[GlKh94] Glauert J.R.W., Khasidashvili Z. On Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of the 4^{th} International workshop on Conditional (and Typed) Term Rewriting Systems, Jerusalem, 1994. To appear in Springer LNCS series. (A version of this paper is available as ftp://ftp.sys.uea.ac.uk/pub/glauert/CTRS.ps.gz)

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

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

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

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

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

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

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

[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, Theoretical Computer Science 121, 1993, p. 279-308.

[Lév78] Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université de Paris VII, 1978.

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

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

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

[Nök94] Nöcker E. Efficient Functional Programming. Compilation and Programming Techniques. Ph. D. Thesis, Katholic University of Nijmegen, 1994.

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