The Longest Perpetual Reductions in Orthogonal Expression Reduction Systems

Zurab Khasidashvili School of Information Systems, UEA Norwich NR4 7TJ England zurab@sys.uea.ac.uk

Abstract

We consider reductions in Orthogonal Expression Reduction Systems (OERS), that is, Orthogonal Term Rewriting Systems with bound variables and substitutions, as in the λ-calculus. We design a strategy that for any given term t constructs a longest reduction starting from t if t is strongly normalizable, and constructs an infinite reduction otherwise. The Conservation Theorem for OERSs follows easily from the properties of the strategy. We develop a method for computing the length of a longest reduction starting from a strongly normalizable term. We study properties of pure substitutions and several kinds of similarity of redexes. We apply these results to construct an algorithm for computing lengths of longest reductions in strongly persistent OERSs that does not require actual transformation of the input term. As a corollary, we have an algorithm for computing lengths of longest developments in OERSs.

1 Introduction

A strategy is perpetual if, given a term t, it constructs an infinite reduction starting from t whenever such a reduction exists, that is, whenever t is not strongly normalizable. Perpetual strategies are mostly interesting because termination of a perpetual reduction (constructed according to a perpetual strategy) implies strong normalization of the initial term. For orthogonal (left-linear and non-overlapping) TRSs a very simple perpetual strategy exists — just contract any innermost redex (O’Donnell [15]). In fact, any complete strategy, i.e., a strategy that in each term contracts a redex that does not erase any other redex, is perpetual. Moreover, one can even reduce redexes all erased arguments of which are strongly normalizable (Klop [11]).

It is easy to see that in any infinite reduction a redex that itself has an infinite reduction, call it an infinite redex, is contracted. Thus in order to construct an infinite reduction one should try to retain at least one potentially infinite redex — a subterm that can become an infinite redex (more precisely, that has a descendant under some reduction that is an infinite redex). Thus any strategy that does not erase potentially infinite redexes is perpetual. In OTRSs, any potentially infinite redex necessarily has an infinite reduction. That is why all the above strategies are perpetual. In orthogonal Expression Reduction Systems (that is, TRSs with bound variables and substitution mechanism [6]) a strongly normalizable subterm may also be a potentially infinite redex — after contraction of an outer redex a term can be substituted in it that makes the subterm no longer strongly normalizable. Thus innermost reductions and complete reductions are no longer perpetual in OERSs. Therefore one can erase only strongly normalizable arguments in which no substitution of external subterms is possible. For the lambda-calculus, such a strategy was found by Barendregt et al. [2].

In this paper, we design a perpetual strategy for all OERSs. It is a generalization of the perpetual strategy of the λ-calculus and of the limit strategy [8]. Our aim is not only to construct an infinite reduction of any given term t whenever it exists, but also to construct a longest possible one if t is strongly normalizable and to find a method to characterize the lengths of longest reductions. The idea is that, as mentioned above, in order to construct perpetual reductions one should try to avoid erasure of subterms in which substitution of terms is possible during reductions of outer redexes. On the other hand, in order to construct a longest possible reductions one should delay contraction of a redex until it will no longer be possible to copy it by reducing an outer redex. The two conditions agree if in each term s one contracts a limit redex, which is defined as follows: choose in s an unabsorbed redex u_{1}, i.e., a redex whose descendants never appear inside redex-arguments; choose an erased argument s_{1} of u_{1} that is not in normal form; choose in s_{1} an unabsorbed redex u_{2}, and so on, as long as possible. The last chosen redex is a limit redex of s.

In non-left-absorbing systems, where no subterms to the left of a contracted redex can appear (i.e., be absorbed) in the arguments of created redexes, the leftmost-outermost redexes are unabsorbed. In particular, the λ-calculus, Combinatory Logic, and all left-normal systems are non-left-absorbing. Therefore the perpetual strategy of Barendregt et al. [2] is a limit strategy. The Conservation Theorem for the λ-calculus [2, 1] states that non-erasing redexes are perpetual. Its proof remains valid for OERSs if one uses the limit strategy instead of the perpetual strategy of [2].

Our method for proving that the reductions constructed according to our perpetual strategy are the longest, and for computing their lengths, is a refinement of Nederpelt-Klop method [14, 10], used to reduce proofs of strong normalization to proofs of weak normalization. For any OERS R, we define the corresponding non-erasing OERS R_{μ}, called the μ-extension of R. We add fresh function symbols μ^{n} in the alphabet of R. For any R-rule r : t → s, we keep the erased arguments of t in the right-hand side of each corresponding R_{μ}-rule r_{μ} : t′ → s′ as μ-erased arguments of s′. Since this transformation affects the structure of redex-creation in R, and since erasure of arguments of a redex depends not only on the rule, but the arguments themselves, we have to introduce infinitely many R_{μ}-rules for each R-rule. This helps to give a natural translation of R-reductions into R_{μ}-reductions and vice-versa. Finally, we also keep all μ-symbols of t′ as μ-erased symbols in s′, since they can be used as counters of steps in longest normalizing reductions. We then show that a term o in an OERS R is strongly normalizable if it is weakly normalizable in R_{μ}, and that the least upper bound of lengths of R-reductions starting from o coincides with the number of μ-occurrences in the R_{μ}-normal form of o.

Unabsorbed redexes exist in any term not in a normal form, but they can be found efficiently only in strongly sequential OERSs [5]. Therefore, our method is applicable to all strongly sequential OERSs that are strongly normalizing. Several typed λ-calculi and typed OTRSs are such OERSs. Moreover, it is not always necessary to do actual transformation of the input term in order to compute the lengths of longest reductions. We show this for the case of strongly persistent OERSs. In such OERSs, creation of redexes is not possible during ‘pure substitution steps’; creation is only possible during the ‘TRS part’ of reduction steps, and the arguments of a contracted redex and the context in which the reduction takes place do not take part in the creation. This kind of creation we call generation. We define several notions to characterize similarity of redexes in OERSs. The above result relies on the fact that strongly similar redexes generate the same number of strongly similar redexes.

The results of this paper with complete proofs are reported in [9].

2 Orthogonal Expression Reduction Systems

Klop introduced Combinatory Reduction Systems (CRSs) in [10] to provide a uniform framework for reductions with substitutions (also referred to as higher order rewriting) as in the λ-calculus [1]. Several other formalisms have been introduced later. We refer to Klop et al. [12] for a survey. Here we use a system of higher order rewriting, Expression Reduction Systems (ERSs), defined in [6] (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} 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 A, B, …, which range over terms, and object metavariables a, b, …, which range over variables. Besides 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_{0} by the result of substitution of terms t_{1}, …, t_{n} for free occurrences of x_{1}, …, x_{n} in t_{0}.

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, 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 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 substitutions) are called weakly similar.

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

Our syntax is close to the syntax 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 [6].

Below we ignore questions relating to renaming of bound variables.

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 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; 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. 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. We refer to the i-th (from the left, i > 0) descendant of o also as (u, i)-descendant of o. Correspondingly, subterms of o have 0 or more descendants. By definition, the descendant, referred to also as (u, @)-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 s′ ⊆ t that is not in u. We call them also (u, ∗)-descendants of s′. 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}; the i-th descendant is referred to as the (u, i)-descendant. All subterms of t_{0}, including free occurrences of x_{1}, …, x_{n}, have exactly one descendant, the (u, 0)-descendent. The descendant or (u, @)- descendent of the contracted redex u itself is its contractum. The pairs (u, i), (u, @), and (u, ∗) are called the indexes of corresponding descendants. The descendants of all redexes except the contracted one are called residuals.

The notions of descendant and residual extend by transitivity to arbitrary R_{fS}-reductions; indexes of descendants and residuals are sequences of indexes of (immediate) descendants and residuals in the chain leading from initial to the final subterm. If P is an R-reduction, then P -descendants and P -residuals are defined to be the descendants and residuals under the refinement of P. The ancestor relation is converse to the descendant relation. We call the co-initial reductions P : t ↠ s and Q : t ↠ e strictly equivalent (written P ≈_{st} Q) if s = e and P -descendants and Q-descendants of any subterm of t are the same in s and e.

An ERS is orthogonal (OERS) if in no term redex-patterns can overlap and, for any reduction step t→^{w}s, if u ⊆ s is a descendant of a redex v ≠ w of t, then u is weakly similar to v. The descendant relation and the following Strict Church-Rosser theorem is vital in the proofs throughout this paper: for any co-initial reductions P and Q in an OERS R there are reductions P′ and Q′ such that P + P′ ≈_{st} Q + Q′ [6].

3 Properties of S-reductions

In this section, we study some properties of substitutions.

We call a subterm s in t essential (written ES(s, t)) if s has at least one descendant under any reduction starting from t and call it inessential (written IE(s, t)) otherwise [7]. The notion of essentiality is a generalization of the notion of neededness [5, 13] in a way that it works for all subterms, bound variables in particular.

Notation Below F V (t) (resp. EF V_{R}(t)) denotes the set of variables having (R-essential) free occurrences in t. For any s ⊆ t, BV_{R}(s) (resp. EBV_{R}(s)) denotes the set of (Ressential) free occurrences of s bound by quantifiers belonging to patterns of R-redexes that are outside s.

We call a subterm e in u = Sx_{1} … x_{n}t_{1} … t_{n}t_{0} u-inessential (written IE(u; e)) if e is in t_{i} for some (1 ≤ i ≤ n) and x_{i} does not have a free occurrence in the S-normal form of t_{0}. The following lemma is easy to prove using the fact that if P : t ↠ t′ and s ⊆ t, then IE(s, t) iff any P -descendant of s is inessential in t′.

Lemma 3.1 (1) Let u = Sx_{1} … x_{n}t_{1} … t_{n}t_{0} ⊆ t. Then IE_{S}(u; t_{i}) iff x_{i} ∉ EF V_{S}(t_{0}). (2) Let s ⊆ t. Then IE_{S}(s, t) iff IE_{S}(u; s) for some S-redex u in t.

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

Lemma 3.2 Let s be obtained from t by replacing non-overlapping proper subterms t_{1}, …, t_{n} with s_{1}, …, s_{n}, respectively, where s_{i} and t_{i} do not contain S-redexes, and let ES_{S}(s_{i}, s) ⇒ BV_{S}(t_{i}) ⊆ BV_{S}(s_{i}) (i = 1, …, n). Further, let s′ and t′ be any corresponding subterms in s and t that are not in replaced subterms. Then IE_{S}(s′, s) ⇒ IE_{S}(t′, t). Proof By induction on the length of s. If t and s are not S-redexes, then the lemma follows easily from Lemma 3.1.(2) and the induction assumption. So suppose that t = Sx_{1} … x_{m}e_{1} … e_{m}e_{0}, s = Sx_{1} … x_{m}o_{1} … o_{m}o_{0}, s′ ⊆ o_{l}, and IE_{S}(s′, s). If IE_{S}(s′, o_{l}), then by the induction assumption IE_{S}(t′, e_{l}) and hence IE_{S}(t′, t). Otherwise, by Lemma 3.1.(3), we have IE_{S}(o_{l}, s). Hence, by Lemma 3.1.(2), IE_{S}(s; o_{l}). Thus, by Lemma 3.1.(1), x_{l} ∉ EF V_{S}(o_{0}). Let us show that x_{l} ∉ EF V_{S}(e_{0}). By Lemma 3.1.(2), if s_{i} ⊆ o_{0}, then ES_{S}(s_{i}, s) iff ES_{S}(s_{i}, o_{0}). Hence, for any S-essential subterm s_{i}, BV_{S}(t_{i}) ⊆ BV_{S}(s_{i}). By the induction assumption, if x_{l} has an S-essential occurrence in e_{0} outside of replaced subterms, then the corresponding occurrence of x_{l} in o_{0} is S-essential. If x_{l} has an S-essential occurrence in a subterm t_{j} ⊆ e_{0}, then, by Lemma 3.1.(3), ES_{S}(t_{j}, e_{0}). By the induction assumption, ES_{S}(s_{j}, o_{0}). Hence BV_{S}(t_{j}) ⊆ BV_{S}(s_{j}). Thus x_{l} has a free occurrence in s_{j}. Since s_{j} does not contain S-symbols, it follows from Lemma 3.1.(2) that this occurrence is S-essential in s_{j} and hence, by Lemma 3.1.(3) and ES_{S}(s_{j}, o_{0}), is S-essential in o_{0}. Hence x_{l} ∉ EF V_{S}(e_{0}) and, by Lemma 3.1.(1), IE_{S}(t; e_{l}). Therefore, by Lemma 3.1.(2), IE_{S}(t; t′) and IE_{S}(t′, t).

Lemma 3.3 Let u = C[t_{1}, …, t_{n}] and v = C[s_{1}, …, s_{n}] be weakly similar redexes, let s_{m_{1}}, …, s_{m_{l}} be the v-main arguments, s_{n_{1}}, …, s_{n_{k}} be the v-erased arguments, and let for each j = 1, …, l : BV (t_{m_{j}}) ⊆ BV (s_{m_{j}}). Then t_{n_{1}}, …, t_{n_{k}} are (not necessarily all) u-erased arguments. Proof Let u → t ↠ o and v → s ↠ e be refinements of u and v, respectively. Then s can be obtained from t by replacing descendants of t_{1}, …, t_{n} with s_{1}, …, s_{n}. Further, all descendants of s_{n_{1}}, …, s_{n_{k}} are \underline{S}-inessential. Therefore if t′_{i} and s′_{i} are corresponding descendants of t_{i} and s_{i} in t and s, then ES\underline{S}(s′_{i}, s) ⇒ BV\underline{S}(t′_{i}) ⊆ BV\underline{S}(s′_{i}). Thus the lemma follows from Lemma 3.2.

4 A Perpetual Strategy for OERSs

In this section, we design a strategy that for a term t in an OERS constructs a longest reduction when t is strongly normalizable, and constructs an infinite reduction otherwise. We use the strategy to generalize the Conservation Theorem [2, 1] to OERSs. We give also a method to determine the lengths of longest reductions of strongly normalizable terms.

Definition 4.1 The μ-extension (Σ_{μ}, R_{μ}) of an OERS (Σ, R) is defined as follows:

1. Σ_{μ} = Σ ∪ {μ^{n} | n = 0, 1, …}, where μ^{n} is a fresh n-ary function symbol. For any subterm s = μ^{n+1}(t_{1}, …, t_{n}, t_{0}) of a term t over Σ_{μ}, the arguments t_{1}, …, t_{n}, as well as subterms and symbols in t_{1}, …, t_{n} and the head-symbol μ itself, are called μ-erased or more precisely μ′-erased, where μ′ is the occurrence of the head symbol of s in t. The argument t_{0} is called μ′-main. Symbols and subterms in t that are not μ-erased are called μ-main. We denote by [t]_{μ} the term obtained from t by removing all μ-erased symbols.

2. R_{μ} is the set of all rules of the form r_{μ} : t′ → s′ such that

(a) there is a rule r : t → s in R such that [t′]_{μ} = t;

(b) t′ is linear; its head symbol is not a μ-symbol; the μ-erased arguments of each μoccurrence μ′ in t′ are term metavariables, and the μ′-main argument is not a term metavariable;

(c) Let A_{1}, …, A_{n} be all μ-main term metavariables of t′, B_{1}, …, B_{j} be all μ-erased term metavariables of t′, and let k be the number of occurrences of μ-symbols in t′. Then

s′ = μ^{m}(\overbrace{μ^{0}, …, μ^{0}}^{k}, B_{1}, …, B_{j}, A_{i_{1}}, …, A_{i_{l}}, s).

3. An assignment θ is admissible for r_{μ} iff the arguments A_{i_{1}}θ, …, A_{i_{l}}θ of the redex t′θ do not have descendants under the reduction step tθ → sθ; and the assignment θ_{μ} such that Aθ_{μ} = [Aθ]_{μ} and aθ_{μ} = aθ for any term metavariable A and object metavariable a is admissible for r.

4. For any r_{μ}-redex u = t′θ, we call arguments that correspond to A_{i_{1}}, …, A_{i_{l}} quasierased arguments of u, and call the arguments that correspond to other metavariables from A_{1}, …, A_{n} quasi-main.

For example, Ap(μ^{3}(A, B, μ^{2}(C, λaD)), μ^{1}(E)) → μ^{8}(μ^{0}, μ^{0}, μ^{0}, A, B, C, E, (E/a)D) and Ap(μ^{3}(A, B, μ^{2}(C, λaD)), μ^{1}(E)) → μ^{7}(μ^{0}, μ^{0}, μ^{0}, A, B, C, (E/a)D) are two β_{μ}-rules with the same left-hand and different right-hand sides. The arguments A, B, and C are μ-erased, and E and D are μ-main. An assignment θ is admissible for the first rule iff aθ ∉ F V (Dθ) and is admissible for the second one otherwise.

Notation ∥t∥_{μ} denotes the number of occurrences of μ-symbols in t.

One can prove using Definition 4.1 that R_{μ} is orthogonal. Let t be a term over Σ_{μ} whose head-symbol is not a μ-symbol. Then t is an r_{μ}-redex (in R_{μ}) iff [t]_{μ} = s is an r-redex (in R). Moreover, if t′ is the contractum of t in R_{μ} and s′ is the contractum of s in R, then [t′]_{μ} = s′. Hence, for any R-reduction Q : s_{0} →^{u_{0}} s_{1} →^{u_{1}} … and for any term t_{0} in R_{μ} such that [t_{0}]_{μ} = s_{0}, there is a reduction Q_{μ} : t_{0} →^{v_{0}} t_{1} →^{v_{1}} … in R_{μ} such that [t_{i}]_{μ} = s_{i}, and u_{i} and v_{i} are corresponding subterms in s_{i} and t_{i} (i = 0, 1, …). If t_{0} has the R_{μ}-normal form t^{∗}, then t_{i} ↠ t^{∗} in R_{μ} and i ≤ ∥t_{i}∥_{μ} ≤ ∥t^{∗}∥_{μ}; hence s_{0} is normalizable in R and R_{μ}. Thus

Lemma 4.1 (Klop [10]) Let t be a term in an OERS R. If t is weakly normalizable in R_{μ}, then t is strongly normalizable in R_{μ} and R.

Proposition 4.1 (1) Let R be an OERS, u and v be R_{μ}-redexes such that u is in an argument of v, and let v→^{u}w in R_{μ}. Then w is an R_{μ}-redex weakly similar to v, and quasimain sequences of v and w coincide.

(2) Let u be a redex in an OERS R and v be an R_{μ}-redex such that [v]_{μ} = u and the sets of free variables of quasi-main arguments of v coincide with that of corresponding arguments of u. Then an argument of v is quasi-erased iff the corresponding argument of u is erased.

(3) Let u be a redex in an OERS R and v be an R_{μ}-redex such that [v]_{μ} = u. Then the corresponding argument of any quasi-erased argument of v is u-erased. Proof The proposition is a corollary of Lemma 3.3.

Definition 4.2 (1) We call a subterm s of a term t unabsorbed in a reduction P : t ↠ e if the descendants of s do not appear inside redex-arguments of terms in P, and call s 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 u_{l} be a redex in a term t defined as follows: choose an unabsorbed redex u_{1} in t; choose an erased argument s_{1} of u_{1} that is not in normal form (if any); choose in s_{1} an unabsorbed redex u_{2}, and so on, as long as possible. Let u_{1}, s_{1}, u_{2}, …, u_{l} be such a sequence. Then we call u_{l} a limit redex and call u_{1}, s_{1}, u_{2}, …, u_{l} a limit sequence of t.

(3) We call a reduction limit if each contracted redex in it is limit, and call a strategy limit if in any term not in normal form it contracts a limit redex.

It is easy to show that a redex is unabsorbed iff it is external [5]. As in OTRSs [5, 7], it can be shown that in any term not in normal form there is an unabsorbed redex, hence a limit redex as well. The following lemma is also proved as in OTRSs [8].

Lemma 4.2 Let u be a limit redex in t and let P : t ↠ e. Then there is no new redex in e that contains a descendant of u in its argument. Proof Let u_{1}, s_{1}, u_{2}, …, u_{l} be the limit sequence of t with u_{l} = u. We prove by induction on |P | that (a): descendants of redexes u_{1}, …, u_{l} do not appear inside arguments of new redexes. If |P | = 0, then (a) is obvious. So let P : t ↠ e′ →^{v} e, let o be a descendant of u in e, and let o′ be its ancestor in e′. It follows from the induction assumption that each redex u_{i} (i = 1, …, l − 1) has exactly one residual u′_{i} in e′ (because contraction of a residual of any of the redexes u_{1}, …, u_{l−1} erases the descendant of u), there is no new redex in e′ that contains o′ in its argument, and o is the only descendant of u. Thus if there is a new redex w in e that contains the residual u′′_{i} of some u_{i} in its argument, then it must be created by v. If v ⊈ u′_{1}, then w contains u′′_{i} in its argument iff it contains the residual of u′_{1} in its argument, but this is impossible since u_{1} is unabsorbed. Thus v ⊆ u′_{1}. Let k be the maximal number such that v is in u′_{k} and let s′_{k} be the descendant of s_{k} in e′. Then v is in s′_{k} and contains u′_{k+1}. Let Q : s_{k} ↠ s′′_{k} consist of steps of P that are made in descendants of s_{k}. Then the residual of u_{k+1} is in an argument of the new redex w ⊆ s′′_{k}. But this is impossible since u_{k+1} is unabsorbed in s_{k}. Thus (a) is valid and the lemma is proved.

Lemma 4.3 Let (Σ, R) be an OERS, P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … → t_{n} be a limit reduction in R, and P_{μ} : s_{0} = t_{0}→^{v_{0}}s_{1}→^{v_{1}} … → s_{n} be its μ-corresponding reduction in R_{μ}. Then

(1) for each k (0 ≤ k ≤ n), the following holds:

(a)_{k}: ∥s_{k}∥_{μ} = k; (b)_{k}: each redex v′_{k} ⊆ s_{k} is μ-main in s_{k}. (c)_{k}: in quasi-main arguments of any redex v′′_{k} in s_{k} there are no μ-symbols.

(2) if P is normalizing, then so is P_{μ}. Proof (1) (a)_{0} − (c)_{0} are obvious. Suppose that (a)_{k} − (c)_{k} hold and let us show (a)_{k+1} − (c)_{k+1}. Let u_{k} = C[o_{1}, …, o_{q}] and v_{k} = C′[e_{1}, …, e_{q}, e′_{1}, …, e′_{m}], where e_{1}, …, e_{q} are μ-main arguments of v_{k} (which correspond to arguments o_{1}, …, o_{q} of u_{k}, respectively) and e′_{1}, …, e′_{m} are μ-erased arguments of v_{k}. Since u_{k} and v_{k} are corresponding redexes in t_{k} and s_{k}, we have [v_{k} ]_{μ}= u_{k} and hence (α): [e_{i}]_{μ} = o_{i} for all i = 1, …, q. Let e_{i_{1}}, …, e_{i_{l}} be the v_{k}-quasi-erased arguments and e_{j_{1}}, …, e_{j_{p}} be the v_{k}-quasi-main arguments. Then the contractum of v_{k} in R_{μ} has the following form: o′ = μμ^{0} … μ^{0}e′_{1} … e′_{m}e_{i_{1}} … e_{i_{l}}o. By Proposition 4.1.(3), o_{i_{1}}, …, o_{i_{l}} are u_{k}-erased, and since u_{k} is limit, (β): o_{i_{1}}, …, o_{i_{l}} are in R-normal form. By (c)_{k}, (γ): there are no occurrences of μ-symbols in e_{j_{1}}, …, e_{j_{p}}, o. (Hence o coincides with the contractum of u_{k}). It follows from (α), (β), and (b)_{k} that (δ): e_{i_{1}}, …, e_{i_{l}} are in R_{μ}-normal form.

By (γ), ∥o′∥_{μ} = ∥v_{k}∥_{μ} + 1. Hence ∥s_{k+1}∥_{μ} = ∥s_{k}∥_{μ} + 1 = k + 1, i.e., (α)_{k+1} holds.

If v′_{k+1} ⊈ o′, then (b)_{k} implies that v′_{k+1} is μ-main. If v′_{k+1} ⊆ o′, then by (b)_{k}, v′_{k+1} ⊈ e′_{1}, …, e′_{m} (since ancestors of e′_{1}, …, e′_{m} are μ-erased arguments of v_{k}) and by (δ), v′_{k+1} ⊈ e_{i_{1}}, …, e_{i_{l}}. Hence v′_{k+1} ⊆ o and by (γ), v′_{k+1} is μ-main. Now (b)_{k+1} is proved.

If o′ ∩ v′′_{k+1} = ∅, then (c)_{k+1} follows immediately from (c)_{k}. If v′′_{k+1} ⊆ o′, then as we have shown above (for v′_{k+1}), v′′_{k+1} ⊆ o and (c)_{k+1} follows from (γ). Suppose now that o′ is a proper subterm of v′′_{k+1} and v′′_{k+1} has an v_{k}-ancestor v_{k}^{∗} in s_{k} for which v′′_{k+1} is a residual. Let u_{k}^{∗} be the corresponding redex of v_{k}^{∗} in t_{k} (it exists because, by (b)_{k}, v_{k}^{∗} is μ-main). Obviously, u_{k} is a proper subterm of u_{k}^{∗} and since u_{k} is limit, it must be in an erased argument of u_{k}^{∗}. By (c)_{k}, v_{k}^{∗}-quasi-main arguments do not contain μ-symbols. Thus the sets of free variables of v_{k}^{∗}-quasi-main arguments coincide with that of corresponding arguments of u_{k}^{∗}. Hence, by Proposition 4.1.(2), v_{k} is in a quasi-erased argument of v_{k}^{∗}. Therefore, by Proposition 4.1.(1), o′ is in a quasi-erased argument of v′′_{k+1} and the quasi-main arguments of v′′_{k+1} coincide with the corresponding quasi-main arguments of v_{k}^{∗}. Thus, by (c)_{k}, in the quasi-main arguments of v′′_{k+1} there are no occurrences of μ-symbols. To prove c_{k+1}, it remains to consider the case then o′ is a proper subterm of v′′_{k+1} and v′′_{k+1} is created by v_{k}. If in quasi-main arguments of v′′_{k+1} there are μ-symbols, then in main arguments of corresponding redex u′′_{k+1} in s_{k+1}, which is also an u_{k}-new redex, there are descendants of redexes contracted in P. But each redex contracted in P is a limit redex. Thus, by Lemma 4.2, their descendants can not occur in arguments of new redexes. Hence, also in this case, there are no μ-symbols in quasi-main arguments of v′′_{k+1}, and (c)_{k+1} is valid.

(2) By (b)_{n}.

Theorem 4.1 A limit strategy is perpetual in OERSs. Moreover, if a term t in an OERS R is strongly normalizable, then a limit strategy constructs a longest normalizing reduction starting from t, and its length coincides with the μ-norm of R_{μ}-normal form of t. Proof If a limit R-reduction P starting from t is normalizing, then by Lemma 4.3 its corresponding R_{μ}-reduction also is normalizing. Hence, by Lemma 4.1, t is strongly normalizable in R. Thus, the limit strategy is perpetual. Now, if t is strongly normalizable, Q is a normalizing R-reduction, and s is an R_{μ}-normal form of t, then |Q| = |Q_{μ}| ≤ ∥s∥_{μ} =(by Lemma 4.3)= |P |.

A proof of perpetuality of the β-reduction strategy that contracts special redexes is presented in Barendregt [1]. It uses only unabsorbness of the leftmost-outermost redexes and therefore generalizes easily to the case of OERSs. The proof of the Conservation Theorem [2, 1] also remains valid for OERSs if one uses the limit strategy instead of the ‘special’ perpetual strategy (which does not work for OERSs). Therefore:

Theorem 4.2 (Conservation Theorem) If a term t in an OERS R has an infinite reduction and t→^{u}s, where u is a non-erasing redex, then s has also an infinite reduction.

An extension of the Conservation Theorem can be found in de Groote [4]. It is a neat translation of Klop’s Lemma 4.1 by simulating λ_{μ} with some reductions on λ-terms. Unfortunately, this is not possible for arbitrary OERSs.

As shown above (Lemmas 4.1 and 4.3), a term in an OERS R is strongly normalizable iff it is weakly normalizable in R_{μ}. The following example shows that, despite the claim of Klop [10] (see p. 181), if R is strongly normalizing, then R_{μ} need not be so.

Example 4.1 Let R = {f(τa(c, A)) → g((τa(A, A)/a)A)}, where c is a constant, a is an object metavariable, and τ is a quantifier sign of arity (1, 2) and scope indicator (1, 2). Creation or a redex inside the contractum is only possible if, say in the case a = x, A has a subterm f(s), i.e., A = C[f(x)], and τa(A, A) = τx(c, c); or if A = C[f(τyx)] with y ≠ x and τa(A, A) = c, but this is impossible. Redex creation is not possible also outside the contractum, because g is not a pattern-symbol. Thus no redex creation is possible in R and hence R is strongly normalizing, while contraction of the redex v = f(τx(μ^{2}(f(x), c), μ^{2}(f(x), c)) in R_{μ} creates itself: v → μ^{2}(f(x), g(μ^{2}(v, c))), and it is easy to see that v is not normalizable in R_{μ}. (Recall that, for the case of OTRSs, R is strongly normalizing iff R_{μ} is weakly normalizing [10, 8].)

5 Longest Reductions in Strongly Persistent OERSs

In this section, we design an algorithm for computing the lengths of longest reductions in strongly persistent ERSs. 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 satisfyed. To this end, we introduce and study strong similarity of redexes. The results generalize some results from [8].

Without restricting the class of (non-conditional) OERSs, we can assume that in righthand sides of rewrite rules the last argument of each metasubstitution is a term-metavariable or a metasubstitution.

Definition 5.1 (1) Let t→^{u}s in an OERS R, let t → t′ ↠ s be its refinement, and let v be a new redex in s. We call v generated if v is a residual of a redex of t′ whose pattern is in the pattern of the contractum of u in R_{f}.

(2) We call an OERS R persistent (written PERS) if each created redex in R is generated.

(3) We call an OERS R strongly persistent (written SPERS) if R_{fS} is persistent.

It is easy to see that a non-simple OERS R is strongly persistent iff the left-hand sides of its rules contain only one function or quantifier symbol. Further, if R is a strongly persistent OERS, then so is R_{μ}. Example 4.1 shows that if R is persistent, then R_{μ} need not be so (in the reduction v = f(τx(μ^{2}(f(x), c)μ^{2}(f(x), c))→^{v}μ^{2}(f(x), g(μ^{2}(v, c)), the pattern of the created v contains argument-symbols of the contracted v). On the other hand, a PERS R such that R_{μ} also is persistent need not be strongly persistent. An example is R = {r_{1} : ∃aA → f((τaA/a)A), r_{2} : g(f(x)) → c}. The proofs of results in this section use only persistency of R_{μ} and hence are valid for a subclass of PERSs properly containing the class of SPERSs and persistent OTRSs (persistency of an OTRS R implies persistency of R_{μ}). We do not know a characterization of the class in terms of redex-creation.

Notation For any s ⊆ t, MBV_{R}(s) (resp. MEBV_{R}(s)) denotes the multiset of (Ressential) free occurrences of s bound by quantifiers belonging to patterns of R-redexes that are outside s (the number of occurrences of a bound variable in the multiset coincides with the number of its (R-essential) occurrences in s).

Definition 5.2 We call weakly similar redexes u = C[s_{1}, …, s_{n}] and v = C[o_{1}, …, o_{n}] respectively similar, strongly similar, R-essentially similar, or strongly R-essentially similar if, for all i, BV (e_{i}) = BV (o_{i}), MBV (e_{i}) = MBV (o_{i}), EBV (e_{i}) = EBV (o_{i}), or MEBV (e_{i}) = MEBV (o_{i}). We denote the equivalence class of redexes strongly similar to u by ⟨u⟩_{s}.

Lemma 5.1 Let R be an SPERS, let u = C[t_{1}, …, t_{n}] and v = C[s_{1}, …, s_{n}] be strongly similar R_{μ}-redexes whose arguments are in normal form and are not variables. Further, let P : u = o_{0}→^{u}o_{1}→^{u_{1}} … and Q : v = e_{0}→^{v}e_{1}→^{v_{1}} … be refinements of rightmost R_{μ}-reductions of u and v that are infinite or end at normal forms. Then it is possible to define one-to-one correspondence between the following occurrences of o_{i} and e_{i}:

(1) \underline{S}-essential redexes and their arguments;

(2) \underline{S}-essential descendants of redexes;

(3) \underline{S}-essential descendants of arguments of u and v, called argument subterms; and

(4) \underline{S}-essential descendants* of free occurrences of variables in t_{j} and s_{j} that are bound in o_{i} and e_{i}, called context variables, where the notion of descendant* is defined similarly to that of descendant with the exception that, during \underline{S}-steps, the occurrences of the replaced bound variables do not have descendants*.

Furthermore, for each i (i = 0, 1, …), the following conditions hold:

(a)_{i}: corresponding \underline{S}-essential redexes in o_{i} and e_{i} are strongly \underline{S}-essentially similar, and u_{i} and v_{i} are corresponding \underline{S}-essential redexes if one of them is \underline{S}-essential.

(b)_{i}: if o^{∗} and e^{∗}, as well as o′′ and e′′, are corresponding \underline{S}-essential occurrences in o_{i} and e_{i}, then o^{∗} ⊆ o′′ iff e^{∗} ⊆ e′′. Proof By induction on i (the case i = 0 is obvious from the assumptions). Assume first that u_{m} = \underline{S}y_{1} … y_{k}t′_{1} … t′_{k}t′_{0} and v_{m} = \underline{S}y_{1} … y_{k}s′_{1} … s′_{k}s′_{0} are \underline{S}-redexes. If u_{m} and v_{m} are \underline{S}-inessential, then all \underline{S}-essential occurrences of o_{m} and e_{m} are outside u_{m} and v_{m}, and each of them has exactly one \underline{S}-essential descendant in o_{m+1} and e_{m+1}, respectively. Hence descendants of corresponding \underline{S}-essential occurrences of o_{m} and e_{m} form pairs of corresponding \underline{S} -essential occurrences in o_{m+1} and e_{m+1}. So suppose that both u_{m} and v_{m} are \underline{S}-essential. It follows from (a)_{m} and (b)_{m} that (α): y_{i} has the same number of corresponding \underline{S}-essential occurrences in t′_{0} and s′_{0} and in each pair of corresponding \underline{S}-essential subterms of t′_{0} and s′_{0}. It follows from Lemma 3.1.(3) that descendants of \underline{S}-essential occurrences of o_{m} and e_{m} are \underline{S}-essential in o_{m+1} and e_{m+1} iff they are substituted for \underline{S}-essential contextvariables. Thus corresponding \underline{S}-essential subterms in o_{m} and e_{m} have the same number of \underline{S}-essential descendants, and corresponding \underline{S}-essential context-variables have the same number of \underline{S}-essential descendants* in o_{m+1} and e_{m+1}; they form pairs of corresponding \underline{S}-essential occurrences in o_{m+1} and e_{m+1}. Since argument-subterms in o_{m} and e_{m} are not variables, different subterms have different descendents. Thus the correspondence between these subterms in o_{m+1} and e_{m+1} remains one-to-one. Since R_{μ} is persistent, no new redexes are created by these steps. Thus (a)_{m+1} follows from (a)_{m} and from the fact that the context-variables form pairs of corresponding occurrences. (b)_{m+1} follows from (α) and (b)_{m}.

Suppose now that u_{m} and v_{m} are R_{μf} -redexes. In this case, there are no \underline{S}-redexes in o_{m} and e_{m}. Obviously, the contractum of u_{m} can be obtained from the contractum of v_{m} by replacing descendants of arguments of v_{m} with the corresponding arguments of u_{m}. Since R_{μ} is persistent, for each new redex w in o_{m+1} there is a unique new redex w′ in e_{m+1}. All the descendants of the occurrences that are outside u_{m} and v_{m} are \underline{S}-essential. By (a)_{m}, u_{m} and v_{m} are strongly similar. Hence, it follows from conditions (a)-(b) of Definition 2.2 and Lemma 3.2 that corresponding new redexes in o_{m+1} and e_{m+1} are either both \underline{S}-essential or both are \underline{S}-inessential. The same holds for corresponding arguments of the corresponding redexes. Corresponding occurrences in o_{m} and e_{m} have the same number of \underline{S}-essential descendants in o_{m+1} and e_{m+1}; together with corresponding \underline{S}-essential new redexes they form pairs of corresponding \underline{S}-essential occurrences in o_{m+1} and e_{m+1}; the correspondence remains one-to-one. Since variables bound by quantifiers belonging to patterns of w and w′ can only occur in the descendants of arguments of u_{m} and v_{m}, and \underline{S}-essential (in o_{m+1} and e_{m+1}) occurrences of context variables form pairs of corresponding \underline{S}-essential occurrences in corresponding arguments of w and w′, it follows from Lemma 3.1.(3) that w and w′ are strongly \underline{S}-essentially similar. Hence (a)_{m+1} follows from (a)_{m}. (b)_{m+1} follows from (b)_{m}.

Definition 5.3 Let R be an SPTRS.

(1) Let t be a term in R_{μ}, let s be a non-variable subterm of t, and let P : t ↠ e be the rightmost innermost normalizing R_{μ}-reduction. Then we define Mult_{μ}(s, t) as the number of P -descendants of s in e.

(2) Let u = C[e_{1}, …, e_{n}] be a redex in R_{μ}, let s′ ⊆ e_{i}, let v = C[o_{1}, …, o_{n}] be a redex strongly similar to u whose arguments o_{1}, …, o_{n} are in R_{μ}-normal form and are not variables, and let Q : v ↠ o be the rightmost innermost normalizing R_{μ}-reduction. Then we define mult_{μ}(u, i) = mult_{μ}(u, s′) = mult_{μ}(⟨u⟩_{s}, i) = Mult_{μ}(o_{i}, v). mult_{μ}(u) = mult_{μ}(⟨u⟩_{s}) is defined to be the number of μ-subterms in o that appear during Q, i.e., that are not descendants of μ-subterms from v. We call numbers mult_{μ}(u, i) and mult_{μ}(⟨u⟩_{s}, i) proper μ-indices of u and ⟨u⟩_{s}, and numbers mult_{μ}(u) and call mult_{μ}(⟨u⟩_{s}) μ-indices of u and ⟨u⟩_{s}.

The correctness of the above definition follows from Lemma 5.1. We have to consider only non-variable subterms because descendants of a bound variable with different indexes can happen to coincide. Alternatively, one could consider all subterms but take into account the multiplicity of each descendant.

The following lemma is proved using Definition 5.3 and the fact that if t be a strongly normalizable term in a PERS R_{μ}, e ⊆ s ⊆ t, and e and s are non-variable R_{μ}-normal forms, then Mult_{μ}(s, t) = Mult_{μ}(e, t).

Below L(t) denotes the length of a longest reduction starting from t.

Lemma 5.2 (1) Let t be a strongly normalizable term in an SPERS R and u_{1}, …, u_{n} be all redexes in t. Then

L(t) = ∑_{i=1}^{n}Mult_{μ}(u_{i}, t)mult_{μ}(u_{i}).

(2) Let t be a strongly normalizable term in an PERS R_{μ} and u_{1}, …, u_{n} be all redexes in t that contain a non-variable subterm s in their arguments. Suppose that s is in m_{i}-th argument of u_{i} (i = 1, …, n). Then

Mult_{μ}(s, t) = ∏_{i=1}^{n}mult_{μ}(u_{i}, s) = ∏_{i=1}^{n}mult_{μ}(u_{i}, m_{i}).

(3) Let u = C[e_{1}, …, e_{k}] be a redex whose arguments e_{1}, …, e_{k} are not variables and are in normal form, in an SPERS R. Then, for all i = 1, …, k,

mult_{μ}(u, j) = mult_{μ}(⟨u⟩_{s}, j) = ∑_{i=1}^{m_{j}}Mult_{μ}(e_{j_{i}}, o),

mult_{μ}(u) = mult_{μ}(⟨u⟩_{s}) = ∑_{i=1}^{m}Mult_{μ}(u_{i}, o)mult_{μ}(u_{i}) + 1,

where o is the contraction of u in R_{μ}, e_{j_{1}}, …, e_{j_{m_{j}}} are all descendants of e_{j} in o, and u_{1}, …, u_{m} are all redexes in o.

Lemma 5.3 Let u and v be strongly similar redexes in an SPERS R, let u→^{u}o and v→^{v}e. Then u and v create the same number of strongly similar redexes. Proof Take in Lemma 5.1 the refinement of u for P and the refinement of v for Q.

Hence, one can define ⟨u_{0}⟩_{s}, ⟨u_{1}⟩_{s} … to be a ⟨u_{0}⟩_{s}-chain or u_{0}-chain if ⟨u_{i} ⟩_{s} generates ⟨u_{i+1}⟩_{s}, i.e., if u_{i} generates a redex strongly similar to u_{i+1}. It is easy to see that a term t in a PERS R is strongly normalizable iff all chains of redexes in t are finite ((⇒) is trivial and (⇐) can be shown using the method of multiset ordering; we could equally use similarity classes for this criterion instead of strong similarity classes). Therefore, the following theorem is a corollary of Theorem 4.1 and Lemma 5.2.

Theorem 5.1 Let t be a term in an SPERS R. Then the least upper bound L(t) of lengths of reductions starting from t can be found using the following:

Algorithm 5.1 Let ⟨u_{1}⟩_{s}, …, ⟨u_{n}⟩_{s} be all strong similarity classes whose member redexes occur in t. If an ⟨u_{i} ⟩_{s}-chain is infinite for at least one i, then L(t) = ∞. Otherwise, using Lemmas 5.2.(3) and 5.2.(2), compute the μ-indices and the proper μ-indices of all classes ⟨u_{i} ⟩_{s}. Finally, using Lemmas 5.2.(2) and 5.2.(1), compute L(t).

For any ⟨u⟩_{s} in a non-creating OERS (where no redex-creation is possible), mult_{μ}(⟨u⟩_{s}) = 1, mult_{μ}(⟨u⟩_{s}, i) = 1 if the i-th argument o_{i} of u does not have a u-descendant, and mult_{μ}(⟨u⟩_{s}, i) coincides with the number of u-descendants of o_{i} otherwise. Since developments in an OERS are reductions in non-creating OERSs up to some isomorphism, a simpler form of Algorithm 5.1 can be used for computing lengths of longest developments in OERSs.

6 Conclusions

We presented an algorithm for constructing longest reductions and computing their lengths in OERSs, and used the algorithm to generalize the Conservation Theorem to OERSs. Bergstra and Klop [3] gave a characterization of erasing β-redexes (K-redexes) for which the Conservation Theorem in λ-calculus still is valid. We leave this question for OERSs to a future investigation. De Vrijer [17] gave another characterization of lengths of longest reductions in a typed λ-calculus. Van der Pol [16] used a semantic method for strong normalization proofs in higher order rewriting systems.

Acknowledgments I enjoyed discussions with H. Barendregt, J. W. Klop, J.-J. Lévy, L. Maranget, G. Mints, V. van Oostrom, Sh. Pkhakadze, F. van Raamsdonk, Kh. Rukhaia, and V. Sazonov. I also would like to thank G. Gonthier, G. Tagviashvili, K. Urbaitis, and F. J. de Vries for their help in the preparation of this paper.

References

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

[2] Barendregt H. P., Bergstra J., Klop J. W., Volken H. Some notes on lambda-reduction, In: Degrees, reductions, and representability in the lambda calculus. Preprint no. 22, University of Utrecht, Department of mathematics, p. 13-53, 1976.

[3] Bergstra J. A., Klop J. W. Strong normalization and perpetual reductions in the Lambda Calculus. J. of Information Processing and Cybernetics 18, 1982, p. 403-417.

[4] De Groote P. The Conservation Theorem revisited. In: M. Bezem, J. F. Groote, eds. Proc. of the International Conference on Typed Lambda Calculi and Applications. Springer LNCS, vol. 664, Utrecht, 1993, p. 163-178.

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

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

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

[8] Khasidashvili Z. Perpetuality and strong normalization in orthogonal term rewriting systems. In: P. Enjalbert, E. W. Mayr, and K. W. Wagner eds. Proc. of 11^{th} Symposium on Theoretical Aspects of Computer Science. Springer LNCS, vol. 775, Caen, 1994, p. 163-174.

[9] Khasidashvili Z. Perpetual reductions in orthogonal combinatory reduction systems. CWI report CS-R9349, 1993.

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

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

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

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

[14] Nederpelt R. P. Strong Normalization for a typed lambda-calculus with lambda structured types. Ph.D. Thesis, Eindhoven, 1973.

[15] O’Donnell M. J. Computing in systems described by equations. Springer LNCS 58, 1977.

[16] Van der Pol J. Termination proofs for Higher-order Rewrite Systems. To appear in: Proc. of International Workshop on Higher-order Algebra, Logic and Term Rewriting, Amsterdam, 1993. Available as logic group preprint series No. 93, Utrecht, 1993.

[17] De Vrijer R. C. Surjective Pairing and Strong Normalization: Two Themes in Lambda Calculus. Ph.D. Thesis, Amsterdam, 1987.