# Lazy Rewriting on Eager Machinery.

1. INTRODUCTIONA 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 0 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 by the pattern G(r). In principle, this means that node v in g is replaced by the root node of G(r), and each node in G(r) that has as label a variable x is replaced by the node in g linked with x. The resulting two graphs [bar]g and [bar]G(r) (with dangling links) are combined to obtain the reduct g' of g. If v is the root node of g, then some care is needed in selecting a new root node for g'.

Definition 2.3.2. The standard rewrite relation [right arrow] on graphs, for a left-linear TRS R, is defined as follows. Assume that l [right arrow] r [element of] R, and assume that l matches node v in graph g. Each variable x in r is linked with a unique node [v.sub.x] in g, owing to the fact that t is linear. Then g [right arrow] g', where g' is constructed as follows.

Construct G(r), such that its nodes do not yet occur in g. Adapt G(r) to [bar]G(r) by renaming, in the image of [childr.sub.G(r)], all occurrences of nodes that have as label a variable x into [v.sub.x]. Adapt g to [bar]g by renaming, in the image of [childr.sub.g], all occurrences of the node v into the root node of [bar]G(r).

--If v is the root node of g, and r is a single variable x then g' = g with as root node [v.sub.x].

--If v is the root node of g and r is not a single variable then g' = [bar]g [union] [bar]G(r) with as root node the root node of [bar]G(r).

--If v is not the root node of g then g' = [bar]g [union] [bar]G(r) with as root node the root node of [bar]g.

It is not hard to see that g' meets the requirements of Definition 2.2.1, so it is a graph.

Remark. For an efficient implementation of graph rewriting it is important to avoid waste of memory space, by means of so-called garbage collection. That is, nodes in a graph that are no longer connected to the root node should be reclaimed. We refrain from a description of garbage collection, because it is not of importance for the rewrite relation as such. The reader is referred to Wilson [1992] for an overview of garbage collection techniques.

Definition 2.3.3. A graph g is called a normal form for a left-linear TRS R if R does not induce any rewrite step g [right arrow] g'.

Henceforth we focus on graph rewriting with the implicit aim to implement term rewriting (e.g., see Baader and Nipkow [1998]). Each parallel reduction in graph rewriting simulates a reduction in term rewriting; see Barendregt et al. [1987] and Kennaway et al. [1994]. That is, consider the left-linear TRS R and a term t. If graph rewriting with respect to R reduces the graph G(t) to the graph g, then term rewriting with respect to R reduces the term t to the term U(g). Moreover, if g is a normal form for graph rewriting with respect to R, then U(g) is a normal form for term rewriting with respect to R.

3. LAZY GRAPH REWRITING

In this section we introduce the notions of a lazy signature, lazy graphs, lazy graph rewriting, and lazy normal forms.

3.1 Lazy Graphs

Definition 3.1.1. In a lazy signature [Sigma] = (V, F, ar), each argument of each function symbol in F is either eager or lazy. The laziness predicate [Lambda] on F x N holds for (f, i) if and only if 1 [is less than or equal to] i [is less than or equal to] ar(f) and the ith argument of f is lazy.

Definition 3.1.2. In a lazy graph g, each node is either eager or lazy, where the root node is always eager.

Each term t over a lazy signature can be adapted to a lazy graph G(t) as before (see Section 2.2), with one extra clause if t = f([t.sub.1], ..., [t.sub.ar(f)]):

--the root node [v.sub.0] of G(t) is eager; each node [v.sub.i] for i = 1, ..., ar(f) is lazy if and only if [Lambda](f, i); all other nodes in G(t) are lazy/eager if they are so in the lazy graphs G([t.sub.1]), ..., G([t.sub.ar(f)]).

An eager node in a lazy graph is called active if it can be reached from the root node via a path of eager nodes. Our notion of lazy graph rewriting only reduces patterns at active nodes.

Definition 3.1.3. The collection of active nodes in a lazy graph g is defined inductively as follows:

--the root node of g is active;

--if v is active, then the eager nodes in [childr.sub.g](v) are active.

A subterm in a term t is said to be active if it corresponds to an active node in G(t).

3.2 Lazy Graph Rewriting

We allow the reduction of redexes at active nodes, and at lazy nodes that are essential in the sense that their contraction may lead to new redexes at active nodes. The reduction of redexes at essential lazy nodes is suspended as much as possible.

We introduce a variation of the notion of matching as formulated in Definition 2.3.1. Intuitively, a left-hand side of a rewrite rule matches modulo laziness an active node v in a lazy graph if it matches up to lazy nodes. These lazy nodes are called essential, to indicate that making them eager and reducing them to normal form could mean the development of a new redex at v.

Definition 3.2.1. A linear term l matches modulo laziness an active node v in a lazy 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)];

--if [v.sub.i] is eager, then [t.sub.i] matches modulo laziness node [v.sub.i] in g, for i = 1, ..., ar(f). If [v.sub.i] is lazy and [t.sub.i] is not a variable, then [v.sub.i] is called essential, for i = 1, ..., ar(f).

We give an example of matching modulo laziness.

Example 3.2.2. Assume a unary function symbol f and constants a and b. Let the lazy graph g consist of two nodes v and v', where the eager root v has label f and its child v' has label a.

--If v' is lazy, then the term f(b) matches modulo laziness the root node v of g, owing to the fact that v has label f. In this case, v' is essential in g.

--If v' is eager, then the term f(b) does not match modulo laziness the root node v of g, due to the fact that its subterm b does not match modulo laziness the active node v' with label a in g.

We define the lazy graph rewrite relation [[right arrow].sub.L] as induced by a left-linear TRS. If the left-hand side of a left-linear rewrite rule l [right arrow] r matches modulo laziness an active node v in a lazy graph g, then g [[right arrow].sub.L] g' where g' is constructed depending on two cases.

(1) The pattern match does not give rise to essential lazy nodes. Then g' can be constructed as in the standard rewrite relation in Definition 2.3.2, where the pattern l in g rooted at v is replaced by the pattern G(r). That is, node v in g is replaced by the root node of G(r), and each node in G(r) with as label a variable x is replaced by the node in g linked with x. If a lazy node in g is linked with a variable in l, then this node is made eager in g' if and only if the variable occurs as an eager argument in r. The laziness annotation of other nodes in g' is inherited from g and G(r). If y is the root node of g, then some care is needed in selecting a new root node for g'.

(2) The pattern match gives rise to essential lazy nodes. Then we may attempt to develop the pattern l at node v, by reducing the subgraph of g that is rooted at such an essential lazy node to normal form. That is, g' can be obtained from g by making an essential lazy node in g eager, so that the subgraph that is rooted at this node can be normalized.

Definition 3.2.3. The lazy rewrite relation [[right arrow].sub.L] on lazy graphs, for a left-linear TRS R, is defined as follows. Assume that l [right arrow] r [element of] R, and assume that l matches modulo laziness an active node v in lazy graph g. Each variable x in r is linked with a unique node [v.sub.x] in g, owing to the fact that l is linear. We distinguish two cases.

(1) Suppose l matching modulo laziness node v in g does not give rise to essential lazy nodes. Then g [[right arrow].sub.L] g', where g' is constructed as follows. Construct G(r), such that its nodes do not yet occur in g. Adapt G(r) to [bar]G(r) by renaming, in the image of [childr.sub.G(r)], all occurrences of nodes with as label a variable y into [v.sub.y]. Adapt g to [bar]g by renaming, in the image of [childr.sub.g], all occurrences of the node v into the root node of [bar]G(r).

--If v is the root node of g, and r is a single variable x then g' = g with as root node [v.sub.x]. [v.suv.x] is eager, while the laziness annotation of all other nodes in g' is inherited from g.

--If v is the root node of g and r is not a single variable then g' = [bar]g [union] [bar]G(r) with as root node the root node of [bar]G(r). For variables y in r, the node [v.sub.y] is lazy in g' if and only if [v.sub.y] is lazy in g and all nodes in G(r) with label y are lazy; the laziness annotation of all other nodes in g' is inherited from g and G(r).

--If y is not the root node of g then g' = [bar]g [union] [bar]G(r) with as root node the root node of [bar]g. For variables y in r, the node [v.sub.y] is lazy in g' if and only if [v.sub.y] is lazy in g and all nodes in G(r) with label y are lazy; the laziness annotation of all other nodes in g' is inherited from g and G(r).

(2) Suppose l matching modulo laziness node v in g does give rise to essential lazy nodes. Let v' be such an essential lazy node. Then g [[right arrow].sub.L] g', where the only distinction between g and g' is that v' is lazy in g and eager in g'.

We give an example of a reduction of a lazy graph by means of the lazy rewrite relation induced by a left-linear TRS.

Example 3.2.4. Assume a unary function symbol f, constants a, b, and c, and a TRS {a [right arrow] b, f(b) [right arrow] c}. Let the lazy graph g consist of two nodes v and v', where the eager root y has label f and its lazy child v' has label a.

v has label f, and its child v' is lazy; so the left-hand side f(b) matches modulo laziness the root node v of g. Since the subterm b of this left-hand side is nonvariable, v' is essential in g. So g [[right arrow].sub.L] g', where g' is obtained from g by making v' eager.

v' has label a and is active in g'. So an application of the rule a [right arrow] b with respect to v' in g' yields g' [[right arrow].sub.L] g", where g" is obtained from g' by renaming the label of v' into b.

The root node v has label f, and its eager child v' has label b in g". So an application of the rule f(b) [right arrow] c with respect to v in g" yields g" [[right arrow].sub.L] g'", where g'" consists only of a root node with the label c. The lazy graph g'" is in lazy normal form.

3.3 Sharing Patterns in Right-Hand Sides

Assume a left-linear TRS R, and suppose a rule l [right arrow] r in R contains multiple occurrences of a nonvariable term t in its right-hand side r. A naive application of this rewrite rule to a graph g would build a separate subgraph in the reduct of g for each occurrence of t in r, after which each of these subgraphs would be evaluated independently. In graph rewriting this waste of space and time can be avoided by the introduction of a let construct, which enables one to share the occurrences of t in r. We show how this let construct can be captured by a transformation of the rewrite rules.

Let P(r) consist of the nonvariable terms that occur more than once in r. Select a t [element of] P(r), such that P(r) contains either no or more than one element of the form f([s.sub.1], ..., [s.sub.i-1], t, [s.sub.i+1], ..., [s.sub.ar(f)]). (Namely, if P(r) contains exactly one such term, then it is more efficient to share the occurrences of f([s.sub.1], ..., [s.sub.i-1], t, [s.sub.i+1], ..., [s.sub.ar(f)]) in r.) A t [element of] P(r) that satisfies the criterion above can be determined efficiently in a bottom-up fashion. We fix a fresh variable y, and replace each occurrence of t in r by y, to obtain a term r'. Let [x.sub.1], ..., [x.sub.n], y be the variables that occur in r'. We introduce a fresh function symbol h of arity n + 1, with [Lambda](h, n + 1) if and only if t does not occur at an active position in r, and [Lambda](h, i) for i = 1, ..., n if and only if [x.sub.i] is a lazy argument in l and does not occur at an active position in r. We replace l [right arrow] r by two rewrite rules:

l [right arrow] h([x.sub.1], ..., [x.sub.n], t)

h([x.sub.1], ..., [x.sub.n], y) [right arrow] r'

These two new rewrite rules together simulate the original rewrite rule l [right arrow] r. The first rule builds the term t as an argument of h; this building process is suspended if t does not occur at an active position in r. In the second rule the term t is represented by the variable y; graph rewriting ensures that the multiple occurrences of y in r' are shared. We repeat this procedure until all multiple occurrences of nonvariable terms in right-hand sides of rewrite rules have been removed.

Strandh [1987] proposed a similar transformation in equational programming [O'Donnell 1985], to share patterns in right-hand sides of equations. Strandh's transformation moreover compresses the size of these patterns. In Section 4.5 we apply a similar strategy to compress the size of lazy arguments in right-hand sides of rewrite rules. Strandh proved that his transformed program simulates the original program, and concluded that the transformation preserves a useful confluence property.

Suppose we want to reduce a lazy graph g. The efficiency of lazy graph rewriting can be optimized by sharing nodes in g. It can be determined, in a bottom-up fashion, whether the subgraphs rooted at distinct nodes in g are the same. If so, then the two nodes can be compressed to a single node.

Similar to the transformation from term to graph rewriting, sharing subterms in right-hand sides and sharing nodes in lazy graphs give rise to a form of parallel rewriting: shared nodes are reduced simultaneously. Each parallel reduction with respect to the transformed TRS simulates a reduction with respect to the original TRS, where the reduction of shared nodes in the transformed TRS corresponds with the reduction of the separate nodes in the original TRS.

3.4 Lazy Normal Forms

Definition 3.4.1. A normal form for [[right arrow].sub.L] is called a lazy normal form.

If we abstract away from laziness annotations of lazy graphs, then there are more lazy normal forms with respect to [[right arrow].sub.L] than that there are normal forms with respect to the standard rewrite relation [right arrow]. The question arises whether all lazy normal forms are acceptable as such. Lazy rewriting takes the view that a subgraph of a lazy normal form only needs to be in normal form if it is rooted at an active node. Therefore, Proposition 3.4.3 shows that a lazy normal form only allows (possibly infinitely many) uninteresting rewrite steps. Hence, we conclude that lazy normal forms are acceptable indeed.

Definition 3.4.2. Let t be a term over a lazy signature, and assume a fresh constant [Zeta]. The term [t.sub.[Zeta]] is obtained by replacing lazy arguments in t by [Zeta]. We write t [[equivalent].sub.[Zeta]] t' if [t.sub.[Zeta]] = [t'.sub.[Zeta]].

Proposition 3.4.3. If g is a lazy normal form and g [[right arrow]* g', then U(g) [[equivalent].sub.[Zeta]] U(g').

PROOF. Assume toward a contradiction that U(g) [[not equivalent].sub.[Zeta]] U(g'). Then there is a rewrite rule that matches some active node in g. Since g is a lazy normal form, this redex in g must involve a lazy node, which according to Definition 3.2.1 (2) is essential. So according to Definition 3.2.3 (2) this lazy node in g can be rewritten, by means of [[right arrow].sub.L], to an eager node. This contradicts the fact that g is a lazy normal form.

4. TRANSFORMATIONS OF REWRITE RULES

In this section we explain how lazy rewriting can be implemented using the same primitives as an implementation of eager rewriting.

4.1 Specificity of Left-Hand Sides

We apply the rightmost innermost rewriting strategy. (The preference for rightmost is not of importance; we could also opt for leftmost innermost rewriting.) Let [dep.sub.g](v) denote the collection of nodes v' in g for which there exists a path in g from v to v'.

v' [element of] [dep.sub.g](v)

v' [element of] [dep.sub.g](v) [conjunction] v" [element of] [childr.sub.g](v') ?? v" [element of] [dep.sub.g](v)

The rightmost innermost ordering [is less than] on nodes in a graph g is defined as follows:

--(Innermost) if v' [element of] [childr.sub.g](v) then v [is less than] v';

--(Rightmost) if [childr.sub.g](v) = [v.sub.1] ... [v.sub.n] and 1 [is less than or equal to] i [is less than] j [is less than or equal to] n, then v' [is less than] v" for all v' [element of] [dep.sub.g]([v.sub.i]) and v" [element of] [dep.sub.g]([v.sub.j]).

We disambiguate overlapping left-hand sides of rewrite rules using a specificity relation ?? from Fokkink et al. [1998]. The definition of ?? below generalizes Fokkink et al. [1998, Def. 2.2.1] by taking into account the laziness annotation. If two left-hand sides are overlapping, then we give priority to the most evolved term structure, so typically x ?? f([t.sub.1], ..., [t.sub.ar(f)]). The specificity relation between two terms f([s.sub.1], ..., [s.sub.ar(f)]) and f([t.sub.1], ..., [t.sub.ar(f)]) is established by first comparing their eager arguments from left to right, and then their lazy arguments from right to left. Let [[equals].sub[Alpha]] denote syntactic equality modulo [Alpha]-conversion, that is, modulo renaming of variables.

Definition 4.1.1. The syntactic specificity relation ?? on terms is defined by

--x ?? f([t.sub.1], ..., [t.sub.ar(f)]);

--f([s.sub.1], ..., [s.sub.ar(f)]) ?? f([t.sub.1], ..., [t.sub.ar(f)]) if there is an eager argument i of f such that

--[s.sub.j] [[equals.sub.Alpha]] [t.sub.j] for eager arguments j [is less than] i of f;

--[s.sub.i] ?? [t.sub.i].

--f([s.sub.1], ..., [s.sub.ar(f)]) ?? f([t.sub.1], ..., [t.sub.ar(f)]) if [s.sub.j] [[equals.sub.[Alpha]] [t.sub.j] for all eager arguments j of f, and there is a lazy argument i of f such that

--[s.sub.j] [[equals.sub.[Alpha]] [t.sub.j] for lazy arguments j [is greater than] i of f;

--[s.sub.i] ?? [t.sub.l].

The specificity relation ?? is extended to rewrite rules by

l ?? l' ?? l [right arrow] r ?? l' [right arrow] r'.

Note that a rewrite rule with a variable as left-hand side is less specific than any rewrite rule with a nonvariable left-hand side.

The specificity relation on terms is not transitive. For example, let the binary function symbol f have two eager arguments. Then f(x,a) ?? f(a,x) and f(a,x) ?? f(a, b), but f(x, a) ?? f(a, b). However, if two linear terms s and t can be unified, then s ?? t, t ?? s, or s [[equals].sub.[Alpha]] t. In order to ensure that each collection of overlapping left-linear rewrite rules contains a most specific rewrite rule, it suffices to require that left-hand sides of distinct rewrite rules are not equal modulo [Alpha]-conversion.

We proceed to present the definition of rightmost innermost lazy rewriting with respect to the specificity relation, denoted by [??.sub.L].

Definition 4.1.2. Given a left-linear TRS R, the binary rewrite relation [??.sub.L] is defined inductively as follows. Suppose the lazy graph g is not a lazy normal form for R. Then there exist rewrite rules in R that match modulo laziness with active nodes in g.

--Select the rightmost innermost active node v in g such that the left-hand side of some rewrite rule in R matches modulo laziness node v in g.

--Select the greatest rule l [right arrow] r in R, with respect to the specificity relation, such that l matches modulo laziness node v in g.

We distinguish two possibilities.

(1) Suppose l [right arrow] r matching modulo laziness node v in g does not give rise to essential lazy nodes. Then, according to Definition 3.2.3 (1), it yields a rewrite step g [[right arrow].sub.L] g' that replaces the pattern l at node v in g by G(r). Define g [??.sub.L] g'.

(2) Suppose l [right arrow] r matching modulo laziness node v in g does give rise to essential lazy nodes. Then, according to Definition 3.2.3(2), it yields a rewrite step g [[right arrow].sub.L] g' that makes the rightmost of these essential lazy nodes in g eager. Define g [??.sub.L] g'.

[??.sub.L] is a subrelation of [[right arrow.sub.L], and these two relations give rise to the same class of lazy normal forms.

4.2 Suppressing Laziness in Right-Hand Sides

For an efficient implementation of the lazy rewrite relation [??.sub.L] that is induced by some left-linear TRS R, it is desirable to have only few lazy arguments in the right-hand sides of rewrite rules. We explain how to get rid of certain laziness annotations in right-hand sides of rewrite rules.

For each rewrite rule l [right arrow] r in R, nonvariable subterms of the right-hand side r that occur as proper subterms of the left-hand side l, and variables in r that occur as an eager argument in l, can be assigned the label eager in r without affecting termination behavior. Namely, such subterms of r are in lazy normal form with respect to [??.sub.L]. We proceed to give a formal argumentation to support this claim.

Let v be the rightmost innermost active node of a lazy graph g, such that the left-hand side of a most specific rewrite rule l [right arrow] r in R matches modulo laziness node v in g. Moreover, suppose this match does not give rise to essential lazy nodes in g. Then, according to Definition 4.1.2 (1), this match induces a reduction g [??.sub.L] g', where the pattern l at node v in g is replaced by G(r). Suppose some subterm t of r occurs as a proper subterm of l, with either t [is not an element of] V or t is an eager argument in l.

l matches modulo laziness node v in g, and t is a subterm of l; so t is linked with a descendant [v.sub.0] of v in g. Since t is a proper subterm of l, v [is less than] [v.sub.0] with respect to the rightmost innermost ordering on nodes in g. Furthermore, since either t is a nonvariable subterm of l or t is all eager argument in l, and l matches modulo laziness node v in g without giving rise to essential lazy nodes, it follows then that [v.sub.0] is active in g. Hence, the subgraph of g with root node [v.sub.0] is a lazy normal form for R. Let v' denote the node in G(r) (and so in g') that stems from the subterm t of r. Since t is linked with [v.sub.0] in g, a linear term matches modulo laziness node [v.sub.0] in g if and only if it matches modulo laziness node v' in g'. So the subgraph of g' with root node v' is a lazy normal form for R.

4.3 Pattern Matching Modulo Laziness

We explain intuitively how laziness annotations in left-hand sides of rewrite rules can be taken into account in a pattern-matching algorithm. Assume that, while attempting to match a linear term l with an active node v in a lazy graph g, we encounter a lazy argument in l. Then this subterm of l and the node in g that should match it are stored as a pair, for future reference. Pattern matching proceeds to check whether l matches modulo laziness node v in g. If in the end this pattern match is successful, then we may have discovered several lazy arguments [l.sb.1], ..., [l.sub.n] in l and corresponding nodes [v.sub.1], ..., [v.sub.n] in g on the way. (See O'Donnell [1985, Sect. 18] for several ways to represent and traverse the stack of pairs <[l.sub.i], [v.sub.i]>.) We make the rightmost node [v.sub.n] eager, and we reduce the subgraph rooted at [v.sub.n]. If this reduction produces a normal form, then we test whether this normal form matches the corresponding subterm [l.sub.n] of l. If so, then the next rightmost node [v.sub.n-1] is made eager, etc. This procedure is repeated until

(1) either a normal form of some node [v.sub.l] does not match the corresponding subterm [l.sub.i] of l, in which case it is concluded that l does not match node v;

(2) or all nodes [v.sub.1], ..., [v.sub.n] have been made eager, and their normal forms matched the corresponding subterms [l.sub.1], ..., [l.sub.n] of l, in which case it is concluded that l matches node v.

In Fokkink et al. [1998] we introduced a pattern-matching algorithm for rightmost innermost rewriting with respect to a specificity relation, which is employed in the eager equational programming language Epic [Walters 1997; Walters and Kamperman 1996]. This pattern-matching algorithm, based on finite automata [Hoffmann and O'Donnell 1982a], can share matchings of the same function symbol in distinct patterns, thus supporting an efficient implementation; see Fokkink et al. [1998]. We adapt the transformation rules in Fokkink et al. [1998, Sect. 3.4] to minimize left-hand sides of rewrite rules, so that they take into account laziness annotations in left-hand sides.

Definition 4.3.1. A rewrite rule f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] r with [x.sub.1], ..., [x.sub.ar(f)] distinct variables is called a most general rule for f.

We transform the rewrite rules of a left-linear TRS R, so that the left-hand sides in the resulting TRS represent the success-transitions of a pattern-matching automaton for the lazy rewrite relation [??.sub.L] as induced by R. Following the specificity rule (see Definition 4.1.1), first the eager arguments of a left-hand side in R are scanned from left to right, and next its lazy arguments are scanned from right to left. In the resulting TRS, left-hand sides contain no more than two function symbols, and lazy arguments in left-hand sides are variables. The transformation distinguishes two principles. The first principle reduces the size of a left-hand side with more than two function symbols, while the second principle makes a lazy nonvariable argument in a left-hand side eager.

(1) Assume that, for some function symbol f and an eager argument i of f, there is a rule in R with left-hand side f([s.sub.1], ..., [s.sub.ar(f)]) that contains more than two function symbols, where [s.sub.i] is not a variable.

We add a fresh function symbol [f.sup.d] to F, which inherits the arity and the laziness annotation from f. All occurrences of the function symbol f inside left-hand sides of rewrite rules are replaced by [f.sup.d].

Each rewrite rule in R of the form

f([s.sub.1], ..., [s.sub.i-1], g([t.sub.1], ..., [t.sub.ar(g)]), [s.sub.i+1], ..., [s.sub.ar(f)]) [right arrow] r

with [s.sub.j] [element of] V for eager arguments j [is less than] i of f is replaced by a rule

(1) [f.sub.g]([s.sub.1], ..., [s.sub.i-1], [t.sub.1], ..., [t.sub.ar](g), [s.sub.i+1], ..., [s.sub.ar(f)]) [right arrow] r.

Here, [f.sub.g] is a fresh function symbol of arity ar(f) + ar(g) - 1, which inherits the laziness annotation from f(_, g(_), _):

--[Lambda]([f.sub.g],j) ?? [Lambda](f,j) for j = 1, ..., i- 1;

--[Lambda]([f.sub.g],j) ?? [Lambda](g,j - i + 1) for j = i, ..., ar(g) + i - 1;

--[Lambda]([f.sub.g],j) ?? [Lambda](f,j - ar(g) + 1) for j = ar(g) + i, ..., ar(f) + ar(g) - 1.

For each [f.sub.g] we add a rule

f ([x.sub.1], ..., [x.sub.i] - 1, g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1, ..., [x.sub.ar(f)]) [right arrow] [f.sub.g]([x.sub.1], ..., [x.sub.l-1], [y.sub.1], ..., [y.sub.ar](g), [x.sub.l+1], ..., [x.sub.ar(f)]).

For each [f.sub.g] for which rule (1) does not contain a most general rule, we add a most general rule

[f.sub.g]([x.sub.1], ..., [x.sub.l-1], y1, ..., [y.sub.ar](g), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sub.d]([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]).

Left-hand sides f([s.sub.1], ..., [s.sub.ar(f)]) of rewrite rules with [s.sub.j] [element of] V for eager arguments j [is less than or equal to] i of f are replaced by [f.sub.d]([s.sub.1], ..., [s.sub.ar(f)]). Finally, we add a rule

f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.ar(f)]).

(2) Assume that, for some function symbol f and a lazy argument i of f, there is a rule in R with left-hand side f([s.sub.1], ..., [s.sub.ar(f)]) where [s.sub.i] is not a variable.

We add a fresh function symbol [f.sup.d] of arity ar(f), with laziness annotation:

--??[Lambda]([f.sup.d], i);

--[Lambda]([f.sup.d],j) ?? [Lambda](f,j) for j [is not equal to] i.

All occurrences of the function symbol f inside left-hand sides of rewrite rules are replaced by [f.sup.d].

Left-hand sides f([s.sub.1], ..., [s.sub.ar(f)]) of rewrite rules with [s.sub.j] [element of] V for eager arguments j of f and for lazy arguments j [is greater than] i of f are replaced by [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]). Finally, we add a rule

f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.ar(f)]).

The two transformation principles above are repeated until each left-hand side contains no more than two function symbols and lazy arguments in left-hand sides are single variables. This transformation halts on each left-linear TRS. Namely, each application of the first principle strictly decreases the sum of the sizes of left-hand sides with more than two function symbols, and this sum is not increased by applications of the second principle. Furthermore, each application of the second principle strictly decreases the total number of lazy nonvariable arguments in left-hand sides.

The transformation involves an extension of the alphabet with the function symbols [f.sup.d] and [f.sub.g], and an adaptation of the class of normal forms: occurrences of f in normal forms are renamed into [f.sup.d]. In Section A.2 in the appendix it is shown that the lazy rewrite relation [??.sub.L] with respect to the transformed TRS simulates the lazy rewrite relation [??.sub.L] with respect to the original TRS, and that this simulation is sound, complete, and termination preserving [Fokkink and van de Pol 1997]. Hence, no information on normal forms for the lazy rewrite relation [??.sub.L] with respect to the original TRS is lost.

The introduction of the function symbol [f.sup.d] in the two transformation principles is reminiscent of a transformation by Thatte [1985] to make TRSes constructor-based; see Thatte [1988], Durand and Salinier [1993], Verma [1995], and Luttik et al. [1996] for subsequent improvements on the correctness of this transformation. Salinier and Strandh [1996] use a similar transformation technique to simulate a forward-branching TRS by a constructor-based strongly sequential TRS; they also prove correctness of their transformation.

Remark. Sherman et al. [1991] optimize the efficiency of the implementation of their pattern-matching automaton for equational programming [O'Donnell 1985] by the elimination of redundant intermediate rewrite steps. Basically, if a function symbol f is not a constructor, then a subterm f([t.sub.1], ..., [t.sub.ar(f)]) in the right-hand side of an equation is replaced by its possible reducts. In general this requires making the arguments [t.sub.i] more specific, by substituting (open) terms for their variables. This optimization could also be applied with respect to our pattern-matching automaton for lazy rewriting.

4.4 Thunking Lazy Nodes in Lazy Graphs

The laziness annotation of a lazy graph and the rewrite relation [??.sub.L] can be implemented using thunks [Ingerman 1961], which enable one to abstract away from laziness annotations and to apply pure rightmost innermost rewriting.

Suppose we want to rewrite a lazy graph by means of [??.sub.L]. Then, first the nodes of the lazy graph that are not active are thunked, to prevent that they can be rewritten in an eager fashion. If a node v is not active, and has label f and children [v.sub.i], ..., [v.sub.ar(f)], then the subgraph f([v.sub.1], ..., [v.sub.ar(f)]) at v is adapted to [Theta]([[Tau].sub.f], [vec.sub.[Alpha]]([v.sub.1], ..., [v.sub.ar(f)])), one where [Alpha] is a string of ar(f) zeros, to mark that the arguments of [vec.sub.[Alpha]] are all lazy. This conversion turns the node v into a normal form, while its label is stored as the token [[Tau].sub.f] and its children are stored as the arguments of [vec.sub.[Alpha]]. The function symbols [Theta], [[Tau].sub.f], and [vec.sub.[Alpha]] for binary strings [Alpha] are all fresh.

--[Theta], called a thunk, is a binary function symbol with two eager arguments.

--The [[Tau].sub.f] for f [element of] F are constants.

--Let [Alpha] be a binary string. The function symbol [vec.sub.[Alpha]] has arity |[Alpha]|, and for i = 1, ..., |[Alpha]| the i-argument of [vec.sub.[Alpha]] is lazy if and only if [[Alpha].sub.i] = 0. The [vec.sub.[Alpha]] are auxiliary function symbols, which enable one to collect several nodes below the second argument of the thunk [Theta].

Precisely, each lazy graph g over the original signature is adapted to a graph g[Theta] over the extended signature as follows.

(1) If v is active in g or if [label.sub.g](v) = x [element of] V, then

[label.sub.g[Theta]] (v) = [label.sub.g](v)

[childr.sub.g[Theta]] (v) = [childr.sub.g](v).

(2) If v is not active in g and [label.sub.g](v) = f [element of] F, then the children of v are made lazy, and two fresh eager nodes v' and v" are added to [g.sub.[Theta]]; thus, we define

[label.sub.g[Theta]] (v) = [Theta] [label.sub.g[Theta]] (v') = [[Tau].sub.f] [label.sub.g[Theta]] (v") = [vec.sub.[Alpha]] [childr.sub.g[Theta]] (v) = v' [multiplied by] v" [childr.sub.g[Theta]] (v') = [element of] [childr.sub.g[Theta]] (v") = [childr.sub.g](v).

Here, [Alpha] consists of ar(f) zeros, and [element of] represents the empty string.

From now on we focus on rewriting lazy graphs over the extended signature. In the remainder of this section and in the next sections, we define and adapt rewrite rules to introduce and eliminate thunks.

Suppose a lazy graph over the extended signature is rewritten according to our lazy rewriting strategy, and an application of a rewrite rule makes a node with the label [Theta] active. Then we want to restore the original graph structure at this node, because active nodes have to be rewritten in an eager fashion. Therefore, we introduce a fresh unary function symbol inst with an eager argument. Moreover, we add left-linear rewrite rules to the TRS, for function symbols f [element of] F:

inst([Theta]([[Tau].sub.f], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.ar(f)]))) [right arrow] f([x.sub.1], ..., [x.sub.ar(f)])

where [Alpha] denotes a string of ar(f) zeros. These rewrite rules find application in Section 4.6, where so-called migrant variables in rewrite rules, which migrate from a lazy argument in the left-hand side to an active position in the right-hand side, are instantiated using the function symbol inst.

4.5 Thunking Lazy Arguments in Right-Hand Sides

Suppose a lazy graph over the extended signature is rewritten according to our lazy rewriting strategy, and suppose a rewrite rule is applied that contains lazy arguments in its right-hand side. Then we have to thunk these lazy arguments in the resulting reduct, according to the ideas explained in Section 4.4. This can be achieved by a transformation of the right-hand sides of rewrite rules.

Consider a left-linear rewrite rule l [right arrow] r, and let the collection S(l, r) of nonvariable lazy arguments in r be nonempty. We select an element t in S(l, r), such that its proper subterms are not in S(l, r). (Namely, if t contains a proper nonvariable lazy argument s, then we first want to thunk s before thunking t; expanding t in an eager argument should not mean expanding s at the same time.) A t [element of] S(l, r) that satisfies the criterion above can be determined efficiently in a bottom-up fashion. We introduce a fresh constant [Lambda], which is added to the signature. Suppose t contains n variables [x.sub.1], ..., [x.sub.n]. Let r' be obtained from r by replacing the lazy argument t in r by

[Theta]([Lambda], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.n]))

where |[Alpha]| = n, and [[Alpha].sub.i] = 0 if and only if [x.sub.i] is a lazy argument in l and does not occur at an active position in r. The rewrite rule l [right arrow] r is replaced by

l [right arrow] r'.

Furthermore, one extra rewrite rule is introduced to restore the original term structure t:

inst([Theta]([Lambda], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.n]))) [right arrow] t

We continue to thunk the remaining nonvariable lazy arguments in the right-hand side of l [right arrow] r'.

4.6 Instantiation of Migrant Variables

Suppose the left-hand side of a most specific rewrite rule l [right arrow] r matches modulo laziness a rightmost innermost active node v in a lazy graph g without giving rise to essential lazy nodes. According to Definition 4.1.2 (1) this yields a rewrite step g [??.sub.L] g'. If a variable x in l is linked with a lazy node [v.sub.x] in g, and if x occurs at an active position in r, then [v.sub.x] becomes active in g'; see Definition 3.2.3 (1). Since [v.sub.x] is lazy, the variable x must occur as a lazy argument in l. In order to be able to abstract away from laziness annotations, we make the transfer of variables from lazy to active explicit, using the function symbol inst.

Definition 4.6.1. A variable x is called migrant for a rewrite rule l [right arrow] r if it occurs as a lazy argument in l and at an active position in r.

The migrant variables of a rewrite rule are instantiated using the function symbol inst as follows. For each rewrite rule l [right arrow] r we determine its collection of migrant variables. The term r' is obtained from r by replacing each migrant variable x by inst(x), and the rewrite rule l [right arrow] r is replaced by

l [right arrow] r'.

Finally, we add a most general rewrite rule for inst, in case this function symbol is applied to a node that is not thunked:

inst(x) [right arrow] x

4.7 Overview

Suppose we want to rewrite a lazy graph by means of a left-linear TRS over a lazy signature, using the lazy rewrite relation [??.sub.L]. We give an overview of the transformations in the previous sections, which are applied so that this rewriting strategy can be performed by means of rightmost innermost rewriting.

(1) Multiple occurrences of a nonvariable term in the right-hand side of a rewrite rule are shared (Section 3.3).

(2) Left-hand sides of rewrite rules are minimized, so that they represent the success-transitions of an automaton for pattern matching modulo laziness with respect to the specificity relation (Section 4.3).

(3) Lazy arguments in right-hand sides of rewrite rules are thunked (Section 4.5).

(4) Rewrite rules are added that are able to eliminate thunks in right-hand sides of rewrite rules (Section 4.5).

(5) The migrant variables of a rewrite rule, which migrate from a lazy argument in the left-hand side to an active position in the right-hand side, are instantiated in the right-hand side (Section 4.6).

(6) A most general rule is added for the function symbol inst (Section 4.6).

(7) In the lazy graph that is to be rewritten, nodes that are not active are thunked (Section 4.4).

(8) General unthunk rules are added to support unthunking of arbitrary terms that may result from thunking input terms (Section 4.4).

Steps (1)-(6) and (8) are performed during compilation of the original TRS. Step (7) is performed at the input of the subject term.

Correctness of step (1) was addressed in Proposition 3.4.3, while correctness of step (2) is discussed in Section A.2 of the appendix. The correctness of steps (3)-(8) also needs to be addressed; these transformations involve an extension of the alphabet with the function symbols [Theta], [[Tau].sub.f], [vec.sub.[Alpha]], [Lambda], and inst, and an adaptation of the class of normal forms. In Section A.3 of the appendix it is shown that eager rewriting with respect to the transformed TRS simulates the lazy rewrite relation [??.sub.L] with respect to the original TRS, and that this simulation is sound, complete, and termination preserving. Hence, no information on normal forms for the lazy rewrite relation [??.sub.L] is lost; see Fokkink and van de Pol [1997].

Suppose the transformed TRS reduces the thunked version of the lazy graph to a normal form, by means of rightmost innermost rewriting. This normal form may contain nodes with the label [f.sup.d] or [Theta]. As a final step we apply the simulation mappings from the appendix to this normal form, which rename labels [f.sup.d] into f, and which replace thunked nodes by their original graph structures.

4.8 An Example

We consider the left-linear TRS with overlapping left-hand sides that was used as a running example in the introduction. Its signature consists of the constant 0, the unary function symbols succ and in f, and the binary function symbols nth and cons, with only the second argument, of cons lazy, and all other arguments eager. The TRS consists of three rewrite rules:

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

Owing to the specificity relation, rule (3) has priority over rule (2).

Recall that eager evaluation of the term nth(succ(0), inf(0)) leads to an infinite reduction. We show in detail how lazy rewriting as described in this article reduces this term to its desired normal form succ(0). Lazy arguments in right-hand sides of rewrite rules are thunked; migrant variables in right-hand sides of rewrite rules are instantiated by means of the inst function; and a most general rule is added for inst. This produces the TRS

(1') inf(x) [right arrow] cons(x, [Theta]([Lambda], [vec.sub.1](x)))

(2) nth(x, cons(y, z)) [right arrow] y

(3') nth(succ(x), cons(y, z)) [right arrow] nth(x, inst(z))

(4) inst([Theta]([Lambda], [vec.sub.1](x))) [right arrow] inf(succ(x))

(5) inst(x) [right arrow] x.

The lazy argument inf(succ(x)) in the right-hand side of rule (1) has been thunked, and rule (4) has been included for unthunking this argument. The migrant variable z in the right-hand side of rule (3) has been instantiated. Finally, rule (5) is the most general rule for inst.

Note that the term nth(succ(0), inf(0)) does not contain lazy arguments, so there is no need to include tokens [[Tau].sub.f], nor rewrite rules to unthunk these tokens, as described in Section 4.4. We transform nth(succ(0), inf(0)) into a graph:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

For simplicity of presentation, nodes are represented by their labels instead of by their names. We reduce this graph to its normal form, by means of rightmost innermost rewriting.

First, the redex at node inf of this graph is contracted by rule (1'):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Next, the redex at the root node of this graph is contracted by rule (3'):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Next, the redex at node inst is contracted by rule (4):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Next, the redex at node inf is contracted by rule (1'):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Finally, the redex at the root node of this graph is contracted by rule (2)

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

This graph is in normal form. It does not contain thunks, so we transform this graph into the term succ(0), and conclude that this is the normal form of nth(succ(0), inf(0)).

5. CONCLUSIONS AND RELATED WORK

We proposed a novel notion of lazy graph rewriting based on a laziness annotation of arguments of function symbols, in which subgraphs at lazy nodes are not required to be in normal form. We have defined transformation rules for left-linear rewrite systems, such that lazy rewriting with respect to the original rewrite system is simulated by eager evaluation with respect to the transformed rewrite system. Our work is somewhat similar in spirit to the use of evaluation transformers in Burn [1991], and to the protection constructors in the equational programming language Q, based on an eager pattern-matching strategy from Graf [1991]. In context-sensitive term rewriting [Lucas 1995] it is indicated for each argument of a function symbol whether or not contraction of redexes inside such an argument is allowed. Recently, Giesl and Middeldorp [1999] presented a transformation of context-sensitive TRSes into ordinary TRSes such that the original context-sensitive TRS is terminating if and only if the resulting ordinary TRS is terminating.

Chew [1980] applied a directed version of congruence closure [Nelson and Oppen 1980] to obtain a term reduction method which avoids multiple evaluation of the same term structure. Similar to our notion of lazy rewriting, Chew's procedure may halt even when no normal form exists. Moreover, Chew's congruence closure can produce structural loops, leading to a finite representation of an infinite term, and the ability to terminate in cases where the normal form is not finite. Our notion of lazy rewriting does not introduce structural loops. The effect of laziness annotations in the presence of Chew's congruence closure deserves further study.

In Scheme [Rees and Clinger 1986] there are special data structures to delay the (eager) evaluation of a term and to force evaluation of such a delayed expression. Our transformations feature the introduction of similar data structures: the thunk O delays computation of the graph below it, while such a thunk can be eliminated by the function inst. The rewrite rules for inst can be implemented efficiently by representing the thunk [Theta] as a tag-bit, so that testing whether a node is a thunk can be performed as a bit test. Our representation of thunks in right-hand sides of rewrite rules is comparable to the frames used in TIM [Wray and Fairbairn 1989], the closures in the STG machine [Peyton Jones and Salkild 1989], and the closure in the heap in the <v, G> machine [Augustsson and Johnsson 1989].

Our implementation of lazy graph rewriting is inspired by the implementation of modern lazy functional languages. These implementations are lazy by nature, but are optimized to perform as much eager evaluation as possible. For example, Clean [Brus et al. 1987] supports the annotation of strict arguments, while OB J3 [Goguen et al. 1993] supports annotations for the evaluation order of arguments. In Categorical ML, based on the Categorical Abstract Machine [Cousineau et al. 1987], lazy constructors are used to achieve similar effects as our transformations. There, transformation of the program must be carried out manually for the most part.

Huet and Levy [1991] consider orthogonal (so, in particular, nonoverlapping) rewrite systems that are sequential. This ensures that a term that is not in weak head normal form always contains a needed redex, which has to be reduced to normal form in any rewriting strategy. Strong sequentiality [Huet and Levy 1991] allows one to determine such needed redexes efficiently. Strandh [1989] advocates restricting further to forward-branching equational programs, for which each state in the pattern-matching automaton can be reached by success-transitions only. This compares nicely with our notion of active nodes. Durand [1994] gives a quadratic algorithm to decide the forward-branching property; in contrast, no polynomial algorithm is known to decide strong sequentiality. Strandh [1989] presents an efficient innermost implementation of forward-branching equational programs, which maintains the outermost reduction strategy. This pattern-matching algorithm does not give rise to a pair stack of (lazy) nodes and patterns a la O'Donnell [1985] (see also Section 4.3). If all arguments of function symbols are annotated lazy, then our notion of lazy rewriting is closely related to Strandh's implementation method, with the distinction that we do not reduce inessential lazy nodes to normal form.

Conventionally, eager evaluation is referred to as call-by-value, while postponed evaluation without sharing results (such as lazy term rewriting) is referred to as call-by-name, and postponed evaluation with sharing results (such as lazy graph rewriting) is referred to as call-by-need. The relations between these three notions have been investigated in several articles. Plotkin [1975] gave simulations of call-by-name by call-by-value, and vice versa, in the context of the [Lambda]-calculus. In the context of higher-order functional programs, Amtoft [1993] developed an algorithm to transform call-by-name programs into call-by-value programs; Steckler and Wand [1994] used a data-flow analysis to minimize thunkification in this context. Okasaki et al. [1994] gave a continuation-passing style transformation of call-by-need into call-by-value, for a particular [Lambda]-calculus.

We list some advantages of our notion of lazy rewriting, compared to "classic" lazy evaluation.

(1) Some transformations of rewrite rules enable an implementation of lazy rewriting using the same primitives as an implementation of eager rewriting.

(2) A laziness annotation can produce normal forms for terms that do not have a finite reduction under any rewriting strategy.

(3) Only a small structure occurs at a (thunked) lazy node that is introduced in some reduct, and this structure is only expanded if the node is made active.

(4) Our implementation of lazy rewriting is fully integrated with pattern matching (based on the specificity of left-hand sides of rewrite rules).

(5) Rewrite rules can be overlapping, and the rewrite system does not need to be sequential.

(6) No rigid distinction is required between constructors and defined function symbols.

(7) Not only in theory, but also in practice, our technique does not rely on properties of built-in algebraic data types such as lists or trees.

Several abstract machines have been used for the implementation of modern lazy functional languages; these include the S-K reduction machine [Turner 1979], the G machine [Johnsson 1984], the Categorical Abstract Machine [Cousineau et al. 1987], TIM [Wray and Fairbairn 19891, the STG machine [Peyton Jones and Salkild 1989], the ABC machine [Plasmeijer and van Eekelen 1993], Gofer [Jones 1994], and HAM [Bailey 1995]. Bailey [1995, Chapt. 7] presents a detailed comparison between several of these abstract machines. We compare the cost of basic data structures and actions in our scheme with some of these implementations. It should be noted that it is extremely difficult to assess the effect of different design choices on performance (e.g., see Peyton Jones and Salkild [1989]), so we only give a qualitative discussion.

--In our approach, unthunking is only performed if all eager pattern matching is successful. This is not possible in lazy functional languages, where the order of pattern matching and its effects on the evaluation of subterms are fixed.

--In our approach, only a small structure occurs at lazy nodes. In contrast, the ABC machine [Plasmeijer and van Eekelen 1993] builds complete graphs at lazy nodes.

--In our approach, no run-time cost is incurred when all arguments in the original rewrite system are annotated eager. Even when all arguments are found to be strict, TIM and the STG machine make a function call to obtain the tag of a constructor term (this is the reason why they are called "tagless"), whereas our implementation only needs to dereference a pointer. Depending on the architecture, this can make quite a difference, because an instruction cache (if present) is invalidated by performing function calls.

--In an implementation that allows overwriting nodes with nodes of arbitrary size, there is no need for the dreaded indirection nodes [Peyton Jones 1987, Section 12.4]. In our transformed rewrite system this role is fulfilled by [Theta]; every node is evaluated exactly once, either by immediate innermost rewriting, or later on, after unthunking the node. In Peyton Jones [1987], the indirection nodes can only be transformed away after a complicated analysis.

APPENDIX

A. CORRECTNESS OF THE TRANSFORMATIONS

We present formal correctness proofs for the transformations in Section 4.

A.1 Simulation

In Fokkink et al. [1998] we used a notion of simulation of one rewrite system by another rewrite system, to prove correctness of transformations of rewrite systems. A simulation consists of a partially defined, surjective mapping [Phi], which relates terms in the simulating rewrite system to terms in the original rewrite system. We focused on deterministic rewrite systems, in which each term can do no more than one rewrite step (cf. O'Donnell [1998, Def. 3.3.3]).

Consider a simulation [Phi] with domain D([Phi]). The simulation [Phi] is said to be sound if each reduction in the simulating rewrite system from a b [element of] D([Phi]) to a b' can be extended to a reduction to a b" [element of] D([Phi]), such that [Phi](b) can be rewritten to [Phi](b") in the original rewrite system. Furthermore, [Phi] is complete if for each normal form b for the simulating rewrite system, b [element of] D([Phi]) and [Phi](b) is a normal form for the original rewrite system. Finally, [Phi] preserves termination if for each term b [element of] D([Phi]) for which the original rewrite system is terminating for [Phi](b), the simulating rewrite system is terminating for b.

Soundness, completeness, and termination preservation are preserved under composition of simulations. Fokkink and van de Pol [1997] prove that if a simulation is sound, complete, and termination preserving, then no information on normal forms in the original rewrite system is lost. That is, there exist mappings parse from original to transformed terms and print from transformed to original terms such that for each original term t its normal form can be computed as follows: compute the normal form of parse(t) and apply the print function to it.

In Fokkink and van de Pol [1997], correctness is proved for fully defined simulations, but the proof easily extends to partially defined simulations; see Fokkink et al. [1998, App. A]. Allowing partially defined simulations enables one to abstract away from fresh function symbols in the simulating system that are always eliminated from a reduct immediately after they are introduced in the reduct (such as the auxiliary function symbols [f.sub.g] in the minimization of left-hand sides). This can reduce the number of cases that have to be considered in the proofs of soundness, completeness, and termination preservation.

Definition A.1.1. An abstract reduction system (ARS) consists of a collection A of elements, together with a binary reduction relation R between elements in A.

Definition A.1.2. A simulation of an ARS (A, R) by an ARS (B, S) is a surjective mapping [Phi]: D([Phi]) [right arrow] A with D([Phi]) [subset or equal to] B.

In the remainder of this section we focus on deterministic ARSes (A, R), in which each element a [element of] A can do an R-step to no more than one element a'. Let R* denote the reflexive transitive closure of R.

Definition A.1.3. Let the deterministic ARS (B, S) simulate the deterministic ARS (A, R) by means of a surjective mapping [Phi] : D([Phi]) [right arrow] A.

--[Phi] is sound if, for each b [element of] D([Phi]) and b' [element of] B with bSb', there is a b" [element to] D([Phi]) with b'S*b" and either [Phi](b) = [Phi](b") or [Phi](b)R[Phi](b").

--[Phi] is complete if, for each normal form b [element of] B for S, b [element of] D([Phi]) and [Phi](b) is a normal form for R.

--[Phi] preserves termination if, for each [b.sub.0] [element of] D([Phi]) that induces an infinite S-reduction [b.sub.0]S[b.sub.1]S[b.sub.2]S ..., there is a k [is greater than or equal to] 1 such that [b.sub.k] [element of] D([Phi]) and [Phi]([b.sub.0])R[Phi]([b.sub.k]).

For a deterministic ARS (A, R), we define that nfR : A [right arrow] A [union] {[Delta]} maps each a [element of] A to its normal form for R; elements that do not have a normal form, because they induce an infinite R-reduction, are mapped to [Delta] (which represents "divergence").

Definition A.1.4. A deterministic ARS (B, S) is a correct transformation of a deterministic ARS (A, R) if there exist mappings parse: A [right arrow] B and print: B [right arrow] A such that the diagram below commutes:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where print([Delta]) = [Delta].

We note that the composition of two correct transformations is again a correct transformation.

Theorem A.1.5. If a simulation [Phi] between two deterministic ARSes is sound, complete, and termination preserving, then it is a correct transformation.

PROOF. See Fokkink et al. [1998, App. A]. (Basically, parse is some inverse of [Phi], and print is [Phi]) [Square]

A.2 Minimization of Left-Hand Sides

We prove that the procedure in Section 4.3 to minimize left-hand sides is correct. Let [Sigma] = (V, F, ar) denote the original lazy signature and G([Sigma]) the collection of lazy graphs over [Sigma]. Furthermore, R is the original left-linear TRS and S the TRS that results after applying one of the two transformation principles in Section 4.3 to R. Finally, ?? and ?? represent the lazy rewrite relation ?? as induced by R and S, respectively. We prove correctness of the two transformation principles in Section 4.3 separately, using simulations.

A.2.1 First Transformation Rule. Suppose we apply the first transformation rule to the left-linear TRS R, with respect to f [element of] F and eager argument i of f. The transformation introduces fresh function symbols: [f.sup.d] has the same arity and laziness annotation as f, while the [f.sub.g] for g [element of] F have arity ar(f) + ar(g) - 1 and inherit their laziness annotation from f (_, g(_), _):

--[Lambda]([f.sub.g], j) ?? [Lambda](f, j) for j = 1, ..., i - 1;

--[Lambda]([f.sub.g], j) ?? [Lambda](g, j - i + 1) for j = i, ..., ar(g) + i - 1;

--[Lambda]([f.sub.g], j) ?? [Lambda](f, j - ar(g) + 1) for j = ar(g) + i, ..., ar(f) + ar(g) - 1.

Let s be the term that is obtained from term s by renaming all occurrences of f into [f.sup.d]. Moreover, let f = [f.sup.d] and g = g for g [element of] F\{f}. The transformed TRS S consists of six collections [S.sub.0]-[S.sub.5]:

--g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] [S.sub.0] iff g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] R with g [is not equal to] f or [s.sub.j] [is not an element of] V for some eager argument j [is less than] i of f;

--f([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sub.g] ([x.sub.1], ..., [x.sub.[Iota]-1], [y.sub.1], ..., [y.sub.ar(g)], [x.sub.i+1], ..., [x.sub.ar(f)]) [element of] [S.sub.1] iff f([s.sub.1], ..., [s.sub.i-1], g([t.sub.1], ..., [t.sub.ar(g)]), [s.sub.[Iota]+1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [element of] V for all eager arguments j [is less than] i of f;

--[f.sub.g]([s.sub.1], ..., [s.sub.i-1], [t.sub.1], ..., [t.sub.ar(g)], [s.sub.i+1], ..., [s.sub.ar(f)]) [right arrow] r [element of] [S.sub.2] iff f([s.sub.1], ..., [s.sub.i-1], g([t.sub.1], ..., [t.sub.ar(g)]), [s.sub.i+1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [element of] V for all eager arguments j [is less than] i of f;

--[f.sub.g]([x.sub.1], ..., [x.sub.l-1], [y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [element] [S.sub.3] iff f([s.sub.1], ..., [s.sub.i-1], g([t.sub.1], ..., [t.sub.ar(g)]), [s.sub.[Iota]+1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [element of] V for all eager arguments j [is less than] i of f, and there is no most general rule for [f.sub.g] in [s.sub.2];

--[S.sub.4] = {f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.ar(f)])};

--[f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] [S.sub.5] iff f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] V for all eager arguments j [is less than or equal to] i of f.

Let [Sigma]' denote the original signature [Sigma] extended with the fresh function symbols [f.sup.d] and [f.sub.g], and let

B = {g [element of] G([Sigma]') | [exists][g.sub.0] [element of] G([Sigma]) ([g.sub.0] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] g)}.

The next two lemmas follow by induction with respect to the length of a derivation with [g.sub.0] [element of] G([Sigma]).

LEMMA A.2.1. If g [element of] B, then the subgraphs rooted at active nodes of g are in B.

LEMMA A.2.2. If g [element of] B, then only active nodes in g can carry labels [f.sub.g].

We prove that the transformation of (G([Sigma]), ??) into (B, ??) is correct, by means of a simulation. The mapping [Phi] D([Phi]) [right arrow] G([Sigma]) is defined for lazy graphs in B that do not contain labels [f.sub.g]. The lazy graph [Phi](g) is obtained from g [element of] D([Phi]) by renaming all labels [f.sup.d] into f. The mapping [Phi] is surjective, because it is the identity mapping on G([Sigma]) [subset or equal to] D([Phi]). Hence, [Phi] constitutes a (partially defined) simulation of (G([Sigma]), [??.sub.R]) by (B, [??.sub.S]). We proceed to prove that [Phi] is sound, complete, and termination preserving.

COMPLETENESS. If g [element of] B is a lazy normal form for S, then g [element of] D([Phi]) and [Phi](g) is a lazy normal form for R.

PROOF. We apply induction on the number of nodes in g. If the root node of g has a variable as label, then clearly g [element of] D([Phi]) and [Phi](g) = g is a lazy normal form for R. We focus on the case where the root node of g has a label h [element of] F [union] {[f.sup.d]}, and children [v.sub.1] ... [v.sub.ar(h)].

g is a lazy normal form for S, and S contains most general rules for the function symbols [f.sub.g], so the active nodes in g are not labeled [f.sub.g]. Together with Lemma A.2.2 this implies that g does not contain labels [f.sub.g] at all, so g [element of] D([Phi]).

Let [g.sub.j] for j = 1, ..., ar(h) denote the subgraph of g that is rooted at [v.sub.j]. Lemma A.2.1 says that [g.sub.j] [element of] B, and so [g.sub.j] [element of] D([Phi]), for eager arguments j of h. Since g is a lazy normal form for S, the [g.sub.j] for eager arguments j of h are lazy normal forms for S. So by induction the [Phi]([g.sub.j]) for eager arguments j of h are lazy normal forms for R. Hence, to conclude that [Phi](g) is a lazy normal form for R, it suffices to show that none of the left-hand sides of rules in R match modulo laziness the root node of [Phi](g). We distinguish four different forms of left-hand sides in R.

1 Let g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] R with g [is not equal to] f. Then g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r is in [S.sub.0]. Since g is a lazy normal form for S, the term g([s.sub.1], ..., [s.ub.ar(g)]) does not match modulo laziness the root node of g. The root node of g has label h and children [v.sub.1] ... [v.sub.ar(h)], so we can distinguish two cases.

1.1 h [is not equal to] g.

Since g [is not equal to] S, it follows that g is not the root label of [Phi](g). So g([s.sub.1], ..., [s.sub.ar(g)]) does not match modulo laziness the root node of [Phi](g).

1.2 [s.sub.j] does not match modulo laziness node [v.sub.j] in g, for some eager argument j of h.

g is a lazy normal form for S, and S contains most general rules for function symbols [f.sub.g] and f, so the active nodes in g are not labeled [f.sub.g] or f. Therefore, active nodes in [Phi](g) with label f correspond to active nodes in g with label [f.sup.d]. So, since [s.sub.j] does not match modulo laziness node [v.sub.j] in g, and j is an eager argument h, [s.sub.j] does not match modulo laziness node [v.sub.j] in [Phi](g). Hence, g([s.sub.1], ..., [s.sub.ar(g)]) does not match modulo laziness the root node of [Phi](g).

2 Let f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [is not element of] V for some eager argument j [is less than] i of f. Then f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r is in [S.sub.0]. We distinguish two cases for the root label h of g: h = [f.sup.d] or h [is not equal to] [f.sup.d].

2.1 h = [f.sup.d].

Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, the root label of [Phi](g) is then unequal to f. So f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

2.2 h = [f.sup.d].

Let g' be obtained from g by renaming its root label [f.sup.d] into f. Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [g.sub.0] [element of] G([Sigma]). The outermost function symbols of right-hand sides of rules in [S.sub.0], [S.sub.1], [S.sub.2], and [S.sub.5], are unequal to [f.sup.d]. Therefore, the label [f.sup.d] of the root node of g must have been introduced by the reduction of g' to g, either in one step by applying rule [S.sub.4] to the root node of g', or in two steps by subsequent applications of rules in [S.sub.1] and [S.sub.3] to the root node of g'.

[s.sub.j] [is not element of] V for an eager argument j [is less than] i of f, so f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] [S.sub.0] is more specific than any of the rules in [S.sub.1] [union] [S.sub.4]. Hence, its left-hand side cannot match modulo laziness the root node of g'. That is, [s.sub.k] for some eager argument k of f does not match modulo laziness node [v.sub.k] in g'. So [s.sub.k] does not match modulo laziness node [v.sub.k] in g. Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, this implies that [s.sub.k] does not match modulo laziness node [v.sub.k] in [Phi](g). Hence, f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

3 Let f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [element of] V for all eager arguments j [is less than] i of f and [s.sub.i] = g([t.sub.1], ..., [t.sub.ar(g)]). Then

f([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sub.g]([x.sub.1], ..., [x.sub.i-1], [y.sub.1], ..., [y.sub.ar(g)], [x.sub.i+1], ..., [x.sub.ar(f)])

is in [S.sub.1] and [f.sub.g]([s.sub.1], ..., [s.sub.i-1], [t.sub.1], ..., [t.sub.ar(g)], [s.sub.i+1], ..., [s.sub.ar(f)]) [right arrow] r is in [S.sub.2]; these rules are abbreviated to [Rho.sub.1] and [Rho.sub.2], respectively. Let h' denote the label of node [v.sub.i] in g. We distinguish three cases, depending on whether or not h = [f.sup.d] and h' = g.

3.1 h [is not equal to] [f.sup.d].

Then the root label of [Phi](g) is unequal to f, so f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

3.2 h' [is not equal to] g.

Then the label of node [v.sub.i] in [Phi](g) is unequal to g, so [s.sub.i] = g([t.sub.1], ..., [t.sub.ar(g)]) does not match modulo laziness node [v.sub.i] in [Phi](g). Since i is an eager argument of f, it follows that f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

3.3 h = [f.sup.d] and h' = g.

Let g' be obtained from g by renaming its root label [f.sup.d] into f. Since g [element of] B, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [g.sub.0] [element of] G([Sigma]). The outermost function symbols of right-hand sides of rules in [S.sub.0], [S.sub.1], [S.sub.2], and [S.sub.5], are unequal to [f.sup.d]. Therefore, the label [f.sup.d] of the root node of g has been introduced by the reduction of g' to g in two steps, by subsequent applications to the root node of g' of rule [Rho.sub.1] in [S.sub.1] and rule

[f.sub.g]([x.sub.1], ..., [x.sub.i-1], [y.sub.1], ..., [y.sub.ar(g)], [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)], [x.sub.i+1], ..., [x.sub.ar(f)])

in [S.sub.3]; this last rule is abbreviated to [Rho.sub.3]. Let g" denote the lazy graph that results after application of [Rho.sub.1] to the root node of g'; in other words, g' [??.sub.S] g" [??.sub.S] g. Let [v'.sub.1] ... [v'.sub.ar(g) denote the children of node [v.sub.i] in g. Rule [Rho.sub.2] [element of] [S.sub.2] is more specific than rule [Rho.sub.3] [element of] [S.sub.3], so the left-hand side of [Rho.sub.2] cannot match modulo laziness the root node of g". Then either [s.sub.k] for some eager argument k [is not equal to] i of f does not match modulo laziness node [v.sub.k] in g", or [t.sub.l] for some eager argument l of g does not match modulo laziness node [v'.sub.l] in g". So either [s.sub.k] or [t.sub.l] does not match modulo laziness node [v.sub.k] or [v'.sub.l] in g, respectively. Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, this implies that [s.sub.k] or [t.sub.l] does not match modulo laziness node [v.sub.k] or [v'.sub.l] in [Rho](g), respectively. So f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

4 Let f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [element of] V for all eager arguments j [is less than or equal to] i of f. Then [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r is in [S.sub.5]. Since g is a lazy normal form for S, the term [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of g. The root node of g has label h and children [v.sub.1] ... [v.sub.ar(h)], so we can distinguish two cases.

4.1 h [is not equal to] [f.sup.d].

Then [Phi](g) does not have root label f, so f([s.sub.1], ..., [s.sub.ar(f)] does not match modulo laziness the root node of [Phi](g).

4.2 [s.sub.k] does not match modulo laziness node [v.sub.k] in g, for some eager argument k of h.

Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, this implies that [s.sub.k] does not match modulo laziness node [v.sub.k] in [Phi](g). Hence, f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

We conclude that none of the left-hand sides of rules in R match modulo laziness the root node of [Phi](g). So [Phi](g) is a lazy normal form for R. [Square]

SOUNDNESS. If g [element of] D([Phi]) and g [??.sub.S] g', then there is a g" [element of] D([Phi]) such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and either [Phi](g) = [Phi](g") or [Phi](g) [??.sub.R] [Phi](g").

PROOF. g [element of] B, so [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [g.sub.0] [element of] G([Sigma]); hence, g' [element of] B. Let the rightmost innermost active S-redex of g be rooted at node v. Rule [S.sub.4] is most general for f, so active descendants v cannot carry the label f. Hence, active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. We distinguish four cases, covering the rewrite rules in S that can match modulo laziness node v in g.

1 Suppose g [??.sub.S] g' is the result of an application of g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r in [S.sub.0]. This match gives rise to a (possibly empty) collection {[v.sub.1], ..., [s.sub.(g)]} of essential lazy nodes in g.

g' [element of] B does not contain function symbols [f.sub.h] (because g and r are free of such function symbols), so g' [element of] D([Phi]). The term g([s.sub.1], ..., [s.sub.ar(g)]) is the most specific left-hand side in S that matches modulo laziness node v in g, and active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. This implies that g([s.sub.1], ..., [s.sub.ar(g)]) is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). Moreover, this match gives rise to the same collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in [Phi](g). Completeness of [Phi] implies that v is the rightmost innermost active R-redex of [Phi](g). Hence, application of g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] R gives rise to

[Phi](g) [??.sub.R] [Phi](g').

So we can take g" = g'.

2 Suppose g [??.sub.S] g' is the result of an application of

f([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sub.g]([x.sub.1], ..., [x.sub.i-1], [y.sub.1], ..., [y.sub.ar(g)], [x.sub.i+1], ..., [x.sub.ar(f)])

in [S.sub.1].

v is the rightmost innermost active S-redex of g, so y is also the rightmost innermost active S-redex of g'. We distinguish two cases, covering the rewrite rules in S that can match modulo laziness node v in g'.

2.1 Suppose [f.sub.g]([s.sub.1], ..., [s.sub.-1], [t.sub.1], ..., [t.sub.ar(g)], [S.sub.i+1], ..., [s.sub.ar(f)]) [right arrow] r in [S.sub.2] is the most specific rule in S that matches modulo laziness node v in g'. Application of this rule gives rise to

g' [??.sub.S] g"

where g" [element of] B does not contain function symbols [f.sub.h] (because g and r are free of such function symbols), so g" [element of] D([Phi]).

[f.sub.g]([s.sub.1], ..., [s.sub.i-1], [t.sub.1], ..., [t.sub.ar(g)], [s.sub.i+1], ..., [s.sub.ar(f)]) is the most specific left-hand side in S that matches modulo laziness node v in g, and active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. This implies that f([s.sub.1], ..., [s.sub.i-1], g([t.sub.1], ..., [t.sub.ar(g)]), [s.sub.i+1], ..., [s.sub.ar(g)]) is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). Completeness of [Phi] implies that v is the rightmost innermost active R-redex of [Phi](g). Hence, application of f([s.sub.1], ..., [s.sub.i-1], g([t.sub.1], ..., [t.sub.ar(g)]), [s.sub.i+1], ..., [s.sub.ar(g)]) [element of] r [element of] R gives rise to

[Phi](g) [??.sub.R] [Phi](g").

2.2 Suppose

[f.sub.g]([x.sub.1], ..., [x.sub.i-1], [y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)], [x.sub.i+1], ..., [x.sub.ar(f)])

in [S.sub.3] is the most specific rule in S that matches modulo laziness node v in g'. Application of this rule gives rise to

g' [??.sub.S] g"

where g" is obtained from g by renaming the label f of v into [f.sup.d]. Then g" [element of] B does not contain function symbols [f.sub.h], so g" [element of] D([Phi]), and moreover

[Phi](g) = [Phi](g").

3 Suppose g [??.sub.S] g' is the result of an application of

f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.ar(f)])

in [S.sub.4]. Then g' [element of] B does not contain function symbols [f.sub.h], so g' [element of] D([Phi]), and moreover

[Phi](g) = [Phi](g').

So we can take g" = g'.

4 Suppose g [??.sub.S] g' is the result of an application of [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r in [S.sub.5]. This match gives rise to a (possibly empty) collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in g.

g' [element of] B does not contain function symbols [f.sub.h] (because g and r are free of such function symbols), so g' [element of] D([Phi]). The term [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) is the most specific left-hand side in S that matches modulo laziness node v in g, and active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. This implies that f([s.sub.1], ..., [s.sub.ar(f)]) is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). Moreover, this match gives rise to the same collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in [Phi](g). Completeness of [Phi] implies that v is the rightmost innermost active R-redex of [Phi](g). Hence, application of f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R gives rise to

[Phi](g) [??.sub.R] [Phi](g').

So we can take g" = g'. [Square]

TERMINATION PRESERVATION. If [g.sub.0] [element of] D([Phi]) induces an infinite reduction [g.sub.0] [??.sub.S] [g.sub.1] [??.sub.S] [g.sub.2] [??.sub.S] ..., then there is a k [is greater than or equal to] 1 such that [g.sub.k] [element of] D([Phi]) and [Phi]([g.sub.0]) [??.sub.R] [Phi]([g.sub.k]).

PROOF. Each application of rule [S.sub.4] and each subsequent application of rules in [S.sub.1] and [S.sub.3] renames a label f into [f.sup.d]. Since [g.sub.0] contains only finitely many nodes with the label f, there can only be a finite number of such applications in a row with respect to [g.sub.0]. Hence, there exists a smallest l [is greater than or equal to] 1 such that either [g.sub.l-1] [??.sub.S] [g.sub.l] is the result of an application of a rule in [S.sub.0] [union] [S.sub.5], or [g.sub.l-1] [??.sub.S] [g.sub.l] [g.sub.l] [??.sub.S] [g.sub.l+1] is the result of subsequent application of rules in [S.sub.1] and [S.sub.2].

--[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the result of applications of the rule [S.sub.4] or subsequent applications of rules in [S.sub.1] and [S.sub.3]. So [g.sub.l-1] is obtained from [g.sub.0] by renaming labels f into [f.sup.d]. Then [g.sub.l-1] [element of] D([Phi]) and [Phi]([g.sub.0]) = [Phi]([g.sub.l-1).

--If [g.sub.l-1] [??.sub.S] [g.sub.l] is the result of an application of a rule in [S.sub.0] or [S.sub.5], then case 1 or 4 in the soundness proof of [Phi], respectively, yields [g.sub.l] [element of] D([Phi]) and [Phi]([g.sub.l-1]) [??.sub.R] [Phi]([g.sub.l]). If [g.sub.l-1] [??.sub.S] [g.sub.l] [??.sub.S] [g.sub.l+1] is the result of an application of rules in [S.sub.1] and [S.sub.2], then case 2.1 in the soundness proof of [Phi] yields [g.sub.l+1] [element of] D([Phi]) and [Phi]([g.sub.l-1]) [??.sub.R] [Phi]([g.sub.l+1]). [Square]

A.2.2 Second Transformation Rule. Suppose we apply the second transformation rule to R, with respect to [element of] F and lazy argument i of f. The transformation introduces a fresh function symbol [f.sup.d] of the same arity as f, and laziness annotation ??[Lambda]([f.sup.d], i) and [Lambda]([f.sup.d], j) ?? [Lambda](f, j) for j [is not equal to] i. Let s be the term that is obtained from term s by renaming all occurrences of f into [f.sup.d]. The transformed TRS S consists of three collections [S.sub.0]-[S.sub.2]:

--g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] [S.sub.0] iff g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] R with g [is not equal to] f, [s.sub.j] [is not element of] V for some eager argument j of f, or [s.sub.j] [is not an element of] V for some lazy argument j [is greater than] i of f;

--[S.sub.1] = {f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.ar(f)])};

--[f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] [S.sub.2] iff f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [element of] V for all eager arguments j of f and all lazy arguments j [is greater than] i of f.

Let [Sigma]' denote the original signature [Sigma] extended with the fresh function symbol [f.sup.d], and let

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The next lemma follows by induction with respect to the length of a derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with [g.sub.0] [element of] G([Sigma]).

LEMMA A.2.3. If g [element of] B, then the subgraphs rooted at active nodes of g are in B.

We prove that the transformation of (G([Sigma]), [??.sub.R]) into (B, [??.sub.S]) is correct, by means of a simulation. The lazy graph [Phi](g) is obtained from g [element of] B by renaming all labels [f.sup.d] into f. The mapping [Phi] : B [right arrow] G([Sigma]) is surjective, because it is the identity mapping on G([Sigma]) [subset or equal to] B. Hence, [Phi] constitutes a (fully defined) simulation of (G([Sigma]), [??.sub.R]) by (B, [??.sub.S]). We proceed to prove that [Phi] is sound, complete, and termination preserving.

COMPLETENESS. If g [element of] B is a lazy normal form for S, then [Phi](g) is a lazy normal form for R.

PROOF. We apply induction on the number of nodes in g. If the root node of g has a variable as label, then clearly [Phi](g) = g is a lazy normal form for R. We focus on the case where the root node of g has a label h [element of] F [union] {[f.sup.d]}, and children [v.sub.1] ... [v.sub.ar(h)].

Let [g.sub.j] for j = 1, ..., ar(h) denote the subgraph of g that is rooted at [v.sub.j]. Lemma A.2.3 says that [g.sub.j] [element of] B for eager arguments j of h. Since g is a lazy normal form for S, the [g.sub.j] for eager arguments j of h are lazy normal forms for S. So by induction the [Phi]([g.sub.j]) for eager arguments j of h are lazy normal forms for R. Hence, to conclude that [Phi](g) is a lazy normal form for R, it suffices to show that none of the left-hand sides of rules in R match modulo laziness the root node of [Phi](g). We distinguish three different forms of left-hand sides in R.

1 Let g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] R with g [is not equal to] f.

Then g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r is in [S.sub.0]. Since g is a lazy normal form for S, the term g([s.sub.1], ..., [s.sub.ar(g)]) does not match modulo laziness the root node of g. The root node of g has label h and children [v.sub.1] ... [v.sub.ar(h)], so we can distinguish two cases.

1.1 h [is not equal to] g.

Since g [is not equal to] f, it follows that g is not the root label of [Phi](g). So g([s.sub.1], ..., [s.sub.ar(g)]) does not match modulo laziness the root node of [Phi](g).

1.2 [s.sub.j] does not match modulo laziness node [v.sub.j] in g, for some eager argument j of h.

g is a lazy normal form for S, and [S.sub.1] is a most general rule for f; so the active nodes in g are not labeled f. Therefore, active nodes in [Phi](g) with label f correspond to active nodes in g with label [f.sup.d]. So, since [s.sub.j] does not match modulo laziness node [v.sub.j] in g, and j is an eager argument h, [s.sub.j] does not match modulo laziness node [v.sub.j] in [Phi](g). Hence, g([s.sub.1], ..., [s.sub.ar(g)]) does not match modulo laziness the root node of [Phi](g).

2 Let f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R with [s.sub.j] [is not element of] V for some eager argument j of f or some lazy argument j [is greater than] i of f.

Then f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r is in [S.sub.0]. We distinguish two cases for the root label h of g: h = [f.sup.d] or h [is not equal to] [f.sup.d].

2.1 [is not equal to] [f.sup.d].

Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, the root label of [phi](g) is then unequal to f. So f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

2.2 h = [f.sup.d].

Let g' be obtained from g by renaming its root label [f.sup.d] into f. Since g [element of] B, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [g.sub.0] [element of] G([Sigma]). The outermost function symbols of right-hand sides of rules in [S.sub.0] and [S.sub.2] are unequal to [f.sup.d], so the label [f.sup.d] of the root node of g must have been introduced by applying rule [S.sub.1] to the root node of g'.

[s.sub.j] [is not element of] V for an eager argument j of f or a lazy argument j [is greater than] i of f, so the rule f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] [S.sub.0] is more specific than [S.sub.1]. Hence, its left-hand side cannot match modulo laziness the root node of g'. That is, [s.sub.k] for some eager argument k of f does not match modulo laziness node [v.sub.k] in g'. So [s.sub.k] does not match modulo laziness node [v.sub.k] in g. Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, this implies that [s.sub.k] does not match modulo laziness node [v.sub.k] in [Phi](g). Hence, f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

3 Let f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R. with [s.sub.j] [element of] V for all eager arguments j of f and all lazy arguments j [is greater than] i of f.

Then [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r is in [S.sub.5]. Since g is a lazy normal form for S, the term [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of g. The root node of g has label h and children [v.sub.1] ... [v.sub.ar(h)], so we can distinguish two cases.

3.1 h [is not equal to] [f.sup.d].

Then [Phi](g) does not have root label f, so f([s.sub.1, ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

3.2 [s.sub.k] does not match modulo laziness node [v.sub.k] in g, for some eager argument k of h.

Since labels f of active nodes in [Phi](g) correspond to labels [f.sup.d] in g, this implies that [s.sub.k] does not match modulo laziness node [v.sub.k] in [Phi](g). Hence, f([s.sub.1], ..., [s.sub.ar(f)]) does not match modulo laziness the root node of [Phi](g).

We conclude that none of the left-hand sides of rules in R match modulo laziness the root node of [Phi](g). So [Phi](g) is a lazy normal form for R. [Square]

SOUNDNESS. If g [element of] B and g ?? g', then [Phi](g) ?? R [Phi](g').

PROOF. g [element of] B, so [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [g.sub.0] [element of] G([Sigma]); hence, g' [element of] B. Let the rightmost innermost active S-redex of g be rooted at node v. Rule [S.sub.1] is most general for f, so active descendants of v cannot carry the label f. Hence, active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. We distinguish three cases, covering the rewrite rules in S that can match modulo laziness node v in g.

1 Suppose g ?? s g' is the result of an application of g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r in [S.sub.0]. This match gives rise to a (possibly empty) collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in g.

g([s.sub.1], ..., [s.sub.ar(g)]) is the most specific left-hand side in S that matches modulo laziness node v in g, and active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. This implies that g([s.sub.1], ..., [s.sub.ar(g)]) is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). Moreover, this match gives rise to the same collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in [Phi](g). Completeness of [Phi] implies that v is the rightmost innermost active R-redex of [Phi](g). Hence, application of g([s.sub.1], ..., [s.sub.ar(g)]) [right arrow] r [element of] R gives rise to

[Phi](g) ?? R [Phi](g').

2 Suppose g ?? s g' is the result of an application of

f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] [f.sup.d]([x.sub.1], ..., [x.sub.ar(f)])

in [S.sub.4]. The lazy graph [Phi](g') only differs from [Phi](g) in that the ith child of v is eager f([x.sub.1], ..., [x.sub.ar(f)]) is the most specific left-hand side in S that matches modulo laziness node v in g, and active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. This implies that some f([s.sub.1], ..., [s.sub.ar(f)]) with [s.sub.i] [is not an element of] V, [s.sub.j] [element of] V for eager arguments j, and [s.sub.j] [element of] V for lazy arguments j [is greater than] i of f, is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). This match gives rise to essential lazy nodes in [Phi](g), the rightmost of which is the ith child of v. Completeness of [Phi] implies that v is the rightmost innermost active R-redex of [Phi](g). Hence,

[Phi](g) ?? R [Phi](g').

3 Suppose g ?? s g' is the result of an application of [f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r in [S.sub.2]. This match gives rise to a (possibly empty) collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in g.

[f.sup.d]([s.sub.1], ..., [s.sub.ar(f)]) is the most specific left-hand side in S that matches modulo laziness node v in g, and active descendants of v in [Phi](g) with label f correspond to nodes in g with label [f.sup.d]. This implies that f([s.sub.1], ..., [s.sub.ar(f)]) is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). Moreover, this match gives rise to the same collection {[v.sub.1], ..., [v.sub.n]} of essential lazy nodes in [Phi](g). Completeness of [Phi] implies that v is the rightmost innermost active R-redex of [Phi](g). Hence, application of f([s.sub.1], ..., [s.sub.ar(f)]) [right arrow] r [element of] R gives rise to

[Phi](g) ?? R [Phi](g').

This finishes the soundness proof of [Phi]. [Square]

TERMINATION PRESERVATION. If [g.sub.0] [element of] B induces an infinite reduction [g.sub.0] ?? s [g.sub.1] ?? s [g.sub.2] ?? s ..., then [Phi]([g.sub.0]) ?? R [Phi]([g.sub.1]).

PROOF. Since [g.sub.0] ?? s [g.sub.1], the soundness property that we derived for [Phi] induces that [Phi]([g.sub.0]) ?? R [Phi]([g.sub.1]). [Square]

A.3 Thunkification

We prove that the transformation rules in Sections 4.4, 4.5, and 4.6 to thunk and unthunk lazy nodes are correct. Let [Sigma] = (V, F, ar) denote the original lazy signature and G([Sigma]) the collection of lazy graphs over [Sigma]. Owing to the minimization of left-hand sides in Section 4.3, the left-hand sides of rewrite rules in the origin left-linear R contain no more than two function symbols, and only variables as lazy arguments. Note that, since lazy arguments in left-hand sides of rewrite rules in R are always variables, pattern matching with respect to these left-hand sides does not give rise to essential lazy nodes. S denotes the TRS that results after applying the transformation rules in Sections 4.4, 4.5, and 4.6 to R. Finally, ?? R represents the lazy rewrite relation ?? L as induced by R, while ?? s represents the rightmost innermost rewrite relation with respect to specificity ordering as induced by S. We prove correctness of the transformation using a simulation.

The transformation introduces fresh function symbols: the thunk [Theta] with two eager arguments, constants [Tau]f for f [element of] F, auxiliary function symbols [vec.sub.[Alpha]] for bit strings [Alpha] of arity |[Alpha]| with [Lambda]([vec.sub.[Alpha]], i) if and only if [[Alpha].sub.i] = 0, constants [Lambda], and the function symbol inst with one eager argument. The transformed TRS S consists of four collections [S.sub.0]-[S.sub.3]:

--l [right arrow] r' [element of] [S.sub.0] iff l [right arrow] r [element of] R and r' is obtained from r as follows:

--we replace, in a bottom-up fashion, lazy nonvariable subterms t by thunks [Theta]([Lambda], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.|[Alpha]|])), with [x.sub.1], ..., [x.sub.|[Alpha]|] the variables in t, and [[Alpha].sub.[Iota]] = 0 if and only if [x.sub.i] is a lazy argument in l and does not occur at an active position in r;

--we replace migrant variables x in r by inst(x).

--inst([Theta]([[Tau].sub.f], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.ar(f)]))) [right arrow] f([s.sub.1], ..., [s.sub.ar(f)]) [element of] [S.sub.1] iff f [element of] F, [Alpha] is a string of ar(f) zeros, [s.sub.i] = inst([x.sub.[Iota]]) for eager arguments i of f, and [s.sub.[Iota]] = [x.sub.i] for lazy arguments i of f.

--inst([Theta]([Lambda], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.|[Alpha]|]))) [right arrow] t' [element of] [S.sub.2] iff [Lambda] and [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.|[Alpha]|]) together represent the term structure t, and t' is obtained from t by replacing migrant variables x in t by inst(x).

--[S.sub.3] = {inst(x) [right arrow] x}.

Let [Sigma]' denote the original signature [Sigma] extended with the fresh function symbols [Theta], [[Tau].sub.f], [vec.sub.[Alpha]], [Lambda], and inst, and let

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We prove that the transformation of (G([Sigma]), [??.sub.R]) into (B, [??.sub.S]) is correct, by means of a simulation [Phi]. This mapping eliminates nodes with the label inst, making the nodes below eager, and replaces thunked graph structures [Theta]([[Tau].sub.f], [vec.sub.[Alpha]]([v.sub.1], ..., [v.sub.ar(f)])) and [Theta]([Lambda], [vec.sub.[Alpha]]([v.sub.1], ..., [v.sub.|[Alpha]|])) by the related graph structures f([v.sub.1], ..., [v.sub.ar(f)]) and G(t), respectively. The lazy graph [Phi](g) [element of] G([Sigma]) is obtained from g [element of] B by repeated applications of the transformation rules below.

1 Let node v have label inst and child v'.

We rename, in the image of the children mapping, all occurrences of v into v'. Next, we eliminate node v from the lazy graph. Finally, we make node v' eager.

2 Let node v have label [Theta] and children v'v". We distinguish two cases.

2.1 Let node v' have label [[Tau].sub.f]. Then v" carries the label [vec.sub.[Alpha]] where [Alpha] consists of ar(f) zeros, and v" has as children the string of lazy nodes [v.sub.1] ... [v.sub.ar(f)]. We change the label of v into f, and supply this node with a string of children [v.sub.1] ... [v.sub.ar(f)]. For i = 1, ..., ar(f), node [v.sub.i] is made eager if and only if i is an eager argument of f. Next, we eliminate nodes v' and v" from the lazy graph.

2.2 Let node v' have label [Lambda]. Then v" carries label [vec.sub.[Alpha]] and children [v.sub.1] ... [v.sub.|[Alpha]|]. Let [Lambda] and [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.|[Alpha]|]) be related to the term t. We construct the graph G(t), which consists of fresh nodes, and add G(t) to the lazy graph. In the image of the children mapping, all occurrences of v are renamed into the root node of G(t). For i = 1, ..., |[Alpha]|, let [v'.sub.i] denote the node in G(t) with the label [x.sub.i]; occurrences of [v'.sub.i] in the image of the children mapping are renamed into [v.sub.i]. Lazy nodes [v.sub.i] for i = 1, ..., |[Alpha]| are made eager if [x.sub.i] is an eager argument in t. Finally, we eliminate the nodes v, v', v", and [v'.sub.i] for i = 1, ..., |[Alpha]|.

The two cases above are applied to g until there are no nodes left with the label inst or [Theta]. The resulting lazy graph is [Phi](g).

The next two lemmas follow by induction with respect to the length of a derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with [g.sub.0] [element of] G([Sigma]).

LEMMA A.3.1. For all g [element of] B, [Phi](g) [element of] G([Sigma]) is well-defined.

LEMMA A.3.2. If g [element of] B, [label.sub.g](v) = f, and i is an eager argument of f, then the ith child of v in g is an eager node in [Phi](g).

The next lemma follows from case 1 in the definition of [Phi], by induction with respect to the length of a path in g from the root node to the active node in question.

LEMMA A.3.3. If g [element of] B does not contain labels inst, then each active node in [Phi](g) inherits its label and children from the corresponding node in g.

The mapping [Phi] : B [right arrow] G([Sigma]) is surjective, because it is the identity mapping on G([Sigma]) [subset or equal to] B. Hence, [Phi] constitutes a (fully defined) simulation of (G([Sigma]), [??.sub.R]) by (B, [??.sub.S]). We proceed to prove that [Phi] is sound, complete, and termination preserving.

COMPLETENESS. If g [element of] B is a normal form for S, then [Phi](g) is a lazy normal form for R.

PROOF. Since g is a normal form for S, and [S.sub.3] is a most general rule for inst, g does not contain labels inst. Consider any active node v in [Phi](g). Lemma A.3.3 implies that v inherits its label and children from node v in g. To conclude that [Phi](g) is a lazy normal form for R, we need to show that none of the left-hand sides in R match modulo laziness node v in [Phi](g). We distinguish the two possible forms of left-hand sides in R.

1 Let f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] r in R.

Then f([x.sub.1], ..., [x.sub.ar(f)]) [right arrow] r' in [S.sub.0] for some term r'. Since g is a normal form for S, f([x.sub.1], ..., [x.sub.ar(f)]) does not match node v in g. This implies [label.sub.g](v) [is not equal to] f, and so [label.sub.[Phi](g)] (v) [is not equal to] f. Hence, f([x.sub.1], ..., [x.sub.ar(f)]) does not match modulo laziness node v in [Phi](g).

2 Let f([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] r in R.

Then f([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) [right arrow] r' in [S.sub.0] for some term r'. Since g is a normal form for S, f([x.sub.1], ..., [x.sub.i-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.[Iota]+1], ..., [x.sub.ar(f)]) does not match node v, in g. This implies either [label.sub.g](v) [is not equal to] f or [label.sub.g](v') [is not equal to] g, where v' is the ith child of v in g. Since i is an eager argument of f, Lemma A.3.2 implies that v is an active node in [Phi](g). So by Lemma A.3.3, v' inherits its label from node v' in g. Hence, either [label.sub.[Phi](g)] (v) [is not equal to] f or [label.sub.[Phi](g)] (v') [is not equal to] g. So f([x.sub.1], ..., [x.sub.[Iota]-1], g([y.sub.1], ..., [y.sub.ar(g)]), [x.sub.i+1], ..., [x.sub.ar(f)]) does not match modulo laziness node v in [Phi](g).

We conclude that [Phi](g) is a lazy normal form for R. []

The next lemma follows by induction with respect to the length of a derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with [g.sub.0] [element of] G([Sigma]).

LEMMA A.3.4. If g [element of] B and node v has label [Theta] in g, then the left-hand sides of rules in S do not match any descendants of v in g.

SOUNDNESS. If g [element of] B and g [??.sub.S] g', then either [Phi](g) = [Phi](g') or [Phi](g) [??.sub.R] [Phi](g').

PROOF. g [element of] B, so [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some [g.sub.0] [element of] G([Sigma]); hence, g' [element of] B. Let the node the rightmost innermost S-redex of g be rooted at node v. We distinguish three cases, covering the rewrite rules in S that can match node v in g.

1 Let g [??.sub.S] g' be the result of an application of l [right arrow] r' in [S.sub.0].

By Lemma A.3.4 the node v does not have an ancestor [Theta] in g, so it is active in [Phi](g). Since l is the most specific left-hand side in S that matches node v in g, it follows that l is the most specific left-hand side in R that matches modulo laziness node v in [Phi](g). Completeness of [Phi] implies that the rightmost innermost active R-redex of [Phi](g) is rooted at v. Hence, using the definition of [Phi], we conclude that application of l [right arrow] r [element of] R gives rise to

[Phi](g) [??.sub.R] [Phi](g').

2 Let g [??.sub.S] g' be the result of an application of

inst([Theta]([[Tau].sub.f], [vec.sub.[Alpha]([x.sub.1], ..., [x.sub.ar(f)]))) [right arrow] f([s.sub.1], ..., [s.sub.ar(f)])

in [S.sub.1]. Then, owing to the definition of [Phi], we have [Phi](g) = [Phi](g').

3 Let g [??.sub.S] g' be the result of an application of inst([Theta]([Lambda], [vec.sub.[Alpha]]([x.sub.1], ..., [x.sub.|[Alpha]|]))) [right arrow] t' in [S.sub.2].

Then, owing to the definition of [Phi], we have [Phi](g) = [Phi](g').

4 Let g [??.sub.S] g' be the result of an application of inst(x) [right arrow] x in [S.sub.3].

Then, owing to the definition of [Phi], we have [Phi](g) = [Phi](g').

This finishes the soundness proof of [Phi]. [Square]

TERMINATION PRESERVATION. If [g.sub.0] [element of] B induces an infinite reduction [g.sub.0] [??.sub.S] [g.sub.1] [??.sub.S] [g.sub.2] [??.sub.S] ..., then there is a k [is greater than or equal to] 1 such that [Phi]([g.sub.0]) [??.sub.R] [Phi]([g.sub.k]).

PROOF. First, we observe that the TRS [S.sub.1] [union] [S.sub.2] [union] [S.sub.3] is terminating.

--Each application of a rule in [S.sub.1] [union] [S.sub.2] strictly decreases the number of labels [Theta], and this number is not increased by applications of the rule in [S.sub.3].

--Each application of the rule in [S.sub.3] strictly decreases the number of labels inst.

So there can only be a finite number of applications of rules in [S.sub.1] [union] [S.sub.2] [union] [S.sub.3] in a row. Then there exists a smallest k [is greater than or equal to] 1 such that [g.sub.k-1] [??.sub.S] [g.sub.k] is the result of an application of a rule in [S.sub.0].

1 Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for i = 1, ..., k - 1 is the result of an application of a rule in [S.sub.1] [union] [S.sub.2] [union] [S.sub.3], the cases 2, 3, and 4 in the soundness proof of [Phi] yield [Phi]([g.sub.i-1]) = [Phi]([g.sub.i]).

2 Since [g.sub.k-1] [??.sub.S] [g.sub.k] is the result of an application of a rule in [S.sub.0], case 1 in the soundness proof of [Phi] yields [Phi]([g.sub.k-1]) [??.sub.R] [Phi]([g.sub.k]).

Hence, [Phi]([g.sub.0]) = ... = [Phi]([g.sub.k-1]) [??.sub.R] [Phi]([g.sub.k]). [Square]

ACKNOWLEDGMENTS

Jaco van de Pol, Piet Rodenburg, and Mark van den Brand provided valuable support. We are indebted to anonymous referees for suggesting many substantial improvements. A considerable part of this research was carried out at the CWI in Amsterdam.

REFERENCES

AMTOFT, T. 1993. Minimal thunkification. In Proceedings, 3rd Workshop on Static Analysis, P. Cousot, M. Falaschi, G. File, and A. Rauzy, Eds. Lecture Notes in Computer Science, vol. 724. Springer-Verlag, Berlin, 218-229.

AUGUSTSSON, L. AND JOHNSSON, T. 1989. Parallel graph reduction with the <y, g>-machine. In Proceedings, 5th Conference on Functional Programming Languages and Computer Architecture. ACM, New York, 202-213.

BAADER, F. AND NIPKOW, T. 1998. Term Rewriting and All That. Cambridge University Press, Cambridge, UK.

BAETEN, J. C. M., BERGSTRA, J. A., KLOP, J. W., AND WEIJLAND, W. P. 1989. Term-rewriting systems with rule priorities. Theor. Comput. Sci. 67, 2/3, 283-301.

BAILEY, S. W. 1995. Hielp, a fast interactive lazy functional language system. Ph.D. thesis, University of Chicago, Chicago. Available at http://www.cs.uchicago.edu/tech-reports/.

BARENDREGT, H. P., VAN EEKELEN, M. C. J. D., GLAUERT, J. R. W., KENNAWAY, J. R., PLASMEIJER, M. J., AND SLEEP, M. R. 1987. Term graph rewriting. In Proceedings, 1st Conference on Parallel Architectures and Languages Europe, J. W. de Bakker, A. J. Nijman, and P. C. Treleaven, Eds. Lecture Notes in Computer Science, vol. 259. Springer-Verlag, Berlin, 141-158.

BRUS, T., VAN EEKELEN, M. C. J. D., VAN LEER, M., PLASMEIJER, M. J., AND BARENDREGT, H. P. 1987. Clean -- a language for functioned graph rewriting. In Proceedings, 3rd Conference on Functional Programming Languages and Computer Architecture, G. Kahn, Ed. Lecture Notes in Computer Science, vol. 274. Springer-Verlag, Berlin, 364-384.

BURN, G. 1991. Lazy Functional Languages: Abstract Interpretation and Compilation. Research Monographs in Parallel and Distributed Computing. Pitman, London.

CHEW, L. P. 1980. An improved algorithm for computing with equations. In Proceedings, 21st IEEE Symposium on Foundations of Computer Science. IEEE, 108-117.

COUSINEAU, G., CURIEN, P.-L., AND MAUNY, M. 1987. The categorical abstract machine. Sci. Comput. Program. 8, 2, 173-202.

DURAND, I. 1994. Bounded, strongly sequential and forward-branching term rewriting systems. Journal of Symbolic Computation 18, 4, 319-352.

DURAND, I. AND SALINIER, B. 1993. Constructor equivalent term rewriting systems. Inf. Process. Lett. 47, 3, 131-137.

FOKKINK, W. J., KAMPERMAN, J. F. T., AND WALTERS, H. R. 1998. Within ARM's reach: compilation of left-linear rewrite systems via minimal rewrite systems. ACM Trans. Program. Lang. Syst. 20, 3, 679-706.

FOKKINK, W. J. AND VAN DE POL, J. C. 1997. Simulation as a correct transformation of rewrite systems. In Proceedings, 22nd Symposium on Mathematical Foundations of Computer Science, I. Privara and P. Ruzicka, Eds. Lecture Notes in Computer Science, vol. 1295. Springer-Verlag, Berlin, 249-258.

FRIEDMAN, D. P. AND WISE, D. S. 1976. CONS should not evaluate its arguments. In Proceedings, 3rd Colloquium on Automata, Languages and Programming, S. Michaelson and R. Milner, Eds. Edinburgh University Press, Edinburgh, 257-284.

GIESL, J. AND MIDDELDORP, A. 1999. Transforming context-sensitive rewrite systems. In Proceedings, 10th Conference on Rewriting Techniques and Applications, P. Narendran and M. Rusinowitch, Eds. Lecture Notes in Computer Science, vol. 1632. Springer-Verlag, Berlin, 271-285.

GOGUEN, J. A., WINKLER, T., MESEGUER, J., FUTATSUGI, K., AND JOUANNAUD, J.-P. 1993. Applications of Algebraic Specifications using OBJ. Cambridge University Press, Cambridge, UK.

GRAF, A. 1991. Left-to-right tree pattern matching. In Proceedings, 4th Conference on Rewriting Techniques and Applications, R. V. Book, Ed. Lecture Notes in Computer Science, vol. 488. Springer-Verlag, Berlin, 323-334.

HARTEL, P. H., FEELEY, M., ALT, M., AUGUSTSSON, L., BAUMANN, P., BEEMSTER, M., CHAILLOUX, E., FLOOD, C. H., GRIESKAMP, W., VAN GRONINGEN, J. H. G., HAMMOND, K., HAUSMAN, B., IVORY, M. Y., JONES, R. E., KAMPERMAN, J. F. T., LEE, P., LEROY, X., LINS, R. D., LOOSEMORE, S., RJEMO, N., SERRANO, M., TALPIN, J.-P., THACKRAY, J., THOMAS, S., WALTERS, H. R., WEIS, P., AND WENTWORTH, P. 1996. Benchmarking implementations of functional languages with "pseudoknot", a float-intensive benchmark. J. Funct. Program. 6, 4, 621-655.

HENDERSON, P. AND MORRIS, J. H. 1976. A lazy evaluator. In Conference Record of the 3rd ACM Symposium on Principles of Programming Languages. ACM, New York, 95-103.

HOFFMANN, C. M. AND O'DONNELL, M. J. 1982a. Pattern matching in trees. J. ACM 29, 1, 68-95.

HOFFMANN, C. M. AND O'DONNELL, M. J. 1982b. Programming with equations. ACM Trans. Program. Lang. Syst. 4, 1, 83-112.

HUET, G. AND LEVY, J.-J. 1991. Computations in orthogonal rewriting systems, parts i and ii. In Computational Logic: Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, Eds. MIT Press, Cambridge, Mass., 395-443.

INGERMAN, P. Z. 1961. Thunks: a way of compiling procedure statements with some comments on procedure declarations. Commun. ACM 4, 1, 55-58.

JOHNSSON, T. 1984. Efficient compilation of lazy evaluation. In Proceedings, ACM Symposium on Compiler Construction. ACM SIGPLAN Not. 19, 6, 58-69.

JONES, M. P. 1994. The implementation of the Gofer functional programming system. Tech. Rep. YALEU/DCS/RR-1030, Yale University, New Haven. Available at http://www.cse.ogi.edu/mpj/pubs/goferimp.html.

KAMPERMAN, J. F. T. 1996. Compilation of term rewriting systems. Ph.D. thesis, University of Amsterdam, Amsterdam. Available at http://www.babelfish.nl.

KAMPERMAN, J. F. T. AND WALTERS, H. R. 1995. Lazy rewriting on eager machinery. In Proceedings, 6th Conference on Rewriting Techniques and Applications, J. Hsiang, Ed. Lecture Notes in Computer Science, vol. 914. Springer-Verlag, Berlin, 147-162.

KAMPERMAN, J. F. T. AND WALTERS, H. R. 1996. Minimal term rewriting systems. In Proceedings, 11th Workshop on Specification of Abstract Data Types, M. Haveraaen, O. Owe, and O.-J. Dahl, Eds. Lecture Notes in Computer Science, vol. 1130. Springer-Verlag, Berlin, 274-290.

KENNAWAY, J. R. 1990. The specificity rule for lazy pattern-matching in ambiguous term rewrite systems. In Proceedings, 3rd European Symposium on Programming, N. D. Jones, Ed. Lecture Notes in Computer Science, vol. 432. Springer-Verlag, Berlin, 256-270.

KENNAWAY, J. R., KLOP, J. W., SLEEP, M. R., AND DE VRIES, F. J. 1994. On the adequacy of graph rewriting for simulating term rewriting. ACM Trans. Program. Lang. Syst. 16, 3, 493-523.

LUCAS, S. 1995. Fundamentals of context-sensitive rewriting. In Proceedings, 22nd Seminar on Current Trends in Theory and Practice of Informatics, M. Bartosek, J. Staudek, and J. Wiedermann, Eds. Lecture Notes in Computer Science, vol. 1012. Springer-Verlag, Berlin, 405-412.

LUTTIK, S. P., RODENBURG, P. H., AND VERMA, R. M. 1996. Correctness criteria for transformations of rewrite systems with an application to Thatte's transformation. Technical Report P9615, University of Amsterdam, Amsterdam.

MYCROFT, A. 1980. The theory and practice of transforming call-by-need into call-by-value. In Proceedings, 4th Symposium on Programming, B. Robinet, Ed. Lecture Notes in Computer Science, vol. 83. Springer-Verlag, Berlin, 269-281.

NELSON, G. AND OPPEN, D. C. 1980. Fast decision procedures based on congruence closure. J. ACM 27, 2, 356-364.

O'DONNELL, M. J. 1977. Computing in Systems Described by Equations. Lecture Notes in Computer Science, vol. 58. Springer-Verlag, Berlin.

O'DONNELL, M. J. 1985. Equational Logic as a Programming Language. MIT Press, Cambridge, Mass.

O'DONNELL, M. J. 1998. Introduction: logic and logic programming languages. In Handbook of Logic in Artificial Intelligence and Logic Programming, D. M. Gabbay, Ed. Vol. 5. Oxford University Press, New York, 1-67.

OGATA, K. AND FUTATSUGI, K. 1997. Implementation of term rewritings with the evaluation strategy. In Proceedings, 9th Symposium on Programming Languages: Implementations, Logics, and Programs, H. Glaser, P. H. Hartel, and H. Kuchen, Eds. Lecture Notes in Computer Science, vol. 1292. Springer-Verlag, Berlin, 225-239.

OKASAKI, C., LEE, P., AND TARDITI, D. 1994. Call-by-need and continuation-passing style. Lisp and Symbolic Computation 7, 1, 57-81.

PEYTON JONES, S. L. 1987. The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs, N.J.

PEYTON JONES, S. L. AND SALKILD, J. 1989. The spineless tagless G-machine. In Proceedings, 4th Conference on Functional Programming Languages and Computer Architecture, D. B. MacQueen, Ed. Addison-Wesley, Reading, Mass., 184-201.

PLASMEIJER, M. J. August 1998. Personal communication.

PLASMEIJER, M. J. AND VAN EEKELEN, M. C. J. D. 1993. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Reading, Mass.

PLOTKIN, G. D. 1975. Call-by-name, call-by-value and the [Lambda]-calculus. Theor. Comput. Sci. 1, 1, 125-159.

REES, J. A. AND CLINGER, W., EDS. 1986. [Revised.sup.3] report on the algorithmic language Scheme. ACM SIGPLAN Not. 21, 12, 37-79.

SALINIER, B. AND STRANDH, R. I. 1996. Efficient simulation of forward-branching systems with constructor systems. Journal of Symbolic Computation 22, 4, 381-399.

SEKAR, R., RAMAKRISHNAN, I. V., AND MISHRA, P. 1997. On the power and limitations of strictness analysis. J. ACM 44, 3, 505-525.

SHERMAN, D., STRANDH, R. I., AND DURAND, I. 1991. Optimization of equational programs using partial evaluation. In Proceedings, 1st Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM SIGPLAN Not. 26, 9, 72-82.

STAPLES, J. 1980. Computation on graph-like expressions. Theor. Comput. Sci. 10, 2, 171-185.

STECKLER, P. AND WAND, M. 1994. Selective thunkification. In Proceedings, 1st Symposium on Static Analysis, B. L. Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 162-178.

STRANDH, R. I. 1987. Optimizing equational programs. In Proceedings, 2nd Conference on Rewriting Techniques and Applications, P. Lescanne, Ed. Lecture Notes in Computer Science, vol. 256. Springer-Verlag, Berlin, 13-24.

STRANDH, R. I. 1988. Compiling equational programs into efficient machine code. Ph.D. thesis, Johns Hopkins University.

STRANDH, R. I. 1989. Classes of equational programs that compile efficiently into machine code. In Proceedings, 3rd Conference on Rewriting Techniques and Applications, N. Dershowitz, Ed. Lecture Notes in Computer Science, vol. 355. Springer-Verlag, Berlin, 449-461.

THATTE, S. R. 1985. On the correspondence between two classes of reduction systems. Inf. Process. Lett. 20, 2, 83-85.

THATTE, S. R. 1988. Implementing first-order rewriting with constructor systems. Theor. Comput. Sci. 61, 1, 83-92.

TURNER, D. A. 1979. A new implementation technique for applicative languages. Softw. Pract. Exper. 9, 1, 31-49.

VERMA, R. M. 1995. Transformations and confluence for rewrite systems. Theor. Comput. Sci. 152, 2, 269-283.

WALTERS, H. R. 1997. Epic and ARM--user's guide. Technical Report SEN-R9724, CWI, Amsterdam. Report and tool set available at http://www.babelfish.nl.

WALTERS, H. R. AND KAMPERMAN, J. F. T. 1996. EPIC: An equational language--abstract machine and supporting tools. In Proceedings, 7th Conference on Rewriting Techniques and Applications, H. Ganzinger, Ed. Lecture Notes in Computer Science, vol. 1103. Springer-Verlag, Berlin, 424-427.

WILSON, P. R. 1992. Uniprocessor garbage collection techniques. In Proceedings, 1st Workshop on Memory Management, Y. Bekkers and J. Cohen, Eds. Lecture Notes in Computer Science, vol. 637. Springer-Verlag, Berlin, 1-42.

WRAY, S. C. AND FAIRBAIRN, J. 1989. Non-strict languages--programming and implementation. Comput. J. 32, 2, 142-151.

Received May 1998; revised September 1998; accepted July 1999

Authors' addresses: W. J. Fokkink, University of Wales Swansea, Department of Computer Science, Singleton Park, Swansea SA2 8PP, Wales, UK; email: W.J.Fokkink@swan.ac.uk; J. F. Th. Kamperman, Reasoning, Inc., 700 East El Camino Real, Mountain View, CA 94040; email: jasper.kamperman@reasoning.com; H. R. Walters, Babelfish, Vondellaan 14, 1217 RX Hilversum, The Netherlands; email: pum@babelfish.nl.

Permission to make digital/hard copy of M1 or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.

WAN FOKKINK University of Wales Swansea

JASPER KAMPERMAN Reasoning, Inc.

and

PUM WALTERS Babelfish

Printer friendly Cite/link Email Feedback | |

Author: | FOKKINK, WAN; KAMPERMAN, JASPER; WALTERS, PUM |
---|---|

Publication: | ACM Transactions on Programming Languages & Systems |

Geographic Code: | 1USA |

Date: | Jan 1, 2000 |

Words: | 24852 |

Previous Article: | Local Type Inference. |

Next Article: | An Automata-Theoretic Approach to Modular Model Checking. |

Topics: |