Perpetual Reductions and Strong Normalization in Orthogonal Term Rewriting 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 Term Rewriting System (OTRS) constructs a longest reduction starting from t if t is strongly normalizable, and constructs an infinite reduction otherwise. We define some classes of OTRSs for which the strategy is easily computable. We develop a method for finding the least upper bound of lengths of reductions starting from a strongly normalizable term. We give also some applications of our results.

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

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

1. Introduction It is shown in O’Donnell [9] that the innermost strategy is perpetual for orthogonal term rewriting systems (OTRSs). That is, contraction of innermost redexes gives an infinite reduction of a given term whenever such a reduction exists. In fact, a strategy that only chooses redexes that do not erase any other redex is perpetual. Moreover, one can even reduce redexes whose erased arguments are strongly normalizable (Klop [7]). For the lambda-calculus, a more subtle perpetual strategy was invented in Barendregt et al. [1]. However, none of these strategies work for all Orthogonal Combinatory Reduction Systems (OCRSs), i.e., OTRSs with bound variables and a substitution mechanism [6].

We design a perpetual strategy for orthogonal term rewriting systems that works also for all orthogonal combinatory reduction systems. Perpetual reductions are interesting because termination of a perpetual reduction starting from a term t implies strong normalization of t (i.e., termination of all reductions starting from t). Our aim is not only to construct an infinite reduction of any given term t whenever it exist, but also to construct a longest reduction if all reductions starting from t are finite. Thus we will be able to characterize the complexity of computations of terms. The idea is that in order to construct a perpetual reduction one should try to avoid erasure of (infinite) redexes. On the other hand, in order to construct a longest possible reduction, one should delay contraction of a redex until it will no longer be possible to duplicate 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 arguments of other redexes; 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 normal form, but there is no general algorithm to find one. So we define some classes of OTRSs, such as persistent, inside-creating, 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.) Unabsorbed redexes can easily be found also in the wide class of strongly sequential OTRSs [3].

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 [8] invented to reduce proofs of strong normalization to proofs of weak normalization (i.e., existence of a normal form). For any OTRS R, we define the corresponding non-erasing OTRS 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 variables 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, 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 the least upper bound of lengths of R-reductions starting from a term 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 t. We show this for the case of persistent TRSs.

Another consequence is that a term t is strongly normalizable in R iff it is weakly normalizable in R_{μ}; this result holds also on the level of OTRSs: an OTRS R is strongly normalizing iff its μ-extension R_{μ} is weakly normalizing [6]. Therefore, for any class of OTRSs that is closed under μ-extension, i.e., contains the μ-extension of each of its elements, one can prove undecidability of weak normalization if undecidability of strong normalization is known, and prove decidability of strong normalization if decidability of weak normalization is known. For example, all the above classes of OTRSs are closed under μ-extension. We describe some applications of our results in section 3. The main results are obtained in section 2.

2. Perpetual strategies in OTRSs We recall some basic notions of TRS theory; one can find comprehensive introductions to the subject in [2] and [7]. A TRS is a pair (Σ, R), where the alphabet Σ consists of variables and function symbols and R is a set of rewrite rules r of the form t → s. The left-hand side t is any term different from a variable, and the term s may only contain variables that occur in t. An r-redex u is obtained from t by substituting arbitrary terms for the variables in t, and the corresponding instance of s is the contractum of u. Arguments of u are subterms of u that correspond to variables of t, and the rest is the pattern of u. Subterms of u rooted at the pattern are called the pattern-subterms of u. The arguments, pattern, and pattern-subterms are defined analogously in the contractum of u. A TRS is orthogonal if it is left-linear and non-ambiguous, i.e., patterns of redexes can never overlap in a term.

A one step reduction in which a redex u in a term o is contracted is written o →^{u}e or o → e. We write P : o ↠ e if P is a reduction of o to e comprising 0 or more steps. A term t is called weakly (resp. strongly) normalizable if t has a normal form (resp. if any reduction starting from t is terminating). An OTRS R is weakly (resp. strongly) normalizing if any term in R is weakly (resp. strongly) normalizable. We use t, s, e, o for terms, u, v, w for redexes, and P, Q for reductions. |P| denotes the length of P. We write s ⊆ t if s is a subterm of t.

For a given OTRS R we now define its “μ-extension” R_{μ}: for each R-rule t → s, we have a set of R_{μ}-rules of the form t′ → μ^{l}(μ^{0}, …, μ^{0}, x_{i_{1}}, …, x_{i_{k}}, s), where μ^{n} is a fresh n-ary function symbol; t is obtained from t′ by removing all except the last arguments of μ-symbols occurring in t′ (we write t = [t′]_{μ}); and x_{i_{1}}, …, x_{i_{k}} are all variables of t that do not occur in s. If a term e has a normal form in R_{μ}, then all R_{μ}-reductions of e are finite, since their lengths can not exceed the number ∥o∥_{μ}of μ-occurrences in R_{μ}-normal form o of e. (Indeed, for any R_{μ}-reduction P : e ↠ e′, we have e′ ↠ o; hence |P| ≤ ∥e′∥_{μ}≤ ∥o∥_{μ}.) For any R-reduction Q : t_{1} → t_{2} → …→ t_{n} we construct a corresponding R_{μ}-reduction Q_{μ} : s_{1} = t_{1} → s_{2} → …→ s_{n} such that [s_{i}]_{μ} = t_{i}. So in order to prove that a term t in R is strongly normalizable it is enough to prove that t has a normal form in R_{μ}. This is the idea of Nederpelt’s method. Now if s_{n} is an R_{μ}-normal form of s_{1}, then ∥s_{n}∥_{μ} is an upper bound of lengths of R-reductions starting from t_{1}. Thus the length of Q is maximal if s_{n} is the R_{μ}-normal form of s_{1} whenever t_{n} is the normal form of t_{1}, and |Q_{μ}| = ∥s_{n}∥_{μ}, i.e., each step of Q_{μ} increases the number of μ-occurrences exactly by 1. This is achieved by contracting the limit redexes only. Indeed, in this case the old μ-occurrences do not duplicate, and the only new μ-symbol created in each step is the head symbol of the contractum.

Definition 2.1 The μ-extension (Σ_{μ}, R_{μ}) of an OTRS (Σ, 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 variable 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 variables, and the μ′-main argument is not a variable (i.e., it contains a function symbol from Σ or a μ-symbol);

(e) if x_{1}, …, x_{n} are all μ-main variables of t′ (from left to right), y_{1}, …, y_{m} are all μ-erased variables of t′, and x_{i_{1}}, …, x_{i_{p}} are all variables among x_{1}, …, x_{n} that do not occur in s, then

s′ = μ^{l}(\overbrace{μ^{0}, …, μ^{0}}^{k}, y_{1}, …, y_{m}, x_{i_{1}}, …, x_{i_{p}}, s),

where k is the number of occurrences of μ-symbols in t′ and l = k + m + p + 1. For any r_{μ}-redex u = t′θ, we call arguments that correspond to x_{i_{1}}, …, x_{i_{l}} quasi-erased arguments of u, and call the arguments that correspond to other variables from x_{1}, …, x_{n} quasi-main. R_{μ} and R are called μ-corresponding OTRSs, and r_{μ} and r are called corresponding rules in R_{μ} and R.

Example 2.1 Let R = {r: f(a, x) → b}. Then R_{μ}-rules have the form

\begin{matrix}f(μ^{k}(x_{1}, …, x_{k−1}, μ^{l}(y_{1}, …, y_{l−1}, …μ^{m}(z_{1}, …, z_{m−1}, a) …)), x) → \\ μ(μ^{0}, …, μ^{0}, x_{1}, …, x_{k−1}, y_{1} …, y_{l−1}, …, z_{1} …, z_{m−1}, x, b) \end{matrix}

For example, r_{μ} : f(μ^{2}(y, μ^{2}(z, a), x) → μ^{6}(μ^{0}, μ^{0}, y, z, x, b)) is an R_{μ}-rule. For any r_{μ}-redex t = f(μ^{2}(o, μ^{2}(s, a)), e), [t]_{μ} = f(a, e) is an r-redex, t′ = μ(μ^{0}, μ^{0}, o, s, e, b) is the contractum of t, and [t′]_{μ} = b is the contractum of f(a, e).

Lemma 2.1 If R is an orthogonal TRS, then so is R_{μ}. Proof Any overlap of patterns of two R_{μ}-redexes in a term t over Σ_{μ} causes an overlap of patterns of corresponding R-redexes in [t]_{μ}.

Lemma 2.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 2.1 (see also Example 2.1).

Corollary 2.1 Let R be an OTRS 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.

Lemma 2.3 Let t be a term in an OTRS R. If t is weakly normalizable in R_{μ}, then t is strongly normalizable in R_{μ} and R. Proof Let s be an R_{μ}-normal form of t and t → t_{1} → …be an R_{μ}-reduction. By Lemma 2.1 and the Church-Rosser theorem, t_{i} ↠ s for all i = 1, 2, …It is easy to see that i ≤ ∥t_{i}∥_{μ}≤ ∥s∥_{μ}. So t is strongly normalizable in R_{μ}. Hence, by Corollary 2.1, t is strongly normalizable in R.

Definition 2.2 Let t →^{u}s and let e be the contractum of u in s. For each argument o of u there are 0 or more arguments of e. We call them (u-)descendants of o. Correspondingly, subterms of o have 0 or more descendants. An argument of u is called (u)-erased if it does not have a descendant, and is called (u)-main otherwise. By definition, the descendant of each pattern-subterm of u is e. Descendants of all redexes of t except u are also called residuals. By definition, u does not have residuals in s. A redex of s is said to be created by contracting u or to be an (u)-new redex if it is not a residual of a redex of t′. It is clear what is to be meant under descendants of subterms that are not in u. The notion of descendant and residual extend naturally to arbitrary reductions. The ancestor relation is the inverse of the descendant relation.

Definition 2.3 We call a redex u complete (resp. ∞-complete) if erased arguments of u are in normal form (resp. are strongly normalizable). A reduction is complete (resp. ∞-complete) if it only contracts complete (resp. ∞-complete) redexes.

Lemma 2.4 Let P : t_{0} →^{u_{0}}t_{1} →^{u_{1}}… → t_{n} be a complete reduction in an OTRS (Σ, R), and let P_{μ} : s_{0} →^{v_{0}} s_{1} →^{v_{1}} … → s_{n} be a corresponding R_{μ}-reduction such that all R_{μ}-redexes in s_{0} are μ-main. Then

(1) for each k (0 ≤ k ≤ n), we have (b)_{k}: any R_{μ}-redex in s_{k} is μ-main.

(2) if P is normalizing, then so is P_{μ}. Proof (1) By induction on k. (b)_{0} is obvious. Suppose that (b)_{k} holds and let us show (b)_{k+1}. Let u_{k} = C[o_{1}, …, o_{m}] and v_{k} = C′[e_{1}, …, e_{m}, e′_{1}, …, e′_{p}], where e_{1}, …, e_{m} are μ-main arguments of v_{k}, which correspond to arguments o_{1}, …, o_{m} of u_{k}, respectively, and e′_{1}, …, e′_{p} are μ-erased arguments of v_{k}. Then the contractum of v_{k} in R_{μ} has the form o′ = μ(μ^{0}, …, μ^{0}, e′_{1}, …, e′_{p}, e_{i_{1}}, …, e_{i_{l}}, o), where o is the contractum of C[e_{1}, …, e_{m}] in (Σ_{μ}, R) and, for each j, o_{i_{j}} is u_{k}-erased. Since v_{k} and u_{k} are corresponding subterms of s_{k} and t_{k}, and e_{i} and o_{i} are corresponding arguments, we have that (α): [e_{i}]_{μ} = o_{i}, i = 1, …, m. Since o_{i_{1}}, …, o_{i_{l}} are u_{k}-erased and u_{k} is complete, we have that (β): o_{i_{1}}, …, o_{i_{l}} are R-normal forms. It follows from (b)_{k} that in e′_{1}, …, e′_{p} there are no R_{μ}-redexes and that R_{μ}-redexes in s_{k+1}, that are not in o′ or are in o, are μ-main. It follows from (b)_{k}, (α), (β), and Lemma 2.2 that e_{i_{1}}, …, e_{i_{l}} are R_{μ}-normal forms. Thus (b)_{k+1} holds and (1) is proved.

(2) By Lemma 2.2 and (b)_{n}.

Recall that a (sequential) strategy selects a redex to be contracted in any given term. A complete (resp. ∞-complete) strategy contracts a complete (resp. an ∞-complete) redex in each step. A strategy is perpetual if it constructs an infinite reduction of any given term whenever such a reduction exists.

Theorem 2.1 A complete strategy is perpetual in orthogonal TRSs. Proof It is enough to show that if t has a normalizing complete reduction P : t ↠ t′, then t is strongly normalizable. Indeed, by Lemma 2.4, the corresponding R_{μ}-reduction of P is also normalizing. Hence, by Lemma 2.3, t is strongly normalizable in R.

Definition 2.4 (1) A TRS is called non-erasing if left- and right-hand sides of each rule in it contain occurrences of the same variables.

(2) A TRS is called weakly innermost normalizing [9] if each term has a normal form reachable by an innermost reduction.

Corollary 2.2 (Church) Let R be a non-erasing OTRS. Then R is weakly normalizing iff it is strongly normalizing.

Corollary 2.3 (O’Donnell [9]) Let R be an OTRS. Then R is strongly normalizing iff it is weakly innermost normalizing.

Theorem 2.2 (Klop [7]) An ∞-complete strategy is perpetual in orthogonal TRSs. Proof It is enough to prove that if t_{0} has a normalizing ∞-complete reduction P : t_{0} →^{u_{0}}t_{1} → …→ t_{n}, then t_{0} is strongly normalizable in R. Since u_{i} is ∞-complete, there is a complete normalizing reduction Q: t_{0} ↠ t_{1} ↠ …↠ t_{n}. Now by Theorem 2.1, t_{0} is strongly normalizable.

The following propositions are obtained in Klop [6]. The proof of Proposition 2.2 is, however, not correct, since it establishes weak normalization of R_{μ} only for terms of R, not for all terms of R_{μ}.

Proposition 2.1 (Klop [6]) A term t in an OTRS R is strongly normalizable iff t is weakly normalizable in R_{μ}. Proof (⇒) From Lemma 2.4. (⇐) From Lemma 2.3.

Proposition 2.2 (Klop [6]) An OTRS R is strongly normalizing iff R_{μ} is weakly normalizing. Proof (⇒) Let t′ be a term in R_{μ}. We prove that t′ is weakly normalizable by induction on the length of t′. By the induction assumption, all μ-erased subterms of t′ are weakly normalizable in R_{μ}. Let t^{∗} be obtained from t′ by their reduction to normal forms. By Lemma 2.4, t^{∗} is weakly normalizable in R_{μ}, since [t^{∗}]_{μ} is strongly normalizable in R. Hence, t′ is weakly normalizable. (⇐) From Lemma 2.3.

Definition 2.5 ([4]) 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.

In [3], Huet and Lévy introduced the notion of external redex of a term and proved that each term not in normal form possesses an external redex. It is easy to show that a redex u ⊆ t is unabsorbed iff u is external in t. Thus we have the following lemma; a short direct proof of it can be found in [4].

Lemma 2.5 In any term t not in normal form there is an unabsorbed redex.

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

It follows from Lemma 2.5 that in any term not in normal form there is a limit redex. 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.

Lemma 2.6 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 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 2.7 Let (Σ, R) be an OTRS, 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_{μ}.

(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 o_{i_{1}}, …, o_{i_{l}} be u_{k}-erased arguments and o_{j_{1}}, …, o_{j_{p}} be u_{k}-main arguments. Then contractum of v_{k} in R_{μ} has the following form: o′ = μ(μ^{0}, …, μ^{0}, e′_{1}, …, e′_{m}, e_{i_{1}}, …, e_{i_{l}}, o), where o is the contractum of C[e_{1}, …, e_{n}] in (Σ_{μ}, R). 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 (α), (β), (b)_{k}, and Lemma 2.2 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_{l_{1}}. Hence v′_{k+1} ⊆ o and v′_{k+1} is μ-main by (γ). 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}^{∗}. Hence v_{k} is in a quasi-erased argument of v_{k}^{∗}. Therefore 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 when 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 a u_{k}-new redex, there are descendants of redexes contracted in P. (Since v_{k} is μ-main, o′ and hence u_{k+1} are also μ-main.) But each redex contracted in P is a limit redex. Thus, by Lemma 2.6, 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. Now (1) is proved.

(2) By Lemma 2.2 and (b)_{n}.

Theorem 2.3 A limit strategy is perpetual in OTRSs. Moreover, if a term t in an OTRS R is strongly normalizable, then a limit strategy constructs a longest normalizing reduction starting from t, and its length coincides with the number of μ-occurrences in an R_{μ}-normal form of t. Proof If a limit R-reduction P starting from t is normalizing, then by Lemma 2.7 its corresponding R_{μ}-reduction also is normalizing. Hence, by Lemma 2.3, 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 2.1)= |Q_{μ}| ≤ (by the CR property of R_{μ})≤ ∥s∥_{μ}=(by Lemma 2.7)= |P|. Thus, P has the maximal length among all reductions of t to normal form.

We now give a direct proof of the fact that limit reductions are the longest. The advantage of the previous proof is that it additionally gives a characterization of lengths of longest reductions.

Lemma 2.8 Let P : t_{0} →^{u_{0}}t_{1} →^{u_{1}}…and t_{0} →^{u}s_{0}, where u is a limit redex. Then there is a reduction Q starting from s_{0} such that |Q| ≥ |P| − 1. Proof Using the Church-Rosser theorem, we can construct the following diagram

[figure: t_{0}; u_{0}; t_{1}; u_{1}; t_{2}; s_{0}; Q_{0}; s_{1}; Q_{1}; s_{2}; u = P_{0}; P_{1}; P_{2}]

where in P_{i} : t_{i} ↠ s_{i} all residuals of u in t_{i} are contracted, and in Q_{i} : s_{i} ↠ s_{i+1} all P_{i}-residuals of u_{i} are contracted. It follows from Lemma 2.6 that u has at most one residual in each term t_{i}, which is complete. Thus if there is an i such that u_{i} is a residual of u, then Q_{i} is empty, s_{j} = t_{j} for all j > i, and Q_{j} contracts exactly one redex. Otherwise, each reduction Q_{k} contracts at least one redex. Hence, we can take the concatenation of Q_{0}, Q_{1}, …for Q.

Corollary 2.4 The limit strategy is perpetual in Orthogonal TRSs, and the limit reductions are longest among reductions starting from a strongly normalizable term.

3. Applications 3.1Recursive perpetual strategies for some classes of OTRSs We now define some classes of OTRSs for which the limit strategy is efficient.

Definition 3.1 (1) Let t →^{u}s in an OTRS R, and let v ⊆ s be a new redex. We call v generated if its pattern is in the pattern of the contractum of u. We call an OTRS R persistent (PTRS) if, for each reduction step in R, any created redex is generated.

(2) We call an OTRS outside-creating if, for any reduction step t →^{u}s, any new redex in s contains at least one symbol above the contractum of u, and call it inside-creating if any new redex in s is inside the contractum of u.

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

(4) We call an OTRS 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 3.1 (1) Let t be a term in a non-absorbing OTRS. Then any outermost redex in t is unabsorbed.

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

Thus a limit redex can be found efficiently in non-absorbing, non-left-absorbing, and non-right-absorbing systems. Note that left-normal OTRSs [9] (where in left-hand sides of rules function symbols precede variables), and Combinatory Logic in particular, are non-left-absorbing. Persistent and inside-creating systems are non-absorbing.

Proposition 3.2 Outside-creating OTRSs are strongly normalizing. Proof Let t be a term in an outside-creating OTRS R. It is easy to see that R_{μ} is outsidecreating as well. Thus, by Lemma 2.3, it is enough to prove that t has a normal form in R. Let P : t → t_{1} → …be an innermost reduction in which any created redex is contracted immediately after creation (each step creates at most one redex). Since a created redex is strictly above the contractum of a contracted redex, the number of redexes of terms in P is decreasing. Thus P is finite.

Remark 3.1 The above proposition is equivalent to Corollary 4.10 of van Raamsdonk [10] stating that all “superdevelopments” in OTRSs are finite.

3.2On decidability of weak and strong normalization Definition 3.2 We call a class ℜ of OTRSs closed under μ-extension if ℜ contains the μ-extension of each of its elements.

Proposition 3.3 Let ℜ be a class of OTRSs closed under μ-extension. Then decidability of weak normalization for OTRSs in ℜ implies decidability of strong normalization for OTRSs in ℜ. Proof For any R ∈ ℜ, weak normalization is decidable for R_{μ} ∈ ℜ. Hence, by Proposition 2.2, strong normalization is decidable for R.

It is easy to see that all classes of OTRSs, defined in Definition 3.1, and the class of strongly sequential OTRSs [3] are closed under μ-extension. Note that although, for any OTRS R, R_{μ} contains infinitely many rules, it is decidable whether a term in R_{μ} is an R_{μ}-redex. Thus the

3. Applications 10

decidability question makes sense for R_{μ}. We show in [5] that weak normalization is decidable in Persistent TRSs. Hence, by Proposition 3.3, strong normalization is also decidable for Persistent TRSs. For inside-creating TRSs, decidability of weak and strong normalization is open. For OTRSs in general, undecidability of strong normalization follows from undecidability of the (uniform) halting problem. Thus, weak normalization is also undecidable.

3.3The least upper bound of lengths of reductions in persistent TRSs We now present an algorithm for finding the least upper bound of lengths of coinitial reductions in persistent TRSs, which does not need to make an actual transformation of an input term. We first recall some results from [5]. Notation We write t = (t_{1}//e_{1}, ..., t_{k}//e_{k})e if e_{1}, ..., e_{k} are non-overlapping proper subterms in e, and t is obtained from e by their replacement with t_{1}, ..., t_{k}, respectively.

Definition 3.3 We call a subterm s in t free if s is not a proper pattern-subterm of a redex in t.

Lemma 3.1 Let t = (e//o)s in a persistent TRS, let e be free in t, and let s and e be strongly normalizable. Then t is strongly normalizable. Proof sketch By persistency, all descendants of e remain free; therefore, infinitely many steps of an infinite reduction starting from t must be performed inside (descendants of) e or outside e, meaning that symbols of e do not belong to patterns of the redexes contracted outside e. But e and s are strongly normalizable. Therefore, t does not possess an infinite reduction.

Definition 3.4 We call a redex in a PTRS R trivial if it is a left-hand side of a rewrite rule in R. We call redexes u and v similar if they are instances the left-hand side of the same rule. We call a redex u finite if its similar trivial redex is strongly normalizable.

Lemma 3.2 ([5]) A term t in a PTRS is strongly normalizable iff any redex in t is finite. Proof (⇒) Obviously, any redex u in t is strongly normalizable. So, by Lemma 3.1, the trivial redex similar to u is strongly normalizable as well. (⇐) By induction on the number n of redexes in t. The case n = 0 is trivial. So let n > 0, u be an innermost redex in t, and s = (x//u)t. By the induction assumption, s is strongly normalizable. Since arguments of u are in normal form and u is a finite redex, Lemma 3.1 implies that u is strongly normalizable. Since t = (u//x)s, we have again by Lemma 3.1 that t is strongly normalizable.

Definition 3.5 let R be a PTRS and r ∈ R. We call an r-tree the maximal tree with rules as nodes and r as the root, such that a redex corresponding to a node has an occurrence in the right-hand side of its ancestor node.

Lemma 3.3 ([5]) An r-redex u in a PTRS R is finite iff the r-tree is finite. Proof (⇒) If the r-tree has an infinite branch r_{0}, r_{1}, ..., then one can construct infinite reduction of the trivial r-redex v →^{v}t_{1} →^{v_{1}}t_{2} →^{v_{2}}…, where v_{1} is an r_{1}-redex created by v, v_{2} is an r_{2}-redex created by v_{1}, and so on. (⇐) By induction on the height n of the r-tree. If n = 0, then contractum s of the trivial r-redex v is normal form. If n > 1, then by the induction assumption, each redex in s is finite. Hence, by Lemma 3.2, s is strongly normalizable. Thus, v is also strongly normalizable, i.e., u is finite.

Definition 3.6 Let R be a PTRS.

(1) Let t be a term in R_{μ}, let s ⊆ 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′ ⊆ e_{i}, let v = C[o_{1}, …, o_{n}] be an rredex (similar to u) with arguments o_{1}, …, o_{n} in R_{μ}-normal form, and let Q : v ↠ o be the rightmost innermost normalizing R_{μ}-reduction. Then, by definition, mult_{μ}(u, i) = mult_{μ}(u, s′) = mult_{μ}(r, i) = Mult_{μ}(o_{i}, v), and mult_{μ}(u) = mult_{μ}(r) is the number of μ-subterms in o that appear during Q, i.e., that are not descendants of subterms with head-symbol μ from (arguments of) u. Numbers mult_{μ}(u, i) and mult_{μ}(r, i) are proper μ-indices of u and r, and numbers mult_{μ}(u) and mult_{μ}(r) are μ-indices of u and r.

The following lemma implies that the definition is correct.

Lemma 3.4 Let u = C[e_{1}, …, e_{n}] and v = C[o_{1}, …, o_{n}] be similar redexes with arguments in normal form in a PTRS R_{μ}, and let P : u = t_{0} →^{u_{0}}t_{1} →^{u_{1}}… and Q : v = s_{0} →^{v_{0}}s_{1} →^{v_{1}}… be the rightmost innermost normalizing R_{μ}-reductions. Then, for each i = 0, 1, …, there is an one-to-one correspondence between

1. redexes in t_{i} and s_{i} such that corresponding redexes are similar, and u_{i} and v_{i} are corresponding.

2. “appeared μ-subterms”, which are descendants of contracta of R_{μ}-redexes in t_{i} and s_{i}. Proof Easy induction on i, using persistency of R_{μ}.

Lemma 3.5 Let t be a normalizable term in a PTRS R_{μ}, let e ⊆ s ⊆ t, and let s be in R_{μ}-normal form. Then Mult_{μ}(s, t) = Mult_{μ}(e, t). Proof Let t ↠ o be the rightmost innermost normalizing R_{μ}-reduction. Then the descendants of s in o are disjoint occurrences of s, and each of them contains exactly one descendant of e.

Notation L(t) denotes the least upper bound of lengths of reductions starting from t.

Lemma 3.6 Let t be a strongly normalizable term in a PTRS R and let 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 where u_{i} is reduced to R_{μ}- normal form, mult_{μ}(u_{i}) new μ-symbols appear (in the beginning of the fragment, all arguments of u_{i} are in R_{μ}-normal form). By Lemma 3.5, during the rest of P each of these mult_{μ}(u_{i}) μ-occurrences is duplicated Mult_{μ}(u_{i}, t)-times. Hence

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

and the lemma follows from Theorem 2.3.

Lemma 3.7 Let t be a strongly normalizable term in a PTRS R_{μ}, let s ⊆ t, and let u_{1}, …, u_{n} be all redexes in t that contain 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 3.5 that, in the fragment of P in which u_{i} is reduced to R_{μ}-normal form, each descendant of s is duplicated mult_{μ}(u_{i}, s) = mult_{μ}(u_{i}, m_{i})-times. Thus, the lemma is obvious.

Lemma 3.8 Let u = C[e_{1}, …, e_{k}] be an r-redex with arguments e_{1}, …, e_{k} in normal form in a PTRS R_{μ}. Then for all j = 1, …, k:

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

mult_{μ}(u) = mult_{μ}(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 3.6 (since all descendants of subterms e_{j_{i}} are pairwise disjoint).

Theorem 3.1 Let t be a term in a PTRS R. Then the least upper bound L(t) of lengths of reductions starting from t can be found by the following

Algorithm 3.1 Let r_{1}, …, r_{n} be all rules in R such that an r_{i}-redex has an occurrence in t (i = 1, …, n). If the r_{i}-tree is not finite for at least one i, then L(t) = ∞. Otherwise, using Lemmas 3.8 and 3.7, find μ-indices and proper μ-indices of all rules r_{i}. Finally, using Lemmas 3.6 and 3.7, find L(t).

Proof From Theorem 2.3 and Lemmas 3.2, 3.3, and 3.6-3.8.

3.4The least upper bound of lengths of developments Let R = \{r_{i} : t_{i} → s_{i}\} be an OTRS and let \underline{R} = \{\underline{r}_{i} : \underline{t}_{i} → s_{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 3.1, which becomes simpler in this case. For any rule \underline{r} ∈ \underline{R}, mult_{μ}(\underline{r}) = 1, and proper μ-indices of \underline{r} can be found immediately from the right-hand side of \underline{r}. Indeed, if \underline{r}: C[x_{1}, …, x_{n}] → s, then mult_{μ}(\underline{r}, i) = 1 if x_{i} does not occur in s, and mult(\underline{r}, i) coincides with the number of occurrences of x_{i} in s otherwise.

Acknowledgments I enjoyed discussions with H. Barendregt, J. W. Klop, J.-J. Lévy, L. Maranget, G. Mints, 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. 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 Utrect, Department of mathematics, p. 13-53, 1976.

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

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

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

5. Khasidashvili Z. On the equivalence of persistent term rewriting systems and recursive program schemes. In: Proc. of the second Israel Symposium on Theory and Computing Systems, Natanya, 1993, p. 240-249.

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

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

8. Nederpelt R. P. Strong normalization for a typed lambda-calculus with lambda structured types. Ph. D. Thesis, Eindhoven, 1973.

9. O’Donnell M. J. Computing in systems described by equations. Springer LNCS 58, 1977. 10.Van Raamsdonk F. A simple proof of confluence for weakly orthogonal combinatory reduction

Systems. Report CS-R9234, CWI Amsterdam, 1992.