Theoretical Computer Science 165:75-95, 1996.

A Sequential Reduction Strategy

Sergio Antoy

Portland State University, U.S.A.

         antoy@cs.pdx.edu

Aart Middeldorp

University of Tsukuba, Japan

                                      ami@is.tsukuba.ac.jp

ABSTRACT

Kennaway proved the remarkable result that every (almost) orthogonal term rewriting system admits a computable sequential normalizing reduction strategy. In this paper we present a computable sequential reduction strategy similar in scope, but simpler and more general. Our strategy can be thought of as an outermost-fair-like strategy that is allowed to be unfair to some redex of a term when contracting the redex is useless for the normalization of the term. Unlike the strategy of Kennaway, our strategy does not rely on syntactic restrictions that imply confluence. On the contrary, it can easily be applied to any term rewriting system, and we show that the class of term rewriting systems for which our strategy is normalizing properly includes all (almost) orthogonal systems. Our strategy is more versatile; in case of (almost) orthogonal term rewriting systems, it can be used to detect certain cases of nontermination. Our normalization proof is more accessible than Kennaway’s. We also show that our sequential strategy sometimes succeeds where the parallel-outermost strategy fails.

1. Introduction

This paper is concerned with the fundamental question how to compute normal forms with respect to a given term rewriting system (TRS for short). Consider the TRS

\begin{aligned}0 + x & → & x \\ S(x) + y & → & S(x + y) \\ 0 × x & → & 0 \\ S(x) × y & → & x × y + y \end{aligned}

specifying addition and multiplication on natural numbers. Suppose we want to normalize the term (0 + (0 × S(0))) + (0 × 0). This term contains three instances of left-hand sides of rewrite rules (so-called redexes):

\overbrace{(0 + \underbrace{(0 × S(0))}_{(2)})}^{(1)} + \overbrace{(0 × 0)}^{(3)}

Redexes (1) and (3) are not contained in larger redexes. We call them outermost redexes. Redexes (2) and (3) are innermost redexes; they do not contain smaller redexes. If we select the leftmost-outermost redex (1) we obtain the term (0×S(0))+(0×0) which contains two redexes. Selecting again the leftmost-outermost redex we obtain the term 0 + (0 × 0). After two further contractions of the leftmost-outermost redex we arrive at the normal form 0. Instead of selecting a single redex in each step, we can also contract redexes in parallel. For instance, redexes (1) and (3) do not interfere, i.e., after contraction of redex (1), redex (3) is not affected, and vice-versa. Also redexes (2) and (3) can be contracted in parallel. If we contract all outermost redexes in parallel we also obtain the normal form 0: (0+(0×S(0)))+(0×0) →^{∗} (0×S(0))+0 → 0+0 → 0.

This work has been supported in part by the National Science Foundation under grant CCR-9406751.

Does it matter which redexes we select for contraction? In the above example the answer is no since the TRS doesn’t admit infinite reduction sequences. Hence, no matter which redexes we select for contraction, we are guaranteed to find a normal form. In general, however, terms may have a normal form but also admit infinite reduction sequences. Hence it is important to adopt a good reduction strategy. Given a TRS and a term, a reduction strategy tells you which redex(es) to contract. The desirable property of reduction strategies is normalization: repeated contraction of the redex(es) selected by the reduction strategy leads to a normal form, if the term under consideration has a normal form. For the important subclass of (almost) orthogonal TRSs several positive results are known. An orthogonal TRS is left-linear and nonoverlapping. If the non-overlapping restriction is relaxed by allowing trivial overlays then we speak of almost orthogonal TRSs. A typical example of an almost orthogonal TRS that is not orthogonal is the two-rule system {⊤ ∨ x → ⊤, x ∨ ⊤ → ⊤}. O’Donnell [8] showed that the parallel-outermost strategy—which evaluates all outermost redexes in parallel—is normalizing for all almost orthogonal TRSs.

The question whether there exists a computable normalizing sequential reduction strategy for all (almost) orthogonal TRSs has received quite a bit of attention. A sequential strategy must choose a single redex for contraction. The main results are summarized below.

(1) Contrary to the situation for λ-calculus, there are orthogonal TRSs for which the leftmostoutermost strategy is not normalizing. Consider for instance the orthogonal TRS (from [4])

\begin{aligned}a & → & b \\ c & → & c \\ f(x, b) & → & d \end{aligned}

and the term t = f(c, a). The leftmost-outermost strategy will select redex c in t and hence produce the infinite reduction sequence t → t → t → · · ·. Nevertheless, parallel-outermost succeeds in normalizing t: t →^{∗} f(c, b) → d. O’Donnell [8] showed that the leftmostoutermost strategy is normalizing for every left-normal orthogonal TRS.^{1} Left-normality means that variables do not precede function symbols in the left-hand sides of the rewrite rules. A typical example of a left-normal orthogonal TRS is combinatory logic.

(2) Huet and Lévy, in a landmark paper [4], formulated the strong sequentiality criterion and showed that every strongly sequential orthogonal TRS admits a computable normalizing sequential reduction strategy. Every left-normal orthogonal TRS is strongly sequential, but there are many strongly sequential orthogonal TRSs that are not left-normal, one example being the TRS of the preceding paragraph. The strategy of Huet and Lévy is based on the fact that for orthogonal TRSs

1 Actually, O’Donnell showed that the leftmost-outermost strategy is normalizing for all left-normal almost orthogonal TRSs. However, it is easy to see that if two rewrite rules in a left-normal almost orthogonal TRS overlap, then one of the rules is an instance of the other. Hence for every left-normal almost orthogonal TRS there exists a left-normal orthogonal TRS with the same rewrite relation. Thus nothing is really added by allowing trivial overlays, rather, it would unnecessarily confuse Figure 1 below.

• every term not in normal form contains a needed redex, and

• repeated contraction of needed redexes leads to the normal form, if it exists. Here a needed redex is a redex with the property that in every reduction sequence (from the term in which the redex occurs) to normal form one of its descendants is contracted. The second statement above can be strengthened to the hypernormalization of needed reduction: there are no infinite reduction sequences starting from a term that has a normal form in which infinitely many needed redexes are contracted. Since needed redexes are in general not computable, this does not give a normalizing sequential strategy for all orthogonal TRSs. Huet and Lévy showed that for strongly sequential orthogonal TRSs at least one of the needed redexes in a term not in normal form can be (efficiently) computed. The orthogonality requirement cannot be weakened to almost orthogonality, simply because needed redexes may not exist for almost orthogonal TRSs, as observed by Sekar and Ramakrishnan [13].

(3) Kennaway [5] showed the remarkable fact that every almost orthogonal TRS admits a computable normalizing sequential reduction strategy. Actually, Kennaway doesn’t restrict himself to TRSs but obtains his result in the very general setting of combinatory reduction systems of Klop [6]. The result of Kennaway is remarkable since it covers TRSs like combinatory logic extended with Berry’s TRS

\begin{aligned}f(a, b, x) & → & c \\ f(b, x, a) & → & c \\ f(x, a, b) & → & c \end{aligned}

This TRS seems to require parallel evaluation of the arguments t_{1}, t_{2}, t_{3} when faced with a term f(t_{1}, t_{2}, t_{3}) since in this TRS it is undecidable whether a term reduces to a or b. Berry’s TRS is an example of a TRS that is not strongly sequential.

(4) Toyama [14] showed that the sequential strategy of Huet and Lévy is normalizing for the larger class of strongly sequential left-linear root-balanced joinable TRSs. The root-balanced joinability requirement is less restrictive than the trivial overlays allowed by Kennaway, but because of the strong sequentiality requirement Toyama’s result does not cover the result of Kennaway. For instance, the almost orthogonal TRS {⊤ ∨ x → ⊤, x ∨ ⊤ → ⊤} is not strongly sequential.

(5) Oyamaguchi [10] extended the work of Huet and Lévy in a different direction. Strong sequentiality is a property based on the left-hand sides of the rewrite rules. Oyamaguchi showed that by incorporating information in the right-hand sides of the rewrite rules, a less restrictive notion of sequentiality can be obtained, while retaining the good properties of strong sequentiality. The resulting class of NV-sequential orthogonal TRSs properly contains all strongly sequential orthogonal TRSs. Although Kennaway’s result applies to all systems covered by Oyamaguchi’s result, the result of Oyamaguchi is of interest because his strategy can be computed in polynomial time, which is not the case for the strategy of Kennaway.^{2} Figure 1 shows the relationships between the above-mentioned results. The area enclosed in the dotted rectangle denotes the class of TRSs for which the parallel-outermost strategy is normalizing. Areas enclosed in numbered solid rectangles correspond to the sequential strategies described above. Observe that parallel-outermost encompasses all known sequential reduction strategies. (The fact that parallel-outermost is normalizing for every strongly sequential leftlinear root-balanced joinable TRS follows from the work of Toyama [14].) All systems in area (3) are confluent. Systems in area (4) are not necessarily confluent, but they do have unique normal forms. (Slightly stronger, every term that has a normal form is confluent.)

2 Moreover, Oyamaguchi obtained his results in 1987, two years before Kennaway’s paper was published.

Recently, Comon [2] showed that strong and NV-sequentiality are decidable properties of left-linear, possible overlapping, TRSs, and van Raamsdonk [12] showed that outermost-fair rewriting is normalizing for weakly orthogonal higher-order rewriting systems.

1 2 5 3 4 Figure 1.

The starting point of the present paper is Kennaway’s result. The strategy of Kennaway is complicated and relies on the confluence property. We define a simpler and intuitive sequential strategy for every TRS and we show that the class of TRSs for which our strategy is normalizing properly includes the class of TRSs for which Kennaway’s strategy is defined. This class is indicated in Figure 1 as the area between the dashed lines. At present it is unclear whether the shaded area is inhabited. All other areas are inhabited. In particular, we will see that there exist TRSs which cannot be normalized by means of the parallel-outermost strategy but for which our sequential strategy succeeds.

Our strategy is versatile. We will show that in case of almost orthogonal TRSs, it can be used as a sufficient condition for the property of having no normal form. This means that for certain terms our strategy will signal that it is useless to contract any redex as the term under consideration has no normal form.

The remainder of the paper is organized as follows. In the next section we formally define the notion of sequential reduction strategy. In Section 3 we describe an abstract game of Klop which is closely related to our strategy. It is well-known that in general it is undecidable whether a term cycles. In Section 4 we give a sufficient and decidable criterion for cyclicity. Using this result, our computable sequential strategy is defined in Section 5. In Section 6 we present our main theorem: if our strategy fails to normalize a term then there exists an infinite so-called outermostfair reduction sequence starting from that term. This result does not rely on orthogonality, quite to the contrary, it holds for every TRS. Our proof is non-trivial but considerably simpler than the normalization proof of Kennaway. Since for almost orthogonal TRSs it is known (O’Donnell [8]) that terms that admit infinite outermost-fair reduction sequences do not have a normal form, an immediate consequence is the normalization of our strategy for all almost orthogonal TRSs. In Section 7 we explain how, in case of almost orthogonal systems, our strategy can be used to detect certain cases of non-termination. Furthermore, we exhibit a non-left-linear TRS which can be normalized by our sequential strategy, but for which parallel-outermost fails. We also mention some directions for further research. In particular, we address the question how to enhance our strategy in order to enlarge the class of TRSs for which it is normalizing.

2. Preliminaries

A signature is a set F of function symbols. Associated with every f ∈ F is a natural number denoting its arity. Function symbols of arity 0 are called constants. The set T (F, V) of terms built from a signature F and a countably infinite set of variables V is the smallest set containing V such that f(t_{1}, …, t_{n}) ∈ T (F, V) whenever f ∈ F has arity n and t_{1}, …, t_{n} ∈ T (F, V). We write c instead of c() whenever c is a constant. Let □ be a fresh constant symbol. A context C is a term in C(F, V) containing precisely one hole. The designation term is restricted to members of T (F, V). If C is a context and t a term then C[t] denotes the result of replacing the hole in C by t. We say that t is a subterm of C[t]. A substitution is a map σ from V to T (F, V) with the property that the set {x ∈ V | σ(x) ≠ x} is finite. If σ is a substitution and t a term then tσ denotes the result of applying σ to t. We call tσ an instance of t.

A rewrite rule l → r is a pair of terms such that the left-hand side l is not a variable and variables which occur in the right-hand side r occur also in l. A TRS is a pair (F, R) consisting of a signature F and a set R of rewrite rules between terms in T (F, V). We often present a TRS as a set of rewrite rules, without making explicit its signature, assuming that the signature consists of the function symbols occurring in the rewrite rules. A TRS R defines a rewrite relation →_{R} on terms as follows: s →_{R} t if there exists a rewrite rule l → r in R, a substitution σ, and a context C such that s = C[lσ] and t = C[rσ]. The subterm lσ of s is called a redex and we say that s rewrites to t by contracting the redex lσ. The subterm rσ of t is called a contractum of the redex lσ. We call s →_{R} t a rewrite step. We usually omit the subscript R. A term without redexes is called a normal form. The set of all normal forms of R is denoted by NF (R). We say that a term t has a normal form if there exists a reduction sequence starting from t that ends in a normal form. A TRS is confluent if for all terms t_{1}, t_{2}, t_{3} with t_{1} →^{∗} t_{2} and t_{1} →^{∗} t_{3} there exists a term t_{4} such that t_{2} →^{∗} t_{4} and t_{3} →^{∗} t_{4}. In a confluent TRS every term has at most one normal form.

A position is a sequence of natural numbers identifying a subterm in a term. The set Pos(t) of positions in a term t is inductively defined as follows: Pos(t) = {ε} if t is a variable and Pos(t) = {ε} ∪ {i·p | 1 ⩽ i ⩽ n and p ∈ Pos(t_{i})} if t = f(t_{1}, …, t_{n}). We say that a position p is above a position q if there exists a position r such that p · r = q. If p is above q we also say that q is below p and we write p ⩽ q. We write p < q if p ⩽ q and p ≠ q. Positions p, q are disjoint, denoted by p ∥ q, if neither p ⩽ q nor q ⩽ p. If p ∈ Pos(t) then t_{|p} denotes the subterm of t at position t and t[s]_{p} denotes the term that is obtained from t by replacing the subterm at position p by the term s. The size |t| of a term t is the number of symbols occurring in it.

A TRS R is left-linear if the left-hand side l of every rewrite rule l → r ∈ R doesn’t contain multiple occurrences of the same variable. Let l_{1} → r_{1} and l_{2} → r_{2} be renamed versions of rewrite rules of a TRS R such that they have no variables in common. Suppose l_{1}_{|p}, for some p ∈ Pos(l_{1}) such that l_{1}_{|p} is not a variable, and l_{2} are unifiable with most general unifier σ. The pair of terms ⟨l_{1}[r_{2}]_{p}σ, r_{1}σ⟩ is called a critical pair of R. If l_{1} → r_{1} and l_{2} → r_{2} are renamed versions of the same rewrite rule, we do not consider the case p = ε. A critical pair ⟨l_{1}[r_{2}]_{p}σ, r_{1}σ⟩ with p = ε is an overlay. A critical pair ⟨s, t⟩ is trivial if s = t. A left-linear TRS without critical pairs is called orthogonal. An almost orthogonal TRS is a left-linear TRS with the property that all its critical pairs are trivial overlays. Almost orthogonal TRSs are called weakly orthogonal in Kennaway [5], but nowadays weak orthogonality is used to denote the larger class of leftlinear TRSs with only trivial critical pairs. A typical example of a weakly orthogonal TRS that is not (almost) orthogonal is the two-rule system {s(p(x)) → x, p(s(x)) → x}. Almost all results obtained for orthogonal TRSs (Klop [7] contains a good overview) carry over to almost orthogonal TRSs, with literally the same proofs, the notable exception being the theory of Huet and Lévy [4] on needed reductions. Weakly orthogonal TRSs are more complicated. Much more information on term rewriting can be found in Dershowitz and Jouannaud [3] and Klop [7]. The latter contains an introduction to the study of reduction strategies.

What is a sequential reduction strategy? In the literature one often finds the following definition:

A sequential reduction strategy is a mapping S that assigns to every term t not in normal form a redex position in t.

This definition serves if the contractum of a redex is unique, which is the case for any TRS that lacks non-trivial overlays, in particular for all weakly orthogonal TRSs. However, if the TRS under consideration does have non-trivial overlays, we are faced with the problem that there are redexes with more than one contractum. Hence we must also supply the rewrite rule according to which the redex has to be contracted. Given a redex and a rule, the contractum is again uniquely determined. How to choose the rewrite rule? There are two possibilities:

• The rewrite rule depends only on the redex. This means that we are given a mapping that assigns to every redex a rewrite rule of whose left-hand side the redex is an instance.

• The rewrite rule depends on the redex and the surrounding context. Clearly the latter option is more general. For instance, a (confluent) TRS like

\begin{aligned}a & → & b \\ b & → & a \\ a & → & c \\ c & → & a \\ f(b, c) & → & d \end{aligned}

cannot be normalized if we opt for the former. For example, the term f(a, a) can only be normalized if we contract the first occurrence of redex a by the rewrite rule a → b and the second occurrence of the same redex by the rewrite rule a → c. (This example also shows that both options lead to unfairness in the sense of Porat and Francez [11].) The simplicity of the former option however makes it possible to reason effectively about the strategy we will present later. Therefore we arrive at the following formal definition.

Definition 2.1. Let R be an arbitrary TRS. A sequential reduction strategy for R consists of the following two components:

• a mapping rule that assigns to every redex of R a rewrite rule of whose left-hand side the redex is an instance, and

• a mapping S that assigns to every term t not in normal form one of its redex positions. We require that both rule and S are computable. The mapping rule induces a mapping contract from redexes to instances of right-hand sides of rewrite rules of R as follows: if rule(t) = l → r then contract(t) = rσ where σ is any substitution satisfying t = lσ. If t is not in normal form then tS denotes the term t[contract(t_{|S(t)})]_{S(t)}, i.e. the result of applying the strategy to t. We write t →_{S} t′ if and only if t′ = tS.

In the remainder of this paper we identify a sequential reduction strategy with its mapping S, that is, we assume that the mapping rule is given but our main results do not depend on its definition. This implies that we cannot prove that our sequential reduction strategy is capable of normalizing the rather simple TRS R = {a → a, a → b} since this depends on rule: a sequential reduction strategy normalizes R if and only if rule(a) = a → b. For TRSs that do not admit non-trivial overlays, in particular for almost and weakly orthogonal TRSs, the identification of a sequential reduction strategy with its mapping S entails no loss of generality since the contractum of a redex is independent of the mapping rule.

It should be stressed that a sequential reduction strategy has no memory. This means that the decision concerning which redex to contract must be solely based on the term at hand and the given TRS, but the reduction sequence leading from the starting term to the present term may not be used. In particular, parallel-outermost cannot be simulated by a sequential reduction strategy since after contracting one outermost redex there is no way of telling which redexes in the resulting term coincide with the remaining outermost redexes in the starting term.

Definition 2.2. A sequential reduction strategy S for a TRS R is normalizing if for every term t that has a normal form there exists a reduction sequence t = t_{1} →_{S} t_{2} →_{S} ⋯ →_{S} t_{n} (with n ⩾ 1) ending in a normal form t_{n}.

Throughout the following we assume that we are dealing with TRSs that satisfy the following two properties:

• it is decidable whether a term is a redex (and hence it is also decidable whether a term is a normal form),

• in every infinite reduction sequence t_{1} → t_{2} → ⋯ in which the size of all terms is uniformly bounded, only finitely many different function symbols and variables occur (and hence the reduction sequence contains a repetition).

These properties are in particular true for all finite TRSs.

We conclude this preliminary section by introducing some notation for manipulating reduction sequences. Let D: t_{1} → t_{2} → t_{3} → ⋯ be an arbitrary infinite reduction sequence. We write D[i, j] (1 ⩽ i < j) to denote the finite portion t_{i} → t_{i+1} → ⋯ → t_{j} and D[i] (i ⩾ 1) to denote the term t_{i}. The concatenation t_{1} →^{+} t_{2} →^{+} t_{3} of two finite reduction sequences D_{1}: t_{1} →^{+} t_{2} and D_{2}: t_{2} →^{+} t_{3} is denoted by D_{1}; D_{2}. If D: t →^{+} t is a cycle then D^{∞} denotes the infinite reduction sequence D; D; D; …. Let D be an arbitrary (finite or infinite) reduction sequence.

If C is a context then C[D] denotes the reduction sequence obtained from D by replacing every term t in D with C[t]. Finally, if p is a position in D[1] such that no redex at a position q < p is contracted in D, then D_{|p} denotes the reduction sequence extracted from D by replacing every term t in D with t_{|p}. In this case the resulting sequence may contain fewer rewrite steps.

3. Klop’s Game

The result of Kennaway [5] covers the TRS combinatory logic extended with the parallel-or rules {⊤ ∨ x → ⊤, x ∨ ⊤ → ⊤}, which is rather surprising since the term t_{1} ∨ t_{2} seems to require parallel evaluation of its arguments t_{1} and t_{2}. In Kennaway [5] (see also Klop [7]) the following abstract game is described which captures the essence of the difficulty of evaluating a term like t_{1} ∨ t_{2} with a sequential strategy.

Suppose we are given two total functions f and g from ℕ_{+}, the set of positive integers, to ℕ. The objects of the game are pairs (x, y) of natural numbers. The search space is defined as a relation between these pairs:

\begin{aligned}(x, y) & → & (f(x), y), \\ (x, y) & → & (x, g(y)), \\ (x, 0) & → & (0, 0), \\ (0, y) & → & (0, 0) \end{aligned}

for all x, y > 0. The goal of the game is to reach (0, 0) from a given pair of natural numbers by adopting a sequential strategy. Sequential means here that, given a pair of positive integers, we must choose between applying function f to the first argument and applying function g to the second argument. Moreover, the choice can only be based on the pair of positive integers at hand (and the functions f and g of course). In particular, the strategy of alternatively applying f and g until one of the numbers become zero—which is guaranteed to produce (0, 0) if this is at all possible—is not allowed. Formally, a sequential strategy is a function S from ℕ_{+} × ℕ_{+} to the set {L, R}. Every sequential strategy S defines a subset of the search space as follows:

(x, y) →_{S} (f(x), y) if S(x, y) = L,
(x, y) →_{S} (x, g(y)) if S(x, y) = R,
(x, 0) →_{S} (0, 0),
(0, y) →_{S} (0, 0)

for all x, y > 0. We say that a sequential strategy S is good if (x, y) →_{S}^{∗} (0, 0) whenever (x, y) →^{∗} (0, 0), for all natural numbers x and y.

In Kennaway [5] it is shown that there exists a good strategy for this game.^{3} The sequential reduction strategy (for almost orthogonal TRSs) defined in [5] however is not related to the solution of this abstract game. We present a slightly different solution. Our solution is very close to the sequential reduction strategy that we define in Section 5.

We define a strategy S by distinguishing two cases. If x ⩽ y then we compute the sequence x, f(x), f^{2}(x), … until we reach an f^{n}(x) with n ⩾ 1 such that

• f^{n}(x) = 0, or • f^{n}(x) > x, or

3 The solution described in [5] is attributed to M. van Leeuwen and H. Mulder.

• f^{n}(x) = f^{m}(x) for some 0 ⩽ m < n. Since there are only finitely many different natural numbers less than x, eventually one of these alternatives is satisfied. We define S(x, y) = R if the last alternative holds with m = 0, and S(x, y) = L in all other cases. If x > y then we compute the sequence y, g(y), g^{2}(y), … until we reach a g^{n}(y) with n ⩾ 1 such that

• g^{n}(y) = 0, or

• g^{n}(y) > y, or

• g^{n}(y) = g^{m}(y) for some 0 ⩽ m < n, and we define S(x, y) = L if the last alternative holds with m = 0, and S(x, y) = R in all other cases. Before showing that S is a good strategy, we illustrate the strategy by means of a simple example. Consider the functions

f(x) = \{ \begin{matrix}x + 1 & if x ≠ 7, \\ 6 & if x = 7 \end{matrix}

and

g(x) = \{ \begin{matrix}2x & if x < 5, \\ 0 & if x = 5, \\ x − 1 & if x > 5. \end{matrix}

Starting from the pair (1, 1), the strategy S produces the following sequence:

(1, 1) →_{S} (2, 1) →_{S} (2, 2) →_{S} (3, 2) →_{S} (3, 4) →_{S} (4, 4) →_{S} (5, 4)
→_{S} (5, 8) →_{S} (6, 8) →_{S} (7, 8) →_{S} (7, 7) →_{S} (7, 6) →_{S} (7, 5)
→_{S} (7, 0) →_{S} (0, 0).

Theorem 3.1. The strategy S just defined is a good strategy. Proof. Suppose the contrary. There exist some functions f, g: ℕ_{+} → ℕ and a pair (x, y) ∈ ℕ×ℕ such that the game terminates for (x, y), but the strategy S computes an infinite sequence from (x, y), rather than reaching (0, 0). Thus, there exists a sequence of moves (x, y) →^{∗} (0, 0) and without loss of generality we can assume that the last step in this sequence is (0, ỹ) → (0, 0), for some positive integer ỹ. Hence there exists an n > 0 such that f^{n}(x) = 0. Since S fails to reach (0, 0) from (x, y), the sequence of moves computed by S must reach (with less than n L choices) a state (x′, y′) after which only R choices are made and for all i ⩾ 0, g^{i}(y′) > 0. That is, the infinite →_{S}-sequence starting from (x, y) must have the following form:

(x, y) →_{S}^{∗} (x′, y′) →_{S} (x′, g(y′)) →_{S} (x′, g^{2}(y′)) →_{S} (x′, g^{3}(y′)) →_{S} ⋯,

Suppose that for all i ⩾ 0 g^{i}(y′) is smaller than x′. This implies that the infinite sequence y′, g(y′), g^{2}(y′), … contains a repetition, say g^{p}(y′) = g^{q}(y′) with 0 ⩽ p < q. Let g^{l}(y′) be a maximal element in the cycle g^{p}(y′), g^{p+1}(y′), …, g^{q}(y′). Then, S(x′, g^{l}(y′)) = L, since neither 0 nor a value greater than g^{l}(y′) is found in the cycle g^{p}(y′), g^{p+1}(y′), …, g^{q}(y′). This contradicts that S always chooses R after reaching (x′, y′). Hence, there exists an i ⩾ 0 such that g^{i}(y′) ⩾ x′. From S(x′, g^{i}(y′)) = R we infer that the sequence x′, f(x′), f^{2}(x′), … contains a repetition and no term in it is 0. This contradicts that f^{n}(x) = 0, since x′ = f^{k}(x) for some k ⩾ 0. We can only conclude that S is a good strategy. □

This solution, which easily generalizes to games with n-tuples (n > 2) of natural numbers, epitomizes the problems of a sequential strategy. A sequential strategy has no past memory, it must look at a term and decide which of its redexes to contract—contracting all redexes in turn, which requires past memory, since some redexes may reduce to themselves, is against the rules. Sequential strategies are natural for strongly sequential (NV-sequential) TRSs, since within this class every term t not in normal has a computable redex that must eventually be contracted to compute the normal form of t.

However, sequential strategies are much less natural for non-strongly sequential TRSs and, in fact, they have been thought impossible for some time. The interest in a computable sequential normalizing strategy for arbitrary (almost) orthogonal TRSs lies in its nature and in its very existence. The strategy that we discuss next is not intended to be efficient, though it is conceptually simple enough to be practical. To ensure normalization, parallel strategies rely on past memory, whereas sequential strategies rely on look ahead. An implementation of our strategy could be given past memory, in particular, it could record which redexes have been discovered to cycle, without destroying its sequential essence. An implementation with this feature would in some cases be more time efficient than a parallel strategy at the possible expense of some space efficiency.

4. Cycle Detection

Let S be a (sequential) reduction strategy for a TRS R. In general it is undecidable whether a term t cycles with respect to S. However, it is decidable whether there exists a cycle t →_{S}^{+} t in which all terms have size less than or equal to some positive integer n.

Definition 4.1. Let S be a sequential reduction strategy for a TRS R. We say that a term t S-cycles within size n > 0, denoted by cyclic(t, n, S), if there exists a cycle

t = t_{1} →_{S} t_{2} →_{S} ⋯ →_{S} t_{m} = t

with m > 1 such that |t_{i}| ⩽ n for all i ∈ {1, …, m}.

Lemma 4.2. Let S be a sequential reduction strategy for a TRS R. Let t be a term and suppose n > 0. It is decidable whether t S-cycles within size n. Proof. Since there are no infinite reduction sequences consisting of pairwise different terms whose size does not exceed n, there exists a finite reduction sequence t = t_{1} →_{S} t_{2} →_{S} ⋯ →_{S} t_{m} with m ⩾ 1 such that t_{1}, …, t_{m−1} are pairwise different terms whose size does not exceed n, and one of the following alternatives holds:

• |t_{m}| > n,

• |t_{m}| ⩽ n and t_{m} ∈ NF (R), or

• |t_{m}| ⩽ n and t_{m} = t_{k} for some k ∈ {1, …, m − 1}. The term t S-cycles within size n if and only if the last alternative holds with k = 1. Hence we can decide whether t S-cycles within size n by simply applying the strategy and check which of the above alternatives holds. □

For deciding whether a term S-cycles within size n, we only need to know what the strategy S does to terms whose size does not exceed n. This observation will be used in the next section where we define our strategy by induction on the size of terms. The proof of Lemma 4.2 suggests the ‘algorithm’ of Figure 2 to compute the predicate cyclic.

cyclic(t, n, S) = \{ \begin{matrix}false & if |t| > n or t ∈ NF (R), \\ φ(t, n, S, ∅, t′) & if |t| ⩽ n and t →_{S} t′ \end{matrix}

φ(t, n, S, T, t′) = \{ \begin{matrix}true & if t′ = t, \\ false & if |t′| > n, or t′ ∈ NF (R), or t′ ∈ T, \\ φ(t, n, S, T ∪ \{t′\}, t′′) & if |t′| ⩽ n, and t′ ∉ T ∪ \{t\}, and t′ →_{S} t′′. \end{matrix}

Figure 2.

5. The Strategy

In this section we define our sequential strategy which will be denoted by S_{ω}. The strategy S_{ω} only needs to know whether a term t S_{ω}-cycles within its own size. From now on we abbreviate cyclic(t, |t|, S_{ω}) with ⊙(t).

Definition 5.1. Let t be a reducible term. By induction on |t| we define a redex position S_{ω}(t) ∈ Pos(t). If |t| = 1 then t is a reducible constant and we define S_{ω}(t) = ε. Let t = f(s_{1}, …, s_{n}). If t is a redex then we define S_{ω}(t) = ε. Suppose t is not a redex. Let m be the number of reducible terms among s_{1}, …, s_{n}. We have 1 ⩽ m ⩽ n. The reducible arguments of t are ordered according to their size. If two reducible arguments have the same size, the one to the left is considered first. Formally, there exists an injective map π from {1, …, m} to {1, …, n} such that

• s_{π(i)} is reducible for all i ∈ {1, …, m},

• |s_{π(1)}| ⩽ |s_{π(2)}| ⩽ ⋯ ⩽ |s_{π(m)}|, and

• if |s_{π(i)}| = |s_{π(j)}| with 1 ⩽ i < j ⩽ m then π(i) < π(j). According to the induction hypothesis, S_{ω}(s) is already defined for all terms s with |s| < |t|. Hence we can determine the validity of ⊙(s_{π(i)}) for all i ∈ {1, …, m}. If there is an i ∈ {1, …, m} such that ⊙(s_{π(i)}) does not hold then we take the smallest such i and define S_{ω}(t) = π(i) · S_{ω}(s_{π(i)}). If there is no such i then we let S_{ω}(t) = π(m) · S_{ω}(s_{π(m)}).

It is easy to see that S_{ω} only selects outermost redexes. We find it convenient to introduce some terminology relating to the selection of the arguments s_{π(1)}, …, s_{π(m)} of t in Definition 5.1. If 1 ⩽ i < j ⩽ m then we call s_{π(i)} a predecessor of s_{π(j)} and we call s_{π(j)} a successor of s_{π(i)}. If 1 ⩽ i < m and ⊙(s_{π(i)}) holds then we say that s_{π(i)} is useless in t. So if S_{ω}(t) ⩾ π(k) then all predecessors of s_{π(k)} are useless in t. We conclude this section by illustrating the workings of our strategy S_{ω} on a small example.

Example 5.2. Consider the (almost orthogonal) TRS

R = \{ \begin{matrix}⊤ ∨ x & → & ⊤ \\ x ∨ ⊤ & → & ⊤ \\ ⊥ ∨ ⊥ & → & ⊥ \\ ∞ & → & ∞ \end{matrix}

and the term t_{1} = (⊥∨∞)∨(∞∨(⊤∨⊥)). We have S_{ω}(⊥∨∞) = 2 and hence ⊥∨∞ →_{S_{ω}} ⊥∨∞. So the first argument of t_{1} S_{ω}-cycles within its own size. Therefore S_{ω}(t_{1}) = 2·S_{ω}(∞∨(⊤∨⊥)). Because ⊙(∞) we have S_{ω}(∞ ∨ (⊤ ∨ ⊥)) = 2 · S_{ω}(⊤ ∨ ⊥). The term ⊤ ∨ ⊥ is a redex, so S_{ω}(⊤∨⊥) = ε. We conclude that S_{ω}(t_{1}) = 2·2 and consequently t_{1} →_{S_{ω}} (⊥∨∞)∨(∞∨⊤) = t_{2}. We already know that ⊙(⊥ ∨ ∞). Hence S_{ω}(t_{2}) = 2 · S_{ω}(∞ ∨ ⊤) = 2 since ∞ ∨ ⊤ is a redex. Therefore t_{2} →_{S_{ω}} (⊥ ∨ ∞) ∨ ⊤ = t_{3}. The term t_{3} is a redex and thus t_{3} →_{S_{ω}} ⊤. So our strategy needs three steps to normalize the term t_{1}.

6. Normalization

In this section we establish a relationship between our strategy S_{ω} and so-called outermost-fair reductions. In O’Donnell [8] this concept—O’Donnell uses the terminology eventually outermost—is defined for almost orthogonal TRSs. The definition we give below applies to all TRSs. It is equivalent to the one in Klop [7], except that we only consider infinite reduction sequences.

Definition 6.1. An infinite reduction sequence D is called outermost-fair if there do not exist a position p and an index n ⩾ 1 such that for all i ⩾ n, D[i]_{|p} is an outermost redex in D[i] which is not contracted in the reduction step D[i, i + 1]. If D is not outermost-fair then every position p satisfying the above condition is said to be unfairly treated by D. If a position is unfairly treated by D we also say that the corresponding outermost redex is unfairly treated. These notions carry over to a cycle D via the associated infinite reduction sequence D^{∞}.

Let us illustrate the concept of outermost-fairness by means of two examples. The infinite reduction sequence D_{1}: f(a) → g(f(a)) → g(g(f(a))) → ⋯ with respect to the TRS

\begin{aligned}a & → & b \\ f(x) & → & g(f(x)) \end{aligned}

is outermost-fair since every term in D_{1} contains a single outermost redex which is immediately contracted. The infinite reduction sequence D_{2}: f(a, c) → f(a, d) → f(a, c) → f(a, d) → ⋯ with respect to the TRS

\begin{aligned}a & → & b \\ c & → & d \\ f(x, d) & → & f(x, c) \end{aligned}

is also outermost-fair. Observe that redex a in D_{2} is only half of the time an outermost redex, even though it is never contracted.

Next we show that if S_{ω} fails to normalize a term t then there exists an (infinite) outermostfair reduction sequence starting from t. The proof proceeds in three steps. First we show that every outermost redex unfairly treated in an S_{ω}-reduction sequence is a subterm of an S_{ω}-cyclic subterm (Lemma 6.3). This result is used to show that if a term admits an S_{ω}-cycle then it has a cycle in which no position is unfairly treated (Lemma 6.6). Finally we transform a presupposed infinite S_{ω}-reduction sequence into an outermost-fair reduction sequence by simply inserting enough cycles (Theorem 6.7).

Definition 6.2. Let D be an infinite reduction sequence. We say that a property P of terms eventually holds for D if P holds for all but a finite number of terms in D.

Observe that a position p is unfairly treated by an infinite S_{ω}-reduction sequence D if and only if the property “t_{|p} is an outermost redex in t and S_{ω}(t) ∥ p” eventually holds for D.

Lemma 6.3. If a position p is unfairly treated in an S_{ω}-reduction sequence D then there exist a term t, an index N ⩾ 1, and a position ε < q ⩽ p such that t is S_{ω}-cyclic and D[i]_{|q} = t for all i ⩾ N. Proof. Suppose D: t_{1} →_{S_{ω}} t_{2} →_{S_{ω}} ⋯ is an infinite reduction sequence in which position p is unfairly treated. This implies the existence of an index M in D and a position p such that for all i ⩾ M p is the position of an outermost redex of t_{i} which is never chosen by S_{ω}. Since S_{ω} is an outermost strategy, it cannot be unfair to position ε, consequently p ≠ ε. Thus, S_{ω} treats p unfairly only by continuously choosing from M onwards some position disjoint from p, despite the fact that p is the position of an outermost redex. In D, infinitely many choices of S_{ω} must fall under some position q (possibly ε) above p, but only finitely many can fall under some other position (possibly p itself) below q. More precisely, there exist a position q and a positive integer k such that

• q·k ⩽ p,

• S_{ω}(t_{i}) > q for infinitely many values of i ⩾ M, and

• S_{ω}(t_{i}) > q·k for finitely many values of i ⩾ M. Hence there exists an index N in D, N ⩾ M, such that no choice of S_{ω} falls under q·k from N onwards, i.e., there is no i ⩾ N such that S_{ω}(t_{i}) > q·k. The subterm of t_{N} at q is compound, since q is strictly above p. Let t_{N}_{|q} = f(s_{1}, …, s_{n}). Since for all i ⩾ M, p is the position of an outermost redex of t_{i} which is never chosen by S_{ω}, no reduction ever takes place above p from M onwards. Thus, for all i ⩾ N, t_{i}_{|q} is of the form f(s_{1}^{i}, …, s_{n}^{i}). Since for all i ⩾ N, no reduction takes place below q·k, s_{k}^{i} = s_{k} for all i ⩾ N. We show that s_{k} is S_{ω}-cyclic. Since infinitely many reductions take place below position q, according to the pigeon-hole principle there exists a j ∈ {1, …, n} such that S_{ω}(t_{i}) ⩾ q·j for infinitely many values of i ⩾ N. Let I be the set of these values. For any i ∈ I, either s_{k} is a predecessor of s_{j}^{i}, or s_{k} is a successor of s_{j}^{i}. First suppose that s_{k} is a successor of s_{j}^{i} for all i ∈ I. This implies that the sequence

s_{j}^{i_{1}} →_{S_{ω}} s_{j}^{i_{2}} →_{S_{ω}} s_{j}^{i_{3}} →_{S_{ω}} ⋯

where I = {i_{1}, i_{2}, i_{3}, …} with i_{1} < i_{2} < i_{3} < ⋯, contains a cycle, for otherwise there would be an l ∈ I such that |s_{j}^{l}| > |s_{k}| and consequently s_{k} would be a predecessor of s_{j}^{l}. Let s_{j}^{m} (with m ∈ I) be a biggest term in such a cycle. Then, s_{j}^{m} cycles within its own size. Hence s_{j}^{m} is useless in t_{m}_{|q}, which is impossible since m ∈ I. We conclude that there exists an i ∈ I such that s_{k} is a predecessor of s_{j}^{i}. This implies that s_{k} is useless in t_{i}_{|q} since a redex in s_{j}^{i} is selected by S_{ω}. Therefore s_{k} is S_{ω}-cyclic, which proves the lemma. □

The following technical result states that if S_{ω} selects a redex in subterm t_{|p} of t, then instead of applying S_{ω} to t we can also replace its subterm t_{|p} by the result of applying S_{ω} to t_{|p}, without changing the final outcome. This does not hold if the contractum of a redex depends on the term in which the redex occurs (cf. the remarks in Section 2).

Lemma 6.4. If S_{ω}(t) ⩾ p then tS_{ω} = t[t_{|p}S_{ω}]_{p}. Proof. We use induction on the position p. If p = ε then the result trivially holds. Suppose p = i·q. In the following we write t_{i} instead of t_{|i}. From the definition of S_{ω} we infer that S_{ω}(t) = i · S_{ω}(t_{i}). Hence

tS_{ω} = t[contract(t_{|S_{ω}(t)})]_{S_{ω}(t)}
= t[contract(t_{|i·S_{ω}(t_{i})})]_{i·S_{ω}(t_{i})}
= t[t_{i}[contract(t_{|i·S_{ω}(t_{i})})]_{S_{ω}(t_{i})}]_{i}
= t[t_{i}[contract(t_{i}_{|S_{ω}(t_{i})})]_{S_{ω}(t_{i})}]_{i}
= t[t_{i}S_{ω}]_{i}.

Since S_{ω}(t_{i}) ⩾ q, the induction hypothesis yields t_{i}S_{ω} = t_{i}[(t_{i}_{|q})S_{ω}]_{q} and therefore

tS_{ω} = t[t_{i}[t_{i}_{|q}S_{ω}]_{q}]_{i}
= t[t_{i}_{|q}S_{ω}]_{i·q}
= t[t_{|p}S_{ω}]_{p}.

□

Lemma 6.5. Let D be any S_{ω}-reduction sequence. If p is a position in D[1] such that no redex at a position q < p is contracted in D, then D_{|p} is an S_{ω}-reduction sequence. Proof. Let t → tS_{ω} be an arbitrary reduction step in D. We have to show that t_{|p} →_{S_{ω}}^{∗} tS_{ω}_{|p}. If S_{ω}(t) ∥ p then tS_{ω}_{|p} = (t[contract(t_{|S_{ω}(t)})]_{S_{ω}(t)})_{|p} = t_{|p}. If S_{ω}(t) ⩾ p then tS_{ω}_{|p} = (t[t_{|p}S_{ω}]_{p})_{|p} = t_{|p}S_{ω} by using Lemma 6.4, and hence t_{|p} →_{S_{ω}} tS_{ω}_{|p}. □

Lemma 6.6. If a term t S_{ω}-cycles then there exists a cycle of t in which every position is fairly treated. Proof. From an S_{ω}-cycle of t we construct a new cycle of t in which every position of t is fairly treated. We prove the lemma by structural induction on t. Let D be an S_{ω}-cycle of t. If t is a constant then it is contracted in D and the only position of t, ε, is treated fairly. Suppose t = f(s_{1}, …, s_{n}) and let P be the set of all positions that are unfairly treated by D. Observe that P ⊂ Pos(t). Let p ∈ P. We show that there exists a cycle D_{p} of t in which position p is fairly treated. Since an outermost strategy cannot treat unfairly position ε, p ≠ ε. Hence p = k · p′ for some k ∈ {1, …, n}. We show that s_{k} S_{ω}-cycles. If a redex in s_{k} is contracted in D then Lemma 6.5 gives us an S_{ω}-cycle of s_{k}, namely D_{|k}: s_{k} →_{S_{ω}}^{+} s_{k}. If no redex in s_{k} is contracted in D, then p′ is a position unfairly treated in D^{∞}, the S_{ω}-reduction sequence of t. In this situation, Lemma 6.3 proves the existence of an S_{ω}-cyclic term at or below position k. Thus, s_{k} is S_{ω}-cyclic also if no redex in s_{k} is contracted in D. Since s_{k} S_{ω}-cycles and is a proper subterm of t, according to the induction hypothesis there exists a cycle of s_{k}, say D_{p′}, in which position p′ is fairly treated. By adding context, we construct a cycle of t in which position p is fairly treated. More precisely, let C be the context t[□]_{k} and define D_{p} = C[D_{p′}]. Now D_{p} is a cycle of t in which position p is fairly treated. The concatenation of D and D_{p} is a cycle of t that is fair to p. Thus, all that remains to be done is to extend D with a “corrective” cycle for each position unfairly treated. Suppose P = {p_{1}, …, p_{m}}. The reduction sequence D; D_{p_{1}}; …; D_{p_{m}} is a cycle of t in which every position is fairly treated. □

Our main theorem is easily derived from the preceding lemma.

Theorem 6.7. If S_{ω} fails to normalize some term then there exists an outermost-fair reduction sequence starting from that term. Proof. Suppose D is an infinite S_{ω}-reduction sequence. For every i ⩾ 1 we define a reduction sequence D_{i}: D[i] →^{∗} D[i] as follows. Let P_{i} ⊆ Pos(D[i]) be the set of all positions p with the property that D[i]_{|p} S_{ω}-cycles. From the preceding lemma we learn that for every p ∈ P_{i} there exists a cycle D_{p} of D[i] in which every position is fairly treated. We define D_{i} as the concatenation of all those cycles. (If P_{i} = ∅ then D_{i} is the empty reduction sequence from D[i] to D[i], otherwise D_{i} is a cycle of D[i].) Now it is easy to see that the sequence D_{1}; D[1, 2]; D_{2}; D[2, 3]; D_{3}; D[3, 4]; … is outermost-fair. □

O’Donnell [8] obtained the following result.

Theorem 6.8. Let R be an almost orthogonal TRS. If a term admits an outermost-fair reduction sequence then it does not have a normal form. □

The normalization of the parallel-outermost strategy for almost orthogonal TRSs is an immediate consequence of Theorem 6.8. Actually from Theorem 6.8 it follows that parallel-outermost is hypernormalizing, i.e., we are able to find normal forms even if we perform (finitely many) arbitrary reductions between successive applications of the parallel-outermost strategy. This in turn implies the hypernormalization of the full-substitution or Gross-Knuth strategy for almost orthogonal TRSs (cf. O’Donnell [8]).

Combining Theorem 6.8 with Theorem 6.7 yields the normalization of S_{ω} for almost orthogonal TRSs.

Corollary 6.9. The strategy S_{ω} is normalizing for almost orthogonal TRSs. □

It should be noted that, unlike parallel-outermost, S_{ω} is not hypernormalizing. An example is provided by the TRS

\begin{aligned}a & → & f(b) \\ f(b) & → & a \\ c & → & d \\ g(x, d) & → & d \end{aligned}

The term g(a, c) is normalized by S_{ω}: g(a, c) → g(f(b), c) → g(f(b), d) → d. However, if we contract the leftmost-outermost redex f(b) after the first S_{ω}-step g(a, c) → g(f(b), c), we obtain a cycle.

7. Concluding Remarks

The ingenious proof of Theorem 6.8 in O’Donnell [8] is not easily digested. In the appendix of Bergstra and Klop [1] O’Donnell’s proof is presented in a more accessible setting and is also generalized to combinatory reduction systems. (Although only orthogonal systems are considered in [1], the presence of trivial overlays doesn’t cause any problems.) We would like to remark that for orthogonal TRSs Theorem 6.8 is easily derived from the work of Huet and Lévy [4] on needed reduction: it is not difficult to show that in every outermost-fair reduction sequence infinitely many needed redexes are contracted. In Section 2 we already remarked that the restriction to orthogonal TRSs is essential in the work of Huet and Lévy. Sekar and Ramakrishnan [13] showed that by generalizing the concept of needed redex to necessary set of redexes the main results of [4] carry over to the almost orthogonal case. In particular, contraction of necessary sets of redexes is hypernormalizing.

It is interesting to note that (in the case of almost orthogonal TRSs) the normalization of both the parallel-outermost strategy and our sequential strategy S_{ω} is based on Theorem 6.8. So it is worthwhile to try to extend Theorem 6.8 to a more general class of TRSs. Van Raamsdonk [12] recently obtained the following result.

Theorem 7.1. Let R be a weakly orthogonal TRS. If a term admits an outermost-fair reduction sequence then it does not have a normal form. □

Corollary 7.2. The strategy S_{ω} is normalizing for weakly orthogonal TRSs. □

As a matter of fact, van Raamsdonk proves her result for the much larger class of (weakly orthogonal) Higher-Order Rewriting Systems of van Oostrom [9]. We believe that also the class of strongly sequential left-linear root-balanced joinable TRSs considered by Toyama [14] should fall within the scope of Theorem 6.8.

Whereas all infinite reduction sequences produced by the parallel-outermost strategy are outermost-fair, this is not the case for S_{ω}. The following example shows that S_{ω} ignores an outermost redex when it ‘believes’ that there is no reason to contract it.

Example 7.3. Consider the TRS

\begin{aligned}a & → & b \\ c & → & c \\ f(b, x) & → & f(a, x) \end{aligned}

and the term t = h(f(a, b), g(g(c))). We have f(a, b) →_{S_{ω}} f(b, b) →_{S_{ω}} f(a, b), so the first argument of t S_{ω}-cycles within its own size. Hence the second argument of t is selected for reduction, which of course gives t →_{S_{ω}} t. Thus S_{ω} produces an infinite reduction sequence in which position 1·1 (corresponding to outermost redex a) is unfairly treated.

In the above example both arguments of the term under consideration S_{ω}-cycle within their own size. Since the TRS is (almost) orthogonal, we might as well stop the evaluation since the term cannot have a normal form. This is justified by our next result.

Theorem 7.4. Let R be an almost orthogonal TRS and t = f(s_{1}, …, s_{n}) a term that is neither a redex nor a normal form. If for all i ∈ {1, …, n} s_{i} is a normal form or ⊙(s_{i}) then ⊙(t). Proof. Since all reducible arguments of t are S_{ω}-cyclic within their own size, t itself is S_{ω}-cyclic within its own size, unless after some contractions in its S_{ω}-cyclic arguments a redex is created, say t →_{S_{ω}}^{+} f(s′_{1}, …, s′_{n}) = t′ with t′ a redex. For all i ∈ {1, …, n} we have s_{i} →_{S_{ω}}^{∗} s′_{i} →_{S_{ω}}^{∗} s_{i}, hence redex t′ can be rewritten to t by internal (i.e. at positions different from ε) contractions. Because R is almost orthogonal, redexes cannot be destroyed by internal contractions. Therefore t must be a redex, contrary to the assumption. We conclude that t S_{ω}-cycles within its own size. □

According to Corollary 6.9, in the case of almost orthogonal TRSs, ⊙(t) implies that t has no normal form. Hence Theorem 7.4 shows how our strategy can be used to detect non-termination. If we are faced with a redex t, we can of course also check whether ⊙(t) holds in order to avoid unnecessary infinite computations. These considerations do not generalize to arbitrary TRSs, as shown in the next example.

Example 7.5. Consider the TRS

\begin{aligned}a & → & b \\ b & → & a \\ c & → & c \\ f(b, x) & → & d \end{aligned}

and the term t = f(a, c). Both arguments of t S_{ω}-cycle within their own size. Nevertheless t has a normal form which can be reached by means of the outermost reduction sequence

f(a, c) → f(b, c) → d.

Observe that S_{ω} will select redex c in t and hence produce an infinite reduction sequence that is not outermost-fair. It should be noted that the above TRS is not root-balanced joinable (in the terminology of Toyama [14]).

One possibility to extend the class of systems for which our strategy is normalizing is that in the case all reducible arguments of a term that is not a redex S_{ω}-cycle within their own size, we may look for a combination of terms in these cycles that creates a redex upwards. For instance, in the above example we see that the combination b and c in the cycles a →_{S_{ω}} b →_{S_{ω}} a and c →_{S_{ω}} c creates the redex f(b, c) which contracts to normal form d. Even if such a combination does not exist we can still test whether it is possible to redefine the mapping rule—which assigns rewrite rules to redexes—in such a way that the present deadlock situation disappears, at least temporarily. These ideas should be investigated further.

In the final example of the paper we justify our earlier claim that our sequential strategy S_{ω} sometimes succeeds where parallel-outermost fails.

Example 7.6. Consider the non-left-linear TRS

R = \{ \begin{matrix}f(x, x) & → & a \\ g(x) & → & f(x, g(x)) \\ c & → & g(c) \end{matrix}

of Klop [6]. This well-known TRS shows that non-left-linearity destroys confluence, even in the absence of critical pairs. The following reduction sequence shows that our strategy S_{ω} normalizes the constant c:

c →_{S_{ω}} g(c) →_{S_{ω}} f(c, g(c)) →_{S_{ω}} f(g(c), g(c)) →_{S_{ω}} a,

whereas the parallel-outermost strategy produces an infinite outermost-fair sequence:

c →^{∗} g(c) →^{∗} f(c, g(c)) →^{∗} f(g(c), f(c, g(c))) →^{∗} ⋯

Unfortunately, our strategy S_{ω} does not normalize all terms of R. For instance, a term like f(g(c), g(g(c))) can only be normalized if we allow contraction of redexes that are not outermost.

Nevertheless, it can be shown that the set of terms which can be normalized by S_{ω} properly includes those for which parallel-outermost succeeds. Of course, if we drop the rewrite rule g(x) → f(x, g(x)) from R then we obtain a confluent TRS for which our strategy S_{ω}, unlike parallel-outermost, is normalizing.

This example shows in particular that Theorem 6.8 doesn’t hold for non-left-linear TRSs (without critical pairs).

References

1. J.A. Bergstra and J.W. Klop, Conditional Rewrite Rules: Confluence and Termination, Journal of Computer and System Sciences 32(3), pp. 323–362, 1986.

2. H. Comon, Sequentiality, Second Order Monadic Logic and Tree Automata, Proceedings of the 10th IEEE Symposium on Logic in Computer Science, San Diego, pp. 508–517, 1995.

3. N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, Vol. B (ed. J. van Leeuwen), North-Holland, pp. 243–320, 1990.

4. G. Huet and J.-J. Lévy, Computations in Orthogonal Rewriting Systems, I and II, in: Computational Logic, Essays in Honor of Alan Robinson (eds. J.-L. Lassez and G. Plotkin), The MIT Press, pp. 396–443, 1991. Previous version: Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems, report 359, INRIA, 1979.

5. J.R. Kennaway, Sequential Evaluation Strategies for Parallel-Or and Related Reduction Systems, Annals of Pure and Applied Logic 43, pp. 31–56, 1989.

6. J.W. Klop, Combinatory Reduction Systems, Ph.D. thesis, Mathematical Centre Tracts 127, Centre for Mathematics and Computer Science, Amsterdam, 1980.

7. J.W. Klop, Term Rewriting Systems, in: Handbook of Logic in Computer Science, Vol. II (eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, pp. 1–116, 1992.

8. M.J. O’Donnell, Computing in Systems Described by Equations, Lecture Notes in Computer Science 58, 1977.

9. V. van Oostrom, Confluence for Abstract and Higher-Order Rewriting, Ph.D. thesis, Vrije Universiteit, Amsterdam, 1994.

10. M. Oyamaguchi, NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term Rewriting Systems, SIAM Journal on Computation 22(1), pp. 114-135, 1993.

11. S. Porat and N. Francez, Fairness in Term Rewriting Systems, Methods of Logic in Computer Science 1, pp. 141–181, 1994.

12. F. van Raamsdonk, On Normalising Strategies, Proceedings of the 2nd International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Paderborn, Lecture Notes in Computer Science, 1995. To appear.

13. R.C. Sekar and I.V. Ramakrishnan, Programming in Equational Logic: Beyond Strong Sequentiality, Information and Computation 104(1), pp. 78–109, 1993.

14. Y. Toyama, Strong Sequentiality of Left-Linear Overlapping Term Rewriting Systems, Proceedings of the 7th IEEE Symposium on Logic in Computer Science, Santa Cruz, pp. 274– 284, 1992.