Termination of context-sensitive rewriting by rewriting ^{⋆}

Salvador Lucas

Departamento de Sistemas Informáticos y Computación Universidad Politécnica de Valencia Camino de Vera s/n, E-46071 Valencia, Spain.

                        e.mail: slucas@dsic.upv.es

Abstract. Context-sensitive rewriting allows us to deal with certain context-replacing restrictions in performing reduction steps. This is useful in avoiding undesirable reductions. In this paper, we study termination of context-sensitive rewriting. We give some conditions under which it is possible to analyze the termination of the context-sensitive rewrite relation induced by a term rewriting system by means of any method to prove termination of rewriting. This allows us to apply all known (and forthcoming) results on termination to context-sensitive rewriting.

Keywords: term rewriting, functional programming, termination.

1 Introduction

Term Rewriting is traditionally considered the operational semantics of functional programming languages [3, 16]. A functional program is a set of equations that are interpreted as left-to-right rewrite rules [5, 15]. Execution of the program for any input data consists of the evaluation of the term using the rewrite rules until it cannot be further reduced (i.e. until a normal form is reached). In a terminating system, no infinite computations are possible.

In context-sensitive rewriting [12, 13], for each symbol in the signature Σ we fix the set of replacing arguments by means of a mapping μ : Σ → ℘(IN) (the replacement map) which specifies the set of positions which can eventually be reduced. This is useful to express some requirements on the ‘intended meaning’ of a function. For example, consider the standard functional definition of the if-then-else operation:

if(true, x, y) → x

if(false, x, y) → y

Given an input if(cond, t, s), we are not interested in reductions on the second and third arguments of the operation if until the condition cond has been evaluated. By defining a replacement map such as μ(if) = {1}, the undesirable reductions on the second and third immediate subterms of the term if(cond, t, s) can be avoided with no extra control.

⋆ This work has been partially supported by CICYT under grant TIC 95-0433-C03-03.

Context-sensitive rewriting has some strong connections with the lazy strategies of functional programming languages. Actually, the mechanism which allows us to prevent the evaluation of some expressions can also be used to declare that these reductions need not to be done. Although giving support to lazy reduction techniques is not the main motivation of our work, context-sensitive rewriting does allow us to express fixed, meaningful and easily implementable restrictions on rewriting, similarly to the way that lazy reduction techniques approximate ‘needed’ reductions à la Huet and Lévy [10]. An approach to these questions which is related with our work can be found in [9].

In this paper, we address the problem of the termination of context-sensitive rewriting by using any method to prove that a TRS terminates. Termination of rewriting is normally proved by defining a noetherian ordering > on terms and checking whether t > s whenever t → s (Manna and Ness’ theorem, [14]). This is equivalent to proving that each instance of every rule l → r in the TRS satisfies l > r in a monotonic noetherian ordering > (Kamin and Lévy, [8]). As suggested by Manna and Ness, ‘it is often convenient to separate reduction orderings into a homomorphism from terms to an algebra with a noetherian ordering’. This can be achieved by means of termination functions [2, 4]. A termination function is a homomorphism from terms to a Σ-algebra (where Σ is the underlying signature). It can also be considered as an extraction function from terms to multisets of selected immediate subterms (see [4]). We show that we can often prove termination of context-sensitive rewriting by first transforming the original TRS into a contracted TRS on a new signature by means of a contracting function. This function can be thought of as a pseudo-termination function in that it projects the original set of terms onto a new set of contracted terms on which we can use the standard methods.

The paper is organized as follows. In Section 2, we briefly recall the technical concepts used in the remainder of the paper. In Section 3, we formulate some basic properties of context-sensitive rewriting. Section 4 provides two basic criteria to ensure termination of context-sensitive rewriting. Section 5 concludes.

2 Preliminaries

Let us first introduce the main notations used in the paper from [5, 11]. V denotes a countable infinite set of variables and Σ denotes a set of function symbols {f, g, …}, each with a fixed arity given by a function ar : Σ → IN. By T (Σ, V) we denote the set of terms. V ar(t) is the set of variable symbols in the term t.

Terms are viewed as labelled trees in the usual way. Occurrences u, v, … are represented by chains of positive natural numbers used to address subterms of t. Occurrences are ordered by the standard prefix ordering: u ≤ v iff there is a chain v′ such that v = u.v′. O(t) denotes the set of occurrences of a term t. t|_{u} is the subterm at occurrence u of t. t[s]_{u} is the term t with the subterm at the occurrence u replaced with s. We refer to any term C that is the same as t everywhere except below u, i.e. there exists a term s such that C[s]_{u} = t, as the context within the replacement occurs.

A rewrite rule is an ordered pair (l, r), written l → r, with l, r ∈ T (Σ, V), l ∉ V and V ar(r) ⊆ V ar(l). l is said to be the left-hand side (lhs) of the rule and r is the right-hand side (rhs). A TRS is a pair R = (Σ, R) where R is a set of rewrite rules. For a given TRS R = (Σ, R), a term t rewrites to a term s (at the occurrence u), written t →_{R} s, if t|_{u} = σ(l) and s = t[σ(r)]_{u}, for some rule l → r in R, occurrence u in t and substitution σ. →_{R} is the one-step rewrite relation for R.

IN_{k}^{+} is an initial segment {1, 2, … k} of the set of positive natural numbers IN^{+}, where IN_{0}^{+} = Ø. We let R denote a binary relation on A, i.e., R ⊆ A × A. We will often write xRy for (x, y) ∈ R. We let R^{∗} denote the reflexive-transitive closure of R. A relation R is noetherian (or terminating) iff there is no infinite sequence a_{1}R a_{2} ⋯ a_{n}R a_{n+1} · · ·.

Given a set A, we denote a k-tuple x_{1}, …, x_{k} of elements as x̃, i.e. x̃ ∈ A^{k}. By x̃[y]_{i} for any i, 1 ≤ i ≤ k we denote a k-tuple where x_{i} is replaced by y in x̃. Given a k-tuple x̃ and a set of positive natural numbers J = {j_{1}, …, j_{q}} ⊆ IN_{k}^{+}, denote as x̃_{J} the q-ary tuple of elements in x̃ extracted by J, i.e. x̃_{J} = x_{j_{1}}, …, x_{j_{q}}. Note that the i-th component x_{i} of x̃ is the |IN_{i}^{+} ∩ J|-th component of x̃_{J}. Given a set B, a function ψ : A → B and a k-ary tuple x̃ ∈ A^{k}, we denote as ψ(x̃) the k-ary tuple of transformed-by-ψ elements, i.e. ψ(x_{1}), …, ψ(x_{k}).

3 Context-sensitive rewriting

3.1 Basic definitions of context-sensitive rewriting

The idea behind the concept of context-sensitive rewriting [12, 13] is to impose a syntactic replacement condition which prevents some reductions. This is achieved by using a map on the signature we call replacement map.

Definition 3.1 (Replacement map) Let Σ be a signature. A mapping μ : Σ → ℘(IN) is a replacement map (or Σ-map) for the signature Σ iff for all f ∈ Σ. μ(f) ⊆ N_{ar(f)}^{+}.

The ordering ⊆ on ℘(IN) extends to an ordering ⊑ on M_{Σ}, the set of all Σ-maps: μ ⊑ μ′ iff μ(f) ⊆ μ′(f) for all f ∈ Σ. It is immediate to see that (M_{Σ}, ⊑, μ_{⊥}, μ_{⊤}) is a complete lattice where μ_{⊥}(f) = Ø and μ_{⊤}(f) = IN_{ar(f)}^{+} for all f ∈ Σ.

The replacement map determines the argument positions which can be reduced for each symbol on the signature. The replacement condition indicates the occurrences which can be rewritten.

Definition 3.2 (Replacement condition) Let Σ be a signature and μ be a Σ-map. Let t ∈ T (Σ, V) be a term. The replacement condition is a relation γ_{μ,t} defined on the set of occurrences O(t) as follows:

γ_{μ,t}(ε).

γ_{μ,f(t̃[s]_{i})}(i.u) ⇔ (i ∈ μ(f)) ∧ γ_{μ,s}(u). We say that the occurrence u of a term t satisfies the replacement condition γ_{μ,t} iff γ_{μ,t}(u).We also say that u is a replacing occurrence of t or that the subterm t|_{u} is a replacing subterm.

We write γ_{t}(u) when the replacement map is clear from the context. Some new notation entailed by the concept of replacement condition: O^{μ}(t) is the set of replacing occurrences of a term t: u ∈ O^{μ}(t) ⇔ u ∈ O(t) ∧ γ_{t}(u). O_{s}^{μ}(t) is the (possibly empty) set of replacing occurrences of a subterm s of t: u ∈ O_{s}^{μ}(t) ⇔ u ∈ O^{μ}(t) ∧ t|_{u} = s. V ar^{μ}(t) is the set of replacing variables of t: x ∈ V ar^{μ}(t) ⇔ O_{x}^{μ}(t) ≠ Ø.

Definition 3.3 (One-step context-sensitive rewrite relation) Let R = (Σ, R) be a TRS and μ be a Σ-map. A term t μ-rewrites to a term s, written t ↪_{R(μ)} s, if t →_{R} s at the replacing occurrence u ∈ O^{μ}(t). ↪_{R(μ)} is the onestep context-sensitive rewrite relation of R wrt μ. ↪_{R(μ)}^{∗} is the context-sensitive rewrite relation of R wrt μ.

In the sequel, we assume that the TRS R = (Σ, R) and Σ-map μ are given, and we drop references to them by just writing ↪ instead of ↪_{R(μ)} to denote the one-step context-sensitive rewrite relation.

Example 3.4 Let ρ : f(x) → x be a rule and t = g(f(a), f(b)) be a term.

a) If μ(g) = Ø, then ρ cannot be applied to reduce t, because neither the occurrence u = 1 nor u = 2 satisfy the replacement condition wrt μ.

b) If μ(g) = {1}, then ρ can be applied to reduce f(a), but it cannot be applied to reduce f(b).

c) If μ(g) = {2}, then ρ can be applied to reduce f(b), but it cannot be applied to reduce f(a).

d) If μ(g) = {1, 2}, then ρ can be applied to reduce both f(a) and f(b).

By analogy to standard rewriting, context-sensitive is closed under replacing context application, i.e., t ↪ s ⇒ C[t]_{u} ↪ C[s]_{u} for every u ∈ O^{μ}(C).

Remark 3.5 Note that with the top Σ-map μ_{⊤} the replacement condition is satisfied for every term t and occurrence u ∈ O(t). This is to say that, given a TRS R, the one-step context-sensitive rewrite relation for μ_{⊤} coincides with the standard one-step rewrite relation, i.e. ↪_{R(μ_{⊤})}=→_{R}.

Given a TRS, the following proposition relates the one-step context-sensitive rewrite relations induced by comparable replacement maps.

Proposition 3.6 (Monotonicity of ↪ with respect to ⊑) Let R = (Σ, R) be a TRS and μ, μ′ be Σ-maps. Then μ ⊑ μ′ ⇒ ↪_{R(μ)}⊆ ↪_{R(μ′)}.

3.2 Examples of application

Improving the evaluation of expressions.

The rules which define the short-cut boolean operators and, or of Lisp are:

\begin{matrix}and(true, x) → x & or(true, x) → true \\ and(false, x) → false & or(false, x) → x \end{matrix}

It is sensible to evaluate up to the normal form the first argument of an input term and(t, s) (or(t, s)), since the outcome is necessary to determine which rule has to be applied to the root. According to the rules, if the first argument reduces to false (true), then any reduction on the second argument is useless, since it does not contribute to computing the value of the resulting expression.

A replacement map μ(and) = μ(or) = {1}, has the effect of delaying the evaluation of redexes which are different from the first argument of the term.

In manipulating lists, another case of study arises. Let us consider the head and tail functions, whose behavior is as follows:

\begin{matrix}head(x :: L) → x \\ tail(x :: L) → L \end{matrix}

head only requires the evaluation of the head of the list and tail only evaluates the rest of the list. This points are only of interest if cons (i.e. ‘::’) does not evaluate its arguments systematically. Programming Languages have been conceived where cons does not evaluate its arguments (or, at least it does not evaluate its second argument) (see [6, 11]). This behavior can easily be achieved in context-sensitive rewriting, by defining μ(::) = Ø (or μ(::) = {1}).

Mechanizing Inference Systems.

Context-sensitive rewriting can be formulated as an Inference System by considering each rewrite rule l → r as a (scheme of) axiom: _{\overline{l→r}}, and introducing as many context-passing rules [11] as replacing indices i ∈ μ(f) for each k-ary function symbol ‘f’ in the signature. That is, for each replacing argument position i, we define the (scheme of) rule \frac{t→s}{f(t_{1},...,t_{i−1},t,...,t_{k})→f(t_{1},...,t_{i−1},s,...,t_{k})}.

Different computational systems have been formalized by using Inference Systems whose axioms and rules match these patterns, as they are weak β-reduction, call-by-name reduction strategies of λ-calculus, and π-calculus. Therefore, we can use context-sensitive rewriting as a suitable mechanization of the execution of processes of these systems. In this way, we can exploit existing rewriting devices (reduction machines, graph reduction, etc.) for efficient implementations [7, 15].

4 μ-termination

We would like to compare the termination behavior of the standard rewriting in a given TRS R and the context-sensitive rewriting in R given a replacement map. To distinguish them, we introduce the following preparatory definition.

Definition 4.1 (μ-termination) Let R = (Σ, R) be a TRS and μ be a Σ-map. We say that R μ-terminates (or R is μ-terminating) iff ↪_{R(μ)} is noetherian.

Proposition 4.2 Let R = (Σ, R) be a TRS. Let μ, μ′ be two Σ-maps such that μ ⊑ μ′. If R μ′-terminates, then R μ-terminates.

Proof. By contradiction, using Proposition 3.6. □

Now we consider the Remark 3.5 to show that any criteria establishing the termination of a TRS R also establishes the μ-termination of R.

Theorem 4.3 Let R = (Σ, R) be a TRS and μ be a Σ-map. If R terminates, then R μ-terminates.

Proof. Immediate from Proposition 4.2, since →_{R}=↪_{R(μ_{⊤})}. □

From Theorem 4.3, we can directly use any ordering > on T (Σ, V) (for example the recursive path ordering >^{∗} in [1, 2]) to check μ-termination of the contextsensitive rewriting by just considering the rules in the TRS (without taking into account the replacement map). Actually we only need to prove that σ(l) > σ(r) for all rules l → r in the TRS and substitutions σ. If this comparison succeeds, then Theorem 4.3 ensures that any context-sensitive rewriting will terminate. We refer to this method as the C_{R}-criterion to check μ-termination. Nevertheless, we can consider many μ-terminating TRSs despite the fact that the C_{R}-test does not succeed.

Example 4.4 Let us consider the nonterminating TRS R = ({f, g}, {f(g(x), y) → f(x, f(g(x), y))}). If we take μ such that μ(f) = μ(g) = {1}, then it is easy to verify that any μ-rewriting on R will eventually terminate.

The example shows that the C_{R}-criterion is not complete. It also illustrates that, when comparing the lhs and rhs of a rewrite rule l → r in order to determine μ-termination of the TRS, we only need to take into account the replacing arguments occurring in l and r. Roughly speaking, since μ(f) = {1} we would find l > r, i.e. f(g(x), y) > f(x, f(g(x), y)) if we forget the second immediate argument both in f(g(x), y) and f(x, f(g(x), y)). This is similar to checking whether f(g(x), □) > f(x, □) (where □ expresses the ‘unnecessary’ arguments, that will not be taken into account in order to prove l > r). This idea will be formalized in the following sections.

4.1 The contractive transformation

In the following section, we are able to state an interesting result: we can investigate μ-termination of a TRS by studying termination of a contracted TRS built using a new signature we call μ-contracted signature which we define as follows.

Definition 4.5 (μ-contracted signature) Let Σ be a signature and μ be a Σmap. The μ-contracted signature Σ^{μ} is as follows: f_{μ} ∈ Σ^{μ} ∧ ar(f_{μ}) = |μ(f)| ⇔ f ∈ Σ.

We connect terms from both signatures Σ and Σ^{μ} by means a function.

Definition 4.6 (μ-contracting function) Let Σ be a signature and μ be a Σ-map. The μ-contracting function τ_{μ} : T (Σ, V) → T (Σ^{μ}, V) is as follows:

– τ_{μ}(x) = x if x ∈ V – τ_{μ}(f(t̃)) = f_{μ}(τ_{μ}(t̃_{μ(f)}))

Note that this function drops the non-replacing immediate subterms of a term t and constructs a ‘μ-contracted’ term by joining the (also transformed) replacing subterms below the corresponding operator of the μ-contracted signature. See below for an illustrative example.

We can observe that this is not a termination function (see [4]) since it is neither a homomorphism (the operations in the contracted signature could have a lesser arity than the corresponding operation in the original one) nor an extraction function (because (i) the extracted-by-μ subterms are joined by a new function symbol of the contracted signature and (ii) the subterms are also transformed by the contracting function). Nevertheless, it deals with a task similar to termination functions, i.e., translating the original set of terms T (Σ, V) into a set (in this case T (Σ^{μ}, V)) on which we can demonstrate the terminating behavior of context-sensitive rewriting.

Example 4.7 (Continued from Example 4.4) We can transform the TRS under consideration into a ‘contracted’ TRS R^{μ} by applying τ_{μ}. This gives: R^{μ} = ({f_{μ}, g_{μ}}, {f_{μ}(g_{μ}(x)) → f_{μ}(x)}).

The next proposition shows how the μ-contracting function changes the location of the immediate subterms.

Proposition 4.8 Let Σ be a signature and μ be a Σ-map. If i ∈ μ(f), then we have τ_{μ}(f(t̃[s]_{i})) = f_{μ}(τ_{μ}(t̃_{μ(f)}[s]_{j})) with j = |IN_{i}^{+} ∩ μ(f)|.

Proof. Immediate from definition of τ_{μ}. □

From this proposition, we know that the i-th immediate (replacing) subterm of t = f(t̃) becomes the |N_{i}^{+} ∩ μ(f)|-th immediate subterm of τ_{μ}(t).

Proposition 4.9 (Surjectivity of τ_{μ}) The μ-contracting function τ_{μ} is surjective. That is, for each s ∈ T (Σ^{μ}, V), there exists t ∈ T (Σ, V) such that s = τ_{μ}(t).

Proof. By structural induction on s ∈ T (Σ^{μ}, V).

1. Base case. If s = x ∈ V, define t = x. If s is a constant f_{μ}, let f be the corresponding symbol of Σ. Then we consider the following two cases:

(a) ar(f) = 0. Define t = f.

(b) ar(f) > 0. By definition of τ_{μ}, this means that μ(f) = Ø. Then, we let

t = f(t̃) for any t̃∈ T (Σ, V)^{ar(f)}.

2. Let s = f_{μ}(s̃), with s̃ ∈ T (Σ^{μ}, V)^{ar(f_{μ})}. By I.H., there exists t̃′ ∈ T (Σ, V)^{ar(f_{μ})} s.t. s̃ = τ_{μ}(t̃′). Define t = f(t̃), for some t̃∈ T (Σ, V)^{ar(f)} s.t. t̃_{μ(f)} = t̃′.

□ This proposition allows us to uniquely consider any term s ∈ T (Σ^{μ}, V) as the image by τ_{μ} of some term t ∈ T (Σ, V). Therefore, we often write τ_{μ}(t) instead of s when s = τ_{μ}(t).

We need to establish some properties of the contracting function which will be used later. In particular, we are interested in relating the structure of a term in T (Σ, V) and the corresponding term (by τ_{μ}) in T (Σ^{μ}, V). We introduce the following definition.

Definition 4.10 Let Σ be a term and μ be a Σ-map. Let t ∈ T (Σ, V). The function ν_{μ,t} : O(t) → (IN − {0})^{∗} is as follows:

– ν_{μ,t}(ϵ) = ϵ

– ν_{μ,f(t̃[s]_{i})}(i.u) = ϵ if i ∉ μ(f)

– ν_{μ,f(t̃[s]_{i})}(i.u) = |N_{i}^{+} ∩ μ(f)|.ν_{μ,s}(u) if i ∈ μ(f)

We will write just ν_{t} instead of ν_{μ,t} when the replacement map μ is clear from the context. This function allows us to obtain the set of occurrences of a contracted term from the occurrences of the original term.

Proposition 4.11 Let Σ be a signature, μ be a Σ-map and τ_{μ} the μ-contracting function. Let t ∈ T (Σ, V) and u ∈ O(t). Then we have O(τ_{μ}(t)) = ν_{t}(O(t)).

An interesting fact concerning the contracting function is related to the preservation of the replacing subterms.

Proposition 4.12 (τ_{μ} preserves the replacing subterms) Let Σ be a signature, μ be a Σ-map and τ_{μ} the μ-contracting function. Let t ∈ T (Σ, V) and u ∈ O^{μ}(t). Assume that z = t|_{u}. Then τ_{μ}(z) = τ_{μ}(t)|_{v}, where v ∈ O(τ_{μ}(t)) satisfies that v = ν_{t}(u).

Proof. Structural induction. The base case is immediate. For the induction step, assume t = f(t̃[z]_{i.u′}), where u = i.u′. Then, we can apply the induction hypothesis to the i-th immediate subterm s of t, since z = s|_{u′}. Therefore, τ_{μ}(z) = τ_{μ}(s)|_{v′}, where v′ = ν_{s}(u′). Since i.u′ ∈ O^{μ}(t), i ∈ μ(f) and by Proposition 4.8, we get τ_{μ}(t) = τ_{μ}(f(t̃[s]_{i})) = f_{μ}(τ_{μ}(t̃_{μ(f)}[s]_{j})), with j = |IN_{i}^{+} ∩ μ(f)|. Therefore, the subterm τ_{μ}(z) occurs at position j.v′ in τ_{μ}(t). By Definition 4.10, we have ν_{t}(i.u′) = j.ν_{s}(u′) = j.v′ = v, and the conclusion follows. □

Corollary 4.13 (τ_{μ} preserves the replacing variables) Let Σ be a signature, μ be a Σ-map and τ_{μ} the μ-contracting function. Let t ∈ T (Σ, V). If x ∈ V ar^{μ}(t), then x ∈ V ar(τ_{μ}(t)).

Proposition 4.14 Let Σ be a signature, μ be a Σ-map and τ_{μ} the μ-contracting function. Let t, s ∈ T (Σ, V). If V ar^{μ}(t) ⊆ V ar^{μ}(s), then V ar(τ_{μ}(t)) ⊆ V ar(τ_{μ}(s)).

Proof. Let us take x ∈ V ar^{μ}(t). By Corollary 4.13, x ∈ V ar(τ_{μ}(t)). Since V ar^{μ}(t) ⊆ V ar^{μ}(s), we also have x ∈ V ar(τ_{μ}(s)), which proves the claim. □

In the following proposition, we prove that the substitution application commutes with the μ-contracting function.

Proposition 4.15 Let Σ be a signature, μ be a Σ-map and τ_{μ} the μ-contracting function. Let t ∈ T (Σ, V) and σ : V → T (Σ, V) a substitution. Let σ_{μ} : V → T (Σ^{μ}, V) such that σ_{μ}(x) = τ_{μ}(σ(x)) for all x ∈ V. Then, we have τ_{μ}(σ(t)) = σ_{μ}(τ_{μ}(t)).

Proof. By structural induction. If t = x ∈ V, then the result is immediate, since τ_{μ}(x) = x. For the induction step, we take t = f(t̃) for some t̃ ∈ T (Σ, V)^{ar(f)}. By I.H., τ_{μ}(σ(t)) = τ_{μ}(σ(f(t̃))) = τ_{μ}(f(σ(t̃))) = f_{μ}(τ_{μ}(σ(t̃_{μ(f)}))) = f_{μ}(σ_{μ}(τ_{μ}(t̃_{μ(f)}))) = σ_{μ}(f_{μ}(τ_{μ}(t̃_{μ(f)}))) = σ_{μ}(τ_{μ}(t)). □

4.2 μ-termination and contracted signature

The μ-contracting function allows us to prove μ-termination in context-sensitive rewriting by proving termination of the ‘contracted’ TRS using any method. However, there is one complication. The μ-contraction of the rewrite rules l → r of a TRS could lead to pairs (τ_{μ}(l), τ_{μ}(r)) which can not be considered as rewrite rules. For example: the rule f(g(x), y) → f(y, f(g(x), y)) with μ(f) = μ(g) = {1} yields (by μ-contracting) the ‘rule’ f_{μ}(g_{μ}(x)) → f_{μ}(y), which does not satisfy the standard non-extra variable condition of rewriting rules.

We overcome this problem by imposing a syntactical restriction on the TRSs on which we want to analyse μ-termination.

Definition 4.16 (TRS with conservative replacing variables) Let Σ be a signature and μ be a Σ-map. A TRS R = (Σ, R) has conservative replacing variables if every replacing variable in the rhs of a rule in R is a replacing variable in the lhs of this rule. Formally: V ar^{μ}(r) ⊆ V ar^{μ}(l) for every rule l → r ∈ R.

Definition 4.17 (μ-contracted TRS) Let R = (Σ, R) be a TRS and μ be a Σ-map. If R is a TRS with conservative replacing variables, we define the μ-contraction R^{μ} = (Σ^{μ}, R^{μ}) of R as follows:

– Σ^{μ} is the μ-contracted signature in Definition 4.5.

– R^{μ} = {τ_{μ}(l) → τ_{μ}(r) | l → r ∈ R}.

The following proposition establishes the correctness of Definition 4.17.

Proposition 4.18 Let R = (Σ, R) be a TRS and μ be a Σ-map. If R is a TRS with conservative replacing variables, then the μ-contraction R^{μ} = (Σ^{μ}, R^{μ}) of of R is a TRS.

Proof. For each rule τ_{μ}(l) → τ_{μ}(r) ∈ R^{μ}, we need to check, whether it verifies τ_{μ}(l) ∉ V and V ar(τ_{μ}(r)) ⊆ V ar(τ_{μ}(l)). The first condition is immediate from Definition 4.6 if R is a TRS. The second condition follows immediately from Definition 4.16 and Proposition 4.14. □

In order to connect μ-rewriting for a TRS and a replacement map and rewriting sequences using the contracted TRS, we introduce the following proposition.

Proposition 4.19 (μ-rewriting in R and rewriting in R^{μ}) Let R = (Σ, R) be a TRS with conservative replacing variables and μ be a Σ-map. Let R^{μ} = (Σ^{μ}, R^{μ}) be the contraction of R. If t ↪_{R(μ)} s, then τ_{μ}(t) →_{R^{μ}} τ_{μ}(s).

Proof. If t ↪_{R(μ)} s, then there exists u ∈ O^{μ}(t), l → r ∈ R and substitution σ : V → T (Σ, V) such that t|_{u} = σ(l) and s = t[σ(r)]_{u}. Assume v = ν_{t}(u), and σ_{μ} : V → T (Σ^{μ}, V) a substitution such that σ_{μ}(x) = τ_{μ}(σ(x)) for all x ∈ V. By Proposition 4.12 and Proposition 4.15, we have that τ_{μ}(t)|_{v} = τ_{μ}(σ(l)) = σ_{μ}(τ_{μ}(l)). By Definition 4.17, if l → r ∈ R, then τ_{μ}(l) → τ_{μ}(r) ∈ R^{μ}. Therefore the term τ_{μ}(t) can be rewritten at occurrence v by using rule τ_{μ}(l) → τ_{μ}(r) ∈ R^{μ} and matching σ_{μ}. The rewritten term is s′ = τ_{μ}(t)[σ_{μ}(τ_{μ}(r))]_{v} = τ_{μ}(t)[τ_{μ}(σ(r))]_{v} = τ_{μ}(t[σ(r)]_{u}) = τ_{μ}(s). □

The next example shows that the converse statement does not hold, i.e. τ_{μ}(t) →_{R^{μ}} τ_{μ}(s) does not imply t ↪_{R(μ)} s.

Example 4.20 Let R = ({a, b, f}, {f(a, b) → a}) and consider a replacement map μ such that μ(f) = {1}. Since R^{μ} = ({a_{μ}, b_{μ}, f_{μ}}, {f_{μ}(a_{μ}) → a_{μ}}) and τ_{μ}(f(a, a)) = f_{μ}(a_{μ}), we get τ_{μ}(f(a, a)) →_{R^{μ}} τ_{μ}(a). However, f(a, a) ↛_{R(μ)} a.

The following theorem establishes the μ-termination of a TRS and a replacement map when the contracted TRS terminates.

Theorem 4.21 (μ-termination of R when R^{μ} terminates) Let R = (Σ, R) be a TRS and μ be a Σ-map. Let R^{μ} = (Σ^{μ}, R^{μ}) be the contracted TRS of R. If R is a TRS with conservative replacing variables, then R μ-terminates if R^{μ} terminates.

Proof. By contradiction. Assume that R does not μ-terminate. Then there exists an infinite μ-derivation t_{1} ↪ t_{2} ↪ ⋯ ↪ t_{n} ↪ ⋯ in R. By Proposition 4.19, we get an infinite derivation τ_{μ}(t_{1}) → τ_{μ}(t_{2}) → ⋯ → τ_{μ}(t_{n}) → ⋯ in R^{μ}, which contradicts the initial hypothesis. □

This theorem gives us a new criterion to detect μ-termination of a TRS. Actually, we can use any standard method to check termination of the μ-contracted TRS. We refer to this new method as the C_{R}^{μ}-criterion to check μ-termination.

Example 4.22 We can apply the C_{R}^{μ}-criterion to demonstrate the μ-termination of the TRS R in the Example 4.4, using the μ-contracted TRS R^{μ} obtained in Example 4.7. By using a recursive path ordering >^{∗} on T (Σ^{μ}, V) based on any precedence on Σ^{μ} = {f_{μ}, g_{μ}}, we get f_{μ}(g_{μ}(x)) >^{∗} f_{μ}(x), i.e. R^{μ} terminates, and therefore R μ-terminates.

Sometimes we can not use directly the C_{R}^{μ}-criterion, but it turns still useful in combination with Proposition 4.2.

Example 4.23 Let us consider the TRS R and the replacement map μ of Example 4.4. Let μ′ be given as follows: μ′(f) = {1} and μ′(g) = Ø. Then, R does not satisfies the conservative replacing variables property w.r.t μ′. Hence we can not apply the C_{R}^{μ′}-criterion. However, since μ′ ⊑ μ and R is μ-terminating (see Example 4.22), by Proposition 4.2, R is μ′-terminating.

4.3 Checking μ-termination

We use the above results to establish a suitable criterion to check μ-termination. First, an example reveals the uncompleteness of the C_{R}^{μ}-criterion.

Example 4.24 Let us consider the TRS R = ({f, g}, {f(g(x)) → f(x)}), and a replacement map μ given by μ(f) = Ø. For this replacement map, R is a TRS with conservative replacing variables. Then, it is easy to demonstrate that R is a μ-terminating TRS (it suffices to consider the C_{R}-criterion and apply a recursive path ordering, for example, to R), but the μ-contracted TRS R^{μ} = ({f_{μ}, g_{μ}}, {f_{μ} → f_{μ}}) is not terminating.

Since we could establish the μ-termination of R by means of the C_{R}-criterion, the example points out the fact that the C_{R}^{μ}-criterion does not include the C_{R}- criterion. On the other hand, from Example 4.4 we conclude that the C_{R}-criterion does not include the C_{R}^{μ}-criterion either.

The example 4.24 also shows that Theorem 4.21 has not a symmetric counterpart, that is, we can not ensure termination of a μ-contracted TRS from the μ-termination of the original.

Now we can formulate a mixed criterion involving both C_{R} and C_{R}^{μ} criteria to test μ-termination.

Theorem 4.25 (μ-termination of a TRS) Let R = (Σ, R) be a TRS with conservative replacing variables given a Σ-map μ. Let R^{μ} = (Σ^{μ}, R^{μ}) be the contracted TRS of R. Then R μ-terminates if R or R^{μ} terminates.

Proof. Immediate from Theorem 4.3 and Theorem 4.21. □

Note that this theorem only applies to TRSs with conservative replacing variables. Fortunately, for general TRSs, we still have the Theorem 4.3 (C_{R}-criterion) to prove μ-termination.

5 Conclusions

Context-sensitive rewriting allows us to deal with context-replacing restrictions in performing reduction steps, thus avoiding some undesirable reductions. Termination is always preserved or improved, as we have shown in this paper.

The restrictions imposed by context-sensitive rewriting are easily implementable. However, in order to get complete benefits from context-sensitive rewriting, more research is needed. In particular, it is interesting to study conditions to ensure that, by defining a concrete replacement map for a given TRS, computations are restricted but not too much, i.e., they will be able to reduce sufficiently a term by context-sensitive rewriting. This would allow us, implicitly, to define the adequate replacement map which is powerful enough to perform computations with context-sensitive rewriting. This task will be addressed in a further work.

References

1. N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science 17:279-301, 1982.

2. N. Dershowitz. Termination of rewriting. Journal on Symbolic Computation, 3:69-115, 1987.

3. N. Dershowitz. A Taste of Rewrite Systems. In P.E. Lauer, editor, Proc. of Functional Programming, Concurrency, Simulation and Automated Reasoning, LNCS 693:199-228, Springer-Verlag, Berlin, 1993.

4. N. Dershowitz and C. Hoot. Natural Termination. Theoretical Computer Science 142(2):179-207, 1995.

5. N. Dershowitz and J.P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243-320. Elsevier, Amsterdam and The MIT Press, Cambridge, MA, 1990.

6. D.P. Friedman and D.S. Wise. CONS should not evaluate its arguments. In S. Michaelson and R. Milner, editors, Automata, Languages and Programming, pages 257-284, Edinburgh University Press, 1976.

7. J. Goguen, C. Kirchner and J. Meseguer. Concurrent Term Rewriting as a Model of Computation. In J.H. Fasel, R.M. Keller, editors, Graph Reduction. Proceedings. of a Workshop. LNCS 279:53-93. Springer-Verlag, Berlin, 1987.

8. S. Kamin and J.J. Lévy. Two generalizations of the recursive path ordering. University of Illinois, 1980.

9. J.F.Th. Kamperman and H.R. Walters. Lazy Rewriting and Eager Machinery. In J. Hsiang, editor, Proc. of the 6th International Conference on Rewriting Techniques and Applications, RTA’95, LNCS 914:147-162, Springer-Verlag, Berlin, 1995.

10. G. Huet and J.J. Lévy. Computations in orthogonal term rewriting systems. In J.L. Lassez and G. Plotkin, editors, Computational logic: essays in honour of J. Alan Robinson. MIT Press, Cambridge, MA, 1991.

11. R. Lalement. Computation as Logic. Masson-Prentice Hall International, 1993.

12. S. Lucas. Computational properties in context-sensitive rewriting. In M. Alpuente and M.I. Sessa, editors, Proc. of 1995 Joint Conference on Declarative Programming, GULP-PRODE’95, pages 435-446, 1995.

13. S. Lucas. Fundamentals of context-sensitive rewriting. In M. Bartǒsek, J. Staudek and J. Wiedermann, editors, Proc. of XXII Seminar on Current Trends in Theory and Practice of Informatics, SOFSEM’95, LNCS 1012:405-412, Springer-Verlag, Berlin, 1995.

14. Z. Manna and S Ness. On the termination of Markov algorithms. In Proc. of the Third Hawaii International Conference on System Science, pages 789-792, 1970.

15. S. L. Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-Hall International, London, 1987.

16. C. Reade. Elements of Functional Programming. Addison-Wesley Publishing Company, 1987.

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