Fundamentals of context-sensitive 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. Recently we have introduced a novel class of rewrite relations we call contextsensitive rewriting that proves useful to mechanize a particular class of inference systems. In this paper, we give a more accurate characterization of some properties of context-sensitive rewriting. We also show that several reduction strategies used in λ-calculus namely weak reduction and lazy (call by name) reduction, can be viewed as an instance of the contextsensitive rewriting.

Keywords: term rewriting systems, regularity, functional programming.

1 Introduction

The theory of Term Rewriting Systems (TRSs) has proven useful to mechanize the execution of functional programs [3] by imposing directionality on the use of equations in proofs [1, 2]. Directed equations, called ‘rewrite rules’, are used to replace equals by equals, but only in the indicated direction. In this scheme, computation consists of rewriting terms to a normal form, i.e. an expression that cannot be rewritten any further [1]. The notion of sequence of rewrites traditionally defines an operational view of computation. The equational origin of term rewriting techniques leads to consider an expression t → s as ‘t equals s’ rather than ‘t becomes s’ [8]. As a consequence, the property of ‘being closed under context application’ (a particular form of the algebraic property of regularity) is essential in the definition of the rewriting relation.

In [6] we have introduced a novel class of rewrite relations, we call context-sensitive rewriting, whose definition is based on regularity. Roughly speaking, given a term t, the subterm of t at the occurrence u is a redex of the context-sensitive rewrite relation iff the symbols in t which label the occurrences above u satisfy a particular condition we call replacement condition.

In this paper, we introduce some properties of the replacement condition, which give a more powerful characterization of the context-sensitive rewriting process. In particular, we show that the evaluation of the replacement condition can be made compositionally. We also show that context-sensitive rewriting satisfies some desirable properties such as stability which allows us to ensure that a (context-sensitive) reducible term also rewrites to another when we instantiate its variable occurrences. This property plays an important role in studying the computational properties of rewriting such as confluence and termination. We also show that several common reduction strategies used in λ-calculus [4, 5], such as weak reduction and lazy reduction, can be viewed as an instance of the context-sensitive rewriting.

The paper is organized as follows. In Section 2, we briefly recall the technical concepts and results used in the remainder of the paper. In Section 3, we shows the basic properties of the context-sensitive rewrite relation. At the end of this section, we illustrate the application of this technique to weak reduction and lazy λ-calculus. We conclude by pointing to some further research.

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

2 Preliminaries

Let us first introduce the main notations used in the paper. For full definitions we refer to [2, 5]. Throughout the paper, V denotes a countable set of variables and Σ denotes a set of function symbols {f, g, …}, each with a fixed arity given by a function ar : Σ → N. By T (Σ, V) we denote the set of terms. Given a term t, V ar(t) is the set of variable symbols in 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, and they are ordered by the prefix ordering: u ≤ v if there exists a w such that u.w = v. By u ∥ v we denote that the occurrences u, v are disjoint, i.e. u ≰ v and v ≰ u. 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 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.

N_{k}^{+} is an initial segment {1, 2, … k} of the set of positive natural numbers N^{+} where N_{0}^{+} = Ø. A homogeneous algebra A is a pair (A, F) where A is a set (the carrier) and F is a set of

mappings {f, g, …}. The mapping ar : F → N associates with each function f in F its arity, i.e. ar(f) = k iff f is a mapping from A^{k} → A.

3 Context-sensitive rewriting

3.1 Regularity

First we summarize the main algebraic concepts that support the context-sensitive rewriting. More details and missing proofs can be found in [6, 7].

Definition 3.1 (Regularity) Let R be a relation on A and f : A^{k} → A be a mapping. We say that R is regular wrt f with index j, 1 ≤ j ≤ k (we also say that R is j-regular wrt f) iff for all a, b, a_{1}, …, a_{k} ∈ A. a R b ⇒ f(a_{1}, …, a_{j−1}, a, …, a_{k}) R f(a_{1}, …, a_{j−1}, b, …, a_{k}). The set m_{R}(f) ⊆ N_{k}^{+} of all indexes j such that R is j-regular wrt f is called the regularity map of R wrt f.

The concept of regularity can be isolated of considering any particular relation by just taking a set of indices for each function in the algebra. This leads to the relation-independent concept of algebraic regularity map.

Definition 3.2 (Algebraic regularity map) Let A = (A, F) be an algebra. A mapping m : F → 2^{N} is an algebraic regularity map (r-map) for A iff for all f ∈ F. m(f) ⊆ N_{ar(f)}^{+}. The set of all r-maps of A is denoted by M_{A}.

We express in a compact mode the regularity property of a relation R wrt each function in a given algebra A = (A, F), according to definition 3.1. The map m_{R} : F → 2^{N} is called the regularity map (or simply the r-map) of R wrt A iff for all f ∈ F. m_{R}(f) is the regularity map of R wrt f. We also say that R is m_{R}-regular wrt A.

The following example shows the regularity maps of a given relation with respect to several algebras. Let us consider the relation R of ‘being multiple of’ in the set Q^{+} of positive rational numbers, i.e. ∀ a, b ∈ Q^{+}. a R b ⇔ ∃c ∈ N . a = b × c. Then the r-map of R wrt (Q^{+}, {+}) verifies m_{R}(+) = Ø, the r-map of R wrt (Q^{+}, {/}) verifies m_{R}(/) = {1} and the r-map of R wrt (Q^{+}, {×}) verifies m_{R}(×) = {1, 2}.

Now we introduce a partial order on r-maps.

Definition 3.3 (Partial order on regularity maps) Let A = (A, F) be an algebra. Let M_{A} be the set of r-maps for A and let m, m′ ∈ M_{A}. We define a partial order ⊑ on M_{A} as follows: m ⊑ m′ ⇔ ∀f ∈ F. m(f) ⊆ m′(f).

It is immediate to see that (M_{A}, ⊑) is a complete lattice. The map m_{⊤} which assigns to each function f ∈ F the whole segment N_{ar(f)}^{+} is the top element and the map m_{⊥} which assigns to each function f ∈ F the empty set Ø is the bottom element.

3.2 Basic properties of context-sensitive rewriting

In this section, we show some powerful properties of context-sensitive rewriting. The idea behind the concept of context-sensitive rewriting is to impose a syntactic replacement condition which prevents one from performing some reduction steps. This is achieved by using a map on the signature we call replacement map. A mapping μ : Σ → 2^{N} is a replacement map (or Σ-map) for the signature Σ iff for all f ∈ Σ. μ(f) ⊆ N_{ar(f)}^{+}.

We use the replacement map to give a condition on the occurrences of a given term where the rewrite rules can be applied.

Definition 3.4 (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_{1},...,t_{i},...,t_{k})}(i.u) ⇔ (i ∈ μ(f)) ∧ γ_{μ,t_{i}}(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.

In the following, we write γ_{t}(u) when the replacement map is clear from the context. Also, let us denote as O^{μ}(t) the set of replacing occurrences of a term t: u ∈ O^{μ}(t) ⇔ u ∈ O(t) ∧ γ_{t}(u).

Roughly speaking, the replacement condition for a term t wrt μ imposes a restriction based on the function symbols which label the path between the root of t and the subterm at occurrence u. To make clear the meaning of this restriction, we present some basic properties of the replacement condition we defined above.

Proposition 3.5 (Compositionality in evaluating the replacement condition) Let Σ be a signature, t ∈ T (Σ, V) and u ∈ O(t). Then the following statement holds: u = u_{1}.u_{2} ⇒ (γ_{t}(u) ⇔ (γ_{t}(u_{1}) ∧ γ_{t|_{u_{1}}} (u_{2}))).

This Proposition allows us to realize the evaluation of replacement conditions in a compositionally mode. As an immediate consequence of this result, we have the following corollaries.

Corollary 3.6 Let Σ be a signature, t ∈ T (Σ, V) and u, v ∈ O(t). The following statements hold:

1. (u ≤ v ∧ γ_{t}(v)) ⇒ γ_{t}(u),

2. (u ≤ v ∧ ¬γ_{t}(u)) ⇒ ¬γ_{t}(v).

Corollary 3.7 Let Σ be a signature, t ∈ T (Σ, V) and u ∈ O(t). The following statement holds: γ_{t}(u) ⇒ (u = u_{1}.u_{2} ⇒ γ_{t|_{u_{1}}} (u_{2}))

We can demonstrate some useful properties related with the persistence of the evaluation of the replacement condition with respect to substitution application and subterm replacement.

Proposition 3.8 (Persistence with respect to substitution application) Let Σ be a signature, t ∈ T (Σ, V) and u ∈ O(t). Let σ : V → T (Σ, V) be a substitution. Then, γ_{t}(u) ⇔ γ_{σ(t)}(u).

Proposition 3.9 (Persistence with respect to subterm replacements) Let Σ be a signature, t, t′ ∈ T (Σ, V) and u, v ∈ O(t). Then,

1. u ≤ v ⇒ (γ_{t}(u) ⇔ γ_{t[t′]_{v}}(u)) and

2. u ∥ v ⇒ (γ_{t}(u) ⇔ γ_{t[t′]_{v}}(u)).

The above results allow us to devise more efficient methods for the evaluation of the replacement condition in context-sensitive systems.

The order ⊑ on algebraic regularity maps can easily be translated to compare replacement maps for a given signature Σ. By abuse of notation, we will use the same symbol ⊑ to denote both orderings. The next result establishes that a replacement condition that holds for a given replacement map is also verified wrt a greater replacement map.

Proposition 3.10 Let Σ be a signature, t ∈ T (Σ, V) and u ∈ O(t). Let μ, μ′ be two Σ-maps such that μ ⊑ μ′. Then we have γ_{μ,t}(u) ⇒ γ_{μ′,t}(u)

Now we introduce the context-sensitive rewriting by means of their one-step reduction relation.

Definition 3.11 (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 reducing the subterm of t at the replacing occurrence u ∈ O^{μ}(t). ↪_{R(μ)} is the one-step context-sensitive rewrite relation of R wrt μ. ↪_{R(μ)}^{∗} is the context-sensitive rewrite relation of R wrt μ.

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

Let us now consider a first example of context-sensitive rewriting. Let α : f(x) → x be a rule and t = g(f(a), f(b)) be a term. a) If μ(g) = Ø then t cannot be reduced, because neither the occurrence u = 1 nor u = 2 satisfies the replacement condition wrt μ. b) If μ(g) = {1}, then we can reduce f(a) but we cannot reduce f(b). c) If μ(g) = {2}, then we can reduce f(b) but we cannot reduce f(a). d) If μ(g) = {1, 2}, then we can be reduce both f(a) and f(b).

The following proposition illustrates the (one-step) context-sensitive version of the ‘being closed under context application’ property. The context-sensitive rewriting is ‘closed under replacing context application’.

Proposition 3.12 (Restricted context replacement) Let C, t, s ∈ T (Σ, V). Let u ∈ O^{μ}(C). If t ↪ s then C[t]_{u} ↪ C[s]_{u}.

Note that for the top Σ-map μ_{⊤} the replacement condition is satisfied for every term t and occurrence u. This is to say that, given a TRS R, the one-step context-sensitive rewrite relation for μ_{⊤} and the standard one-step rewrite relation coincide, i.e. ↪_{R(μ_{⊤})}=→_{R}. Now we show that the context-sensitive rewriting is stable under substitution.

Proposition 3.13 (Stability of ↪) Let R = (Σ, R) be a TRS, μ be a Σ-map and σ : V → T (Σ, V) be a substitution. Then t ↪ s ⇒ σ(t) ↪ σ(s).

The following proposition establishes that, given a TRS, the one-step context-sensitive rewrite relation induced by a replacement map includes the relation induced by a lesser replacement map.

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

3.3 Context-sensitive rewriting and Inference Systems

In [7] we have proven that a TRS R = (Σ, R) and a Σ-map μ generate an inference system (IS) which transition relation and the context-sensitive rewrite relation ↪_{R(μ)} coincide. Roughly speaking, the axioms of the IS are instances of the rewrite rules and a contextual inference rule is defined for each k-ary symbol f ∈ Σ and each argument i ∈ μ(f). The basic inference system associated to R and μ, denoted by I(R, μ), is defined as follows:

1. α : l → r ∈ R iff (a_{α}) \overline{l ⋄ r} is an (scheme of) axiom of I(R, μ)

2. For each f ∈ Σ, k = ar(f), i ∈ μ(f) and terms t_{1}, …, t_{k}, s_{i}

(r[f, i]) \frac{t_{i} ⋄ s_{i}}{f(t_{1}, …, t_{i}, …, t_{k}) ⋄ f(t_{1}, …, s_{i}, …, t_{k})} is a rule of I(R, μ)

The relation defined by I(R, μ) on T (Σ, V) (that is, its deductive closure) is denoted by →_{I(R,μ)}.

This is the class of ISs that context-sensitive rewriting mechanizes, i.e. those ISs such that →_{I(R,μ)}= ↪_{R(μ)}. Conversely, given an IS such that every rule fits the pattern r[f, i], we define a TRS by taking the axioms of the IS as rewrite rules and we attach a replacement map according to the existing contextual inference rules r[f, i].

Now, if we want to define an abstract machine that computes the transition relation of such an IS we can modify a standard rewriting machine (such as the graph reduction machine [10]) to deal with the restrictions imposed by the replacement condition. Roughly speaking, in order to execute a program with respect to a set of rewrite rules, the evaluator of a rewriting machine must follows the following algorithm (until a normal form is reached) [10]:

1. selecting the next redex to be reduced and

2. reducing it.

To accomodate this to a context-sensitive rewriting system we must to take into account the replacement condition in the first step.

3.4 Examples and applications

Let us consider the λ-calculus. A λ-term M ::= x | λx.M | MN is represented as a tree by considering each λx as an unary symbol, application as a binary symbol @ and each variable as a symbol of arity zero [5]. This is expressed by means of the signature Σ_{λ} = C_{V} ∪ Λ_{x} ∪ {@}, where Λ_{x} = {λ_{x}| x ∈ V } and C_{V} is a set of arbitrary constants (one for each variable symbol). The immediate β-reduction of λ-calculus →_{β}, can be obtained from the following inference system [4, 5], which we refer to as IS_{β} (in spite of the introduction of Σ_{λ}, we express IS_{β} in the standard λ-notation):

(red) \overline{(λx.P)Q ▷ P [x := Q]}

We can see that any instance of the axiom scheme (red) can be taken as a rewrite rule (λx.P)Q → P [x := Q]. In the sequel, R_{λ} is the set of rules which are instances of the (red) axiom scheme.

(rλ) \frac{M ▷ M′}{λx.M ▷ λx.M′}  (r1) \frac{M ▷ M′}{MN ▷ M′N}  (r2) \frac{M ▷ M′}{NM ▷ NM′}

Note that the context passing rules (rλ), (r1) and (r2) fit the pattern r[f,i].

Example 3.15 (Weak β-reduction) Let us consider the weak β-reduction, a restriction on the β-reduction of λ-calculus. For this reduction, an abstraction λx.M is irreducible, even if M contains a redex. This corresponds to drop the rule (rλ) in IS_{β}, thus obtaining IS_{w} whose only rules are r1 and r2. We can simulate this behavior with context-sensitive rewriting by considering the following TRS R = (Σ_{λ}, R_{λ}) and the Σ_{λ}-map μ_{w} defined as follows: μ_{w}(@) = {1, 2}, μ_{w}(f) = Ø for all f ∈ Σ_{λ} − {@}.

Example 3.16 (Lazy λ-calculus) Now consider the lazy λ-calculus, another restriction on the β-reduction used by the majority of functional languages to avoid the ‘eagerness’ in evaluating functional applications. To delay the evaluation of an application MN we need only one context passing rule, namely (r1) to constitute IS_{z}, the inference system for lazy λ-calculus. We can simulate this behavior with context-sensitive rewriting by considering the following TRS R = (Σ_{λ}, R_{λ}) and the Σ_{λ}-map μ_{z} defined as follows: μ_{z}(@) = {1}, μ_{z}(f) = Ø for all f ∈ Σ_{λ} − {@}.

The R. Milner’s π-calculus [9] is a computational scheme which models concurrency. In [7] we define a TRS and a replacement map whose context-sensitive rewriting can be seen as a mechanization of the π-calculus process execution.

4 Further research

We have introduced a powerful characterization of the context-sensitive rewriting process. We have examined several computational properties of context-sensitive relations and demonstrated that they are stable under substitution and closed under replacing context application.

A first approach to the characterization of confluence of context-sensitive rewriting can be found in [6]. A desirable direction for further research will be the definition of syntactic criteria to ensure the confluence and termination of induced context-sensitive rewriting when we attach a replacement map to a given term rewriting system.

5 Acknowledgements

I would like to thank María Alpuente and Germán Vidal for their encouragement and support. Also, I am grateful to Asunción Casanova, Javier Oliver and Javier Piris for their helpful comments and corrections.

References

1. N. Dershowitz. A Taste of Rewrite Systems. In P.E. Lauer, editor, Proc of Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693 of Lecture Notes in Computer Science, pages 199-228, Berlin, 1993.

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

3. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification. volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1985.

4. J.R. Hindley and J.P. Seldin. Introduction to Combinators and λ-Calculus. Cambridge University Press, 1986.

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

6. S. Lucas. Computational properties in context-sensitive rewriting. In Proc. of 1995 Joint Conference on Declarative Programming, GULP-PRODE’95. To appear.

7. S. Lucas and J. Oliver. Context-sensitive rewriting. Technical report DSIC-II/23/94.

8. J. Meseguer. Conditional Rewriting Logic as an Unified Model of Concurrency. Journal of Theoretical Computer Science, 96:73-155, 1992.

9. R. Milner. The polyadic π-calculus: A tutorial. In F.L. Brauer, W Bauer and H Schwintenberg, editors, Logic and Algebra of Specifications, Springer-Verlag, Berlin, 1993.

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

11. D. Plaisted. Equational Reasoning and Term Rewriting Systems. In D. Gabbay and J. Siekmann, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, volume 1, 1994.

This article was processed using the L^{A}TEX macro package with LLNCS style