|
COPYRIGHT 2000 Association for Computing Machinery, Inc.
1. INTRODUCTION
A term-rewriting system (TRS) provides a mechanism to reduce terms to their normal forms, which cannot be reduced any further. A TRS consists of a number of rewrite rules l [right arrow] r, where l and r are terms. For any term t, such a rule allows one to replace subterms [Sigma](l) of t by [Sigma](r), for substitutions [Sigma]. The structure [Sigma](l) is called a fedex (reducible expression) of t. A term can contain several redexes, so that the question arises: which of these redexes should actually be reduced. There are two standard strategies:
--outermost rewriting reduces a redex as close as possible to the root of the parse tree of the term;
--innermost (or eager) rewriting reduces a redex as close as possible to the leaves of the parse tree of the term.
On the one hand, outermost rewriting often displays better termination behavior (e.g., see O'Donnell [1977]), meaning that it can give rise to fewer infinite reductions. Namely, an innermost redex that gives rise to an infinite reduction may be eliminated by the contraction of an outermost redex. Moreover, outermost rewriting can produce a sequence of partial results (prefixes of the normal form) that is useful even when this strategy does not terminate. This is interesting if the output of one program is connected to the input of another; it may be that the nonterminating subcomputations in the first program are not necessary for the termination of the second program. On the other hand, the implementation of innermost rewriting usually involves less run-time overhead, mainly for two reasons. First, it does not require the expensive building of redexes, as their contexts can be inspected after contraction of the redex. Second, after the application of a rewrite rule, the subterms in the reduct that are innermost with respect to the pattern at the right-hand side of the rewrite rule are known to be irreducible, which avoids repeated inspection of such structures.
The aim of lazy evaluation [Friedman and Wise 1976; Henderson and Morris 1976], which underlies lazy functional languages (e.g., see Plasmeijer and van Eekelen [1993]) and equational programming [Hoffmann and O'Donnell 1982b], is to combine an efficient implementation with good termination properties. During the lazy evaluation of a term it is decided whether the input term is in weak head normal form, meaning that it is not a redex. If this decision procedure requires the reduction of a proper subterm, then ideally it selects a needed redex [Huet and Levy 1991], for which it is certain that no rewriting strategy can eliminate it. Needed redexes can be determined (efficiently) for orthogonal TRSes that are (strongly) sequential; see Huet and Levy [1991] and O'Donnell [1985]. If a term is decided to be in weak head normal form, then its outermost function symbol is presented as output, and its arguments are subsequently reduced to weak head normal form.
Hartel et al. [1996, p. 649] conclude that "non-strict compilers do not achieve ... the performance of eager implementations" and that "interpreters for strict languages (Caml Light, Epic) do seem on the whole to be faster than interpreters for non-strict languages (NHC, Gofer, RUFLI, Miranda)." A bottleneck for the performance of lazy evaluation, compared to eager evaluation, is that it requires a considerable amount of bookkeeping. In order to reduce this kind of overhead, in practice lazy evaluation is often adapted to do a lot of eager evaluation. Strandh [1988; 1989] showed for the restricted class of forward-branching equational programs that lazy evaluation can be performed efficiently on eager hardware.
Arguments that can be rewritten eagerly without affecting termination behavior are called strict. Strictness analysis, initiated by Mycroft [1980], attempts to identify these arguments statically. In lazy functional languages, strictness analysis and programmer-provided strictness annotations are used to do as much eager evaluation as possible. For example, Clean [Brus et al. 1987] supports the annotation of strict arguments, which are evaluated in an eager fashion. In Clean, experience shows how in a lazy program most arguments can be annotated as strict without influencing the termination behavior of the program [Plasmeijer 1998].
We investigate how an eager implementation can be adapted to do some lazy evaluation. We propose the notion of a laziness annotation, which assigns to each argument of a function symbol either the label "eager" or the label "lazy." Only redexes that are not the subterm of a lazy argument (the so-called "active" redexes) are reduced whenever possible, according to the innermost rewriting strategy. This notion of lazy rewriting avoids rewriting at lazy arguments to a large extent. Laziness annotations can be provided by a strictness analyzer, in which case all arguments that are not found to be strict get the annotation lazy, or by a programmer. In practice, strictness analyzers can be quite conservative, so that they may indicate far too many lazy arguments; e.g., see Sekar et al. [1997].
A standard application of lazy evaluation, where compared to eager evaluation it improves both termination behavior and performance, is the if-then-else construct:
if(true, x,y) [right arrow] x
if(false, x,y) [right arrow] y.
A sensible laziness annotation makes the first argument of if eager and the last two arguments lazy. Then, evaluation of a term if(s, [t.sub.0], [t.sub.1]) first reduces s to either true or false; next the term is rewritten to [t.sub.0] or [t.sub.1], respectively, and finally this reduct is evaluated. Thus, laziness avoids that both [t.sub.0] and [t.sub.1] are reduced, because one of these evaluations would be irrelevant, depending on the evaluation of s.
We give an example, which also appears in Ogata and Futatsugi [1997], to explain the use of laziness annotations in more detail. The following TRS returns an element from an infinite list of natural numbers. Note that the left-hand sides of the second and third rule are overlapping. Following ideas from Baeten et al. [1989] and Kennaway [1990], the third rule is given priority over the second rule, because its left-hand side is more specific.
(1) inf(x) [right arrow] cons(x, inf(succ(x))) (2) nth(x, cons(y,z)) [right arrow] y (3) nth(succ(x), cons(y,z)) [right arrow] nth(x,z)
For k [is greater than or equal to] 0, outermost rewriting reduces the term nth([succ.sup.k](0), inf(0)) to its normal form [succ.sup.k](0), by k alternating applications of rules (1) and (3), followed by a final application of rules (1) and (2). However, the innermost rewriting strategy does not detect this reduction, but produces an infinite reduction instead, using only rule (1). For instance, in the case k = 0, eager evaluation yields
[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]
In order to avoid such infinite reductions, we can define the second argument of cons to be lazy, while the arguments of the function symbols inf, nth, and succ, and the first argument of cons are defined to be eager. Lazy rewriting with respect to this laziness annotation provides a finite reduction for the term nth(0, inf(0)). Namely, after the first reduction step
[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]
it is not allowed to reduce the lazy second argument inf(succ(0)) of cons. So the only reduction that remains is
[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]
which produces the normal form 0.
Lazy rewriting extends the class of weak head normal forms, owing to the fact that we do not require the lazy arguments of a normal form to be in normal form. For instance, in the example above, the laziness annotation even produces a normal form for the term inf(0), which does not have a finite reduction at all. Namely, after the first rewrite step
[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]
it is not allowed to reduce the lazy argument inf(succ(0)) of cons. So the term cons(0, inf(succ(0))) is a lazy normal form, i.e., a normal form with respect to the laziness annotation.
Laziness annotations can be implemented by irreducible encodings called thunks [Ingerman 1961], which make it possible to forget about laziness, and focus on eager evaluation only. That is, before a term is rewritten, first its lazy arguments f([t.sub.1], ..., [t.sub.n]) are thunked as follows. Such a subterm is transformed into [Theta]([[Tau].sub.f], [t.sub.1], ..., [t.sub.n]), where the special function symbol [Theta] represents a thunk, and the special constant [[Tau].sub.f] is a token related to the function symbol f. Moreover, the arguments [t.sub.1], ..., [t.sub.n] are thunked following the same procedure. This conversion turns the lazy argument f([t.sub.1], ..., [t.sub.n]) into a normal form, while its original term structure is stored by means of the tokens [[Tau].sub.g] for function symbols g that occur in f([t.sub.1], ..., [t.sub.n]). Extra rewrite rules are added to restore the original term structure, if this thunk is placed in an eager argument. Furthermore, lazy arguments in right-hand sides of rewrite rules are transformed as follows. If a rewrite rule l [right arrow] r contains a lazy argument t in its right-hand side r, with variables [x.sub.1], ..., [x.sub.n], then we replace t in r by [Theta]([Lambda], [x.sub.1], ..., [x.sub.n]). The [Lambda] is a special constant that registers the term structure of t. Rewrite rules are added to transform this structure into t, if it is placed in an eager argument. An additional advantage of this last procedure is that the lazy subterm t is compressed to a structure whose size is determined by its number of variables. We only have to spend the time and space needed to build t if it is made eager. If, however, the lazy argument t is eliminated, then this construction is avoided. Strandh [1987] presented a similar compression technique in equational programming.
Lazy rewriting of terms would hamper the efficiency of its implementation, because this could lead to duplication of arguments that are not in normal form. For example, suppose a rule
f(x) [right arrow] g(x,x)
is applied to a term f(t), in the setting of eager evaluation with a laziness annotation. Then it may be the case that the term t is not a normal form, due to the fact that it contains subterms that are thunks. These thunks are duplicated in the reduct g(t,t). In order to solve this inefficiency, lazy evaluation is usually performed by graph rewriting [Staples 1980] instead of term rewriting. In graph rewriting, the two arguments of g(x,x) point to the same node in the graph, so that in g(t,t) the thunks in t are not duplicated. A term can be considered as a graph, and the graph reducts of this graph, with respect to some TRS, can be expanded into terms again. These terms can also be obtained from the original term by term rewriting with respect to the same TRS; see Barendregt et al. [1987]. Hence, each parallel reduction in graph rewriting simulates a reduction in term rewriting. As a matter of fact, even without laziness annotation, implementation of eager evaluation of terms usually boils down to graph rewriting. Namely, storing a term such as g(t, t) as a graph, in which the two arguments t point to the same node, saves memory space. See O'Donnell [1985] for an overview of the pragmatics of implementing graph rewriting in the setting of equational programming.
It is customary in graph rewriting to restrict to left-linear TRSes, in which left-hand sides of rewrite rules do not contain multiple occurrences of the same variable. TRSes that are not left-linear require checks on syntactic equality, which have a complexity that is related to the sizes of the graphs to be checked. In innermost rewriting, each TRS can be simulated efficiently by a left-linear TRS, using an equality function; e.g., see Kamperman [1996, p. 28]. Most functional languages feature many-sortedness, conditional rewrite rules, and a higher-order syntax. A TRS over a many-sorted signature can be treated as a single-sorted TRS after it has been type-checked, so we take the liberty to only consider single-sorted TRSes. A sensible way to compile conditional TRSes is to eliminate conditions first. In innermost rewriting, conditions of the form s [down arrow] t (i.e., s and t have the same normal form) can be expressed by means of an equality function. For example, a rewrite rule x [down arrow] y ?? f(x, y) [right arrow] r is simulated by the TRS
f(x, y) [right arrow] g(eq(x, y),x, y)
g(true, x, y) [right arrow] r
g(false, x, y) [right arrow] f'(x, y).
Alternatively, conditions can be evaluated after pattern matching, by an extension of the pattern-matching automaton. Since the complications related to the implementation of conditions are orthogonal to the matters investigated in this article, we only consider unconditional TRSes. Finally, we focus on first-order terms. The notion of a laziness annotation extends to a higher-order syntax without complications, giving rise to our notion of lazy rewriting. The implementation of this generalization, however, requires further study.
Left-hand sides of rewrite rules are allowed to be overlapping. In most functional languages such ambiguities are resolved by means of a textual ordering, which makes the priority of a rewrite rule dependent on its position in the layout of the TRS. Kennaway [1990] argued that textual ordering has an unclear semantics, and advocated the use of specificity ordering, in which a rewrite rule has higher priority if its left-hand side has more syntactic structure. Specificity ordering makes sense, because reversal of this priority would mean that only rewrite rules with minimal syntactic structure in their left-hand sides would ever be applied. Kennaway showed how to transform a TRS with specificity ordering into an orthogonal, strongly sequential TRS. Specificity ordering from Kennaway does not resolve ambiguities between overlapping rules such as f(a, x) [right arrow] r and f(y, b) [right arrow] r'. In Kamperman and Walters [1996] and Fokkink et al. [1998], this ordering was refined by comparing the syntactic structure of arguments of left-hand sides of rewrite rules from left to right. For example, f(a, x) [right arrow], r has higher priority than f(y, b) [right arrow] r', because the first argument a of the left-hand side f(a, x) has more syntactic structure than the first argument y of the left-hand side f(y, b).
In this article the specificity ordering from Kamperman and Walters [1996] and Fokkink et al. [1998] is adapted in such a way that it takes into account the laziness annotation. Left-hand sides of rewrite rules are minimized, so that they agree with the success-transitions of the corresponding pattern-matching automaton of Hoffmann and O'Donnell [1982a]. Minimization of left-hand sides mimics scanning left-hand sides with respect to their specificity. As minimization breaks up this scan into small steps, it is advantageous for the presentation and for the correctness proofs. Minimization has the additional benefit that it leads to implementations that are better structured and thus more easy to maintain. In comparison with a straightforward scan, minimization incurs a small cost at compile-time, but not at run-time. Although the number of rewrite steps increases in a linear fashion, the complexity of executing a single rewrite step decreases, which in practice leads to comparable performance (cf., Fokkink et al. [1998]).
We explained that lazy nodes in graphs are thunked, and that the original rewrite rules are adapted to introduce thunks in right-hand sides and to minimize left-hand sides. The transformations involve an extension of the original alphabet and an adaptation of the class of normal forms. We prove that eager evaluation with respect to the transformed TRS simulates lazy rewriting with respect to the original TRS, using a simulation notion from Fokkink and van de Pol [1997]. This simulation is shown to be sound, complete, and termination preserving, which implies that no information on normal forms in the original TRS is lost.
This article is set up as follows. Sections 2 and 3 present the notions of standard and lazy graph rewriting, respectively. Section 4 explains how lazy rewriting can be converted to eager rewriting by the introduction of thunks. Section 5 contains a comparison with related work. Appendix A presents the correctness proof. Earlier versions of this article appeared as Kamperman and Walters [1995] and Kamperman [1996, Chapt. 6].
2. STANDARD GRAPH REWRITING
In this section we present the preliminaries, including a formal definition of graphs. Furthermore, we define the notion of standard graph rewriting, following for example Staples [1980] and Barendregt et al. [1987].
2.1 Term-Rewriting Systems
Definition 2.1.1. A signature [Sigma] consists of
--a countably infinite set V of variables x, y, z, ...;
--a nonempty set F of function symbols f, g, h, ..., disjoint from V, where each function symbol f is provided with an arity ar(f), being a natural number.
Each i [element of] {1, ..., ar(f)} is called an argument of f. Function symbols of arity are called constants.
Definition 2.1.2. Assume a signature [Sigma] = (V, F, ar). The set of (open) terms l, r, s, t, ... over [Sigma] is the smallest set satisfying
--all variables are terms;
--if f [element of] F and [t.sub.1], ..., [t.sub.ar(f)] are terms, then f([t.sub.1], ..., [t.sub.ar(f)]) is a term.
[t.sub.i] is called the ith argument of f([t.sub.1], ..., [t.sub.ar(f)]). Syntactic equality between terms is denoted by =.
Definition 2.1.3. A rewrite rule is an expression l [right arrow], r with l and r terms, where all variables that occur in the right-hand side r also occur in the left-hand side l.
A term-rewriting system (TBS) R consists of a finite set of rewrite rules.
Definition 2.1.4. A term is linear if it does not contain multiple occurrences of the same variable.
A rewrite rule is left-linear if its left-hand side is linear. A TRS is left-linear if all its rules are.
2.2 Term Graphs
A term graph is an acyclic rooted graph, in which each node has as label a function symbol or variable, and in which its number of children is compatible with the arity of its label.
Definition 2.2.1. A term graph g consists of
--a finite collection N of nodes;
--a root node [v.sub.0] [element of] N;
--a labeling mapping [label.sub.g]: N [right arrow], F [union] V;
--a children mapping [childr.sub.g] : N [right arrow] N*, where N* denotes the collection of (possibly empty) strings over N.
Furthermore, the term graph g must be acyclic; that is, there exists a well-founded ordering [is less than] on N such that if v' [element of] [childr.sub.g](v) then v' [is less than] v. Finally, if [label.sub.g](v) = f, then [childr.sub.g](v) = [v.sub.1] ... [v.sub.ar(f)], where intuitively [v.sub.i] represents the ith argument of f. If [label.sub.g](v) [element of] V, then [childr.sub.g](v) is the empty string.
Each term t can be adapted to a term graph G(t).
--If t = x, then G(t) consists of a single root node, with label x and no children.
--If t = f([t.sub.1], ..., [t.sub.ar(f)]), then the root node of G(t) carries the label f, and its ith child is the root node of G([t.sub.i]) for i = 1, ..., ar(f).
Reversely, each term graph g can be unraveled to obtain a term U(g). Let [v.sub.0] denote the root node of g.
--If [label.sub.g]([v.sub.0]) = x, then U(g) = x.
--If [label.sub.g]([v.sub.0]) = f and [childr.sub.g]([v.sub.0]) = [v.sub.1] ... [v.sub.ar(f)], then we construct the terms U([g.sub.1]), ..., U([g.sub.ar(f)]), where [g.sub.i] differs from g only in the fact that it has root node [v.sub.i]. We define U(g) = f(U([g.sub.1]), ..., U([g.sub.ar(f)])).
In the sequel, term graph is abbreviated to graph.
2.3 Graph Rewriting
We present the notion of standard graph rewriting, induced by a left-linear TRS. First, we give an inductive definition for matching a linear term with a pattern in a graph.
Definition 2.3.1. A linear term l matches node v in graph g if
(1) either l is a variable, in which case l is linked with v;
(2) or l = f([t.sub.1], ..., [t.sub.ar(f)]), and
--[label.sub.g](v) = f and [childr.sub.g](v) = [v.sub.1] ... [v.sub.ar(f)];
--[t.sub.i] matches [v.sub.i] in g, for i = 1, ..., ar(f).
Note that each variable in l is linked with only one node in g, owing to the fact that l is linear.
If the left-hand side of a left-linear rewrite rule l [right arrow] r matches a node v in a graph g, then this may give rise to a rewrite step, in which the pattern l at node v in g is replaced...
Read the full article for free courtesy of your local library.
|
Bookmark this article
Print this article
Link to this article
Email this article
Digg It!
Add to del.icio.us
RSS
