Minimal and Optimal Relative Normalization in Orthogonal Expression Reduction Systems

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

Abstract

This paper continues an investigation into the theory of normalization relative to desirable sets of normal forms, started in [GKh94]. In particular, we prove existence of minimal normalizing reductions for regular stable sets of normal forms, and give a sufficient and necessary conditions for a normalizing (w.r.t. M) reduction to be minimal. As a corollary we obtain the relative standardization theorem. Further, we generalize Lévy’s optimality theory to the case of all stable sets of normal forms, and establish a relationship between relative minimal and optimal reductions. We also introduce and study a relative notion of essentiality.

Correspondence Address

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

Email: jrwg@sys.uea.ac.uk Tel: +44 603 592671 Fax: +44 603 507720

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

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. They also defined the class of strongly sequential OTRSs where a needed redex can be found efficiently in any term.

Barendregt et al. [BKKS87] generalized the concept of neededness to the λ-calculus. They studied neededness not only w.r.t. normal forms, but also w.r.t. head-normal forms – a redex is head-needed if its residuals are contracted in each reduction to a head-normal form. The authors proved correctness of the two needed strategies for computing normal forms and head-normal forms, respectively. In [Mar92], Maranget studied 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 [GKh94], 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 M so that each existing notion of neededness can be given by specifying Π or M. 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.

Natural conditions are imposed on M, called stability, that are sufficient and necessary so that each M-normalizable term not yet in M (not in M-normal form) has at least one M-needed redex, and so that repeated contraction of M-needed redexes in a term t will lead to an M-normal form of t whenever there is one. A set M of terms is stable if it is closed under permutation: for any t ∉ M, any P : t → → o ∈ M, and any Q : t → → e, the final term of P/Q, the residual of P under Q, is in M; and is closed under unneeded expansion: for any e→^{u}o such that e ∉ M and o ∈ M, a residual of u is contracted in any reduction from e to a term in M. It is shown also that if a stable M is regular, i.e., if M-unneeded redexes cannot duplicate or erase M-needed ones, then the M-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 M-normal forms. A reduction P : t → → s with t ∉ M and s ∈ M is said to be M-minimal if it does no more work than any other Mnormalizing reduction Q : t → → e, i.e., the residual [Lév78] P/Q of P under Q is empty. The final term in the M-minimal reduction is said to be an M-minimal M-normal form. M-minimal normal forms are useful to compute since any other M-normal form is accessible from the M-minimal one. Besides the classical results on standardisation, our research on minimal M-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.

We show that, for any stable and regular M, any M-normalizable term not yet in M possesses an M-needed M-unabsorbed redex, and repeated contraction of such redexes gives M-minimal Mnormalizing reductions. These redexes play the role of standard redexes w.r.t. M, since they are M-needed and cannot be duplicated. We further give a sufficient and necessary criterion for an M-normalizing reduction to be M-minimal. We show also that M-minimal reductions need not exist if M is stable but is irregular.

To give the characterization of M-minimal reductions, we introduce a relative notion of essentiality. A subterm s ⊆ t is said to be M-essential if it has a descendant under at least one M-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 (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 [GKh94]).

For the case of normal forms, essentiality coincides with Maranget’s concept of neededness, while in the general case, for stable M, the concepts of neededness and essentiality are different. All M-needed redexes are M-essential. M-unneeded redexes may be M-essential, in which case they contribute to the minimal M-normal form, or can be M-inessential in which case they will be erased under any reduction to M-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 M, replacing an M-inessential subterm by another term may lead to an M-essential subterm at the same position, and the M-normal form of the term may be changed.

Our study of optimal normalization w.r.t. stable sets M 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 M-needed family-reductions, which contract all members of a family containing an M-needed redex in a multi-step, reach M in the least number of family-reduction steps. We also prove that weakly M-needed reductions, which contract in an arbitrary order redexes that belong to M-needed families but need not be M-needed themselves, are M-normalizing as well. This is not at all immediate, since if M is not regular, reductions that may contain finite sequences of M-unneeded steps in addition to M-needed steps need not me M-normalizing (see [GKh94]).

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

The rest of the paper is organized as follows. In section 2, we introduce higher order rewriting through Expression Reduction Systems. In section 3, we review the theory of relative normalization from [GKh94]. In section 4, we introduce relative essentiality and unabsorbedness, and study M-minimal reductions for stable regular sets M. In section 5, we study the relative notion of essentiality. In section 6, we review the labelling system of Kennaway&Sleep [KeSl89] for OERSs, used to develop the uniform optimality theory in section 7. Finally, in section 8 we establish a relationship between relative optimal and minimal reductions. Sections 2 and 6 are taken from [Kha94] and [GKh94], respectively, to make the paper self-contained.

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. We refer to Klop et al. [KOR93] and van Oostrom [Oos94] for a survey. Here we use a system of higher order rewriting, Expression Reduction Systems (ERSs), defined in Khasidashvili [Kha92] (under the name of CRSs).

Definition 2.1 (1) Let Σ be an alphabet, comprising variables v_{0}, v_{1}, …; 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.

(2) Metaterms are constructed from terms, term metavariables, which range over terms, and object metavariables, which range over variables. Apart from the usual rules for term-formation, one is allowed to have metasubstitutions — expressions of the form (A_{1}/a_{1}, …, A_{n}/a_{n})A_{0}, where a_{i} are object metavariables and A_{j} are metaterms. Metaterms that do not contain metasubstitutions are called simple metaterms. An assignment maps each object metavariable to a variable and each term 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 subterms of the form (t_{1}/x_{1}, …, t_{n}/x_{n})t with the result of substitution of terms t_{1}, …, t_{n} for free occurrences of x_{1}, …, x_{n} in t.

Definition 2.2 (I) 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 metaterms such that t is a simple metaterm and is not a metavariable, and each term metavariable that occurs in s occurs also in t. Further:

(1) The metaterms t and s do not contain variables, and each occurrence of an object metavariable in t and s is bound. The metaterm s may contain occurrences of object metavariables that do not occur in t. They are called additional object metavariables.

(2) Each rule r : t → s has a set of admissible assignments AA(r) such that, for any assignment θ ∈ AA(r):

(a) occurrences of variables in sθ that correspond to additional object metavariables of s do not bind variables in subterms that correspond to term metavariables of s.

(b) For any term metavariable A and any object metavariable a occurring in t or s, and any admissible assignment θ such that aθ ∈ F V (Aθ), an occurrence of Aθ in sθ is in the scope of an occurrence of aθ in sθ iff any occurrence of Aθ in tθ is in the scope of an occurrence of aθ in tθ.

(c) For any rule r : t → s in R and any admissible assignment θ ∈ AA(r), tθ is an r-redex or an R-redex, and sθ is the contractum of tθ. Redexes that are instances of the left-hand side of the same rule (i.e., with the same set of admissible assignments) are called weakly similar.

(II) R is simple if right-hand sides of R-rules are simple metaterms.

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.

Our syntax is close to that of the λ-calculus and of First Order Logic. For example, the β-rule is written as β : Ap(λaA, B) → (B/a)A, where a is to be instantiated by a variable and A and B are to be instantiated by terms. The expression (B/a)A is a metasubstitution, and its instance (t/x)s denotes the result of substitution of the term t for x in the term s. To express ‘pure’ substitutions syntactically (instead of metasyntactically) we use S-reduction rules S^{n+1}a_{1} … a_{n}A_{1} … A_{n}A_{0} → (A_{1}/a_{1}, …, A_{n}/a_{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 a_{1}, …, a_{n} and A_{1}, …, A_{n}, A are pairwise distinct object and term metavariables, respectively. 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 We use a, b for object metavariables, A, B for term metavariables, c, d for constants, t, s, e, o for terms and metaterms, u, v, w for redexes, and P, Q, N for reductions. We write s ⊆ t if s is a subterm of t. A one-step reduction in which a redex u in a term t is contracted is written as t →^{u} s or t → s. 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.

For any ERS R, R_{f} is the ERS obtained from R by adding symbols \underline{S}^{n+1} in the alphabet and by replacing in right-hand sides of the rules all metasubstitutions of the form (t_{1}/a_{1}, …, t_{n}/a_{n})t by \underline{S}^{n+1}a_{1} … a_{n}t_{1} … t_{n}t, respectively. For example, the β_{f} rule would be β_{f} : Ap(λaA, B) → \underline{S}^{2}aBA. If R is simple, then R_{fS} =_{def} R_{f} =_{def} R. Otherwise R_{fS} =_{def} R_{f} ∪ \underline{S}, where \underline{S}-rules are obtained from S-rules by underlining the S-symbols (to distinguish S-redexes that are created by R_{f}-steps). For each step e = C[t_{i}θ] →^{u} C[s_{i}θ] = o in R there is a reduction P : e = C[t_{i}θ] → C[s′_{i}θ] → → C[sθ] = o in R_{fS}, where C[s′θ] → → C[sθ] is the rightmost innermost normalizing \underline{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 headed at 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}, including free occurrences of x_{1}, …, x_{n}, have exactly one descendant. 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. 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 (descendants of all redexes except the contracted redex are residuals).

The definition of orthogonality in ERSs is similar to the case of TRSs: 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 co-initial 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 strict Church-Rosser property:

Theorem 2.1 (1) [Klo80] For any co-initial reductions P and Q in an OERS, P +Q/P ≈_{L} Q+P/Q. (2) [Kha92] (Strict Church-Rosser) Let P ≈_{L} Q, in an OERS. Then P ≈_{st} Q.

3 Relative neededness

In this section, we review some notions and results from [GKh94], used below.

Definition 3.1 ([GKh94]) (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 M be a set of terms in an OERS R. We call a redex u ⊆ t M-needed, written NE_{M}(u, t), if at least one residual of it is contracted in any reduction from t to a term in M, and call it Munneeded, written UN_{M}(u, t), otherwise.

Definition 3.2 ([GKh94]) (1) We call a set M of terms stable if:

(a) M is closed under permutation: for any t ∉ M, any P : t → → o ∈ M, and any Q : t → → e, the final term of P/Q, which we will call the canonical join of P and Q, is in M; and

(b) M is closed under unneeded expansion: for any e→^{u}o such that e ∉ M and o ∈ M, u is M-needed.

(2) We call a stable set M regular if M-unneeded redexes cannot duplicate or erase M-needed ones.

The most appealing examples of stable sets, for an OERS, are the set of normal forms [HuLé91], the set of head-normal forms [BKKS87], the set of weak-head-normal forms (a partial result is in [Mar92]), and the set of constructor-head-normal forms for constructor TRSs [Nök94]. All the above sets are closed under reduction. Clearly, Huet&Levy-neededness [HuLé91] is neededness w.r.t. the set of normal forms. It was shown in [GKh94] that Maranget’s notion of neededness [Mar92] coincide with neededness w.r.t. the set of all fair reductions (Huet&Levy- and Marangetneededness coincide for normalizable terms).

Theorem 3.1 (Uniform Normalization [GKh94]) Let M be a stable set of terms in an OERS R.

(1) Any M-normalizable term t in R not in M-normal form contains an M-needed redex.

(2) If t is M-normalizable, then any M-needed reduction starting from t ends at a term in M.

We call a reduction that does not contain steps t → s with t ∈ M and s ∉ M an M-reduction.

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

(3) Let t be M-normalizable, and let t→^{u}s. Then any M-needed redex v ⊆ t different from u has an M-needed residual in s.

4 Minimal relative normalization

Definition 4.1 We call a subterm s in t P -essential if it has a P -descendant, and call it P - inessential otherwise. We call s ⊆ t M-essential if it is P -essential for at least one M-normalizing P starting from t, and call it M-inessential otherwise.

Definition 4.2 (1) We call a redex u ⊆ t persistently M-needed if all residuals of u along Mnormalizing reductions starting from t are M-needed.

(2) We call a redex u ⊆ t quasi-persistently M-needed if every residual of u along M-normalizing reductions starting from t is either M-needed or M-inessential.

Definition 4.3 We call an M-normalizing reduction P M-minimal if P ◁Q for any M-normalizing Q that is co-initial with P. If P : t → → s is M-minimal, then we call s an M-minimal M-normal form of t.

It follows immediately from Definition 4.3 that if M is stable and t ∉ M is M-normalizable, then t has exactly one M-minimal M-normal form s; and for any other M-normal form e of t, it holds that s → → e.

Lemma 4.1 Let M be stable. Then every quasi-persistently M-needed M-normalizing reduction is M-minimal. Proof Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be quasi-persistently M-needed M-normalizing reduction, let P_{i} : t_{0}→^{u_{0}} … → t_{i}, and let Q : t_{0} → → o be any M-normalizing reduction. By stability of M, Q_{i} = Q/P_{i} is M-normalizing. Since u_{i} is quasi-persistently M-needed and Q_{i} is M-normalizing, it follows that u_{i}/Q_{i} = ∅. Hence P/Q = ∅, i.e., P is M-minimal.

Definition 4.4 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.5 (1) We call a subterm s of a term t F -unabsorbed in an F -reduction P : t → → e if none of the descendants of s along P appear in arguments of F -redexes, and call it F -absorbed in P otherwise. We call s F -unabsorbed in t if it is F -unabsorbed in any F -reduction starting from t and F -absorbed in t otherwise.

(2) We call s M-unabsorbed if it is F_{M}^{n}(t)-unabsorbed, where F_{M}^{n}(t) is the set of M-needed redexes of t. We call a reduction P M-unabsorbed if each redex contracted in it is. (It is shown below that all F_{M}^{n}(t)-reductions are M-normalizing if t is.)

We have that a redex u ⊆ t is unabsorbed [Kha93, GKh94] 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, GKh94] 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.2 Let F ≠ ∅ be a set of redexes in a term t. Then F contains an F -unabsorbed redex.

Corollary 4.1 Let M be stable. Any term t in an OERS not in M-normal form contains an M-needed M-unabsorbed redex. Proof It is enough to take F_{M}^{n}(t) for F in Lemma 4.2.

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

Example 4.1 Consider R = {f(x) → g(x, x), a → b}, take for M the set of terms not containing a as a leftmost innermost node, and take t = f(a). Obviously, M is closed under unneeded expansion, because the only M-needed redex in a term t ∉ M is the leftmost occurrence of a in it, and M is closed under reduction. M is not regular, because in the term f(a) the outermost redex is Munneeded, while the innermost one is M-needed. Further, there are three M-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.) We have P ◁̸Q, Q ◁̸P, and N ◁̸P. Hence none of the reductions is M-minimal.

Remark 4.1 This doesn’t mean of course that no reasonable notion for M-minimality exists for irregular stable M. For example, one could define P to be M-minimal if P/Q is M-unneeded for any Q co-initial with P. But this is left for a future investigation.

Lemma 4.3 (Push Lemma) Let M be a regular stable set. For any M-reduction P there is an M-needed Q containing the same number of steps as that of M-needed steps in P such that Q ◁ P; if P is moreover M-normalizing, then so is Q. Proof The lemma was proved in [Kha88, Kha93] for the case of essential and inessential reductions in place of M-needed and M-unneeded ones. The same proof applies in our case.

Lemma 4.4 (1) Let M be regular and stable. If a redex u ⊆ t is M-unabsorbed, then it need not be unabsorbed in t, but it cannot be duplicated and is persistently M-needed.

(2) If M is stable and is not regular, then an M-unabsorbed redex u ⊆ t need not be either persistently or quasi-persistently M-needed. Proof (1) Let P : t → → o, not necessarily an F_{M}^{n}-reduction. By Lemma 3.1.(3), it is enough to show that u can have at most one residual along P, and its residuals can only be absorbed inside arguments of M-unneeded redexes, and hence cannot be either erased to duplicated. Assume on the contrary that, say in the last step of P and not before, the residual u′ of u is absorbed in an argument of an M-needed redex w′. By Lemma 4.3, there are M-needed P′ and M-unneeded P′′ such that P ≈_{L} P′ + P′′. Since u′ and w′ are M-needed and P′′ is M-unneeded, it follows from Lemma 3.1.(2) that there are M-needed u′′ and w′′ in the final term of P′ such that u′′ is in an argument of w′′. This is a contradiction, since P′ is M-needed, and hence an F_{M}^{n}-reduction, and u is F_{M}^{n}-unabsorbed.

(2) Take R and M as in Example 4.1, and consider P : t = f(a) → f(b) = s. Then a in t is Mneeded, so is its leftmost residual in s, but the rightmost residual is M-unneeded and M-essential. Hence a ⊆ t is not either persistently or quasi-persistently M-needed. But a ⊆ t is M-unabsorbed, since the only F_{M}^{n}(t)-reduction is N : f(a) → f(b), and a is F_{M}^{n}(t)-unabsorbed in N.

We can call a reduction Q standard for a co-initial reduction P if it contracts redexes that are unabsorbed in reductions Levy-equivalent to P, and call a reduction a standard normalizing reduction if it contracts unabsorbed redexes; standard reductions are also needed w.r.t. reductions Levy-equivalent to P and w.r.t. the set of normal forms, respectively. This definition is consistent with the definition of standard reduction in the literature. Obviously, a term in an OERS may contain unabsorbed redexes that are not M-needed, for a regular stable M. But M-unabsorbed redexes can be considered as standard w.r.t. M, since they are M-needed and cannot be duplicated. Therefore we have the following corollary.

Corollary 4.2 (Relative Standardization Theorem) Let M be a regular stable set of terms in an OERS, and t be an M-normalizing term that is not in M. Then t has a standard M-normalizing reduction.

Theorem 4.1 For any regular stable M, and any M-normaliable t ∉ M, there is an M-minimal M-needed reduction starting from t; P can be chosen M-unabsorbed. Proof Let P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … t_{n} be an M-unabsorbed reduction, and Q : t_{0} → → e be any Mnormalizing reduction. It is enough to show that P ◁ Q. Let P_{i} : t_{0}→^{u_{0}} … → t_{i}. By stability of M, Q_{i} = Q/P_{i} is M-normalizing. By Lemma 4.3, there is an M-needed M-normalizing Q_{i}^{∗} such that Q_{i}^{∗} ◁ Q_{i}. Since u_{i} is F_{M}^{n}-unabsorbed and Q_{i}^{∗} is M-needed M-normalizing, therefore an F_{M}^{n}-reduction, we have that u_{i}/Q_{i}^{∗} = ∅. Now, since Q_{i}^{∗} ◁ Q_{i}, we have that u_{i}/Q_{i} = ∅, i.e., P/Q = ∅.

Lemma 4.5 Let M be stable, let t ∉ M, and let P : t → → o be M-minimal. Then a subterm s ⊆ t is M-essential iff it is P -essential. Proof (⇐) is immediate. (⇒) Let s be M-essential. Then it is Q-essential for some M-normalizing Q. Since P is M-minimal, we have P ◁ Q, and hence Q ≈_{L} P + P′ for some P′. Therefore, by Theorem 2.1, s is P -essential as well.

Theorem 4.2 For any regular stable M in an OERS, P is M-minimal iff it is quasi-persistently M-needed. Proof (⇐) is Lemma 4.1. (⇒) Let P : t_{0}→^{u_{0}}t_{1} → … → t_{n} be a reduction that is not quasipersistently M-needed M-normalizing, let P_{i} : t_{0}→^{u_{0}} … → t_{i}, and let Q : t_{0} → → o be M-unabsorbrd, hence quasi-persistently M-needed by Lemma 4.4, M-minimal reduction. By stability of M, Q_{i} = Q/P_{i} is M-normalizing. Suppose that u_{i} is not quasi-persistently M-needed, i.e., there is Q^{∗} : t_{i} → → e_{i} such that u_{i} has a Q^{∗}-residual u_{i}^{∗} that is M-essential and M-unneeded. Let Q′ : e_{i} → → o_{i} be M-minimal (it exists by Theorem 4.1). Q′ doesn’t contract the residuals of u_{i}^{∗} since they are M-unneeded, and u_{i}^{∗} has a Q′-residual by Lemma 4.5. Hence, u_{i}/(Q^{∗} + Q′) = ∅. Since Q is quasipersistently M-needed, so is Q_{i}. Hence, by Lemma 4.1, Q_{i} is M-minimal, and thus Q_{i} ◁ Q^{∗} + Q′. Therefore, u_{i}/Q_{i} ≠ ∅ and hence P/Q ≠ ∅ – a contradiction, since P is M-minimal.

Proposition 4.1 Let M be a set of terms closed under permutation in an OERS. Then for any t ∉ M and any M-normalizing M-needed P, Q starting from t, C(P) ≈_{L} C(Q) (see Definition 6.1).

Proof Let Q : t→^{u_{0}}t_{1}→^{u_{1}} → … →^{u_{n−1}}t_{n}, C(Q) : t→^{u_{0}}t_{1}→^{u_{1}} → … →^{u_{m−1}}t_{m}, Q_{i} : t→^{u_{0}}t_{1}→^{u_{1}} → … →^{u_{i−1}}t_{i},

and P_{i} = C(P)/Q_{i}. We shall show by induction on i that u_{i}/P_{i} = ∅. Since Q is M-needed, for all 0 ≤ i < n, a residual of u_{i} is contracted in P_{i} (P_{i} is M-normalizing since M is closed under permutation). Since P_{i} contracts only residuals of redexes contracted in C(P), a redex from the family of u_{i} is contracted in P. Since in the final term of C(P) there is no redex from the family of u_{i} and by the induction assumption Q_{i}/C(P) = ∅, u_{i} does not have P_{i}-residuals, i.e., u_{i}/P_{i} = ∅. Any redex u_{j} with n ≤ j < m is in the family of some redex contracted in Q, hence of some redex contracted in P, and it does not have residuals under P_{j} by the same argument. Hence C(Q)/C(P) = ∅ and C(P) ≈_{L} C(Q) follows.

5 Properties of M-essential subterms

The following properties of M-essential and M-inessential subterms follow immediately from the definition of the descendant relation for subterms.

Lemma 5.1 (1) [GKh94] 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_{M}(e, t). Then ES_{M}(s, t).

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

Notation We write t = (t_{1}//s_{1}, …, t_{n}//s_{n})s if s_{1}, …, s_{n} are disjoint subterms in s and t is obtained from s by replacing them with t_{1}, …, t_{n}, respectively.

Definition 5.1 [GKh94] Let t = (t_{1}//s_{1}, …, t_{n}//s_{n})s in an OERS R and let P : s = e_{0} →^{v_{0}} e_{1} →^{v_{1}} … be an R_{fS}-reduction. We define the reduction P ∥(t, {s_{1}, …, s_{n}}) : t = o_{0} →^{u_{0}} o_{1} →^{u_{1}} … as follows.

(1) If v_{0} is an R_{f}-redex and its pattern does not overlap with s_{1}, …, s_{n}, then u_{0} is the corresponding subterm of v_{0} in t = o_{0}.

(2) If v_{0} is an \underline{S}-redex that is outside the replaced subterms, then u_{0} is the corresponding \underline{S}-redex in t_{0}.

(3) If v_{0} is an R_{f}-redex that is not inside the subterms s_{1}, …, s_{n} and its pattern does overlap with some of s_{1}, …, s_{n}, then u_{0} = ∅.

(4) If v_{0} is in some of subterms s_{1}, …, s_{n}, then u_{0} = ∅.

In the first case, o_{1} is obtained from e_{1} by replacing the descendants of s_{1}, …, s_{n} with the corresponding descendants of t_{1}, …, t_{n}, respectively; in the second case, o_{1} is obtained from e_{1} by replacing outermost descendants of s_{1}, …, s_{n} with the corresponding descendants of t_{1}, …, t_{n}; in the third case, o_{1} is obtained from e_{1} by replacing the descendant of v_{0} by the descendant of its corresponding subterm in o_{0}, and by replacing the descendants of the subterms s_{i} that do not overlap with v_{0} by the corresponding descendants of t_{i}; in the fourth case, o_{1} is obtained from e_{1} by replacing the descendants of s_{1}, …, s_{n} with the corresponding descendants of t_{1}, …, t_{n}, respectively. Thus, in o_{1} we can choose the redex u_{1} analogously, and so on. (When s_{1}, …, s_{n} are clear from the context, we write P ∥(t) for P ∥(t, {s_{1}, …, s_{n}}).)

Remark 5.1 Note that the ∥ relation generalizes the notion of a residual of a reduction under a co-initial development to the non-orthogonal case.

Lemma 5.2 If a subterm or s ⊆ t is M-inessential, then it is M-unneeded. Proof Let u ∈ t ∉ M be M-inessential and let P : t → → o ∈ M. Then it follows immediately from Definition 5.1 that Q∥(t, {u}) is M-normalizing and does not contract the residuals of u.

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

(2) If P′ is M-minimal and N is M-inessential, then P is M-minimal as well. Proof (1) By Theorem 4.2, P is persistently M-needed. Hence, so is P′ = P/N, and again by Theorem 4.2, P′ is M-minimal.

(2) We can construct the following diagram

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

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

We have to show that Q ◁ P. We have that N/Q = N/P = ∅, since N is M-inessential and M 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 M-minimal

Lemma 5.4 (1) Descendants of M-inessential subterms of an M-normalizable term s under any reduction N : s → → o remain M-inessential; the M-minimal normal forms of s and o coincide.

(2) Let N : s → → o be M-inessential and let s′ ⊆ s be M-essential. Then s′ has exactly one N-descendant o′ ⊆ o, and o′ is M-essential. Proof (1) Let s′ be M-inessential, let P : s → → e be an M-minimal reduction, and let t′ be an N-descendant of s′. By Lemma 5.3, P/N is M-minimal. Further, P + N/P ≈_{st} N + P/N, hence t′ does not have P/N-descendants. Thus t′ is M-inessential by Lemma 4.5. The M-minimal normal forms of s and o coincide because N/P = ∅.

(2) Let P : s → → e be M-minimal. Then by Lemma 4.5, s′ has a P -descendant. Since N is M-inessential, we have that N/P = ∅, and hence P ≈_{st} N + P/N. Further, s′ has exactly one Ndescendant o′ by Lemma 5.1, and o′ has P/N-descendant. By Lemma 5.3.(1), P/N is M-minimal. Hence o′ is M-essential by Lemma 4.5.

It is shown in [GKh94] that if s_{1}, …, s_{n} are inessential in s and t = (t_{1}//s_{1}, …, t_{n}//s_{n})s, then t_{1}, …, t_{n} are inessential in t. The following example shows that, straingely enough, 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 M = {t ∥ t = a or t contains a variable}. Then any M-normaliable term not in M-normal form has the shape f(… (f(a)) …), only the outermost f-redexes are M-needed, and their contraction yield the M-normal form a. Thus M is regular and stable. Now take s = f(a) and t = f(x). Then a is M-inessential in s – it does not have descendants in the only M-normal form a of s; but x is M-essential in t, since t ∈ M.

6 A labelling for OERSs

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 the labelling system for the λ-calculus introduced by Lévy [Lév78]. Each label of Kennaway&Sleep [KeSl89] is a tuple of labels, built up from a set of base labels. For any OERS R, terms in the corresponding labelled OERS R^{L} are those of R where each subterm has one or more labels, represented as a string of labels. A labelling of a term is initial if all its subterms are labelled by different base labels. The signature of a labelled term is the tuple of all its labels, from left to right. Rules of R^{L} are those of R where pattern-symbols in left-hand sides are labelled by a string of labels except for the head-symbol, which has just one label (a string of length one). Each subterm (including metavariables) in the right-hand side of a rule bears the signature of the corresponding left-hand side. Further, a redex-index of a redex is the maximal depth of nesting in the labels of the corresponding left-hand side of the rule. The index Ind(P) of a reduction P is the maximal redex-index of redexes contracted in it.

The crucial property of the labelling is given by the following proposition.

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

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

Another importent property of labelled reductions is given by the following proposition. First recall that an OERS has a decreasing redex labelling [Klo80] if there is a map F from redexes of R to ordinals such that: if u is a residual of v, then F (u) ≥ F (v), and if u creates v, then F (u) > F (v). It is shown in [Klo80] that any reduction in an OERS having a decreasing redex labelling is terminating. Therefore:

Proposition 6.2 [Klo80, Lév78] Any reduction in which only redexes with a bounded redex-index are contracted is terminating.

Remark 6.1 The above propositions are obtained for OCRS [KOR93], but it is strightforward to carry them over OERSs. □

Definition 6.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 ≃ 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, a family completion of P, written C(P), is a reduction obtained from P by contracting redexes belonging to the families of redexes contracted in P as long as possible.

(3) For any co-initial reductions P and Q, the redexes Qv and P u are in the same labellingfamily if for any initial labelling of the initial term of P and Q, they bear the same labels.

Proposition 6.1 implies that the labelling-family relation is indeed a family relation. As pointed out in [AsLa94], for OERSs in general the zig-zag and labelling family relations do not coincide. Below by family we always mean the labelling-family. Termination of family completions of any finite reduction follows from Proposition 6.2. Strong equivalence of all family completions of a reduction follows easily from Proposition 6.1.

7 The uniform optimality theorem

Definition 7.1 Let P : t→^{u_{0}}t_{1}→^{u_{1}}t_{1} … →^{u_{n−1}}t_{n} in an OERS R, and let M be a set of terms of R. We call u ∈ t_{i} weakly M-needed w.r.t. t→^{u_{0}}t_{1}→^{u_{1}}t_{1} … → t_{i} if u is in the (labelling) family of an M-needed redex occurring in some t_{j}. A reduction is weakly M-needed if each redex contracted in it is so (w.r.t. the initial reduction).

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

Theorem 7.1 Let M be a stable set of terms in an OERS R, and t be an M-normalizable term in R. Then any weakly M-needed reduction starting from t is terminating. Proof Let P : t → → s be an M-normalizing reduction and Q : t→^{u_{0}}t_{1}→^{u_{1}} … be a weakly M-needed reduction. Further, let Q_{i} : t→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i} and P_{i} = P/Q_{i}. By Proposition 6.1, Ind(P_{i}) ≤ Ind(P). Since Q is weakly M-needed, for each i, there is an M-needed redex u′_{i} in some t_{j} that is in the same family as u_{i}. Since at least one residual of u′_{i} is contracted in P_{j} (P_{j} is M-normalizing by the closure of M under permutation), F AM(Q) ⊆ F AM(P). Thus one has again by Proposition 6.1 that Ind(Q) ≤ Ind(P) and Q is terminating by Proposition 6.2.

The above theorem allows one to propagate once obtained M-neededness information along the reduction, and to contract safely (without a danger of loosing the M-normal form whenever it exists) any residual of an M-needed redex, even if not M-needed any longer.

Definition 7.2 A multistep reduction P : t_{0} → → t_{1} → → … → → t_{n} is called a family-reduction if each P_{i} : t_{i} → → t_{i+1} is a development of a set F_{i} of redexes belonging to the same family. ∥P ∥ will denote the number of multisteps in P. The family-reduction P is complete if each P_{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 M-needed if each F_{i} contains at least one M-needed redex (i.e., if the (single-step) reduction corresponding to P is weakly M-needed).

Corollary 7.1 Let M be a stable set of terms in an OERS R, and t be an M-normalizable term in R. Then any M-needed family-reduction staring from t is eventually M-normalizing.

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}, 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.2 Let M be a stable set of terms in an OERS R, and t be an M-normalizable term in R. Then any M-needed complete family-reduction starting from t is M-optimal in the sense that it reaches the M-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 M-normalizing family-reduction and Q : t → → e be an M-needed complete family-reduction. It follows from the proof of Theorem 7.1 that 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 M-needed family-reduction that in each step contracts all the M-needed redexes of some family and may not contract its M-unneeded members, call it M-needed semicomplete family-reduction, is still optimal. It follows from Theorem 4.2 that such a reduction is M-minimal as well iff every M-needed redex contracted in it is quasi-persistently M-needed. For example, g(a) → f(a, a) → f(b, a) is both M-minimal and M-optimal semi-complete familyreduction in R = {g(x) → f(x, x), a → b}, where M is the set of terms not containinig a at the leftmost innermost position. However, the following example shows that a term in an OERS need not posses an M-minimal M-optimal family-reduction.

Example 8.1 Consider the OERS R = {σaAB → δa(((A/a)B/a)A), f(A) → g(A, A)}, and let M be the set of terms not containing left-spine redexes, i.e., redexes having at least one patternsymbol on the left-spine of the term. Then M is closed under unneeded expansion because for any t ∉ M such that t→^{u}s ∈ M, u must be the outermost left-spine redex. Also, M 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 M. Thus M is stable. M is moreover regular, since if there is an M-needed M-reduction P : t → → s, with t ∉ M and s ∈ M, such that the residuals of u ∈ t are not contracted in P, then each residual of u along P that gets on the left-spine is erased 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 M-needed.

Now let us consider the term t = σx(f(x), x). There are two M-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 M-needed) and Q : t → σx(G(x, x), x) → δx(G(G(x, x), G(x, x))), but neither reaches the M-minimal M-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 example works is that the redexes of the same family are nested, and there is no ‘hierarchy’ in nesting of redexes of different families. Therefore one might think that M-minimal M-optimal reductions may still exist for every term in OTRSs and the λ-calculus, for stable regular M, since in these OERSs there is a ‘hierarchy’ in nesting of redexes of different families, and the residuals of a redex under any reduction are disjoint. Unfortunately, that is not the case, as shown by the following examples.

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

Example 8.3 Take for M the set of λ-terms in head-normal form, which is regular and stable, 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 M-minimal reduction. In order to reach e from t by a semi-complete M-needed family reduction, one should delay contraction of M-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 M-needed, and their contraction would make e unreachable – there is no occurrence of w in (λz.zvz)(λz.zvz). It remains to note that there are no other redexes in o.

9 Future work

As already mentioned in [GKh94], It would be interesting to investigate perpetual strategies, strong sequentiality, and strictness analyses for arbitrary stable set of normal forms.

Acknowledgements

We thank A. Asperti, J. R. Kennaway and L. Maranget, for useful comments.

References

[AsLa94] Asperti A., Laneve C. The family relation in Interaction Systems. In: Proc. of the 2^{nd} International Symposium on Theoretical Aspects of Computer Software, TACS’94, Springer LNCS, v. 789, M. Hagiya, J. C. Mitchell, eds. Sendai, 1994, p. 366-384.

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

[DeJo90] Dershowitz N., Jouannaud J.-P. Rewrite Systems. In: J. van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 6, vol. B, 1990, p. 243-320.

[GKh94] Glauert J.R.W.G., 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 appiar in Springer LNCS series. Available from a PC member N. Dershowitz.

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

[Ken94] Kennaway J. R. A conflict between call-by-need computation and parallelism. Workshop on conditional (and typed) term rewriting systems, Jerusalem, 1994.

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

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

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

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

[Kha94] Khasidashvili Z. On higher order recursive program schemes. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172-186.

[Klo80] Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980.

[Klo92] Klop J. W. Term Rewriting Systems. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1-116.

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

[Lé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-calculuus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalizm, 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.

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