Perpetual Reductions in Orthogonal Combinatory Reduction Systems

Zurab Khasidashvili

CWI P.O. Box 4079, 1009 AB Amsterdam, The Netherlands

Abstract

We design a strategy that for any given term t in an Orthogonal Combinatory Reduction System (OCRS) (that is, a Term Rewriting System with bound variables and substitutions) constructs a longest reduction starting from t if t is strongly normalizable, and constructs an infinite reduction otherwise. We develop a method for finding the least upper bound of lengths of reductions 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 finding lengths of longest reductions in “strongly persistent” OCRSs. As a corollary, we have an algorithm for finding lengths of longest developments in orthogonal CRSs.

AMS Subject Classification (1991): 68Q42. CR Subject Classification (1991): F4.2, F4.1.

Keywords & Phrases: orthogonal combinatory reduction systems, perpetual reductions, strong normalization, reduction strategies, strongly persistent combinatory reduction systems. Note: Part of this work was completed during an enjoyable visit of the author at CWI in the summer of 1993.

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 [20]. 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 [15].

It is easy to see that in any infinite reduction a redex that itself has an infinite reduction, called an infinite redex, is contracted. Thus in order to construct an infinite reduction one should try to retain at least one “potential” 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 potential infinite redexes is perpetual. In OTRSs, any potential infinite redex necessarily has an infinite reduction. That is why all the above strategies are perpetual. In orthogonal Combinatory Reduction Systems (that is, TRSs with bound variables and substitution mechanism [14, 8, 19, 10]) a strongly normalizable subterm may also be a potential infinite redex — after contraction of an outer redex a term can be substituted in it that makes the subterm no more strongly normalizable. Thus innermost reductions and complete reductions are no more perpetual in OCRSs. 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. [3].

In this paper, we design a perpetual strategy for all orthogonal combinatory reduction systems. Our aim is not only to construct an infinite reduction of any given term t whenever it exist, but also to construct a longest possible one if t is strongly normalizable. Thus we will be able to characterize the complexity of computations of terms. The idea is that, as mentioned above, in order to construct perpetual reductions one should try to avoid erasure of redexes in which substitution of terms is possible during reductions of outer redexes. On the other hand, in order to construct the longest possible reductions one should delay contraction of a redex until it will no more 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.

An unabsorbed redex exists in any term not in a normal form, but there is no general algorithm to find one. So we define some classes of OCRSs, such as non-absorbing, non-left-absorbing, and non-right-absorbing systems, for which the unabsorbed redexes are easy to find. For example, in non-left-absorbing systems, no subterm can be absorbed to the left of the contracted redex, so the leftmost-outermost redexes are unabsorbed. (In particular, the λ-calculus and the combinatory logic are non-left-absorbing.)

We develop a method for proving that the reductions constructed according to our perpetual strategy are indeed the longest, and for finding their lengths. Our method is similar to the Nederpelt’s method [18], invented to reduce proofs of strong normalization to proofs of weak normalization (i.e., existence of a normal form). For any OCRS R, we define the corresponding non-erasing OCRS R_{μ}, called the μ-extension of R. We add fresh function symbols μ^{n} of arity n (n = 0, 1, …) 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 have a natural translation of R-reductions into R_{μ}-reductions and vice-versa. Finally, we keep also 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 OCRS 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.

To find this number, sometimes it is not necessary to do actual transformation of o. We show this for the case of strongly persistent CRSs, where 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 OCRSs. The above results relay on the fact that strongly similar redexes generate the same number of strongly similar redexes.

2. Orthogonal Combinatory Reduction Systems Combinatory Reduction Systems have been introduced in Klop [14] to provide a uniform framework for reductions with substitutions, as in the λ-calculus and its extensions [2]. Different formalisms are proposed in Kennaway and Sleep [8] ((Functional) Combinatory Reduction Systems), Khasidashvili [9] (Expression Reduction Systems), and Nipkow [19] (Higher-order Rewrite Systems). They are extensions of Term Rewriting Systems [5, 15] by means of variable binding and substitution mechanisms. Restricted notions of CRSs were first introduced in Pkhakadze [22] and Aczel [1]. A comparison of some formalisms of rewriting systems with bound variables and substitution mechanism (referred to also as higher order rewrite systems), can be found in van Oostrom and van Raamsdonk [21]. A survey paper is Klop et al. [16]. Here we describe a system of higher order rewriting as defined in Khasidashvili [10]; it is based on the syntaxs of [22].

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 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 A, B, …, which range over terms, and object metavariables a, b, …, which range over variables. Apart from the usual rules for termformation, 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) A Combinatory Reduction System (CRS) 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.

Example 2.1 Operator signs ∃ and ∃! for “there exists” and “there exists exactly one”, having the arity (1, 1) and the scope indicator (1), can be defined using Hilbert’s operator (sign) τ as follows:

∃aA → (τaA/a)A
∃!aA → ∃aA ∧ ∀a∀b(A ∧ (b/a)A ⇒ a = b)

where ∀ is the quantifier sign with arity (1, 1) and scope indicator (1) for “for any”. Any assignment is admissible for the ∃-rule. An assignment θ is admissible for the ∃!-rule iff bθ ∉ FV (Aθ). Obviously, b is an additional object metavariable.

Remark 2.1 Terms o and e are called congruent, notation o ≅ e, if o is obtained from e by renaming bound variables. The conditions in Definition 2.2 imply that, for any rule r : t → s, if θ, θ′ ∈ AA(r), then tθ ≅tθ′ implies sθ ≅sθ′. Below we identify all congruent terms.

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, σ for operators and operator signs, 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, i.e., the number of steps, of P. If the last term of P coincides with the initial term of Q, then P + Q denotes the concatenation of P and Q. ∅_{t}, or simply ∅, denotes the empty reduction of a term t; the symbol ∅ is also used to denote the empty set.

Definition 2.3 A term t in a CRS R is said to be in normal form (nf) or to be a nf if it does not contain redexes. If s ↠ t and t is a nf, then t is called a normal form of s. A term is called weakly normalizable if it has a nf and is called strongly normalizable if it does not possess an infinite reduction. A CRS R is called weakly normalizing (resp. strongly normalizing) if each term in R is weakly normalizable (resp. strongly normalizable).

Definition 2.4 Let t → s be a rule in a CRS R and θ be an assignment. Subterms of a redex v = tθ that correspond to term metavariables of t are the arguments of v, and the rest is the pattern of v. Subterms of v rooted at the pattern are called the pattern-subterms of v. If R is a simple CRS, then arguments, pattern, and pattern-subterms are defined analogously in the contractum sθ of v.

Definition 2.5 A rewrite rule t → s in a CRS R is left-linear if t is linear, i.e., no term metavariable occurs more than once in t. R is left-linear if each rule in R is so. R = {r_{i} | i ∈ I} is non-ambiguous or non-overlapping if in no term redex-patterns can overlap, i.e., if r_{i}-redex u contains an r_{j}-redex u′ and i ≠ j, then u′ is in an argument of u, and the same holds if i = j and u′ is a proper subterm of u. R is orthogonal (OCRS) if it is left-linear and non-overlapping, and if v and w are any R-redexes such that w is in an argument of v and v →^{w}v′, then v′ is also a redex weakly similar to v.

Definition 2.6 The CRS S is a CRS comprising rules of the form

S^{n+1}a_{1} …a_{n}A_{1} …A_{n}A → (A_{1}/a_{1}, …, A_{n}/a_{n})A, 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. Each assignment is admissible for any rule in S. We call A_{1}, …, A_{n} the mobile arguments of S^{n+1} and call A immobile. (In the sequel we omit the superscript in S^{n+1}.)

Definition 2.7 Let R = {r_{i} : t_{i} → s_{i} | i ∈ I} be an OCRS. If R is simple, then R_{fS} =_{def} R_{f} =_{def} R, and otherwise R_{fS} =_{def} R_{f} ∪ \underline{S}, where

1. \underline{S} = \{\underline{S}a_{1} …a_{n}A_{1} …A_{n}A → (A_{1}/a_{1}, …, A_{n}/a_{n})A | n = 1, 2, …\}. All assignments are admissible for \underline{S}-rules. (We assume that symbols \underline{S}^{n+1}do not occur in the alphabet of R. The arity and the scope indicator of \underline{S}^{n+1}coincide with that of S^{n+1}).

2. R_{f} = {r′_{i} : t_{i} → s′_{i} | i ∈ I}, where s′_{i} is obtained from s_{i} by replacing all metasubstitutions (t_{1}/a_{1}, …, t_{n}/a_{n})t with \underline{S}^{n+1}a_{1} …a_{n}t_{1} …t_{n}t, respectively.

3. An assignment θ is admissible for an R_{f}-rule r′_{i} iff the assignment θ\underline{S} that to each term metavariable A assigns the \underline{S}-normal form of Aθ and that coincides with θ on object metavariables is admissible for r_{i}.

4. For each step e = C[t_{i}θ] →^{u}C[s_{i}θ] = o in R (corresponding to the rule r_{i} and an admissible assignment θ) 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 expansion of u and denote it by Ex(u). The notion of expansion generalizes naturally to arbitrary R-reductions.

Definition 2.81. Let t →^{u}s in a simple OCRS and e be the contractum of u in s. For each argument t^{∗} of u there are 0 or more arguments of e. We call them (u−)descendants of t^{∗}. Correspondingly, subterms of t^{∗} have 0 or more descendants. The descendant of each patternsubterm of u that is not a variable is e. (We do not define descendants of “variable patternsubterms”, which are binding variables). It is clear what is to be meant under descendants of subterms that are not in u. The notion of descendant extends naturally to arbitrary reductions in simple OCRSs.

2. Let t →^{u}s, where u = Sx_{1} …x_{n}t_{1} …t_{n}t_{0}, and let e be the contractum of u in s. For each mobile argument t_{i} of u (i = 1, …, n) there are substituted occurrences of t_{i} in e. We call them u-descendants of t_{i}. By definition, they also are u-descendants of corresponding free occurrences of the variable x_{i} in t_{0}. Subterms in t_{i} have the same number (possibly none) of descendants in s. The descendant of u is e. It is clear what is to be meant under descendants of subterms that are not in u, or are in t_{0} and are not free occurrences of variables x_{1}, …, x_{n}. The notion of descendant extends naturally to S-reductions with 0 or more steps.

3. Let P : t ↠ s in an OCRS R and let Q = Ex(P). It is clear from (1) and (2) what is to be meant under Q-descendants of subterms in t. We call a subterm o′ ∈ s a P-descendant of a subterm o ∈ t if o′ is a Q-descendant of o, and call o in this case a P-ancestor of o′.

4. Let t →^{u}s. Descendants of all redexes of t except u are also called residuals. By definition, u does not have residuals in s. A redex v ⊆ s is a (u)-new redex or a created redex if it is not a residual of a redex in t. The notion of residual of redexes extends naturally to reductions with 0 or more steps.

3. Properties of S-reductions 6

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

Notation If F is a set of redexes in t and P : t ↠ s, then F/P denotes the set of all residuals of redexes from F in s. If F = {u}, then we write u/P for {u}/P. In the following, F will also denote a complete F-development, where the residuals of redexes from F are contracted as long as possible. Similarly, if u ∈ t, then u will also denote the reduction t →^{u}s.

Definition 2.10 Let Q : t ↠ s and t →^{u}e. Then the residual Q/u of Q by u is defined modulo permutation of non-overlapping steps by induction on |Q| as follows. If Q = ∅_{t}, then Q/u = ∅_{e}. If Q = Q′ + v, then Q/u = Q′/u + v/(u/Q′).

Definition 2.11 Let P : t ↠ s and Q: t ↠ e. Then the residual P/Q of P by Q and the residual Q/P of Q by P are defined modulo permutation of non-overlapping steps by induction on |P| as follows.

(1) If P = ∅_{t}, then P/Q = ∅_{e} and Q/P = Q.

(2) If P = P′ + u, then P/Q = P′/Q + u/(Q/P′) and Q/P = (Q/P′)/u. We write P ⊔ Q for P + Q/P.

Theorem 2.1 (Strict Church-Rosser [10]) Let R be an OCRS, and P and Q be co-initial reductions in R. Then P ⊔ Q ≈_{st} Q ⊔ P.

3. Properties of S-reductions In this section, we study some properties of substitutions. In particular, we prove a strengthened version of the Replacement Lemma [12].

Definition 3.1 Let t be a term in an OCRS. 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.

The notion of essentiality is a generalization of the notion of neededness [7, 17] in a way that it works for all subterms, bound variables in particular. The following two lemmas are valid for all OCRSs; the proofs are similar to the case of orthogonal TRSs [11].

Lemma 3.1 Let s_{0}, …, s_{k} ⊆ t be such that IE(s_{i}, t) for all i = 0, …, k. Then there exists a reduction P starting from t such that none of the subterms s_{0}, …, s_{k} have P-descendants. Proof Let P_{i} be a reduction starting from t such that s_{i} does not have P_{i}-descendants (P_{i} exists since IE(s_{i}, t)). Then, by Theorem 2.1, one can take P = (…(P_{1} ⊔ P_{2}) ⊔ …⊔ P_{n}).

Lemma 3.2 Let P : t ↠ t′ and s ⊆ t. Then IE(s, t) iff any P-descendant s′ of s is inessential in t′. In particular, if t′ is a normal form, then ES(s, t) iff s has a P-descendant. Proof (⇒) Let IE(s, t). Then there is some reduction Q starting from t such that s does not have Q-descendants. By Theorem 2.1, P +Q/P ≈_{st} Q+P/Q. Hence, s′ does not have P/Q-descendants, i.e., IE(s′, t′). (⇐) If all u-descendants of s are inessential in t′, then, by Lemma 3.1, there is some reduction P′ starting from t′ under which none of them have descendants. Thus s does not have P + P′-descendants, i.e., IE(s, t).

Notation Below EFV_{R}(t) denotes the set of variables having R-essential free occurrences in t and FV (s) denotes the set of variables having free occurrences in s. We write t = (t_{1}//e_{1}, …, t_{k}//e_{k})e if t is obtained from e by replacing non-overlapping proper subterms e_{1}, …, e_{n} in e with t_{1}, …, t_{n}, respectively. For any s ⊆ t, BV_{R}(s) denotes the set of free occurrences of s bound by quantifiers belonging to patterns of R-redexes that are outside s.

Definition 3.2 Let u = Sx_{1} …x_{n}t_{1} …t_{n}t_{0} and t′_{0} be an S-normal form of t_{0}. A subterm e in u is called u-inessential (written IE(u; e)) if e is in t_{i} for some (1 ≤ i ≤ n) and x_{i} ∉ FV (t′_{0}).

Lemma 3.3 Let u = Sx_{1} …x_{n}t_{1} …t_{n}t_{0} ⊆ t. Then IE_{S}(u; t_{i}) iff x_{i} ∉ EFV_{S}(t_{0}). Proof By Lemma 3.2, if t′_{0} is the S-normal form of t, then EFV_{S}(t_{0}) = FV (t′_{0}).

Lemma 3.4 Let s ⊆ t. Then IE_{S}(s, t) iff IE_{S}(u; s) for some S-redex u in t. Proof sketch One can take for u the redex whose residual erases all descendants of s in the rightmost innermost normalizing S-reduction.

Lemma 3.5 Let e ⊆ s ⊆ t. Then ES_{S}(e, t) iff ES_{S}(e, s) and ES_{S}(s, t). Proof (⇒) From Definition 3.1. (⇐) By Lemma 3.4, the redex that would make e inessential can neither occur in s nor contain s in its argument.

Lemma 3.6 Let s = (s_{1}//t_{1}, …, s_{n}//t_{n})t, 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.4 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.5, we have IE_{S}(o_{l}, s). Hence, by Lemma 3.4, IE_{S}(s; o_{l}). Thus, by Lemma 3.3, x_{l} ∉ EFV_{S}(o_{0}). Let us show that x_{l} ∉ EFV_{S}(e_{0}). By Lemma 3.4, 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.5, 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 Since t_{j} ≺_{S} s_{j}, x_{l} has a free occurrence in s_{j}. Since s_{j} does not contain S-symbols, it follows from Lemma 3.4 that this occurrence is S-essential in s_{j} and hence, by Lemma 3.5 and ES_{S}(s_{j}, o_{0}), is S-essential in o_{0}. Hence x_{l} ∉ EFV_{S}(e_{0}) and, by Lemma 3.3, IE_{S}(t; e_{l}). Therefore, by Definition 3.2 and Lemma 3.4, IE_{S}(t; t′) and IE_{S}(t′, t).

Remark 3.1 The above lemma is a strengthened version of the Replacement Lemma [12].

Definition 3.3 Let u = C[s_{1}, …, s_{n}] be a redex with context C[ ] and arguments s_{1}, …, s_{n}. Further, let j_{1}, …, j_{k} be the maximal subsequence of 1, …, n such that s_{j_{1}}, …, s_{j_{k}} do not have u-descendants, and i_{1}, …, i_{m} be the maximal subsequence of 1, …, n such that s_{i_{1}}, …, s_{i_{m}} do have u-descendants. We call j_{1}, …, j_{k} the erased sequence of u or the u-erased sequence, call s_{j_{1}}, …, s_{j_{k}} (u-)erased arguments, call i_{1}, …, i_{m} the (u-)main sequence, and s_{i_{1}}, …, s_{i_{m}} (u-)main arguments.

Notation Let C[A_{1}, …, A_{n}] be the left-hand side of a rule r in an OCRS R, where C[ , …, ] is a context and A_{1}, …, A_{n} are term metavariables. Sometimes we write C[\overline{a_{1}} A_{1}, …, \overline{a_{n}}A_{n}] for C[A_{1}, …, A_{n}], where \overline{a_{i}} is the set of metavariables \{a_{i_{1}}, …, a_{i_{n_{i}}}\} such that A_{i} is in the scope of an occurrences of each object metavariable from \overline{a_{i}}. Correspondingly, an r-redex is written C[\overline{x_{1}}t_{1}, …, \overline{x_{n}}t_{n}], where t_{1}, …, t_{n} are arguments and t_{i} is in the scope of each variable from \overline{x_{i}} = {x_{i_{1}}, …, x_{i_{n_{i}}}}. Lemma 3.7 Let u = C[\overline{x_{1}}t_{1}, …, \overline{x_{n}}t_{n}] and v = C[\overline{y_{1}} s_{1}, …, \overline{y_{n}}s_{n}] be weakly similar redexes, let m_{1}, …, m_{l} be the v-main sequence, n_{1}, …, n_{k} be the v-erased sequence, and let for each j = 1, …, l : \overline{x_{m_{j}}} ∩ FV (t_{m_{j}}) ⊆ \overline{y_{m_{j}}} ∩ FV (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 expansions 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}, respectively. By Definition 3.3 all descendants of s_{n_{1}}, …, s_{n_{k}} are \underline{S}-inessential. Therefore it follows from conditions (a)-(b) of Definition 2.2 and the assumptions that 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.6.

4. Perpetual strategies in OCRSs In this section, we design a strategy that for a term t in an OCRS constucts a longest reduction when t is strongly normalizable, and constructs an infinite reduction otherwise. We give also a method to determine the lengths of longest reductions of strongly normalizable terms. Our method is similar to Nederpelt’s method [18], by which proving strong normalization in a typed λ-calculus gets reduced to proving weak normalization. Nederpelt’s method was reinvented and used by Klop [14] for orthogonal CRSs. Some of the results of this section can also be found in Klop [14]; our proofs are simpler. Definition 4.1 The μ-extension (Σ_{μ}, R_{μ}) of an OCRS (Σ, 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) the term t′ is linear (i.e., no term metavariable appears twice or more in t′);

(c) the head symbol of t′ is not a μ-symbol, i.e., it coincides with the head symbol of t;

(d) the μ-erased arguments of each occurrence μ′ of a μ-symbol in t′ are term metavariables, and the μ′-main argument is not a term metavariable (i.e., is headed by a function symbol from Σ or a μ-symbol);

(e) Let A_{1}, …, A_{n} be the enumeration from left to right of all μ-main term metavariables of t′, B_{1}, …, B_{j} be the enumeration from left to right of all μ-erased term metavariables of t′, let A_{i_{1}}, …, A_{i_{l}} be a subsequence of A_{1}, …, A_{n}, 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)

where m = k + j + l + 1.

3. An assignment θ is admissible for r_{μ} iff

(f) the arguments A_{i_{1}}θ, …, A_{i_{l}}θ of the redex t′θ do not have descendants under the reduction step tθ → sθ; and

(g) the assignment θ_{μ} such that Aθ_{μ} = [Aθ]_{μ} and aθ_{μ} = aθ for any term metavariable A and object metavariable a is admissible for r.

4. We call R_{μ} and R μ-corresponding OCRSs, and call r_{μ} and r corresponding rules.

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

Example 4.1 Let R = {r : f(c, x) → d}, where c and d are constants. Then R_{μ}-rules have the form

\begin{matrix}f(μ^{k}(A_{1}, …, A_{k−1}, μ^{l}(B_{1}, …, B_{l−1}, …μ^{m}(C_{1}, …, C_{m−1}, c) …)), x) → \\ μ(μ^{0}, …, μ^{0}, A_{1}, …, A_{k−1}, B_{1} …, B_{l−1}, …, C_{1} …, C_{m−1}, A, d) \end{matrix}

For example, r_{μ} : f(μ^{2}(B, μ^{2}(C, c), A) → μ^{6}(μ^{0}, μ^{0}, B, C, A, d) is an R_{μ}-rule. For any r_{μ}-redex t = f(μ^{2}(o, μ^{2}(s, c)), e), [t]_{μ} = f(c, e) is an r-redex, t′ = μ(μ^{0}, μ^{0}, o, s, e, d) is the contractum of t, and [t′]_{μ} = d is the contractum of f(c, e).

Example 4.2 Consider the β-rule of the λ-calculus

β : Ap(λaA, B) → (B/a)A

On the picture below, two β_{μ}-rules with the same left-hand side and different right-hand sides are shown.

[figure: Ap; μ^{3}; μ^{1}; A; B; μ^{2}; C; λa; D; μ^{0}; μ^{0}; μ^{0}; μ^{0}; A; B; C; (E/a)D; μ^{0}; μ^{0}; μ^{0}; μ^{0}; A; B; C; E; μ^{8}; μ^{9}; (E/a)D; E]

The arguments A and B are μ-erased and E and D are μ-main. An assignment θ is admissible for the first rule iff aθ ∈ FV (Dθ) and is admissible for the second one iff aθ ∉ FV (Dθ).

Lemma 4.1 Let R be an OCRS, t be a term in R_{μ}, let [t]_{μ}= t′, let u be a μ-main S-redex in t, u′ be its μ-corresponding S-redex in t′, let t→^{u}s, and t′→^{u′}s′. Then [s]_{μ}= s′. Proof Let e ⊆ s be the contractum of u and e′ ⊆ s′ be the contractum of u′. It is enough to show that [e]_{μ}= e′. Let u = Sx_{1} …x_{n}t_{1} …t_{n}t_{0}. Then e = μt_{i_{1}} …t_{i_{k}}t′_{0}, where t′_{0} = (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}

4. Perpetual strategies in OCRSs 10

and t_{i_{1}}, …, t_{i_{k}} are erased arguments of u. Thus [e]_{μ}= [t′_{0}]_{μ}, u′ = [u]_{μ}= Sx_{1} …x_{n}[t_{1}]_{μ}…[t_{n}]_{μ}[t_{0}]_{μ}, and e′ = ([t_{1}]_{μ}/x_{1}, …, [t_{n}]_{μ}/x_{n})[t_{0}]_{μ}. An occurrence o in [e]_{μ} = [t′_{0}]_{μ} is μ-erased iff it is in a substituted occurrence t′_{i} of t_{i} and is μ-erased in t′_{i}, or o is outside of substituted occurrences of t_{1}, …, t_{n} in t′_{0} and there is a μ-occurrence μ′ outside of these substituted occurrences such that o is μ′-erased. In the first case the ancestor of o is μ-erased in t_{i} and in the second case the ancestor of o is μ-erased in t_{0}. Thus [e]_{μ}= [t′_{0}]_{μ} = ([t_{1}]_{μ}/x_{1}, …, [t_{n}]_{μ}/x_{n})[t_{0}]_{μ} = e′.

Lemma 4.2 Let t be a term over Σ_{μ} the head-symbol of which is not a μ-symbol, and let [t]_{μ} = s. Then t is an r_{μ}-redex iff s is an r-redex, where r_{μ} and r are corresponding rules in R_{μ} and R, respectively. Moreover, if t′ is the contractum of t in R_{μ} and s′ is the contractum of s in R, then [t′]_{μ} = s′. Proof From Definition 4.1 and Lemma 4.1.

Corollary 4.1 Let R be an OCRS and s_{0} →^{u_{0}}s_{1} →^{u_{1}}…be a reduction in R. Then, for any term t_{0} in R_{μ} such that [t_{0}]_{μ} = s_{0}, there is a reduction 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, …).

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

Proposition 4.1 (1) Let R be an OCRS, 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 quasi-main sequences of v and w coincide.

(2) Let u be a redex in an OCRS 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 OCRS 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.7.

Lemma 4.3 If R is an orthogonal CRS, then so is R_{μ}. Proof Any overlap of patterns of two R_{μ}-redexes in a term t over Σ_{μ} causes also an overlap of patterns of corresponding R-redexes in [t]_{μ}. Hence, since R is non-overlapping, so is R_{μ}. If u and v are R_{μ}-redexes such that v is in an argument of u and u→^{v}w, then, by Proposition 4.1.(1), w is weakly similar to u. Therefore, R_{μ} is orthogonal (because it is left-linear).

Lemma 4.4 Let R be an OCRS. Then R_{μ} is Church-Rosser. Proof From Lemma 4.3 and Theorem 2.1.

Lemma 4.5 Let t be a term in an OCRS R. If t is weakly normalizable in R_{μ}, then t is strongly normalizable in R_{μ} and R. Proof Let s be an R_{μ}-nf of t and t → t_{1} → …be an R_{μ}-reduction. By Lemma 4.4, t_{i} ↠ s for all i = 1, 2, . . .. It is easy to see that i ≤ ∥t_{i}∥_{μ}≤ ∥s∥_{μ}. Thus t is strongly normalizable in R_{μ}. Hence, by Corollary 4.1, t is strongly normalizable in R.

Definition 4.2 A rule r : t → s in an OCRS R is called non-erasing if each term-metavariable occurring in t has an occurrence in s that is not in a mobile subterm of a metasubstitution. R is non-erasing if each R-rule is so.

It is easy to check that R is non-erasing iff, for any R-reduction step e→^{u}o, each argument of u has a descendant in o, and the latter holds iff FV (e) = FV (o).

Lemma 4.6 Let R be a non-erasing OCRS, P : t_{0} → t_{1} → … → t_{n} be a reduction in R, and Q: s_{0} = t_{0} → s_{1} → …→ s_{n} be its μ-corresponding reduction in R_{μ}. Then

(1) All redexes in s_{i} are μ-main (i = 1, …, n).

(2) If P is normalizing, then so is Q. Proof (1) Since R is non-erasing, μ-symbols in s_{i} are occurrences of μ^{1}. Thus no subterms of s_{i}, and hence no redexes, are μ-erased.

(2) From (1) and [s_{n}]_{μ}= t_{n}.

Theorem 4.1 (Extension of Church’s theorem, Klop [14]) Let R be a non-erasing OCRS and t be a weakly normalizable term in R. Then t is strongly normalizable. Proof From Lemma 4.6 and Lemma 4.5.

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

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

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

Similarly to the case of OTRSs [11], it can be shown that in any term not in normal form there is an unabsorbed redex, hence a limit redex as well.

Lemma 4.7 Let u be a limit redex in t and 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 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.8 Let (Σ, R) be an OCRS, 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}}t_{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-nf. 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 (α), (β),(b)_{k}, and Lemma 4.2 that (δ): e_{i_{1}}, …, e_{i_{l}} are in R_{μ}-nf.

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 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.7, 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 Lemma 4.2 and (b)_{n}.

Theorem 4.2 A limit strategy is perpetual in OCRSs. Moreover, if a term t in an OCRS 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_{μ}-nf of t. Proof If a limit R-reduction P starting from t is normalizing, then by Lemma 4.8 its corresponding R_{μ}-reduction also is normalizing. Hence, by Lemma 4.5, 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| =(by Corollary 4.1)= |Q_{μ}| ≤ (by the CR property of R_{μ})≤ ∥s∥_{μ}=(by Lemma 4.8)= |P|. Thus, P has the maximal length among all reductions of t to normal form.

Proposition 4.2 (Klop [14]) A term t in an OCRS R is strongly normalizable iff t is weakly normalizable in R_{μ}. Proof (⇒) From Lemma 4.8. (⇐) From Lemma 4.5.

The following example shows that, despite the claim of Klop [14] (p. 181, Remark 6.2.5), if R is strongly normalizing, then R_{μ} does not need to be strongly normalizing.

Example 4.3 Let R = {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). During r-step creation inside contractum is only possible when, 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), i.e., A = c, or A = C[f(τyx)] with y ≠ x and τa(A, A) = c, but this of course never happens. During r-step creation of a redex is not possible also outside contractum, because in this case the outermost g of the contractum should belong to the pattern of a new redex, but this is impossible 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 [14, 12].)

Similarly to the case of OTRSs [12], one can define subclasses of OCRSs for which the unabsorbed redexes can be found efficiently; hence the limit strategy is efficient.

Definition 4.5 (1) We call an OCRS non-absorbing if, for any reduction step t →^{u}s, arguments of any new redex in s are in the contractum of u.

(2) We call an OCRS non-left-absorbing (resp. non-right-absorbing) if, for any reduction step t →^{u}s, any argument of a created redex in s is inside the contractum of u or to the right (resp. to the left) of it.

Proposition 4.3 (1) Let t be a term in a non-absorbing OCRS. Then any outermost redex in t is unabsorbed.

(2) Let t be a term in a non-left absorbing (resp. non-right-absorbing) OCRS. Then the leftmostoutermost (resp. the rightmost outermost) redex in t is unabsorbed. Proof From Definitions 4.3 and Definition 4.5.

Remark 4.1 It is easy to see that the leftmost redexes in λ-terms are unabsorbed. Therefore the perpetual strategy of Barendregt et al. [3] is a limit strategy. The proof presented in Barendregt [2] uses only unabsorbness of the leftmost redexes and therefore generalizes easily to the case of OCRSs. The proof of the Conservation Theorem [2] also remain valid for OCRSs: if a term t has an infinite reduction and t→^{u}s, where u is a non-erasing redex, then s has also an infinite reduction. Bergstra and Klop [4] gave a characterization of erased redexes (i.e. K-redexes) for which the Conservation Theorem in λ-calculus still is valid. Another extension of the Conservation Theorem that can be used for strong normalization proofs of several typed λ-calculi can be found in de Groote [6]. We leave this questions for OCRSs to a future investigation.

The direct proof of the fact that the perpetual reductions are the longest in OTRSs, presented in [12], cannot be generalized to the case of OCRSs (complete redexes does not necessarily remain complete because main arguments may become erased after some steps in the main arguments).

5. Longest reductions in strongly persistent OCRSs In this section, we design an algorithm for finding the lengths of longest reductions in strongly persistent CRSs; as a corollary we obtain an algorithm for finding exact upper bounds of lengths of developments in orthogonal CRSs. To this end, we introduce and study strong similarity of redexes.

Without restricting the class of OCRSs, we can assume that in right-hand sides of rewrite rules the immobile argument of each metasubstitution is a term-metavariable or a metasubstitution. For example, we can replace the metasubstitution f((B/a)g(A)) by the ”equivalent” metasubstitution f(g((B/a)A)), and the metasubstitution (A_{1}/a_{1}, A_{2}/a_{2})σaA_{0}, where σ is a quantifier sign of arity (1, 1) and a ≠ a_{1}, a_{2}, by σa((A_{1}/a_{1}, A_{2}/a_{2})A_{0}). (If a = a_{1} or a = a_{0}, then we first rename the bound object metavariables). Hence, we can have the following definition.

Definition 5.1 (1) Let t→^{u}s in an OCRS R, let t → t′ ↠ s be its expansion, 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 OCRS R persistent (written PCRS) if, for any R-reduction step, each created redex is generated.

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

(4) We call an OCRS R left-canonical if, for any R-rule t → s, the pattern of t consists of one operator, i.e., t has the form σa_{1} …a_{m}A_{1} …A_{n}, where σ is an operator sign of arity (m, n) (σ is a function iff m, n = 0).

(5) We call an OCRS R non-creating if no redex-creation is possible during reduction steps in R.

Remark 5.1 In [13], we call left-canonical CRSs Higher Order Recursive Program Schemes. It is easy to see that a non-simple OCRS R is strongly persistent iff it is left canonical [13].

Lemma 5.1 If R is a strongly persistent OCRS, then so is R_{μ}. Proof If R is simple, then the lemma is obvious. Otherwise, by the above remark, R is left canonical and so is R_{μ}; thus R_{μ} is strongly persistent.

Remark 5.2 Example 4.3 shows that if R is persistent, then R_{μ} does not need to be persistent (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 PCRS R such that R_{μ} also is persistent does not need to be strongly persistent. For example, let R = {r_{1} : ∃aA → f((τaA/a)A), r_{2} : g(f(x)) → c}. Since {r_{1}} is left-canonical, {r_{1μ}} also is left-canonical, hence persistent. Since {r_{2}} is simple and is persistent, {r_{2μ}} is also persistent. Hence, because of “independence” of r_{1} and r_{2}, R_{μ} is persistent. But R is not strongly persistent, since it is nonsimple and is not left-canonical.

Definition 5.2 Let C[\overline{a_{1}} A_{1}, …, \overline{a_{n}}A_{n}] be the left-hand side of a rewrite rule r in an OCRS R and let C[\overline{x_{1}}t_{1}, …, \overline{x_{n}}t_{n}] be an r-redex.

(1) The characteristic system of u (written CS(u)) is the set of pairs (a_{i_{j}} , A_{i}) such that x_{i_{j}} ∈ FV (t_{i}) (i = 1, …, n, j = 1, …, n_{i}). In this case, u is an (r, CS(u))-redex. A characterized rule (C-rule for short) is a pair (r, CS(r)), where CS(r) is a characteristic system for some R-redex. The main characteristic system MCS(u) of u is the subset of CS(u) containing a pair (a_{i_{j}}, A_{i}) iff i-th argument of u is main.

(2) The strong characteristic system of u (written SCS(u)) is the set of triples of the form (a_{i_{j}}, A_{i}, n_{i_{j}}) such that (a_{i_{j}} , A_{i}, n_{i_{j}}) ∈ SCS(u) iff x_{i_{j}} has n_{i_{j}} free occurrences in t_{i}. In this case, u is an (r, SCS(u))-redex. A strongly characterized rule (SC-rule for short) is a pair (r, SCS(r)), where SCS(r) is a strong characteristic system for some R-redex. The main strong characteristic system MSCS(u) of u is the subset of SCS(u) containing a triple (a_{i_{j}}, A_{i}, n_{i_{j}}) iff i-th argument of u is main.

(3) We call weakly similar redexes u and v respectively similar, m-similar, strongly similar, or strongly m-similar if CS(u) = CS(v), MCS(u) = MCS(v), SCS(u) = SCS(v), or MSCS(u) = MSCS(v).

Proposition 5.1 Let u and v be m-similar redexes in an OCRS R. Then an argument of u is main iff its corresponding argument in v is main. Proof The proposition is a corollary of Lemma 3.7.

Definition 5.3 Let u = C[\overline{x_{1}}t_{1}, …, \overline{x_{n}}t_{n}] and v = C[\overline{y_{1}} s_{1}, …, \overline{y_{n}}s_{n}] with \overline{x_{i}} = \{x_{i_{1}}, …, x_{i_{n_{i}}}\} and \overline{y_{i}} = \{y_{i_{1}}, …, y_{i_{n_{i}}}\} be weakly similar redexes. We call u and v strongly \underline{S}-essentially similar (resp. strongly \underline{S}-essentially m-similar if x_{i_{j}} and y_{i_{j}} have the same number of \underline{S}-essential occurrences in t_{i} and s_{i} for all i = 1, …, n; j = 1, …, n_{i} (resp. for all i = 1, …, n; j = 1, …, n_{i} such that t_{i} and s_{i} are main arguments of u and v, respectively). (Note that if the arguments of u and v do not contain \underline{S}-redexes, then strong \underline{S}-essential (m-)similarity and strong (m-)similarity of u and v coincide.)

Lemma 5.2 Let R be a SPCRS, let u = C[\overline{x_{1}}t_{1}, …, \overline{x_{n}}t_{n}] and v = C[\overline{x_{1}}s_{1}, …, \overline{x_{n}}s_{n}] be strongly m-similar R_{μ}-redexes whose arguments are in nf 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 expansions 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 \overline{x_{j}} in t_{j} and s_{j} (j = 1, …, n), called context variables, where notion of descendant* is defined similarly to that of descendant with the exception that, during \underline{S}-steps \underline{S}x_{1} …x_{n}t_{1} …t_{n}t_{0} → (t_{1}/x_{1}, …, t_{n}/x_{n})t_{0}, free occurrences of x_{1}, …, x_{n} in t_{0} 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 m-similar (in fact, strongly \underline{S}-essentially similar if m > 1), 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. Suppose that we have defined the corresponding \underline{S}-essential occurrences in o_{m} and e_{m} in such a way that (a)_{m} and (b)_{m} hold. 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 \underline{S}-essential corresponding occurrences of o_{m} and v_{m} form pairs of corresponding 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 Corollary 3.5 and Definition 3.1 that descendants of \underline{S}-essential occurrences of o_{m} and v_{m} are \underline{S}-essential in o_{m+1} and e_{m+1} iff they are substituted for \underline{S}-essential context-variables. 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, by Lemma 5.1, R_{μ} is persistent, no new redexes are created in 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, by Lemma 5.1, 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. Apart from these occurrences, descendants of only occurrences that are in main arguments of u_{m} and v_{m} can be \underline{S}-essential in o_{m+1} and e_{m+1}. By (a)_{m}, u_{m} and v_{m} are strongly m-similar. Hence, it follows from conditions (a)-(b) of Definition 2.2 and Lemma 3.6 that corresponding new redexes in o_{m+1} and e_{m+1} are either both essential or both are inessential, the same holds for corresponding arguments of the corresponding redexes, and 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.5 that w and w′ are strongly \underline{S}-essentially similar. Hence (a)_{m+1} follows from (a)_{m}. (b)_{m+1} follows easily from (b)_{m}. Definition 5.4 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, by definition, Mult_{μ}(s, t) is the number of P-descendants of s in e.

(2) Let u = C[e_{1}, …, e_{n}] be an r-redex in R_{μ}, let s′ be a non-variable subterm in e_{i}, let v = C[o_{1}, …, o_{n}] be an r-redex strongly m-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_{μ}- reductions. Then, by definition, mult_{μ}(u, i) = mult_{μ}(u, s′) = mult_{μ}(r, SCS(u), i) = Mult_{μ}(o_{i}, v), and mult_{μ}(u) = mult_{μ}(r, SCS(u)) is a number of μ-subterms in o that appear during Q, i.e., that are not descendants of μ-subterms from (the pattern and arguments of) v. Numbers mult_{μ}(u, i) and mult_{μ}(r, SCS(r), i) are called proper μ-indices of u and (r, SCS(u)), and numbers mult_{μ}(u) and mult_{μ}(r, SCS(u)) are called μ-indices of u and (r, SCS(u)).

The correctness of the above definition follows from Lemma 5.2.

Lemma 5.3 Let t be a strongly normalizable term in a PCRS R_{μ}, e ⊆ s ⊆ t and e and s be non-variable R_{μ}-nfs. Then Mult_{μ}(s, t) = Mult_{μ}(e, t). Proof Let t = t_{0} → t_{1} → …→ t_{n} be the expansion of the rightmost normalizing R_{μ}-reduction. Let us define pairs (s_{i}^{j}, e_{i}^{j}) of descendants of s and e in t_{i} (if any) for each i = 1, …in such a way that (α)_{i}: there is no redex in t_{i} that contains e_{i}^{j} and does not contain s_{i}^{j}. Obviously, the pair (s, e) satisfies (α)_{0}. Suppose that pairs of descendants of s and e are defined in t_{m} in such a way that (α)_{m} holds and let t_{m}→^{u_{m}}t_{m+1}. If u_{m} is not an S-redex or an \underline{S}-redex, then it ie clear that for any pair (s_{m}^{k}, e_{m}^{k}) of corresponding descendants of s and e in t_{m}, s_{m}^{k} and e_{m}^{k} have the same number of descendants, and these descendants form the pairs of corresponding occurrences in t_{m+1}. Since R_{μ} is persistent, new redexes in t_{m+1} (if any) are not inside the descendants of s_{m}^{k} in t_{m+1}. Hence (α)_{m+1} follows immediately from (α)_{m} in this case. Suppose now that u_{m} = Sx_{1} …x_{l}s_{1} …s_{l}s_{0} is an Sredex or an \underline{S}-redex. By (α)_{m}, there is no pair (s_{m}^{k}, e_{m}^{k}) in t_{m} such that e_{m}^{k} ⊆ u_{m} ⊆ s_{m}^{k}. Thus either both s_{m}^{k} and e_{m}^{k} are in the same argument of u_{m} or non of them is in u_{m}. Hence s_{m}^{k} and e_{m}^{k} have the same number of descendants and they form pairs of corresponding occurrences in t_{m+1}. Since R_{μ} is persistent, there are no new redexes in t_{m+1}. Thus (α)_{m+1} follows immediately from (α)_{m}. Now it is clear that s and e have the same number of descendants in t_{n}, i.e., Mult_{μ}(s, t) = Mult_{μ}(e, t).

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

Lemma 5.4 Let t be a strongly normalizable term in an SPCRS R and u_{1}, …, u_{n} be all redexes in t. Then

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

Proof Let P : t ↠ o be the rightmost innermost normalizing R_{μ}-reduction and let u_{1}, …, u_{n} be the enumeration of redexes in t from right to left. In the fragment of P in which (the residual of) u_{i} is reduced to R_{μ}-nf, mult_{μ}(u_{i}) new μ-symbols appear (in the beginning of the fragment, all arguments of u_{i} are already in R_{μ}-nf). By Lemma 5.3, during the rest of P each of these μ-occurrences is copied Mult_{μ}(u_{i}, t)-times. Hence

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

and the lemma follows from Theorem 4.2.

Lemma 5.5 Let t be a strongly normalizable term in an PCRS 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})

Proof Let P : t ↠ o be the rightmost innermost normalizing R_{μ}-reduction. It follows from Lemma 5.3 that, in the fragment of P in which (the residual of) u_{i} is reduced to R_{μ}-nf, each descendant of s is copied mult_{μ}(u_{i}, s) = mult_{μ}(u_{i}, m_{i})-times. Thus the lemma follows from persistency of R_{μ}.

Lemma 5.6 Let u = C[e_{1}, …, e_{k}] be an r-redex whose arguments e_{1}, …, e_{k} are not variables and are in normal form, in an SPCRS R. Then, for all i = 1, …, k,

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

mult_{μ}(u) = mult_{μ}(r, SCS(r)) = ∑_{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. Proof From Definition 5.4 and Theorem 4.2.

Lemma 5.7 Let u and v be strongly m-similar redexes in an SPCRS R, let u→^{u}o and v→^{v}e. Then u and v create the same number of strongly similar redexes. Proof If in the Lemma 5.2 one takes for P the expansion of u and for Q the expansion of v, then it follows from Lemma 5.2 that for each u-new redex in o there is exactly one strongly similar v-new redex in e.

Corollary 5.1 Let u and v be strongly m-similar redexes in an OCRS R, let u→^{u}o and v→^{v}e. Then u and v generate the same number of strongly similar redexes.

Definition 5.5 We call a sequence of SC-rules (r_{0}, SCS(r_{0})), (r_{1}, SCS(r_{1})), …an (r_{0}, SCS(r_{0}))- chain if an (r_{i+1}, SCS(r_{i+1}))-redex is generated by contraction of any (r_{i}, SCS(r_{i}))-redex. For any (r_{0}, SCS(r_{0}))-redex u, we also call an (r_{0}, SCS(r_{0}))-chain an u-chain.

The correctness of the above definition follows from Lemma 5.7. In [13], we used C-rules instead of SC-rules to define chains of redexes, but it is easy to see that for each chain of C-rules there is a chain of SC-rules with the same length, and vice versa. Therefore, the following theorem from [13] remains valid for the above definition of chains of redexes.

Theorem 5.1 ([13]) A term t in a PCRS R is strongly normalizable iff all chains of redexes in t are finite.

Theorem 5.2 Let t be a term in an SPCRS 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 (r_{1}, SCS(r_{1})), …, (r_{n}, SCS(r_{n})) be all strongly characterized rules such that an (r_{i}, SCS(r_{i}))-redex has an occurrence in t (i = 1, …, n). If an (r_{i}, SCS(r_{i}))-chain is infinite for at least one i, then L(t) = ∞. Otherwise, using Lemmas 5.6 and 5.5, find the μ-indices and the proper μ-indices of all rules (r_{i}, SCS(r_{i})). Finally, using Lemmas 5.5 and 5.4, find L(t).

Proof From Theorems 5.1 and 4.2, and Lemmas 5.4-5.7.

Remark 5.3 It is easy to see that the above results remain valid if we use “main” μ-indices and “main” proper μ-indices MSCS( ) instead of μ-indices and proper μ-indices SCS( ).

5.1The least upper bound of lengths of developments Let R = \{r_{i} : t_{i} → s_{i} | i ∈ I\} be an OCRS and let \underline{R}= \{\underline{r}_{i} : \underline{t}_{i} → s_{i} | i ∈ I\}, where \underline{t}_{i} is obtained from t_{i} by underlining its head-symbol. Terms in \underline{R} are constructed in the usual way with the restriction that underlined symbols may only occur as head-symbols of redexes. Then, for each development P : e_{0} → e_{1} → …→ e_{n} of e_{0} in R (in which only residuals of redexes from e_{0} are contracted), there is a reduction P′ : e′_{0} → e′_{1} → …→ e′_{n} in \underline{R}such that e′_{i} is obtained from e_{i} by underlining head-symbols of residuals of redexes from e_{0}. Obviously, \underline{R}is persistent, since no creation of redexes is possible in it. Thus, to find least upper bounds of developments in R, one can use Algorithm 5.1, which becomes simpler in this case: for any strongly characterized rule (\underline{r}, SCS(\underline{r})), mult_{μ}(\underline{r}, SCS(\underline{r})) = 1, mult_{μ}(\underline{r}, SCS(\underline{r}), i) = 1 if the i-th argument o_{i} of an (R, SCS(r))-redex does not have a descendant, and mult_{μ}(\underline{r}, SCS(\underline{r}), i) coincides with the number of descendants of o_{i} otherwise.

Acknowledgments I enjoyed discussions with H. Barendregt, J. W. Klop, J.-J. Lévy, L. Maranget, G. Mints, V. van Oostrom, Sh. Pkhakadze, 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 preparation of this paper. References

1. Aczel P. A general Church-Rosser theorem. Preprint, University of Manchester, 1978.

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

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

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

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

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

7. Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In: Computational Logic, Essays in Honor of Alan Robinson, ed. by J.-L. Lassez and G. Plotkin, MIT Press, 1991.

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

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

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

11.Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of the fifth International Conference on Rewriting Techniques and Applications, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.

12.Khasidashvili Z. Perpetual reductions and strong normalization in orthogonal term rewriting

systems. CWI report, July 1993. 13.Khasidashvili Z. Higher order recursive program schemes are Turing incomplete. CWI report,

July 1993. 14.Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Ams-

terdam, 1980. 15.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. 16.Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction Systems: introduction

and survey. In: To Corrado Böhm. To appear in J. of Theoretical Computer Science, 1993. Available as a Free University report IR-327, Amsterdam, June 1993.

17.Maranget L. “La stratégie paresseuse”, Thèse de l’Université de Paris VII, 1992. 18.Nederpelt R. P. Strong Normalization for a typed lambda-calculus with lambda structured

types. Ph.D. Thesis, Eindhoven, 1973. 19.Nipkow T. Higher order critical pairs. In: proc. of sixth annual IEEE symposium on Logic in

Computer Science, Amsterdam, 1991, p. 342-349. 20.O’Donnell M. J. Computing in systems described by equations. Springer LNCS 58, 1977. 21.Van Oostrom V., van Raamsdonk F. Comparing Combinatory Reduction Systems and Higher-

order Rewrite Systems. To appear as a CWI report, 1993. 22.Pkhakadze Sh. Some problems in the Notation Theory (in Russian). Proceedings of I. Vekua

Institute of Applied Mathematics of Tbilisi State University, Tbilisi 1977.