Perpetuality and Strong Normalization in Orthogonal Term Rewriting Systems

Zurab Khasidashvili

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

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. For some classes of OTRSs 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.

1 Introduction

It is shown in O’Donnell [12] 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 contracts redexes that do not erase any other redex is perpetual. Moreover, one can even reduce redexes whose erased arguments are strongly normalizable (Klop [10]). For the lambda-calculus, a more subtle perpetual strategy was invented in Barendregt et al. [1]. However, none of these strategies are general enough to capture perpetuality in all Orthogonal Combinatory Reduction Systems (OCRSs), i.e., OTRSs with bound variables (Klop [9]).

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. It is shown in [8] that the limit strategy is perpetual also in OCRSs.

An unabsorbed redex exists in any term not in normal form, but there is no general algorithm to find one. However, for some classes of OTRSs, such as persistent, inside-creating, non-absorbing, non-left-absorbing, and non-right-absorbing systems, the unabsorbed redexes are easy to find. For example, in non-left-absorbing systems, where no subterm can be absorbed to the left of the contracted redex, the leftmostoutermost redexes are unabsorbed (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 [4].

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 Nederpelt’s method [11] by which proving strong normalization in a typed λ-calculus gets reduced to proving weak normalization (i.e., existence of a normal form). Nederpelt’s method was reinvented and used by Klop [9] for OCRSs. For any OTRS R, we define the corresponding non-erasing OTRS R_{μ} which contain special function symbols μ^{n} and show that the least upper bound of lengths of Rreductions 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.

Further, 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 [9]. 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. Complete proofs can be found in [7].

2 Perpetual strategies in OTRSs

We recall some basic notions of TRS theory; one can find comprehensive introductions to the subject in [3] and [10]. 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 the R_{μ}-normal form o of e. (Indeed, for any R_{μ}- reduction P : e ↠ e′, we have e′ ↠ o; hence |P | ≤ ∥e′∥_{μ} ≤ ∥o∥_{μ}.) For any Rreduction 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. (In [7], we give a simple direct proof of the fact that limit reductions are the longest.)

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}} quasierased 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 (the orthogonality of R_{μ} is easy to check), 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 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.2 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 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 by descendants of subterms that are not in u. The notions 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 the 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.3 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}, 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.1 that e_{i_{1}}, …, e_{i_{l}} are R_{μ}-normal forms. Thus (b)_{k+1} holds and (1) is proved.

(2) By Lemma 2.1 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 OTRSs.

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.3, the corresponding R_{μ}- reduction of P is also normalizing. Hence, by Lemma 2.2, t is strongly normalizable in R.

As a corollary, one has that a non-erasing OTRS is weakly normalizing iff it is strongly normalizing (Church), and that the innermost strategy is perpetual in OTRSs (O’Donnell [12]).

Theorem 2.2 (Klop [10]) An ∞-complete strategy is perpetual in OTRSs.

Proof. It is enough to prove that if t_{0} has a normalizing ∞-complete reduction P : t_{0} →^{u_{0}} t_{1} →^{u_{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 [9]. The proof of Proposition 2.2 is, however, not correct — a proof of Proposition 2.1 is presented as a proof of Proposition 2.2, while the former establishes weak normalization of R_{μ} only for terms of R, not for all terms of R_{μ}. The difference is significant for the applications presented below.

Proposition 2.1 (Klop [9]) A term t in an OTRS R is strongly normalizable iff t is weakly normalizable in R_{μ}.

Proof. (⇒) From Lemma 2.3. (⇐) From Lemma 2.2.

Proposition 2.2 (Klop [9]) 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.3, t^{∗} is weakly normalizable in R_{μ}, since [t^{∗}]_{μ} is strongly normalizable in R. Hence, t′ is weakly normalizable. (⇐) From Lemma 2.2.

Definition 2.4 (1) ([5]) We call a subterm s of a term t unabsorbed in a reduction P : t ↠ e if the descendants of s do not appear inside redex-arguments of terms in P, and call s absorbed in P otherwise. We call s unabsorbed in t if it is unabsorbed in any reduction starting from t, and absorbed in t otherwise.

(2) Let u_{l} be a redex in a term t defined as follows: choose an unabsorbed redex u_{1} in t; choose an erased argument s_{1} of u_{1} that is not in normal form (if any); choose in s_{1} an unabsorbed redex u_{2}, and so on, as long as possible. Let u_{1}, s_{1}, u_{2}, …, u_{l} be such a sequence. Then we call u_{l} a limit redex and call u_{1}, s_{1}, u_{2}, …, u_{l} a limit sequence of t.

In [4], 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. A direct short proof of the existence of an unabsorbed redexes in any term not in normal form can be found in [5]. Thus 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.4 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.5 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 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), 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.1 that (δ): e_{i_{1}}, …, e_{i_{l}} are in R_{μ}-normal form.

By (γ), ∥o′∥_{μ} = ∥v_{k}∥_{μ} +1. Hence ∥s_{k+1}∥_{μ} = ∥s_{k}∥_{μ} +1 = k +1, i.e., (α)_{k+1} holds. If v′_{k+1} ⊈ o′, then (b)_{k} implies that v′_{k+1} is μ-main. If v′_{k+1} ⊆ o′, then, by (b)_{k},

v′_{k+1} ⊈ e′_{1}, …, e′_{m} (since ancestors of e′_{1}, …, e′_{m} are μ-erased arguments of v_{k}) and, by (δ), v′_{k+1} ⊈ e_{i_{1}}, …, e_{i_{l}}. Hence v′_{k+1} ⊆ o and 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.4, 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.1 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.5 its corresponding R_{μ}-reduction also is normalizing. Hence, by Lemma 2.2, 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.5)= |P |. Thus, P has the maximal length among all reductions of t to normal form.

3 Applications

3.1 Recursive perpetual strategies for some classes of OTRSs

We now define some classes of OTRSs, introduced in [5], 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.

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

It is easy to see [5] that outermost redexes in non-absorbing OTRSs, leftmostoutermost redexes in non-left-absorbing OTRSs, and rightmost-outermost redexes in non-right-absorbing OTRSs are unabsorbed. Thus a limit redex can be found efficiently in these systems. Note that left-normal OTRSs [12] (where in left-hand sides of rules function symbols precede variables), and Combinatory Logic in particular, are non-left-absorbing. Persistent systems are non-absorbing.

Proposition 3.1 Outside-creating OTRSs are strongly normalizing.

Proof. It is easy to see that if R is an outside-creating OTRS, then so is R_{μ}. Thus, by Lemma 2.2, it is enough to prove that R is weakly normalizing. Let P 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 terminating.

Remark 3.1 Proposition 3.1 is equivalent to Corollary 4.10 of van Raamsdonk [13] stating that all “superdevelopments” in OTRSs are finite.

3.2 On 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.2 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 [4] 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 decidability question makes sense for R_{μ}. We show in [5] that weak normalization is decidable in Persistent TRSs. Hence, by Proposition 3.2, 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.3 The least upper bound of lengths of reductions in persistent TRSs

We now present an algorithm for finding the least upper bound of lengths of co-initial reductions in persistent TRSs, which does not need to make an actual transformation of an input term. In particular, Recursive Program Schemes [2] are persistent. Developments also can be represented as reductions in persistent TRSs. We first recall some results from [6].

Definition 3.3 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 of the lefthand side of a same rule r ∈ R. We call u finite if its similar trivial redex is strongly normalizable. 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.1 ([6]) (1) An r-redex u in a PTRS R is finite iff the r-tree is finite. (2) A term t in a PTRS is strongly normalizable iff any redex in t is finite.

Definition 3.4 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 r-redex 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 correctness of Definition 3.4.(2) can be shown by induction on |Q|.

Lemma 3.2 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. An easy application of Definition 3.4.

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

Lemma 3.3 Let t be a strongly normalizable term in a PTRS 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 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.2, 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.4 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 sketch From Definition 3.4 and Lemma 3.2.

Lemma 3.5 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 sketch From Definition 3.4.

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.5 and 3.4, find μ-indices and proper μ-indices of all rules r_{i}. Finally, using Lemmas 3.3 and 3.4, find L(t).

Proof sketch From Theorem 2.3 and Lemmas 3.1 and 3.3-3.5.

3.4 The 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, 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} : C[x_{1}, …, x_{n}] → s ∈ \underline{R}, mult_{μ}(\underline{r}) = 1, 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, J. R. Kennaway, 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 Utrecht, Department of mathematics, p. 13-53, 1976.

2. Courcelle B. Recursive Applicative Program Schemes. In: J.van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 9, vol.B, 1990, p. 459-492.

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

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

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

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

7. Khasidashvili Z. Perpetual reductions and strong normalization in orthogonal term rewriting systems. CWI Report CS-R9345, Amsterdam, July 1993.

8. Khasidashvili Z. Perpetual reductions in orthogonal combinatory reduction systems. CWI Report CS-R9349, Amsterdam, July 1993.

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

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

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

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

13. Van Raamsdonk F. A simple proof of confluence for weakly orthogonal combinatory reduction Systems. Report CS-R9234, CWI Amsterdam, 1992.

This article was processed using the LaTEX macro package with LLNCS style