Properties of a First-order Functional Language with Sharing

Zena M. Ariola

Computer & Information Science Department University of Oregon Arvind Laboratory for Computer Science Massachusetts Institute of Technology

A calculus and a model for a first-order functional language with sharing is presented. In most implementations of functional languages, argument subexpressions in a function application are shared to avoid their repeated evaluation. Recursive functions are typically implemented using graphs with cycles. Compilers for these languages sometimes employ non left-linear and left-cyclic rules for optimizations. A Graph Rewriting System (GRS) to address these concerns is developed. It is shown that a GRS without interfering rules is confluent. Along the lines of Lévy’s term model for the λ-calculus, a semantics of such a GRS is also presented. An application of the term model to compiler optimizations is discussed.

Keywords and phrases: Graph Rewriting Systems, Term Rewriting Systems, Non left-linear Rules, Cyclic Terms and Rules, Non interfering Rules, Confluence, Term Models, Compiler Optimizations.

1. Introduction

Sharing of subexpressions is of utmost importance in the implementation of functional languages. Consider the function definition F x = x+x and the expression F(2+3). Any decent implementation, independently of the evaluation strategy (normal-order or applicative-order) it employs, will evaluate the subexpression 2 + 3 only once. Several compiler optimizations are about increasing the sharing of subexpressions to avoid their repeated evaluation. In this paper, we discuss the syntactic and semantic properties of a calculus, which is adequate for capturing the sharing of subexpressions in first-order functional languages. The results of this paper are also relevant to compiling higher-order functional languages, because compilers of such languages often employ a technique known as “lambda-lifting” [13]. The program that results after lambda-lifting is in a “supercombinatory” form, and is treated as a first-order program [12].

A way to capture sharing is to represent the expression as a graph instead of a linear text string or tree. This allows sharing of identical terms through pointers, and avoids repeated evaluation of identical terms as it is commonly done in normal-order reduction. Graph reduction for the λ-calculus was proposed by Wadsworth in order to bring together the advantages of both the applicative and the normal order evaluation [20]. Wadsworth also formally proved the correctness of his graph reduction technique. As an aside, Wadsworth also showed that his graph reduction did not capture enough sharing to lead to an optimal interpreter. More recently a new graph structure, which allows sharing of “contexts”, has been proposed in [14, 17]. This latter technique leads to provably optimal interpreters for the λ-calculus [18]. In this paper, however, we are not concerned with optimality questions, and we restrict our attention to “argument sharing” in a language which is simpler than the λ-calculus.

Much of the past work on graph rewriting has been to prove its correctness with respect to either the λ-calculus [20] or Term Rewriting Systems [7, 8, 9, 16]. In contrast, this paper explores graph rewriting as a system in its own right, and makes no attempt to prove the correctness of a graph implementation with respect to a “tree (or unshared) view” of the computation. Motivated by what we have observed in real implementations of functional languages, we explore syntactic and semantic properties of graphs with cycles, and rewriting rules that recognize or create cycles. In this respect our calculus goes farther than either [20] or [8] where only acyclic graphs are considered. Without cyclic graphs some important implementation ideas are ruled out. More recently, Klop et al. [15] have extended the Barendregt’s graph rewriting system to deal with cycles. However, their approach is significantly different from ours in that they model cyclic graph rewriting as “transfinite reduction” of infinitary graph terms.

In the following, we formally introduce a Graph Rewriting System (GRS). The basic feature of a GRS is the block construct, i.e., letrec. A block in a GRS is not treated as syntactic sugar for application; it is central to expressing the sharing of subexpressions. Our GRS includes cyclic terms and permits both non left-linear rules and left-cyclic rules. We prove that in the absence of interfering rules a GRS is confluent. This is a more general result than the confluence theorem in [15]. We think that our approach also leads to a simpler proof of confluence than in [15].

We also develop a term model for a GRS without interfering rules along the lines of Lévy’s term model for the λ-calculus. We introduce the notion of “information content” associated to a term, and show that the information content defines a congruence on the set of terms. This result can be applied in a straightforward manner to show the partial correctness of those optimizations that simply increase the sharing in a term. An example of such an optimization is the common subexpression elimination. Moreover, the result implies the partial correctness of the cyclic implementation of the Y-rule.

The paper is organized as follows: In Section 2, we introduce graph rewriting taking combinatory logic as an example, and compare our notation with that of Barendregt’s [8]. We formally describe GRSs, in Section 3. We introduce an ordering on terms based on sharing of subterms, and formulate the notion of a redex using this ordering. In Section 4, we introduce GRSs without interfering rules and prove their confluence. Section 5 gives a term model for the semantics of non-interfering GRSs. In Section 6, we apply the results of Section 5 to prove the correctness of some compiler optimizations, while in Section 7 we discuss directions for future work.

2. An Example: A Graph Rewriting System for Combinatory Logic

Given the TRS rule F(x) − ; − ; → G(x, x), the term F(+(2, 3)) can be rewritten to G(+(2, 3), +(2, 3)). That is, the term +(2, 3) is substituted for each occurrence of the variable x on the right-hand side of the above rule, and is thus, duplicated. A graph rewriting system avoids this duplication of work by substituting a pointer to +(2, 3) for each reference to variable x, as depicted below:

Our formalism for expressing graph rewriting is based on the observation that a natural way to represent a graph textually is to associate an identifier to each node of the graph, and then write down all the interconnections as a recursive let-block. Equivalently we can say that we associate a name to each subexpression of a term. For example, the above term F(+(2, 3)) will be expressed as:

\{ \begin{matrix}t_{1} = +(2, 3); \\ t_{2} = F(t_{1}); \\ In t_{2}\} \end{matrix}

In applying the above rule, the name t_{1}, and not the expression +(2, 3), will be substituted for each occurrence of x, leading to the term:

\{ \begin{matrix}t_{1} = +(2, 3); \\ t_{2} = G(t_{1}, t_{1}); \\ In t_{2}\} \end{matrix}

The substitution of an expression such as +(2, 3) is not permitted to avoid duplication of work. Only when +(2, 3) becomes a value, i.e., 5, it can be substituted for each free occurrence of t_{1}. Therefore, we think that an essential feature of a language to model sharing is a recursive let-block construct with a suitable notion of substitutable values.

The syntax of GRS terms is given in Figure 1. Superscript on a function symbol indicates its “arity” i.e., the number of arguments it is supposed to have; constants are assumed to be function symbols of arity 0. Throughout this paper we consider constants to be (in implementation parlance) “unboxed”. Thus, they are never shared and are freely substitutable. “Boxed” values can be modeled in a straightforward manner by wrapping a function symbol of arity one (say, called Box) around a value. The textual order of bindings in a block is not relevant, and the variable names on the left-hand side in a block must be pairwise distinct. Furthermore, for technical convenience we make a stronger assumption, that is, no variable name can be defined more than once on the left-hand side in a term regardless of its lexical level. Ω is a special term whose significance will become clear when we formally define the notion of a redex in Section 3.4. Next we informally present the GRS for combinatory logic, and relate our GRS notation to Barendregt’s [8].

Consider the S rule:

Ap (Ap (Ap (S, x), y), z) − ; − ; → Ap (Ap (x, z), Ap (y, z))

SE  ∈ Simple Expression
E  ∈ Expression
F^{k}  ∈ F^{k}
Constant ∈ F^{0}

\begin{aligned}SE & ::= & V ariable | Constant \\ E & ::= & SE \\ & | & F^{k} (SE_{1}, ⋯, SE_{k}) \\ & | & Block \\ & | & Ω \\ Block & ::= & \{ [Binding; ]^{∗} In SE\} \\ Binding & ::= & V ariable = E \\ T erm & ::= & E \end{aligned}

Figure 1. Syntax of terms of a GRS with signature F

Figure 2. Graph rule for the S combinator

which is shown in Barendregt et al. graph notation in Figure 2. Intuitively, applying this rule consists of allocating three new nodes, root′_{r}, n′_{1} and n′_{2}, corresponding to root_{r}, n_{1} and n_{2}, respectively, (build phase) and redirecting all the pointers to the redex node (i.e., the node matching root_{l}) to the node root′_{r} (redirection phase). Notice that the redirection phase does not affect the graph matching the subgraph g ≡ Ap (Ap (S, x), y) (included in dotted lines in Figure 2), thus we call the subgraph g the precondition of the above rule. In order to represent the right-hand side (i.e., rhs) of the S rule textually we simply write down the graph rooted at root_{r} as a recursive let-block. Thus, the Sg rule, that is, the S rule in GRS notation, can be written as follows:

\frac{x_{1} = Ap (x_{2}, z_{2}) ; x_{2} = Ap (S, z_{3})}{x = Ap (x_{1}, z_{1}) − ; − ; → x = \{ \begin{matrix}t_{1} & = & Ap (z_{3}, z_{1}); \\ t_{2} & = & Ap (z_{2}, z_{1}); \\ t & = & Ap (t_{1}, t_{2}); \\ & In t\} \end{matrix}}

Variables, such as t_{1}, t_{2} and t, that occur on the rhs of the rule but not on the lhs or in the precondition, generate new corresponding variables for each application of the rule.

Similarly the Kg rule, that is, the K rule in GRS notation is expressed as follows:

\frac{x_{1} = Ap (K, z_{2})}{x = Ap (x_{1}, z_{1}) − ; − ; → x = z_{2}}

\{ \begin{matrix}w_{1} = Ap (S, P); \\ w_{2} = Ap (w_{1}, Q); \end{matrix} w_{3} = ^{Ap (w_{2}, R);}_{ρ} w_{4} = G (w_{1}, w_{3}); In w_{4}\}  − ; − ; →_{w_{3}} M_{1} ≡ \{w_{1} = Ap (S, P); w_{2} = Ap (w_{1}, Q); w_{3} = \{ \begin{matrix}t′_{1} = Ap (P, R); \\ t′_{2} = Ap (Q, R); \\ t′ = Ap (t′_{1}, t′_{2}); \\ In t′\} \end{matrix} w_{4} = G (w_{1}, w_{3}); In w_{4}\} ≡_{α} \{w_{1} = Ap (S, P); w_{2} = Ap (w_{1}, Q); t′_{1} = Ap (P, R); t′_{2} = Ap (Q, R); t′ = Ap (t′_{1}, t′_{2}); w_{4} = G (w_{1}, t′); In w_{4}\} ≡_{α} \{w_{1} = Ap (S, P); t′_{1} = Ap (P, R); t′_{2} = Ap (Q, R); t′ = Ap (t′_{1}, t′_{2}); w_{4} = G (w_{1}, t′); In w_{4}\}

Figure 3. Graph reduction and its corresponding GRS reduction

In Figure 3 we show the graph reduction in Barendregt notation and our notation using the following term:

M ≡ \{ \begin{aligned}w_{1} & = & Ap (S, P); \\ w_{2} & = & Ap (w_{1}, Q); \end{aligned} w_{3} = \underbrace{Ap (w_{2}, R);}_{ρ} w_{4} = G (w_{1}, w_{3}); In w_{4}\}

Intuitively, the two bindings in the box inside M match the precondition and the subterm ρ matches the lhs of the Sg rule according to the following substitution:

x = w_{3}, x_{1} = w_{2}, x_{2} = w_{1}, z_{3} = P, z_{2} = Q, z_{1} = R

Since w_{3} corresponds to x, it is called the root of the redex. Using the above substitution an instance of the rhs of the Sg rule is created. It introduces fresh copies for the bound variables of the rhs of the Sg rule. This step corresponds to the build phase of the Barendregt system. Subsequently, variable w_{3} is bound to the newly instantiated term. Thus obtaining M_{1}. This rebinding of w_{3} corresponds to the redirection phase in Barendregt. M_{1} is then canonicalized by flattening blocks and substituting variables and constants in M_{1}. The introduction of fresh variables during the instantiation of the rhs of a rule removes the need to rename variables when blocks are flattened. There is one more step called the garbage collection, that is, the deletion of nodes that are not reachable from the root. Thus, the definition of variable w_{2} is eliminated because it is no longer reachable from node w_{4}. The term M is said to rewrite to the final term so obtained. Notice that the final term is indeed the term corresponding to the rightmost graph in Figure 3.

There is, however, a subtle difference between the two systems which shows up in the presence of “projection” rules and cyclic graphs. For example, given the rule x = I(y) − ; − ; → x = y, and the cyclic term M ≡ {t = I(t); In t}, M − ; − ; → M, following the Barendregt system, while M − ; − ; → {t = t; In t}, following our system. As explained later {t = t; In t} becomes ⊙, a symbol which represents a “meaningless” term. This difference has a strong impact on the confluence of GRSs. We will further clarify these issues after introducing GRSs formally in Section 3.

3. GRS: Terms, Rules and Reduction

3.1. GRS terms

Definition 3.1. (GRS term) A GRS term over signature F = F^{0} ∪ F^{1} ∪ ⋯ is defined inductively as follows:

(i) a variable x is a term; (ii) a constant c, where c ∈ F^{0}, is a term; (iii) Ω is a term; (iv) F^{k}(y_{1}, ⋯, y_{k}) is a term if ∀i, 1≤i<k, y_{i} is either a variable or a constant, and F^{k} ∈ F^{k};

(v) {x_{1} = e_{1}; ⋯; x_{p} = e_{p}; In x} is a term if (v.1) ∀i, 1≤i≤p, x_{i} is a variable and e_{i} is a term; (v.2) x is either a constant or a variable; (v.3) ∀i, j, 1≤i<j ≤p, x_{i} ≢ x_{j}. The order of bindings in a block term is irrelevant.

Clause (v.3) prevents multiple definitions of a variable; for example, {x = 3; x = 4; ⋯ In z} is not a legal term. For technical convenience we assume that if the main term M is of the form F^{k}(y_{1}, ⋯, y_{k}) or Ω then M has a name associated to it, that is, M ≡ {t = M; In t}. We also assume that {In x} ≡ x.

Definition 3.2. (Root of a term) Given a GRS term M, the root of M, Root(M), is :

(i) M, if M is either a constant or a variable; (ii) x, if M is {x_{1} = e_{1}; ⋯ x_{p} = e_{p}; In x}.

Definition 3.3. (Free Variables of a GRS term) The set of free variables of a GRS term M, FV(M), is defined inductively as follows:

(i) FV(x) = {x} (ii) FV(c) = ∅ (iii) FV(Ω) = ∅ (iv) FV(F^{k}(y_{1}, ⋯, y_{k})) = ⋃{FV(y_{i}) | 1≤i≤k}

(v) FV({x_{1} = e_{1}; ⋯; x_{p} = e_{p}; In x}) = (⋃{FV(e_{i}) | 1 ≤ i ≤ p} ∪ FV(x)) − {x_{1}, ⋯, x_{p}}. Where − is the set difference operator.

Definition 3.4. (Bound Variables of a GRS term) The set of bound variables of a GRS term M, BV(M), is defined inductively as follows:

(i) BV(x) = ∅ (ii) BV(c) = ∅ (iii) BV(Ω) = ∅ (iv) BV(F^{k}(y_{1}, ⋯, y_{k})) = ∅

(v) BV({x_{1} = e_{1}; ⋯; x_{p} = e_{p}; In x}) = {x_{1}, ⋯, x_{p}} ∪ (⋃{BV(e_{i}) | 1≤i≤p}).

Definition 3.5. (Variables of a GRS term) The set of variables of a GRS term M, Var(M), is defined to be FV(M) ∪ BV(M).

Definition 3.6. (Constants of a GRS term) The set of constants of a GRS term M, Constants(M), is defined inductively as follows:

(i) Constants(x) = ∅

(ii) Constants(c) = {c} (iii) Constants(Ω) = ∅ (iv) Constants(F^{k}(y_{1}, ⋯, y_{k})) = ⋃{Constants(y_{i}) | 1≤i≤k}

(v) Constants({x_{1} = e_{1}; ⋯; x_{p} = e_{p}; In x}) = (⋃{Constants(e_{i}) | 1≤i≤p}) ∪ Constants(x).

For technical convenience we will assume the following variable convention. Variable convention: i.) all bound variables of a term are distinct; ii.) all bound and free variables of a term are distinct.

The following two terms are illegal because of this variable convention.

\{ \begin{matrix}x = \{ \begin{matrix}y = +(w, w); \\ In y\}; \end{matrix} \\ w = +(y, x); \\ In w\} \end{matrix}  \{ \begin{matrix}x = \{ \begin{matrix}x = +(w, w); \\ In x\}; \end{matrix} \\ w = +(y, x); \\ In w\} \end{matrix}

Definition 3.7. (Substitution operation) Given a GRS term M, y ∈ (V ariable ∪ F^{0}), and z ∈ V ariable such that {y, z} ⊈ BV(M), the substitution of y for each free occurrence of z in M, written as M[y/z], is defined inductively as follows:

(i) z[y/z] = y (ii) x[y/z] = y , if x ≢ z (iii) c[y/z] = c (iv) Ω[y/z] = Ω

(v) F^{k}(y_{1}, ⋯, y_{k})[y/z] = F^{k}(y_{1}[y/z], ⋯, y_{k}[y/z]) (vi) {x_{1} = e_{1}; ⋯; x_{p} = e_{p}; In x}[y/z] = {x_{1} = e_{1}[y/z]; ⋯; x_{p} = e_{p}[y/z]; In x[y/z]}

3.2. Canonical forms of terms

Consider the following terms:

\{ \begin{matrix}x = 8; \\ z = \{ \begin{matrix}y = x; \\ w = +(x, y); \\ In w\}; \end{matrix} \\ In z\} \end{matrix}  \{ \begin{matrix}x = 8; \\ y = x; \\ w = +(x, y); \\ In w\}; \end{matrix} \{ \begin{matrix}w = +(8, 8); \\ In w\} \end{matrix}

These terms have different syntactic structure, however, we consider this difference merely syntactic noise. While the following terms:

\{ \begin{matrix}w = +(x, y); \\ In w\}; \end{matrix}  \{ \begin{matrix}w = +(x_{1}, y_{1}); \\ In w\} \end{matrix}

which differ only in the reference to the free variables will not be considered the same. We also consider the following two terms to be distinct because Ω is not a “substitutable value”.

\{ \begin{matrix}x = F(y, z); \\ y = Ω; \\ z = Ω; \\ In x\} \end{matrix}  \{ \begin{matrix}x = F(y, y); \\ y = Ω; \\ In x\} \end{matrix}

We introduce the following rules to compute the canonical form of a term.

Block Flattening rule:

{x = { y_{1} = e′_{1}; ⋯ y_{m} = e′_{m};  {x = y
In y}; − ; − ; → y_{1} = e′_{1}; ⋯ y_{m} = e′_{m};
x_{1} = e_{1}; ⋯ x_{n} = e_{n};  x_{1} = e_{1}; ⋯ x_{n} = e_{n};
In z}  In z}

Substitution rules:

{x_{1} = e_{1}; ⋯ x = c; ⋯ x_{n} = e_{n}; In z} − ; − ; → {x_{1} = e_{1}[c/x]; ⋯ x_{n} = e_{n}[c/x]; In z[c/x]}  c ∈ F^{0}
{x_{n} = e_{n}; ⋯ x = y; ⋯ x_{n} = e_{n}; In z} − ; − ; → {x_{n} = e_{n}[y/x]; ⋯ x_{n} = e_{n}[y/x]; In z[y/x]}  x ≢ y
{x_{n} = e_{n}; ⋯ x = x; ⋯ x_{n} = e_{n}; In z} − ; − ; → {x_{n} = e_{n}[⊙/x]; ⋯ x_{n} = e_{n}[⊙/x]; In z[⊙/x]}

where ⊙ is a special constant. These rules formalize the notion of a substitutable expression, and say that only constants and variables (provided x and y are distinct variables) can be substituted freely. Moreover, note that a binding like x = y or x = c is deleted after the substitution. If we encounter a degenerate binding like x = x then we substitute the special constant ⊙ for x. Disallowing such bindings does not help because they can arise as a consequence of doing a reduction. In fact, as pointed out in Section 2, given the rule x = I(y) − ; − ; → x = y, the term {x = I(x); In x} will go to ⊙.

Definition 3.8. (Canonical form) Given a GRS term M, the canonical form of M is computed using the following two steps:

1. Flatten all blocks in M using the Block Flattening rule. Then apply the Substitution rules to the term as many times as they apply. Let the result be \overline{M}.

2. Eliminate the garbage, that is, the subterms of \overline{M} that are unreachable from the root of M. Let the result be GC(\overline{M}).

Proposition 3.9. The canonical form of a GRS term M always exists and is unique.

Proof. Since there are only a finite number of blocks in M, and an application of the Block Flattening rule eliminates one block without creating a new one, the Block Flattening rule can be applied only a finite number of times. The final flattened term is unique since the Block flattening rule has the diamond property.

There are only a finite number of bindings of the form x = y or x = c or x = x in the flattened term. Each of these bindings can be eliminated in one substitution step without creating a new binding. Furthermore, because of the third substitution rule (i.e., the introduction of ⊙), the substitution rules also have the diamond property. Hence \overline{M} exits and is unique.

GC(\overline{M}) is unique by the definition of garbage collection. □

Renaming rule:

{x_{1} = e_{1}; ⋯; x_{p} = e_{p}; In x} − ; − ; → {x_{1} = e_{1}[x′_{j}/x_{j}]; ⋯; x′_{j} = e_{j}[x′_{j}/x_{j}]; ⋯; x_{p} = e_{p}[x′_{j}/x_{j}] In x[x′_{j}/x_{j}]}

where x′_{j} is a new variable. The renaming rule is similar to the α-renaming in the λ-calculus.

Definition 3.10. (α-equivalence) Given GRS terms M and N, M and N are said to be α-equivalent, written as M ≡_{α} N, iff GC(\overline{M}) ≡ GC(\overline{N}) up to renaming.

The canonicalization rules plus renaming do not affect the “graph” associated to a term, in other words, all α-equivalent terms will correspond to rooted isomorphic graphs.

3.3. GRS rules

Definition 3.11. (GRS rule) A GRS rule τ is a set of preconditions, x_{1} = e_{1}, ⋯, x_{n} = e_{n}, and a lefthand side, l, and a right-hand side, r, and is written as:

\frac{x_{1} = e_{1}; ⋯; x_{n} = e_{n}}{x = l − ; − ; → x = r}

where:

(i) the pattern of rule τ, {x_{1} = e_{1}; ⋯ x_{n} = e_{n}; x = l; In x}, is a block-term in canonical form, and l ≢ Ω; (ii) r is a term such that FV(r) ⊆ Var({x_{1} = e_{1}; ⋯ x_{n} = e_{n}; x = l; In x}).

The pattern of rule τ is denoted by P(τ). The term r is called the right-hand side of the rule and is denoted by RHS(τ). The free variables of the pattern of τ are called the meta-variables of rule τ.

Notice that restriction (i) makes it impossible to give a GRS rule to rewrite a constant or a variable. In general, a GRS rule does not contain any Ωs.

Definition 3.12. (GRS) A GRS is a structure (A(F), R), where A(F) is the set of GRS terms defined over signature F, and R is a set of GRS rules.

Definition 3.13. (Left-linear rule) A GRS rule τ is said to be left-linear iff ∀y ∈ Var(P(τ)), y is referenced at most once in P(τ).

Definition 3.14. (Left-acyclic rule) A GRS rule τ is said to be left-acyclic iff ∀y ∈ BV(P(τ)), y is not reachable from itself in P(τ). Otherwise the rule is said to be a left-cyclic rule.

The rule, x = A(x) − ; − ; → x = 0, is an example of a left-cyclic rule. Notice that a left-cyclic rule is always non left-linear.

3.4. Identifying redexes and ω-ordering

There are subtle issues involved in identifying redexes in a term. Consider the following two rules:

τ_{1} : \frac{x_{1} = F(0); x_{2} = F(0)}{x = G(x_{1}, x_{2}) − ; − ; → x = 0}  τ_{2} : \frac{x_{1} = F(0)}{x = G(x_{1}, x_{1}) − ; − ; → x = 0}

and the following two terms:

M ≡ \{ \begin{matrix}t_{1} = F(0); \\ t_{2} = F(0); \\ t_{3} = G(t_{1}, t_{2}); \\ In t_{3}\} \end{matrix}  N ≡ \{ \begin{matrix}t_{1} = F(0); \\ t_{2} = G(t_{1}, t_{1}); \\ In t_{2}\} \end{matrix}

On the basis of the intuitive description given in Section 2, we can undoubtedly say that τ_{1} matches M, with substitution “x = t_{3}, x_{1} = t_{1}, x_{2} = t_{2}”, and τ_{2} matches N with substitution “x = t_{2}, x_{1} = t_{1}”. Does rule τ_{1} applies to N? or does rule τ_{2} applies to M? Rule τ_{1} does indeed apply to the term N by matching both the preconditions to the same binding, that is, by the substitution “x_{1} = t_{1}, x_{2} = t_{1}, x = t_{2}”. However, there is no variable substitution that can make τ_{2} applicable to M. Thus, the preconditions of a rule can be satisfied by overlapping bindings, moreover, the left-hand side of a rule can also overlap its precondition, as shown in the following example. Consider the rule:

\frac{x_{1} = G(y)}{x = G (x_{1}) − ; − ; → x = 0}

and the term M ≡ {t = G(t); In t}. The substitution “x = t, x_{1} = t, y = t” makes G(t) both a redex and its precondition! We can capture the notion of a redex in terms of an ordering on terms.

Definition 3.15. (ω-ordering: ≤_{ω}) Given GRS terms M and N in canonical form, M ≤_{ω} N iff ∃ a function σ :

                      Var(M) ∪ Constants(M) → Var(N) ∪ Constants(N)

such that:

(i) ∀c ∈ Constants(M), σ(c) = c; (ii) ∀x ∈ FV(M), σ(x) = x; (iii) ∀x ∈ BV(M), if x = F^{k}(y_{1}, ⋯, y_{k}) in M then σ(x) ∈ BV(N) and σ(x) is bound to F^{k}(σ(y_{1}), ⋯, σ(y_{k})) in

N; (iv) σ(Root(M)) = Root(N). σ is called the substitution function induced by the ordering.

Notice that according to condition (iii) if x is bound to Ω then x can be mapped to any variable or constant in N. Intuitively, M ≤_{ω} N if N can be obtained from M by replacing Ω with any other term or by increasing the sharing in M. This is a generalization of the ordering on TRS terms introduced by Huet and Lévy [11].

Proposition 3.16. The ω-ordering is a partial order with Ω as the least element.

Proof. See [5]. □

The following examples may enhance the reader’s intuition about ω-ordering.

Consider the following acyclic terms:

M_{1} ≡ {x_{1} = G(x_{2}, x_{2}); x_{2} = F(0); In x_{1}}
M_{2} ≡ {x_{1} = G(x_{2}, x_{3}); x_{2} = F(0); x_{3} = F(0); In x_{1}}
M_{3} ≡ {x_{1} = G(x_{2}, x_{2}); x_{2} = Ω; In x_{1}}
M_{4} ≡ {x_{1} = G(x_{2}, x_{3}); x_{2} = Ω; x_{3} = Ω; In x_{1}}

Notice that M_{2} ≤_{ω} M_{1}, M_{3} ≤_{ω} M_{1}, and M_{4} is ≤_{ω} M_{1}, M_{2} and M_{3}. However, M_{2} and M_{3} are not related. Now consider the following cyclic terms:

N_{1} ≡ {x_{1} = F(x_{1}); In x_{1}}
N_{2} ≡ {x_{1} = F(x_{2}); x_{2} = F(x_{1}); In x_{1}}
N_{3} ≡ {x_{1} = F(x_{2}); x_{2} = F(x_{3}); x_{3} = F(x_{1}); In x_{1}}

Notice that N_{2} ≤_{ω} N_{1} and N_{3} ≤_{ω} N_{1} but N_{2} and N_{3} are not related.

We use ω-ordering as follows in defining a redex. We bind all meta-variables of a rule to Ω. Such a term is called the closure of a rule. If term p is the closure of rule τ then a term M is said to be a τ-redex if p ≤_{ω} M.

Definition 3.17. (Closure of a rule) Given a GRS rule τ, where P(τ) ≡ {x_{1} = e_{1}; ⋯ x_{n} = e_{n}; x = l; In x}, the closure of τ, written as Cl(τ), is the term {y_{1} = Ω; ⋯ y_{m} = Ω; x_{1} = e_{1}; ⋯ x_{n} = e_{n}; x = l; In x}, where {y_{1}, ⋯, y_{m}} = FV(P(τ)).

Definition 3.18. (Subterm rooted at x_{i}) Given a GRS term M ≡ {x_{1} = e_{1}; ⋯ x_{p} = e_{p}; In x} in canonical form, and x_{i} ∈ BV(M), the subterm of M rooted at x_{i}, written as M@x_{i}, is the term GC({x_{1} = e_{1}; ⋯ x_{p} = e_{p}; In x_{i}}).

Definition 3.19. (Redex) A redex in a GRS term M in canonical form is a triple (τ, z, σ) such that:

(i) τ is a GRS rule; (ii) z ∈ BV(M), such that Cl(τ) ≤_{ω} M@z; (iii) σ is the substitution induced by Cl(τ) ≤_{ω} M@z. z is said to be the root of the redex. If z = Root(M) then M itself is said to be a redex. The set containing the roots of all redexes in M is denoted by ℜ(M).

For example, consider the following rule:

τ : x = G(y, y) − ; − ; → x = 0

and the term M ≡ {z = G(z_{1}, z_{1}); z_{1} = F(0); z_{2} = H(z); In z_{2}} which has the following graph:

M@z is a redex because Cl(τ) ≡ {y = Ω; x = G(y, y); In x} ≤_{ω} M@z.

Definition 3.20. (Distinct Redexes) Two redexes ρ_{1} = (τ_{1}, z_{1}, σ_{1}) and ρ_{2} = (τ_{2}, z_{2}, σ_{2}) in a GRS term M in canonical form are said to be distinct if τ_{1} ≠ τ_{2} or z_{1} ≠ z_{2}.

3.5. Reduction

We have explained informally, in Section 2, that a GRS reduction consists of first making a copy of the right-hand side of the rule, and then replacing the root of the redex with that copy. Therefore, we introduce the notion of an instance of a term M for a given substitution σ, and the operation of replacement. An instance of M is created by substituting σ(x) for each free occurrence of variable x in M, and by renaming each bound variable of M.

Definition 3.21. (Instance of a term) Given a GRS term M in canonical form and a substitution σ, an instance of M, written as M^{σ}, is defined inductively as follows:

(i) x^{σ} = σ(x), where x is either a constant or a variable; (ii) Ω^{σ} = Ω; (iii) F^{k}(y_{1}, ⋯, y_{k})^{σ} = F^{k}(y_{1}^{σ}, ⋯, y_{k}^{σ});

(iv) { x_{1} = e_{1}; ; ⋮ ; x_{p} = e_{p}; ; In x}^{σ} = { x′_{1} = (e_{1}[x′_{1}/x_{1}] ⋯ [x′_{p}/x_{p}])^{σ}; ; ⋮ ; x′_{p} = (e_{p}[x′_{1}/x_{1}] ⋯ [x′_{p}/x_{p}])^{σ}; ; In (x[x′_{1}/x_{1}] ⋯ [x′_{p}/x_{p}])^{σ}}

where x′_{i}, 1≤i≤ p, are new variables.

The above definition does not depend on the order of the substitutions because x′_{i} ∉ Var(M).

Given a rule τ, and a redex (τ, z, σ) in M, the reduction step consists of replacing the term bound to z by (RHS(τ))^{σ} ( i.e., an instance of the right-hand side of τ).

Definition 3.22. (Replacement) Given GRS terms M and N, where N is in canonical form and BV(N)∩ Var(M) = ∅, the replacement of the term bound to z in M by N, written as M[z ← N], is defined as follows:

(i) M, if z ∉ BV(M); (ii) {x_{1} = e_{1}; ⋯; z = N; ⋯; x_{n} = e_{n}; In x}, if M ≡ {x_{1} = e_{1}; ⋯; z = e_{i} ⋯; x_{n} = e_{n}; In x}.

Notice that no renaming occurs during the replacement, thus the free variables of N can get captured. Moreover, the bound variables of M, which are different from z, are not affected by the replacement.

Notation: M[Z ← Ω], where Z = {z_{1}, ⋯, z_{n}} will stand for M[z_{1} ← Ω] ⋯ [z_{n} ← Ω].

Now we state certain useful properties of replacement.

Proposition 3.23. Given GRS terms M, N_{1} and N_{2} in canonical form such that (BV(N_{1}) ∩ BV(N_{2})) = ∅, (BV(N_{1}) ∪ BV(N_{2})) ∩ Var(M) = ∅, and variables z_{1}, z_{2} such that z_{1} ≢ z_{2}, and {z_{1}, z_{2}} ⊈ BV(N_{1}) ∪ BV(N_{2}):

M[z_{1} ← N_{1}][z_{2} ← N_{2}] ≡ M[z_{2} ← N_{2}][z_{1} ← N_{1}].

Proof. By cases on the existence of z_{1} and z_{2} in BV(M). □

The following proposition shows that under appropriate circumstances the garbage collection step can be postponed.

Proposition 3.24. Given GRS terms M and N, such that N is in canonical form. If BV(N) ∩ Var(M) = ∅ and FV(N) ⊆ Var(GC(\overline{M})) then

GC(\overline{GC(\overline{M})[z ← N]}) ≡ GC(\overline{\overline{M}[z ← N]}).

Proof. The garbage collection does not affect N. The condition FV(N) ⊆ Var(GC(\overline{M})) guarantees that the garbage not picked up by the inner GC is not affected by N, and thus is collected by the outer GC. □

Proposition 3.25. Given GRS terms M, N, P and P′ in canonical form, and variable z′ such that

(i) BV(P) ∩ Var(M) = ∅; (ii) P′ ≡_{α} P; (iii) BV(P′) ∩ Var(N) = ∅. If M ≤_{ω} N let σ_{MN} be the substitution function induced by the ω-ordering, z be such that σ_{MN}(z) = z′, and Z = {s | s ∈ BV(M), σ_{MN}(s) = z′, s ≢ z}, then

GC(GC(\overline{M[z ← P]})[Z ← Ω]) ≤_{ω} GC(\overline{N[z′ ← P′]}).

Proof. We first show the following

GC(M[z ← Ω][Z ← Ω]) ≤_{ω} GC(\overline{N[z′ ← P′]})

that is we want to show that the function σ_{MN} restricted to the domain of elements occurring in GC(M[z ← Ω][Z ← Ω]) is the substitution function induced by GC(M[z ← Ω][Z ← Ω]) ≤_{ω} GC(\overline{N[z′ ← P′]}). Suppose it is not, then it must be the case that for an element, say x, occurring in GC(M[z ← Ω][Z ← Ω]), σ_{MN}(x) does not occur in GC(\overline{N[z′ ← P′]}). This means that the replacement of the term bound to z′ by P′ in N has removed the path to σ_{MN}(x). However, this means that the corresponding path in M gets removed also by setting to Ω z and all the elements of Z. Contradiction, therefore it must be the case that σ_{MN}(x) occurs in GC(\overline{N[z′ ← P′]}).

Moreover, for all elements x in BV(P), let x′ be its renamed version. The following function:

σ′(x) = \{ \begin{matrix}σ_{MN}(x) & x ∈ GC(GC(\overline{M[z ← Ω]})[Z ← Ω]) \\ x′ & x ∈ BV(P) \end{matrix}

determines the ordering:

GC(GC(\overline{M[z ← P]})[Z ← Ω]) ≤_{ω} GC(\overline{N[z′ ← P′}]) ≡ N_{1}.

□

Definition 3.26. (Reduction) Given a GRS term M in canonical form and a rule τ, M reduces to N by doing the τ-redex at z in M, written as M − ; − ; →_{z}^{τ} N, iff (τ, z, σ) is a redex in M, and N ≡ GC(\overline{M[z ← (RHS(τ))^{σ}]}). The reflexive and transitive closure of − ; − ; → is denoted by − ; → ; →.

The redex (τ, z, σ) is often given the name ρ, and sometimes we will also use the notation M − ; − ; →_{ρ} N to show the reduction of redex ρ. Note that each replacement is followed by a canonicalization step.

3.6. Descendant of a redex

Definition 3.27. (Descendant of a redex) Given two distinct redexes ρ_{1} = (τ_{1}, z_{1}, σ_{1}) and ρ_{2} = (τ_{2}, z_{2}, σ_{2}) in a GRS term M in canonical form, the descendant of ρ_{2} with respect to the reduction M − ; − ; →_{ρ_{1}} M_{1} (written as ρ_{2} \ ρ_{1}):

(i) does not exist, if z_{2} ∉ BV(M_{1}); (ii) is the triple ρ′_{2} = (τ_{2}, z_{2}, σ′_{2}), if z_{2} ∈ BV(M_{1}) and σ′_{2} is:

σ′_{2}(x) = \{ \begin{matrix}σ_{2}(x) & σ_{2}(x) ≠ z_{1} \\ Root(r_{1}^{σ_{1}}) & σ_{2}(x) = z_{1} and Root(r_{1}^{σ_{1}}) ≠ z_{1} \\ ⊙ & σ_{2}(x) = z_{1} and Root(r_{1}^{σ_{1}}) = z_{1} \end{matrix}

The descendant of a redex does not necessarily exists, and even if it exists, it is not necessarily a redex, as illustrated by the following example. Consider the following two rules:

\begin{matrix}τ_{1} : \frac{x_{1} = G(y)}{x = F(x_{1}) − ; − ; → x = x_{1}} \\ τ_{2} : x = G(0) − ; − ; → x = 0 \end{matrix}

and the following reduction:

{ t_{1} = F(t_{2}); t_{2} = G(0); In t_{1}}
[figure: τ_{2}; τ_{1}]
{ t_{1} = F(0); In t_{1}}  { t_{2} = G(0); In t_{2}}

The two redexes in the above term are ρ_{1} = (τ_{1}, t_{1}, σ_{1}), where σ_{1} is “x = t_{1}, x_{1} = t_{2}, y = 0”, and ρ_{2} = (τ_{2}, t_{2}, σ_{2}), where σ_{2} is “x = t_{2}”, respectively. ρ_{2} \ ρ_{1} is (τ_{2}, t_{2}, σ′_{2}), where σ′_{2} is “x = t_{2}”, and is still a redex. On the other hand, ρ_{1} \ ρ_{2} = (τ_{1}, t_{1}, σ′_{1}), where σ′_{1} is “x = t_{1}, x_{1} = 0, y = 0”, is no longer a redex.

Remark 3.28. A GRS is non-duplicative, that is, the descendant of a redex, if it exists, is unique.

4. Confluence of a GRS without interfering rules

Not all GRSs are confluent, however, we can show that for a restricted class, namely GRSs without interfering rules, confluence is guaranteed. We introduce the notion of compatible terms [11] which will be used, among other things, to define the notion of interference among rules. The idea is that terms which are not ordered, may still have a common upper bound. As we shall see later, such terms potentially interfere with each other.

Definition 4.1. (Compatible terms) Given GRS terms M_{1} and M_{2} in canonical form, M_{1} and M_{2} are said to be compatible, written as M_{1} ↑_{ω} M_{2}, iff ∃M_{3} such that M_{1} ≤_{ω} M_{3} and M_{2} ≤_{ω} M_{3}.

For example, consider the following terms:

M_{1} ≡ {x_{1} = G(x_{2}, x_{2}); x_{2} = Ω; In x_{1}}

M_{2} ≡ {x_{1} = G(x_{2}, x_{3}); x_{2} = F(0); x_{3} = F(0); In x_{1}}
M_{2} ≡ {x_{1} = G(x_{2}, x_{3}); x_{2} = F(0); x_{3} = H(0); In x_{1}}

M_{1} and M_{2} are compatible with least upper bound: {x_{1} = G(x_{2}, x_{2}); x_{2} = F(0); In x_{1}}. On the other hand, M_{3} is not compatible either with M_{1} or M_{2}.

Definition 4.2. (Interference) Given two distinct GRS rules τ_{1} and τ_{2}, τ_{1} is said to interfere with τ_{2} iff ∃x ∈ BV(P(τ_{1})) such that Cl(τ_{1})@x ↑_{ω} Cl(τ_{2}).

Definition 4.3. (Self-interference) Given a GRS rule τ, τ is said to be self-interfering iff ∃x ∈ BV(P(τ_{1}))−Root(P(τ)) such that Cl(τ)@x ↑_{ω} Cl(τ).

Definition 4.4. (GRSNI) If all rules in a GRS are non self-interfering and pairwise non-interfering then the GRS is called a GRSNI.

For example, the following rule:

τ : \frac{x_{1} = L(y)}{x = L(x_{1}) − ; − ; → x = 0}

interferes with itself because Cl(τ)@x_{1} ↑_{ω} Cl(τ). The following rules:

τ_{1} : x = Or(y, True) − ; − ; → x = True

τ_{2} : x = Or(True, y) − ; − ; → x = True

also interfere because Cl(τ_{1}) ↑_{ω} Cl(τ_{2}), with Or(True, True) being the upper-bound.

Definition 4.5. (Ordering on Redexes) Given two distinct redexes ρ_{1} = (τ_{1}, z_{1}, σ_{1}) and ρ_{2} = (τ_{2}, z_{2}, σ_{2}) in a GRS term M in canonical form:

(i) ρ_{1} occurs inside ρ_{2}, written as ρ_{1} ⪯ ρ_{2}, iff z_{1} ∈ {σ_{2}(x) | x ∈ BV(P(τ_{2}))}; (ii) ρ_{2} occurs inside ρ_{1}, written as ρ_{2} ⪯ ρ_{1}, iff z_{2} ∈ {σ_{1}(x) | x ∈ BV(P(τ_{1}))}; (iii) ρ_{1} and ρ_{2} are disjoint iff ρ_{1} ⪯̸ ρ_{2}, and ρ_{2} ⪯̸ ρ_{1}. Furthermore, if ρ_{1} ⪯ ρ_{2} and ρ_{2} ⪯ ρ_{1} then ρ_{1} and ρ_{2} are said to overlap at the root.

Proposition 4.6. Given a GRSNI term M in canonical form, any two distinct redexes ρ_{1} and ρ_{2} in M are mutually disjoint.

Proof. Let ρ_{1} = (τ_{1}, z_{1}, σ_{1}) and ρ_{2} = (τ_{2}, z_{2}, σ_{2}). Suppose ρ_{1} ⪯ ρ_{2}. Then by Definition 4.5, ∃x ∈ BV(P(τ_{2})), say x_{2}, such that z_{1} = σ_{2}(x_{2}). Therefore, we have Cl(τ_{2})@x_{2} ↑_{ω} Cl(τ_{1}), with M@z_{1} being the upper bound. Since rules τ_{1} and τ_{2} are non-interfering, we have reached a contradiction. Similarly, if ρ_{2} ⪯ ρ_{1}. Hence ρ_{1} and ρ_{2} must be disjoint. □

Proposition 4.7. In a GRSNI reduction, the descendant of a redex, except for the redex being reduced, if it exists, is always a redex.

Proof. Let M − ; − ; →_{ρ} M_{1}, where ρ = (τ, z, σ). Let ρ_{1} = (τ_{1}, z_{1}, σ_{1}) be a distinct redex occurring in M, such that z_{1} ∈ BV(M_{1}). We want to show that ρ_{1} \ ρ = (τ_{1}, z_{1}, σ′_{1}) is a redex, that is, σ′_{1} is a substitution function from Cl(τ_{1}) to M_{1}@z_{1}. According to the definition of descendant of a redex (Definition 5.10), σ′_{1} differs from σ_{1} only at z, the root of redex ρ. Therefore, there are only two reasons why (τ_{1}, z_{1}, σ′_{1}) may not be a redex:

(1) the new definition of z;

(2) the canonicalization of M[z ← RHS(τ)^{σ}] removes some elements in the range of σ_{1}. The first reason is not possible because, by Proposition 4.6, all distinct redexes in M are disjoint, and therefore, if ∃x ∈ Var(P(τ_{1})), such that σ_{1}(x) = z then x ∈ FV(P(τ_{1})). The second reason is also not possible because if a variable or a constant in the range of σ_{1} is accessible from z_{1} in M then it has to be accessible from z_{1} in M_{1}. □

Theorem 4.8. (Subcommutativity of a GRSNI) Given a GRSNI term M in canonical form, and two distinct redexes ρ_{1} and ρ_{2} in M, if M − ; − ; →_{ρ_{1}} M_{1} and M − ; − ; →_{ρ_{2}} M_{2}, then ∃ M_{3} such that M_{2} − ; − ; →_{ρ_{1}\ρ_{2}}^{0/1} M_{3} and

M_{1} − ; − ; →_{ρ_{2}\ρ_{1}}^{0/1} M_{3}.

Proof. Let ρ_{1} = (τ_{1}, z_{1}, σ_{1}), and ρ_{2} = (τ_{2}, z_{2}, σ_{2}). Then, M_{1} ≡ GC(\overline{M[z_{1} ← r_{1}^{σ_{1}}]}), where r_{1} = RHS(τ_{1}), and M_{2} ≡ GC(\overline{M[z_{2} ← r_{2}^{σ_{2}}]}), where r_{2} = RHS(τ_{2}).

The proof is by cases on the existence of the descendant of redexes ρ_{1} and ρ_{2}, respectively.

1: ρ_{2} \ ρ_{1} = (τ_{2}, z_{2}, σ′_{2}) and ρ_{1} \ ρ_{2} = (τ_{1}, z_{1}, σ′_{1}). By Proposition 4.7 (τ_{2}, z_{2}, σ′_{2}) and (τ_{1}, z_{1}, σ′_{1}) must be redexes. Thus, we want to show the following:

GC(\overline{M_{1}[z_{2} ← r_{2}^{σ′_{2}}]}) ≡ GC(\overline{M_{2}[z_{1} ← r_{1}^{σ′_{1}}]})

We have:

GC(\overline{M_{2}[z_{1} ← r_{1}^{σ′_{1}}]})
≡ GC(\overline{GC(\overline{M[z_{2} ← r_{2}^{σ_{2}}]})[z_{1} ← r_{1}^{σ′_{1}}]})
≡ GC(\overline{\overline{M[z_{2} ← r_{2}^{σ_{2}}]}[z_{1} ← r_{1}^{σ′_{1}}]})  By Proposition 3.24
≡ GC(\overline{M[z_{2} ← r_{2}^{σ_{2}}][z_{1} ← r_{1}^{σ_{1}}]}) Implied by the definition of the descen-

dant of a redex (Definition 5.10) and of the canonicalization procedure (Definition 3.2).

≡ GC(\overline{M[z_{1} ← r_{1}^{σ_{1}}][z_{2} ← r_{2}^{σ_{2}}]})  By Proposition 3.23.
≡ GC(\overline{\overline{M[z_{1} ← r_{1}^{σ_{1}}]}[z_{2} ← r_{2}^{σ′_{2}}]})  Definitions 5.10 and 3.2.
≡ GC(GC(\overline{\overline{M[z_{1} ← r_{1}^{σ_{1}}]})[z_{2} ← r_{2}^{σ′_{2}}]}) By Proposition 3.24
≡ GC(\overline{M_{1}[z_{2} ← r_{2}^{σ′_{2}}]})

2: ρ_{1} \ ρ_{2} = (τ_{1}, z_{1}, σ′_{1}) and ρ_{2} \ ρ_{1} does not exists. We need to show :

M_{1} ≡ GC(\overline{M_{2}[z_{1} ← r_{1}^{σ′_{1}}]})

We have:

GC(\overline{M_{2}[z_{1} ← r_{1}^{σ′_{1}}]})
≡ GC(\overline{M[z_{1} ← r_{1}^{σ_{1}}][z_{2} ← r_{2}^{σ_{2}}]}) Following the argument in Case 1.
≡ GC(\overline{\overline{M[z_{1} ← r_{1}^{σ_{1}}]}[z_{2} ← r_{2}^{σ′_{2}}]})
≡ GC(GC(\overline{M[z_{1} ← r_{1}^{σ_{1}}]}))  Since z_{2} is not reachable in \overline{M[z_{1} ← r_{1}^{σ_{1}}]}.
≡ GC(\overline{M[z_{1} ← r_{1}^{σ_{1}}]})
≡ M_{1}

3: ρ_{2} \ ρ_{1} = (τ_{2}, z_{2}, σ′_{2}) and ρ_{1} \ ρ_{2} does not exists. The same as Case 2. 4: Both ρ_{2} \ ρ_{1} and ρ_{1} \ ρ_{2} do not exist. If ρ_{1} \ ρ_{2} does not exist then there must be a path from z_{2} to z_{1} in M. Analogously, if ρ_{2} \ ρ_{1} does not exist then there must be a path from z_{1} to z_{2} in M. Therefore, it must be the case that there exists a cycle involving z_{1} and z_{2}. Without loss of generality, let us assume there exists a path from the root of M to z_{1} without visiting z_{2}. This implies that independently of the reduction of ρ_{2}, z_{1} ∈ BV(M_{2}), that is, ρ_{1} \ ρ_{2} exists in M_{2}. We reach a contradiction, therefore, this case cannot arise.

□

Corollary 4.9. A GRSNI is confluent up to α-equivalence.

Consider the following projection rules:

\begin{matrix}τ_{1} : x = I(y) & − ; − ; → & x = y \\ τ_{2} : x = J(y) & − ; − ; → & x = y \end{matrix}

and the following term M:

\{ \begin{matrix}x = I(y); \\ y = J(x); \\ In x\} \end{matrix}

then M will have the following reduction:

M
[figure]
M_{1} ≡ {x = I(x); In x}  M_{2} ≡ {x = J(x); In x}
[figure]
⊙

Notice that if both M_{1} and M_{2} are not reduced to ⊙, the confluence property will be lost, as was observed in [15]. Barendregt’s graph reduction system is not confluent precisely because of the absence of such a reduction.

Hereafter, we will use the notation GRSC to denote a confluent GRS.

5. A Graph Model for GRS

We are interested in defining an equality on the set of terms, such that the equality is useful in analyzing the correctness of compiler optimizations. If we want equal terms to be freely substitutable for each other, then the equality must be preserved by terms formed by putting equal terms in the same context, which is defined as follows :

Definition 5.1. (Context) A context is a GRS term obtained by extending the syntactic category E of Definition 3.1 with the special symbol □.

Notation: We write C[□] for an arbitrary context, such as {x_{1} = e_{1}; ⋯ x_{n} = e_{n}; z = □; In x}, and C[M] for the term {x_{1} = e_{1}; ⋯ x_{n} = e_{n}; z = □; In x}[z ← M] ≡ {x_{1} = e_{1}; ⋯ x_{n} = e_{n}; z = M; In x}. As in any replacement operation BV(M) ∩ BV(C[□]) = ∅, for C[M] to be a legal term. Observe that the free variables of a term M can get bound in C[M].

Thus, for a compiler, a useful equality must have the property M = N ⟹ ∀C[□], C[M] = C[N]. This means that the equality has to be a congruence with respect to the formation rules of terms. An optimization will be considered correct if it preserves equality.

An example of an equivalence relation is convertibility. If two terms M_{1} and M_{2} are convertible and the GRS is confluent, then it follows that there will not be any context that can distinguish between them. Thus, convertibility is a congruence. Therefore, independent of the meaning or observations we associate to a term, a minimal requirement that will have to be satisfied is that all terms in the set {M′ | M − ; → ; → M′} have the same meaning. It follows that all optimization rules drawn from the set of rewriting rules will be automatically meaning preserving. However, as pointed out in [20], convertibility makes too fine a distinction to be interesting; it does not capture the computational behavior of a term. For example, consider the following two rules:

τ_{1} : x = F(y) − ; − ; → x = F(y)  τ_{2} : x = G(y) − ; − ; → x = {t = G(t_{1}); t_{1} = G(y); In t}

and the terms:

M ≡ {y = F(z); In y}  N ≡ {y = G(z); In y}

M is not convertible to N or viceversa. Yet from a computational point of view, we would like to consider them as producing no information. We may be tempted to extend convertibility by equating all terms without normal form. However, it has been shown by Wadsworth in [20] that this will lead to an inconsistent theory. For example, if terms M and N do not have normal forms, then both the following terms in SK-combinatory logic:

M_{1} ≡ \{ \begin{matrix}t = Ap(x, K); \\ t_{1} = M; \\ t_{2} = Ap(t, t_{1}); \\ In t_{2}\} \end{matrix}  N_{1} ≡ \{ \begin{matrix}t = Ap(x, S); \\ t_{1} = N; \\ t_{2} = Ap(t, t_{1}); \\ In t_{2}\} \end{matrix}

will not have normal forms either, and thus, will be equated. However, by plugging both of them in the context {x = K; z = □; In z} we can derive K = S. As shown in [6], this will immediately lead to an inconsistent theory, and will cause all terms to be equated.

The notion of head normal form (hnf) was introduced by Wadsworth to syntactically characterize the class of terms that cannot be equated. Intuitively, a term does not have a head normal form if no information can be extracted by reducing that term in any context, that is, the term is totally undefined. For example, the two terms M and N, introduced earlier, are totally undefined, while the above terms M_{1} and N_{1} have some information contained in them. For example, we know that whichever term M_{1} reduces to will have a stable prefix of the form: { t = Ap(x, K); t_{1} = □; t_{2} = Ap(t, t_{1}); In t_{2}}. Similarly for N_{1}, {t = Ap(x, S); t_{1} = □; t_{2} = Ap(t, t_{1}); In t_{2}} constitutes a stable prefix. Informally the hnf of a term embodies its maximum stable prefix. Since the hnf’s of M_{1} and N_{1} are different they cannot be equated. Furthermore, if two terms M and N do not contain any information, i.e., do not have hnf’s, it intuitively implies that the terms C[M] and C[N] will exhibit the same behavior and thus, can be equated. In this manner, we have performed a further classification of the terms without normal forms into ones that contain some information and those which contain no-information. It is therefore legitimate to ask which terms in head normal forms can be equated. Convertibility may still be too restrictive, as shown by the following example, where Cons is the usual list contructor:

M ≡ \{ \begin{matrix}x = Cons(y, z); \\ y = F(0); \\ z = Cons(w, Nil); \\ w = F(0); \\ In x\} \end{matrix}  N ≡ \{ \begin{matrix}x = Cons(y, z); \\ y = F(0); \\ z = Cons(y, Nil); \\ In x\} \end{matrix}

Graphs for M and N may be drawn as follows:

M and N are in normal form but clearly not inter-convertible. However, if internal representation of lists is ignored by an observer then both the terms represent the same unfolded list, F(0) : F(0) : Nil. If the GRS containing these terms has a non left-linear rule, it may be possible to distinguish between such terms. Thus, such terms cannot be equated without disallowing non left-linear rules.

We should also notice that M ≤_{ω} N, i.e., M has “less sharing” than N in the above example. Does it mean that M is “less defined” than N in the sense that one can compute less with M than with N?. We would like to answer the above question without delving into heavy duty model theory. We have carefully said “compute” to emphasize that we are interested in studying what a term represents from an operational point of view. In particular, we are interested in observing the gradual syntactic building up of the final term.

We introduce a function ω to compute the stable part of a term, that is, the part of the term that will not change as more reductions are performed on it. The ω function captures what Lévy has called the direct approximation of a λ-calculus term [18], and Welch has called the instantaneous semantics of a term [21]. Take the following term:

P ≡ \{ \begin{matrix}t = Ap(Y, f); \\ In t\} \end{matrix}

where the rule for the Y combinator is expressed as:

x = Ap(Y, f) − ; − ; → x = {t = Ap(f, t_{1}); t_{1} = Ap(Y, f); In t}.

Since Ap(Y, f) occurring in P is a redex, we cannot predict what Ap(Y, f) will produce without reducing it. Thus, without any prior knowledge of the reduction, we will have to assert that no information is associated to P, otherwise, a wrong assumption may lead to a situation where we have to retract what was printed earlier. Thus, we will say that ω(P) = Ω, where Ω stands for no information. Let’s perform one-step reduction on P to obtain the term:

P_{1} ≡ \{ \begin{matrix}t = Ap(f, t_{1}); \\ t_{1} = Ap(Y, f); \\ In t\} \end{matrix}

At this point notice that all further reductions of P_{1} will produce terms with context: {t = Ap(f, □); In t}. Thus, we can safely say that ω(P_{1}) is:

Ap

[figure]
f  Ω

In general, we will have:

Ω [figure: Ap; f  Ω] [figure: Ap; f  Ap; f  Ω] ⋯

Notice that as more reductions are performed the stable part should get larger, that is, ω(P) ≤_{ω} ω(P_{1}) ≤_{ω} ω(P_{2}) · · ·. We remind the reader that ≤_{ω} is the syntactic ordering on terms which captures both the sharing and the fact that Ω is less than any other term. Assuming that this chain has a limit, then, even though the term P does not have a normal form, it may still have a precise meaning.

We collect all the (stable) information gathered by reducing P in a set, called W^{∗}(P), and say that it represents the information content of P. We can now formulate our original question regarding the impact of sharing on a program’s behavior as follows: if M has less sharing than N then is W^{∗}(M) contained in W^{∗}(N)? As we shall see shortly, this is indeed the case in the absence of interfering rules.

It is also interesting to analyze if M “less defined” then N implies that for all context C[□], C[M] is “less defined” than C[N]? That is, is the equality induced by W^{∗} a congruence? Later we will see that, in the absence of interfering rules, the equality introduced by information content is also a congruence. Thus, the collection of stable information contained in GRS terms does indeed turn out to be a model for GRS without interfering rules.

We will need the following definition shortly.

Definition 5.2. (Initial Ω-form of a term, M_{Ω}) Given a GRS term M in canonical form, M_{Ω} is the term GC(M[ℜ(M) ← Ω]).

5.1. Instant semantics

The instant semantics of a GRS term M is obtained by computing its stable part, where stable part means the part of M which will not change by further reductions. A solution that comes to mind is to replace each redex in a term by an Ω, that is, to treat M_{Ω} as stable. Intuitively, this seems right because a redex can become any expression, and Ω is less than all expressions. Furthermore, it seems that if M → N then M_{Ω} ≤_{ω} N_{Ω}. Unfortunately, this solution has a problem, as shown by the following example. Consider the rules:

τ_{1} : x = F(y, y) − ; − ; → x = 4 τ_{2} : x = I(y) − ; − ; → x = y

and the following reduction:

M ≡ \{ \begin{matrix}t = F(t_{1}, t_{2}); \\ t_{1} = A(0); \\ t_{2} = I(t_{1}); \\ In t\} \end{matrix} − ; − ; →_{t_{2}}^{τ_{2}} M_{1} ≡ \{ \begin{matrix}t = F(t_{1}, t_{1}); \\ t_{1} = A(0); \\ In t\} \end{matrix}

The only redex in M is rooted at t_{2}, and thus, its stable part is the following term M_{2}:

F

[figure]
A  Ω

↓ 0

However, since M_{1} is a redex, M_{1} does not contain any stable information. Thus, the information contained in M_{1} is less than the information contained in M. This is contrary to our intuition that the information should not decrease with reduction. The problem is due to the presence of rule τ_{2} which can introduce sharing. If we want to compute the instant semantics of a term without analyzing the rhs of rules then we have to assume that the arc pointing to Ω in M_{2} can be redirected to point to the node of label A, and thus making M_{2} a τ_{1}-redex. In other words, we should not treat M_{2} as being in stable form. However, M_{Ω} does give the stable part of a term M in a Recursive Program Schema (RPS)!

5.1.1. Stable information in RPS and TRS

We remind the reader that a Recursive Program Schema (RPS) is a TRS which has a finite set of function symbols {F_{1}, ⋯, F_{n}} (the “unknown” or user-defined functions) where F_{i} has arity m_{i}, and a disjoint set of basic function symbols {G_{1}, ⋯, G_{m}} (the “known” functions), where G_{j} has arity l_{j}. The rewrite rules of a RPS have the form F_{i}^{m_{i}}(x_{1}, ⋯, x_{m_{i}}) − ; − ; → t_{i}, 1 ≤ i ≤ n, where all variables x_{i}, 1 ≤ i ≤ m_{i}, are pairwise distinct and t_{i} is an arbitrary term built from variables and functions, F_{i}, ⋯, G_{j}, · · ·. Furthermore, for each F_{i} there is exactly one rule.

Lemma 5.3. For any RPS term M, M_{Ω} is the stable prefix of M.

Proof. If M_{Ω} = Ω then M_{Ω} is obviously stable. If M_{Ω} ≠ Ω then ∀N such that M_{Ω} ≤_{ω} N, N cannot be a redex at the root, in other words, M_{Ω} is stable. □

However, M_{Ω} is not necessarily the stable prefix for a TRS term M†. Consider the following rules:

\begin{matrix}τ_{1} : A(x) & − ; − ; → & B(x) \\ τ_{2} : F(B(x)) & − ; − ; → & 0 \end{matrix}

and the reduction:

M ≡ F(A(x)) − ; − ; → N ≡ F(B(x))

M_{Ω} is F(Ω), while N_{Ω} is Ω, and M_{Ω} ≰_{ω} N_{Ω}. Thus, we erroneously assumed that F(Ω) is a stable prefix. A TRS differs from an RPS in that even though the TRS term F (Ω) is not a redex it can become one by increasing its information, for example, by substituting B(x) for Ω. This phenomena is called the upward creation of redexes. Reduction of a term in the λ-calculus can also result in the upward creation of redexes. To cope with this problem in the λ-calculus, Wadsworth[20] and Lévy[18] had introduced the notion of an ω-rule, which reduces any term that can become a redex (by upward creation) to Ω. The ω-rule for the λ-calculus is:

Ω M − ; − ; → Ω.

The ω-rule associated to τ_{1} and τ_{2} will be F(Ω) − ; − ; → Ω. However, in the presence of non left-linear rules it is difficult to generate ω-rules for a TRS as shown by the following example. We remind the reader that non left-linearity in a TRS is interpreted as tree equivalence on terms. Now consider the TRS rule F(y, y) − ; − ; → y. Suppose we generate the following ω-rules:

\begin{matrix}F(Ω, y) − ; − ; → Ω \\ F(y, Ω) − ; − ; → Ω \end{matrix}

then the term M ≡ F(A(0), A(Ω)) will be in stable form. However, it should not be because by replacing Ω by 0, M becomes a redex.

5.1.2. ω-redex

Non left-linear rules constitute a problem for a GRS also. Since we want to include them in our analysis, we abandon the idea of generating ω-rules, and instead introduce a new notion of redex, called ω-redex [11]. A ω-redex captures our intuition about why a term should be rewritten to Ω. It consists of analyzing a term to see if it can become a redex by either replacing Ω with some other term or by increasing the sharing in the term. The stable part of a term M will be computed by first replacing all redexes in M by Ω, and then by reducing all ω-redexes to Ω .

Notice that we have taken a conservative approach in determining which terms can become redexes; we may reduce to Ω some terms, which may never become a redex. However, we also need to guarantee that not too much information is lost. Since the stable part will be a part of our criteria for equating terms, we may end up equating far too many terms and lose congruence. Clearly if we reduce everything to Ω, all terms will get equated and we will immediately have an inconsistent model. As we will see in Section 5.5, a way of

† Private communication with Jean-Jacques Lévy.

guaranteeing that not too much information is lost is by showing that the behavior of a term C[M] can be inferred from the observations about M. Consider the rules:

\begin{matrix}τ_{1} : x = F(y, y) − ; − ; → x = 4 \\ τ_{2} : \frac{x_{1} = F(0, 1)}{x = G(x_{1}) − ; − ; → x = 3} \end{matrix}

and terms M ≡ F(0, 1) and N ≡ F(2, 1). Suppose we compute the stable information of term M by applying the (incorrect) rule: x = F(y_{1}, y_{2}) − ; − ; → x = Ω. Then both ω(M) and ω(N) will be Ω and as such they will be equated. Now consider the context C[□] ≡ {t_{1} = G(t_{2}); t_{2} = □; In t_{1}}. C[M] produces 3 as a possible observation, while C[N] does not. Thus, we erroneously equate terms which are not “extensionally equal”. It seems that we cannot discard any information that can be used to build terms. By treating ω(M) as Ω we discard too much information as can be seen by the fact that by plugging the observations of M in C[□] we will not be able to observe 3.

5.2. ω-reductions and its properties

Definition 5.4. (ω-redex) A ω-redex in a GRS term M in canonical form is a pair (τ, z) such that:

(i) τ is a rule; (ii) z ∈ BV(M) and z is not bound to Ω; (iii) Cl(τ) ↑_{ω} M@z and Cl(τ) ≰_{ω} M@z. z is called the root of the ω-redex. If z is also the root of the term M then M is said to be a ω-redex. The set containing the roots of all ω-redexes is denoted by ℜ_{ω}(M).

Notice that because of condition (iii), a ω-redex cannot be an ordinary redex. For the example given at the beginning of Section 5.1, we have that Cl(τ_{1}) ≰_{ω} M_{2} and Cl(τ_{1}) ↑_{ω} M_{2}, thus, M_{2} is a ω-redex, and will be reduced to Ω in computing the stable part of M_{2}.

Definition 5.5. (Distinct ω-redexes) Two ω-redexes ρ_{1} = (τ_{1}, z_{1}) and ρ_{2} = (τ_{2}, z_{2}) in a GRS term M in canonical form are said to be distinct if either τ_{1} ≠ τ_{2} or z_{1} ≠ z_{2}.

Proposition 5.6. Given GRS terms M_{1} and M_{2} in canonical form, if M_{1} ≤_{ω} M_{2} then

(i) if M_{2} is a ω-redex then M_{1} is either a ω-redex or Ω; (ii) if M_{2} is a redex then M_{1} is either a redex, a ω-redex or Ω.

Proof. (i) From the definition of ω-redex we have that ∃ τ such that M_{2} ↑_{ω} Cl(τ). Therefore, if M_{1} is not Ω it must be a ω-redex. Analogously for point (ii). □

Definition 5.7. (ω-reduction) Given a GRS term M in canonical form, M ω-reduces to N by doing the τ ω-redex at z, written as M − ; − ; →_{z}^{τ}_{ω} N, iff (τ, z) is a ω-redex in M and N ≡ GC(M[z ← Ω]). A term is said to be in ω-normal form when it has no ω-redexes.

Note that since Ω is not a substitutable value, M[z ← Ω] is in canonical form.

In the following, we analyze the effect of ω-reductions and normal reductions on ω-redexes and redexes, respectively. It turns out that an ω-reduction cannot destroy an ω-redex, even in the presence of interfering rules, and an ω-reduction cannot destroy a redex in the absence of interfering rules. However, a reduction can destroy an ω-redex even in the absence of interfering rules.

Definition 5.8. (Descendant of a ω-redex with respect to ω-reduction) Given two distinct ωredexes ρ_{1} = (τ_{1}, z_{1}) and ρ_{2} = (τ_{2}, z_{2}) in a GRS term M in canonical form, the descendant of ρ_{2} with respect to the reduction M − ; − ; →_{ρ_{1}}_{ω} M_{1} (written as ρ_{2} \ ρ_{1}):

(i) does not exist, if z_{2} ∉ BV(M_{1}); (ii) is the pair ρ′_{2} = (τ_{2}, z_{2}), if z_{2} ∈ BV(M_{1}).

Proposition 5.9. Given ω-redexes ρ_{1} = (τ_{1}, z_{1}) and ρ_{2} = (τ_{2}, z_{2}) in a GRS term M in canonical form, if M − ; − ; →_{ρ_{1}}_{ω} M_{1} and z_{2} ∈ BV(M_{1}) then either ρ_{2} \ ρ_{1} is an ω-redex or z_{2} is bound to Ω in M_{1}.

Proof. Since M_{1} ≡ GC(M[z_{1} ← Ω]), M_{1} ≤_{ω} M. Therefore, if z_{2} ∈ BV(M_{1}) then M_{1}@z_{2} ≤_{ω} M@z_{2}. Therefore, by Proposition 5.6, ρ_{2} \ ρ_{1} is either a ω-redex or Ω. □

Definition 5.10. (Descendant of a redex with respect to ω-reduction) Given an ω-redex ρ_{1} = (τ_{1}, z_{1}) and a redex ρ_{2} = (τ_{2}, z_{2}, σ_{2}) in a GRS term M in canonical form, the descendant of ρ_{2} with respect to the reduction M − ; − ; →_{ρ_{1}}_{ω} M_{1} (written as ρ_{2} \ ρ_{1}):

(i) does not exist, if z_{2} ∉ BV(M_{1}); (ii) is the triple ρ′_{2} = (τ_{2}, z_{2}, σ′_{2}), if z_{2} ∈ BV(M_{1}), and σ′_{2} is:

σ′_{2}(x) = \{ \begin{matrix}σ_{2}(x) & σ_{2}(x) ≠ z_{1} \\ Ω & σ_{2}(x) = z_{1} \end{matrix}

Proposition 5.11. Given an ω-redex ρ_{1} = (τ_{1}, z_{1}) and a redex ρ_{2} = (τ_{2}, z_{2}, σ_{2}) in a GRSNI term M in canonical form, if M − ; − ; →_{ρ_{1}}_{ω} M_{1} and z_{2} ∈ BV(M_{1}) then ρ_{2} \ ρ_{1} is a redex.

Proof. If z_{2} ∈ BV(M_{1}) then by Definition 5.10, ρ_{2}\ρ_{1} = (τ_{2}, z_{2}, σ′_{2}). By non-interference, if ∃x, σ_{2}(x) ≠ σ′_{2}(x) it must be the case that x ∉ BV(P(τ_{2})). Moreover, suppose ∃x ∈ BV(P(τ_{2})), σ′_{2}(x) does not occur in M_{1}, it means that all paths from z_{2} to σ′_{2}(x) go through z_{1}. Since z_{1} ∉ BV(P(τ_{2})), x ∉ BV(P(τ_{2})). We reached a contradiction, therefore, ∀x ∈ BV(P(τ_{2})), σ′_{2}(x) occurs in M_{1}. Since the new definition of z_{1} and the garbage collection do not affect the substitution σ′_{2}, ρ_{2} \ ρ_{1} is a redex. □

Definition 5.12. (Descendant of an ω-redex with respect to reduction) Given a redex ρ_{1} and an ω-redex ρ_{2} = (τ_{2}, z_{2}) in a GRS term M in canonical form, the descendant of ρ_{2} with respect to the reduction M − ; − ; →_{ρ_{1}} M_{1} (written as ρ_{2} \ ρ_{1}):

(i) does not exist, if z_{2} ∉ BV(M_{1}); (ii) is the pair ρ′_{2} = (τ_{2}, z_{2}), if z_{2} ∈ BV(M_{1}).

Proposition 5.13. Given a redex ρ_{1} = (τ_{1}, z_{1}, σ_{1}) and an ω-redex ρ = (τ, z) in a GRSNI term M in canonical form, if M − ; − ; →_{ρ_{1}} M_{1} and z ∈ BV(M_{1}) then ρ \ ρ_{1} is either an ω-redex or it can become so after having perfomed some additional reductions on M_{1}. In other words, ∃M_{n}, M_{1} − ; − ; →_{ρ_{2}} M_{2} − ; − ; →_{ρ_{3}} M_{3} ⋯ − ; − ; →_{ρ_{n}} M_{n}, and ρ \ (ρ_{1} ∪ ρ_{2} ⋯ ρ_{n}) is an ω-redex.

Proof. Since ρ is an ω-redex, ∃N, M ≤_{ω} N such that σ_{MN}(z) is the root of a τ-redex in N, where σ_{MN} is the induced substitution function. Let z′_{1} = σ_{MN}(z_{1}) be the root of the redex (τ_{1}, z_{1}, σ′_{1}), and let N_{1} be such that N − ; − ; →_{z′_{1}} N_{1}. Let Z = {z′ | z′ ∈ BV(M), σ_{MN}(z′) = z′_{1}, z′ ≢ z_{1}}. By Proposition 3.25 we have:

GC(M_{1}[Z ← Ω]) ≤_{ω} GC(\overline{N[z′_{1} ← r^{σ′_{1}}]}) ≡ N_{1}

Moreover, by Proposition 4.7 the descendant of the redex rooted at σ_{MN}(z) in N must be a redex in N_{1}. Therefore, by Proposition 5.6 we have that ρ \ ρ_{1} must be either a redex, an ω-redex or Ω in GC(M_{1}[z ← Ω]). By non-interference it follows that the only condition applicable is for ρ \ ρ_{1} to be an ω-redex. □

Proposition 5.14. Given an ω-redex ρ_{1} and a redex ρ_{2} in a GRSNI term M in canonical form, if M − ; − ; →_{ρ_{1}}

ω M_{1} and M − ; − ; →_{ρ_{2}} N, then ∃N′, P, N − ; → ; → N′, N′ − ; − ; →^{0/1}_{ω} P and M − ; − ; →^{0/1} P.

Proof. By cases on the existence of the descendant of ρ_{1} and ρ_{2}.

1: ρ_{1} \ ρ_{2} = (τ_{1}, z_{1}) and ρ_{2} \ ρ_{1} = (τ_{2}, z_{2}, σ_{2}). If ρ_{2} \ ρ_{1} exists by Proposition 5.11 it must be a redex. Therefore we will only consider the following cases:

1.1: ρ_{1} \ ρ_{2} is an ω-redex and ρ_{2} \ ρ_{1} is a redex Similar argument as in Theorem 4.8.

1.2: ρ_{1} \ ρ_{2} is not an ω-redex and ρ_{2} \ ρ_{1} is a redex.

Follows from Proposition 5.13. 2: ρ_{1} \ ρ_{2} does not exist and ρ_{2} \ ρ_{1} = (τ_{2}, z_{2}, σ_{2}). Follows from Proposition 5.11.

3: ρ_{1} \ ρ_{2} = (τ_{1}, z_{1}) and ρ_{2} \ ρ_{1} do not exist. Follows from Proposition 5.13.
4: ρ_{1} \ ρ_{2} and ρ_{2} \ ρ_{1} do not exist. As in Theorem 4.8 this case cannot arise.

□

Proposition 5.15. Given a GRSNI term M in canonical form, if M − ; → ; → _{ω} M_{1} and M − ; → ; → N, then

∃N′, P, N − ; → ; → N′, N′ − ; → ; →_{ω} P and M − ; → ; → P.

Proof. By induction on the lenght of the reductions M − ; → ; →_{ω} M_{1} and M − ; → ; → N. □

The stable part of a term M, i.e., ω(M), will then be computed by first replacing all distinct redexes occurring in M by Ω and then computing the ω-normal form of the term so obtained. Before giving the formal definition of the ω-function we introduce some properties of ω-redexes and ω-reduction.

Theorem 5.16. (Subcommutativity of − ; → ; →_{ω}) Given two distinct ω-redexes ρ_{1} and ρ_{2} in a GRS term

M in canonical form, if M − ; − ; →_{ρ_{1}}_{ω} M_{1} and M − ; − ; →_{ρ_{2}}_{ω} M_{2}, then ∃ M_{3} such that M_{2} − ; − ; →_{ρ_{1}\ρ_{2}}^{0/1}_{ω} M_{3} and M_{1} − ; − ; →_{ρ_{2}\ρ_{1}}^{0/1}_{ω} M_{3}.

Proof. Let ρ_{1} = (τ_{1}, z_{1}), ρ_{2} = (τ_{2}, z_{2}), and M_{1} ≡ GC(M[z_{1} ← Ω]), M_{2} ≡ GC(M[z_{2} ← Ω]). If z_{1} ≡ z_{2} then M_{1} ≡ M_{2} ≡ M_{3}. If z_{1} ≢ z_{2} then the proof, analogous to Theorem 4.8, is by cases on the existence of ρ_{1} \ ρ_{2} and ρ_{2} \ ρ_{1}. We show the first two cases only.

1: ρ_{2} \ ρ_{1} = (τ_{2}, z_{2}) and ρ_{1} \ ρ_{2} = (τ_{1}, z_{1}).

By Proposition 5.9 ρ_{1} \ ρ_{2} and ρ_{2} \ ρ_{1} must be ω-redexes. Thus, we want to show the following:

GC(M_{1}[z_{2} ← Ω]) ≡ GC(M_{2}[z_{1} ← Ω]).

We have:

GC(M_{1}[z_{2} ← Ω])
≡ GC(GC(M[z_{1} ← Ω])[z_{2} ← Ω]) By Proposition 3.24
≡ GC(M[z_{1} ← Ω][z_{2} ← Ω])  By Proposition 3.23
≡ GC(M[z_{2} ← Ω][z_{1} ← Ω])  By Proposition 3.24
≡ GC(GC(M[z_{2} ← Ω])[z_{1} ← Ω])
≡ GC(M_{2}[z_{1} ← Ω])

2: ρ_{1} \ ρ_{2} = (τ_{1}, z_{1}) and ρ_{2} \ ρ_{1} does not exists.

We need to show:

M_{1} ≡ GC(M_{2}[z_{1} ← Ω])

We have:

GC(M_{2}[z_{1} ← Ω])
≡ GC(GC(M[z_{2} ← Ω])[z_{1} ← Ω])
≡ GC(GC(M[z_{1} ← Ω])[z_{2} ← Ω]) Following argument in Case 1.
≡ GC(M[z_{1} ← Ω])  Since z_{2} ∉ M_{1} and GC is idempotent
≡ M_{1}

□

Corollary 5.17. − ; → ; →_{ω} is confluent.

Proposition 5.18. − ; → ; →_{ω} is strongly normalizing.

Proof. Suppose there are n function symbols in a term M. Each ω-reduction gets rid off one function symbol and does not introduce any new ones. Thus, the lenght of ω-reduction on M is bounded by n. □

Since ω-reductions are strongly normalizing and confluent we can now define the ω-function as follows:

Definition 5.19. (ω-function) Given a GRS term M, ω(M) is the ω-normal form of M_{Ω}.

We now discuss two additional properties of the ω-function, that are, its monotonicity with respect to ≤_{ω}, and with respect to reduction. These will be very useful in later proofs.

Proposition 5.20. (Monotonicity of ω-function with respect to ≤_{ω}) Given GRS terms M and N in canonical form, if M ≤_{ω} N then ω(M) ≤_{ω} ω(N).

Proof. Let σ_{MN} be the substitution function from M to N induced by M ≤_{ω} N.

Let Z = {z | z ∈ BV(M), z is not bound to Ω, σ_{MN}(z) ∈ ℜ(N)}, and Z′ = {z | z ∈ BV(M), z is not bound to Ω, σ_{MN}(z) ∈ ℜ_{ω}(N)}. From Proposition 3.25 we have:

GC(M[Z ← Ω][Z′ ← Ω]) ≤_{ω} ω(N_{Ω}) = ω(N).

By Proposition 5.6 we have (Z ∪ Z′) ⊆ (ℜ(M) ∪ ℜ_{ω}(M)). Therefore, by Proposition 5.9 we have:

ω(M) ≤_{ω} GC(M[Z ← Ω][Z′ ← Ω]) ≤_{ω} ω(N).

□

Proposition 5.21. (Monotonicity of ω-function with respect to reduction) Given GRS terms M and N in canonical form, if M − ; → ; → N then ω(M) ≤_{ω} ω(N).

Proof. The proof is by induction on the number of reduction steps. Suppose M − ; − ; →_{ρ} N, where ρ = (τ, z, σ), then N ≡ GC(\overline{M[z ← P]}), for some term P. Since ω(M) = ω(GC(M[z ← Ω])) and GC(M[z ← Ω]) ≤_{ω} GC(\overline{M[z ← P]}), then from the monotonicity of the ω-function with respect to ≤_{ω} (Proposition 5.20) we have that ω(M) ≤_{ω} ω(N). The result then follows by induction. □

5.3. Meaning of a GRS term

We collect all observable information about GRS terms in a set called ω-graphs.

Definition 5.22. (ω-graphs: Set of observations) Given a GRS, the set of all observations, called ω-graphs, is defined as:

ω-graphs = ⋃{ω(M) | ∀ GRS terms M}.

We would like to define the meaning of a term M as the limit of the set of our observations, that is, {ω(M′) | M − ; → ; → M′}. However, ω-graphs does not guarantee the existence of such a limit. Therefore, we apply the ideal completion method to turn ω-graphs into a complete partial order [10]. Given a partial order (A, ≤), a subset D of A is an ideal iff (i) D is non-empty. (ii) ∀a, b ∈ D, ∃c ∈ D, a ≤ c and b ≤ c, (iii) ∀c ∈ D, if ∃d ∈ A, d ≤ c then d ∈ D.

Definition 5.23. (ω-graphs^{∞}: Domain of observations) Given a GRS, the domain of observations, called ω-graphs^{∞}, is the ideal completion of ω-graphs, that is:

ω-graphs^{∞} = {I | I ⊆ ω-graphs and I is an ideal }.

To reflect this change in our domain of observations, we include all ω-graph terms smaller than ω(M) in our observations as follows:

Definition 5.24. (W^{∗}: The information content of a GRS term) Given a GRS term M in canon-

ical form, W^{∗}(M) = {a | a ∈ ω-graphs, a ≤_{ω} ω(M′), M − ; → ; → M′}.

We need to define under what conditions W^{∗}(M) is an element of ω-graphs^{∞}, that is, W^{∗}(M) is an ideal.

Proposition 5.25. (W^{∗}(M) is an ideal for GRSC) For all GRSC terms M, W^{∗}(M) is in ω-graphs^{∞}.

Proof.

(i) W^{∗}(M) is not empty since it contains at least Ω; (ii) We show that W^{∗}(M) is a directed set, that is, ∀a, b ∈ W^{∗}(M), ∃c, such that a ≤_{ω} c and b ≤_{ω} c. If

a ∈ W^{∗}(M), it means that ∃M_{1}, such that M − ; → ; → M_{1} and a ≤_{ω} ω(M_{1}). Analogously, ∃M_{2}, M − ; → ; → M_{2} and b ≤_{ω} ω(M_{2}). Follows from the confluence of − ; → ; → that ∃M_{3}, M_{1} − ; → ; → M_{3} and M_{2} − ; → ; → M_{3}. Moreover, from the monotonicity of the ω-function with respect to − ; → ; → (Proposition 5.21) we have:

a ≤_{ω} ω(M_{3}) and b ≤_{ω} ω(M_{3})

that is, ω(M_{3}) is the element we were looking for. (iii) W^{∗}(M) is closed downwards by definition.

□

Let’s now define a semantic ordering based on the information content.

Definition 5.26. (⊑g: Information ordering) Given GRS terms M and N in canonical form, M ⊑g N iff W^{∗}(M) ⊆ W^{∗}(N).

If we want W^{∗} to be our interpretation function, W^{∗} will have to satisfy some properties, that is, the meaning will have to be preserved by reduction, and it will have to be compositional. In other words:

Soundness : M − ; → ; → N ⟹ M ≡g N
Congruence : M ≡g N ⟹ C[M] ≡g C[N]

We will first show the soundness, and then later come back to a discussion of congruence after a digression on the impact of sharing on the meaning function.

Proposition 5.27. (Soundness of ≡g) Given GRSC terms M and N in canonical form, if M − ; → ; → N then M ≡g N.

Proof. Trivially, N ⊑g M. Next, we prove that M ⊑g N. Let P ∈ W^{∗}(M), it means that ∃M_{1}, M − ; → ; → M_{1} and P ≤_{ω} ω(M_{1}). From the confluence of − ; → ; → we know that ∃M_{2}, M_{1} − ; → ; → M_{2} and N − ; → ; → M_{2}. From the monotonicity of the ω-function with respect to reduction (Proposition 5.21), we have that P ≤_{ω} ω(M_{1}) ≤_{ω} ω(M_{2}). Since ω(M_{2}) ∈ W^{∗}(N), then P ∈ W^{∗}(N) as well. □

5.4. Impact of sharing on program behavior

What is the impact of sharing on program behavior, that is,

M ≤_{ω} N ⟹ M ⊑g N ?

It turns out that in the presence of interfering rules the above will not hold. Consider the following GRS which has confluent but interfering rules:

τ_{1} : \frac{x_{1} = B(0) | x_{2} = C(0)}{x = A(x_{1}, x_{2}) − ; − ; → x = 0}

τ_{2} : x = C(0) − ; − ; → x = B(0)

τ_{3} : x = B(0) − ; − ; → x = C(0)

and the following terms:

M ≡ \{ \begin{matrix}t_{1} = A(t_{2}, t_{3}); \\ t_{2} = B(0); \\ t_{3} = B(0); \\ In t_{1}\} \end{matrix}  N ≡ \{ \begin{matrix}t_{1} = A(t_{2}, t_{2}); \\ t_{2} = B(0); \\ In t_{1}\} \end{matrix}

then, it is easy to see that W^{∗}(M) = {Ω, 0}, while W^{∗}(N) = {Ω, {x_{1} = Ω; x_{2} = A(x_{1}, x_{1}); In x_{2}}}. Therefore, M ≤_{ω} N and M ⋢g N. However, there is no such problem for a GRS without interfering rules.

Theorem 5.28. (Monotonicity of ⊑g with respect to ≤_{ω}) Given GRSNI terms M and N in canonical form, if M ≤_{ω} N then M ⊑g N.

Proof. We prove that if M − ; → ; → M′, then ∃N′ such that N − ; → ; → N′ and ω(M′) ≤_{ω} ω(N′). The proof is by induction on the number of reduction steps of M − ; → ; → M′.

Let M − ; − ; →_{ρ} M_{1}, where ρ = (τ, z, σ). Let σ_{MN} be the substitution function from M to N induced by M ≤_{ω} N. Then ρ′ = (τ, z′, σ′), where z′ = σ_{MN}(z), and σ′ = σ_{MN} ∘ σ, is a redex in N. Let N − ; − ; →_{ρ′} N_{1}, and Z = {s | s ∈ BV(M), s not bound to Ω, σ_{MN}(s) = z′ and s ≢ z}. That is, Z is the set of all variables in M, distinct from z, which are mapped into z′. From Proposition 3.25 we have:

GC(GC(\overline{M[z ← r^{σ}]})[Z ← Ω]) ≤_{ω} GC(\overline{N[z′ ← r^{σ′}]}) ≡ N_{1}.

By Proposition 5.6 Z ⊆ {ℜ(M) ∪ ℜ_{ω}(M)} Therefore, since by Propositions 5.9 we have:

ω(M_{1}) = ω(GC(GC(\overline{M[z ← r^{σ}]})[Z ← Ω])).

Therefore, by monotonicity of the ω-function with respect to ≤_{ω} (Proposition 5.20) we have:

ω(M_{1}) ≤_{ω} ω(N_{1}).

Notice that any redex in M_{1}, that does not belong to Z, is a redex in GC(M_{1}[Z ← Ω]) (Proposition 4.7), and therefore it must be a redex in N_{1}. The result then follows by induction. □

This theorem leads to a simple but powerful result regarding the behavior of terms obtained by plugging terms, related by sharing, into any context.

Corollary 5.29. Given GRSNI terms M and N, if M ≤_{ω} N then ∀C[□], C[M] ⊑g C[N].

Proof. It follows from the fact that if M ≤_{ω} N then C[M] ≤_{ω} C[N]. □

It will be shown later this result can be applied in a straightforward manner to show the partial correctness of those compiler optimizations that simply increase the sharing in a term.

5.5. Congruence

Consider the rule:

τ : x = F(y) − ; − ; → x = {t = F(y); t_{1} = Cons(y, t); In t_{1}}

and the following two terms:

M ≡ {x = Cons(1, x); In x}  N ≡ {x = F(1); In x}

Notice that N ≰_{ω} M, but given the chain:

N − ; − ; → N_{1} − ; − ; → N_{2} − ; − ; → ⋯ − ; − ; → N_{i} − ; − ; → ⋯

where N_{i} ≡ {t_{0} = F(1); t_{1} = Cons(1, t_{0}); ⋯ t_{i} = Cons(1, t_{i−1}); In t_{i}}, we have that:

ω(N) ≤_{ω} ω(N_{1}) ≤_{ω} ⋯ ≤_{ω} ω(N_{i}) ≤_{ω} ⋯ ≤_{ω} M.

In fact, using induction on i we can show that N ⊑g M, and one would correctly guess that ∀C[□], C[M] ⊑g C[N]. However, this does not follow from Corollary 5.29. We need to show that ⊑g is a congruence relation. Note that terms like M and N arise in the cyclic implementation of recursive rules, such as the Y-rule.

A way of assuring that ⊑g is a congruence is to show that the behavior of C[M], for any context C[□], can be inferred from the observations about M, that is,

∀C[□], C[M] ≡g ⨆{C[P] | P ∈ W^{∗}(M)}.

In other words, the context should be a continuous operation with respect to our observations. (Notice that W^{∗}(⨆{C[P] | P ∈ W^{∗}(M)}) = ⋃{W^{∗}(C[P]) | P ∈ W^{∗}(M)}). We will first prove:

∀C[□], ⨆{C[P] | P ∈ W^{∗}(M)} ⊑g C[M]

that is, by plugging the observations of M in the context we do not produce more information than the one contained in C[M].

Lemma 5.30. Given a GRSNI term M and context C[□], ⨆{C[P] | P ∈ W^{∗}(M)} ⊑g C[M].

Proof. Suppose M − ; → ; → M′, then ∀P, P ≤_{ω} ω(M′) we have:

P  ≤_{ω} M′
C[P] ⊑g C[M′] by monotonicity of ⊑g with respect to ≤_{ω} (Corollary 5.29)
≡g C[M] by soundness of ≡g (Proposition 5.27).

□

The other direction:

∀C[□], C[M] ⊑g ⨆{C[P] | P ∈ W^{∗}(M)}

requires some more machinery. We want to show that each observation of C[M] can be obtained by first observing M and then plugging those observations instead of M in the context. The proof has two basic steps. First we show that each reduction sequence C[M] − ; → ; → N can be reordered, such that, if the sequence contains any redexes that are descendants of redexes in M then in the reordered sequence these redexes are performed before all others. Second, we show that the ω-function does not lose too much information. Since the ω-function involves two steps – first computing M_{Ω} and then applying ω-reductions – we will analyze the impact of these steps separately.

In the following, we will use the notation M {↗ → \atop Z(M)} N, where Z(M) ⊆ R(M), to mean that no descendant of redexes in Z(M) is reduced.

Proposition 5.31. Given a GRSNI term M in canonical form, if C[M] − ; → ; → N then ∃M′, M − ; → ; → M′ and C[M′] ^{{↗ → \atop M′}} N.

Proof. Let Z(M) be the set of redexes in M contracted during the reduction C[M] − ; → ; → N, that is, Z(M) = {z ∈ BV(M) | ∃i, C[M] − ; → ; → N_{i} − ; − ; →_{z} N_{i+1} − ; → ; → N}. Then by the subcommutative property of GRSNI (Theorem 4.8), ∃M′, C[M] − ; − ; →_{cd(Z(M))} C[M′] and C[M′] ^{{↗ → \atop M′}} N, where cd(Z(M)) denotes a complete development with respect to Z(M). □

Proposition 5.32. Given a GRSNI term M in canonical form, if M {↗ → \atop Z(M)} N then GC(M[Z(M) ← Ω]) − ; → ; → GC(N[Z(M) ← Ω]).

Proof. Follows from Proposition 4.7. □

Proposition 5.33. Given GRSNI terms M and N, if M − ; → ; →_{ω} N then M ≡g N.

Proof. Since N ≤_{ω} M, and by monotonicity of ⊑g with respect to ≤_{ω} (Theorem 5.28), we have that N ⊑g M. In order to prove the other direction, let M − ; → ; →_{ω} M_{1} and M − ; → ; → N. From Proposition 5.15 ∃N′, P, N − ; → ; → N′, N′ − ; → ; →_{ω}P and M_{1} − ; → ; → P. The result then follows from the fact that ω(N) ≤_{ω} ω(N′) = ω(P). □

Lemma 5.34. Given GRSNI terms M and N, and context C[□], if C[M] {↗ → \atop M} N then ω(N) ⊑g C[ω(M)].

Proof. By Proposition 5.32 we have:

C[GC(M[ℜ(M) ← Ω])] − ; → ; → GC(N[ℜ(M) ← Ω])

Moreover, by the soundness of reduction (Proposition 5.27):

C[GC(M[ℜ(M) ← Ω])] ≡g GC(N[ℜ(M) ← Ω])

Since ω(N) ≤_{ω} GC(N[ℜ(M) ← Ω]), from the monotonicity of ⊑g with respect to ≤_{ω} (Proposition 5.28), we

Properties of a First-order Functional Language with Sharing 33

have:

ω(N) ⊑g GC(N[ℜ(M) ← Ω]) ≡g C[GC(M[ℜ(M) ← Ω])]

Since C[GC(M[ℜ(M) ← Ω])] − ; → ; →_{ω} C[ω(M)], and by Proposition 5.33 ω-reductions preserve the meaning:

C[GC(M[ℜ(M) ← Ω])] ≡g C[ω(M)].

Therefore, ω(N) ⊑g GC(N[ℜ(M) ← Ω]) ≡g C[GC(M[ℜ(M) ← Ω])] ≡g C[ω(M)]. Pictorially we have:

C[M] {↗ → \atop M} N
∨
C[GC(M[ℜ(M) ← Ω])] > GC(N[ℜ(M) ← Ω])
ω  ∨ω
C[ω(M)]  > ω(N)

□

Lemma 5.35. Given a GRSNI term M and context C[□], C[M] ⊑g ⨆{C[P] | P ∈ W^{∗}(M)}. Proof. Since

C[M] ≡g ⨆{Q | Q ∈ W^{∗}(C[M])}

we want to show that:

⨆{Q | Q ∈ W^{∗}(C[M])} ⊑g ⨆{C[P] | P ∈ W^{∗}(M)}

that is, ∀Q ∈ W^{∗}(C[M]), ∃P ∈ W^{∗}(M) such that Q ⊑g C[P]. If Q ∈ W^{∗}(C[M]) it means that C[M] − ; → ; → N and Q ≤_{ω} ω(N), and, therefore, by monotonicity of ⊑g with respect to ≤_{ω} (Theorem 5.28), we have Q ⊑g ω(N). By Proposition 5.31, given the reduction C[M] − ; → ; → N, ∃M′, M − ; → ; → M′ and C[M′] ^{{↗ → \atop M′}} N. Therefore, by Lemma 5.34 we have:

ω(N) ⊑g C[ω(M′)]

Since ω(M′) ∈ W^{∗}(M), by letting P ≡ ω(M′) we have that Q ⊑g C[P]. □ Theorem 5.36. Given a GRSNI term M and context C[□], C[M] ≡g ⨆{C[P] | P ∈ W^{∗}(M)}. Proof. Follows from Lemma 5.30 and Lemma 5.35. □ Theorem 5.37. (Congruence of ≡g with respect to the context operation) Given GRSNI terms M and N, and context C[□], if M ≡g N then C[M] ≡g C[N]. Proof.

C[M] ≡g ⨆{C[P] | P ∈ W^{∗}(M)} by Theorem 5.36
≡g ⨆{C[Q] | Q ∈ W^{∗}(N)} by the hypothesis
≡g C[N]  by Theorem 5.36

□

Properties of a First-order Functional Language with Sharing 34

We stressed again that in the presence of interfering rules, ≡g is not guaranteed to be a congruence. Consider the rules:

τ_{1} : x = A(y) − ; − ; → x = A(y)
τ_{2} : x = B(y) − ; − ; → x = B(y)
τ_{3} : \frac{x_{1} = A(y)}{x = F(x_{1}) − ; − ; → x = 2}
τ_{4} : \frac{x_{1} = B(y)}{x = F(x_{1}) − ; − ; → x = 3}

and the following two terms:

M ≡ \{ \begin{matrix}t = A(x); \\ In t\} \end{matrix}  N ≡ \{ \begin{matrix}t = B(x); \\ In t\} \end{matrix}

Notice that M ≡g N, but the context {t_{1} = F(t_{2}); t_{2} = □; In t_{1}} can distinguish between M and N.

6. Correctness of Optimizations If we let (A(F), R_{opt}) be a GRS, where A(F) represents the set of terms over signature F, and R_{opt} a set

of optimization rules, then correctness can be formulated as follows: Definition 6.1. (Total correctness) An optimizer (A(F), R_{opt}) is totally correct with respect to a GRSNI (A(F), R) iff ∀ M ∈ A(F), if M − ; → ; → N using rules in R_{opt} then M ≡g N. In many situations it is acceptable if optimizations produce a more defined program. Definition 6.2. (Partial correctness) An optimizer (A(F), R_{opt}) is partially correct with respect to a GRSNI (A(F), R) iff ∀ M ∈ A(F), if M − ; → ; → N using rules in R_{opt} then M ⊑g N. Fact 6.3. If M − ; − ; → M_{1} by applying the common subexpression elimination rule then M ≤_{ω} M_{1}. Proposition 6.4. The common subexpression elimination is partially correct with respect to a GRSNI. Proof. Directly from the above fact and Corollary 5.29. □

Let GRSY be a non-interfering GRS containing the following Y-rule:

Y-rule : x = Ap(Y, f) − ; − ; → x = \{ \begin{matrix}t = Ap(f, t_{1}); \\ t_{1} = Ap(Y, f); \\ In t\} \end{matrix}

We can avoid the redex rooted at t_{1} on the right hand side of the above rule by using the following cyclic Y-rule:

Yc-rule : x = Ap(Y, f) − ; − ; → x = Ap(f, x)

Proposition 6.5. The cyclic Y-rule is partially correct with respect to a GRSY.

Proof. Suppose M − ; − ; → M_{1} using the Y-rule and M − ; − ; → M_{2} using the Yc-rule. Then M_{1} ⊑g M_{2} and the result follows from Theorem 5.37. □

However, if want to prove the total correctness of the cyclic implementation of the Y rule or the common subexpression elimination rule, then we need to impose further restrictions on the GRS rules. In particular, non left-linear rules (which include left-cyclic rules) will have to be disallowed. Furthermore, sharing will have to be ignored from the observations as well. The reader may refer to [1], where such a term model based on Böhm trees is presented.

Surprisingly, the following algebraic rules:

\begin{matrix}∗(x, 0) − ; − ; → 0 \\ ∗(x, 1) − ; − ; → x \end{matrix}

are not partially correct according to our model. Consider the following reduction:

M_{1} ≡ {x = G(7); y = ∗(x, 1); In y} − ; − ; → M′_{1} ≡ {x = G(7); In x}.

As long as G(7) is a redex, ω(M_{1}) ≤_{ω} ω(M′_{1}). However, if G(7) is not a redex, then there is no relationship between ω(M_{1}) and ω(M′_{1}). Such situations can arise either because of type errors or deadlocks. We illustrate the deadlock situation by the following example:

M_{2} ≡ {x = ∗(y, 5); y = ∗(x, 1); In x} − ; − ; → M′_{2} ≡ {x = ∗(x, 5); In x}.

Notice M_{2} is type correct but it cannot produce an integer as an answer. However, in our term model, without the optimization M_{2} will produce itself as an answer, and with the optimization it will produce M′_{2}, which is not related to M_{2}. We believe that cycles involving “strict operators” should not be observable, that is, the observations of both M_{2} and M′_{2} should be Ω.

7. Future directions

We have defined a class of GRSs which can express sharing of terms, including cyclic terms. Our GRS admits both non left-linear and left-cyclic rules. We prove the confluence of GRSNI, that is, a GRS with non interfering rules, and develop a term model a la Lévy for these GRS. Furthermore, we apply the semantic relation to show the partial correctness of important optimizations such as the common subexpression elimination and the cyclic implementation of the Y-rule. The main advantage of our approach is its simplicity because it avoids infinitary terms and associated transfinite reduction.

The motivation for this work came from a desire to formalize the compilation process of Id, an implicitly parallel language [19]. Id has a purely functional, higher-order, non-strict core. In addition Id also contains logical variables in the form of I-structures and mutable variables in the form of M-structures. The compiler of Id is expressed as a series of translations into simpler and simpler languages. In our prior work we have introduced the Kid (Kernel id) language [3] and the P-TAC (Parallel Three Address Code) language [2], and provided the translation of Id into Kid and of Kid into P-TAC [4]. We have tried to formalize many optimizations in the Id compiler in terms of source-to-source transformations on these intermediate languages.

Functional subset of P-TAC can be seen as an example of the GRS presented in this paper. Functional Kid, however, is more general due to the presence of λ-abstraction. A model for a GRS with λ-abstraction will provide a sound mathematical basis for the functional subset of the Id language. However, even proving confluence for the λ-calculus with sharing is a difficult problem.

Another direction of work would be to incorporate a notion of types, and the distinction between strict and non-strict operators in our GRS framework. This will allow one to prove the correctness of compiler optimizations, such as the algebraic rules.

Yet another direction would be incorporate I-structures and M-structures in our GRS. Elsewhere, we have shown the confluence of a GRS with I-structures [2]. I-structures operations can be expressed using “multirooted rules”. However, a term model for a GRS with I-structures would require a very different treatment of unconnected subterms and garbage collection.

Acknowledgements

This work was done at the Laboratory for Computer Science at MIT, and at the University of Oregon. Funding for this work has been provided in part by the Advanced Research Projects Agency of the U.S. Department of Defense under the Office of Naval Research contracts N00014-92-J-1310 (MIT)

We would like to express immense gratitude to Jean-Jacques Lévy, and Jan Willem Klop for insightful discussions.

References

1. Z. Ariola. Relating Graph and Term Rewriting via Böhm Models. In Proc. RTA ’93, Montreal, Canada, June, 1993.

2. Z. Ariola and Arvind. P-TAC: A Parallel Intermediate Language. In Proc. ACM Conference on Functional Programming Languages and Computer Architecture, London, UK, September 1989.

3. Z. Ariola and Arvind. A Syntactic Approach to Program Transformations. In Proc. ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, New Haven, CT, June 1991.

4. Z. Ariola and Arvind. Compilation of Id. In Proc. of the Fourth Workshop on Languages and Compilers for Parallel Computing, Santa Clara, CA, Springer-Verlag LNCS 589, August 1991.

5. Z. M. Ariola and J. W. Klop. Equational Term Graph Rewriting. Technical Report Draft, 1993.

6. H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.

7. H. Barendregt, T. Brus, M. van Eekelen, J. Glauert, J. Kennaway, M. van Leer, M. Plasmeijer, and M. R. Sleep. Towards an Intermediate Language based on Graph Rewriting. In Proceedings of the PARLE Conference, Eindhoven, The Netherlands, Springer-Verlag LNCS 259, June 1987.

8. H. Barendregt, M. van Eekelen, J. Glauert, J. Kennaway, M. Plasmeijer, and M. Sleep. Term Graph Rewriting. In Proceedings of the PARLE Conference, Eindhoven, The Netherlands, Springer-Verlag LNCS 259, June 1987.

9. T. Brus, M. van Eekelen, M. vam Leer, and M. Plasmeijer. Clean - A language for Functional Graph Rewriting. In Proc. ACM Conference on Functional Programming Languages and Computer Architecture, Portland, OR, Springer-Verlag LNCS 274, 1987.

10. M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

11. G. Huet and J.-J. Lévy. Computations in Orthogonal Rewriting Systems II. Technical report, INRIA, Rocquencourt, France, 1990.

12. R. J. M. Hughes. Super-combinators. In Proceedings of Lisp and Functional Programming, Pittsburg, PA, 1982.

13. T. Johnsson. Lambda Lifting: Transforming Programs to Recursive Equations. In Proceedings of Functional Programming Languages and Computer Architecture, Nancy, France, Springer-Verlag LNCS 201, September 1985.

14. V. Kathail. Optimal Interpreters for Lambda-calculus Based Funtional Languages. PhD thesis, Dept. of Electrical Engineering and Computer Science, MIT, Cambridge, MA, May 1990.

15. J. Kennaway, J. Klop, M. Sleep, and F. de Vries. Transfinite Reductions in Orthogonal Term Rewriting Systems. In Proc. RTA ’91, Springer-Verlag LNCS, 1991.

16. R. Kennaway. Implementing Term Rewrite Languages in Dactl. Theoretical Computer Science, Vol. 1, 1990.

17. J. Lamping. An algorithm for optimal lambda calculus reduction. In Proc. ACM Conference on Principles of Programming Languages, San Francisco, CA, January 1990.

18. J.-J. Lévy. Réductions Correctes et Optimales dans le Lambda-Calcul. PhD thesis, Universite Paris VII, Paris, France, October 1978.

19. R. S. Nikhil. Id (Version 90.0) Reference Manual. Technical Report CSG Memo 284-a, Laboratory for Computer Science, MIT, Cambridge, MA, USA, July 1990.

20. C. Wadsworth. Semantics And Pragmatics Of The Lambda-Calculus. PhD thesis, University of Oxford, Oxford, UK, September 1971.

21. P. Welch. Continuous Semantics and Inside-out Reductions. In λ-Calculus and Computer Science Theory, Italy, Springer-Verlag LNCS 37, March 1975.

Table of Contents

1 Introduction 2 An Example: A Graph Rewriting System for Combinatory Logic 3 GRS: Terms, Rules and Reduction

3.1 GRS terms 3.2 Canonical forms of terms 3.3 GRS rules 3.4 Identifying redexes and ω-ordering 3.5 Reduction 3.6 Descendant of a redex

4 Confluence of a GRS without interfering rules 5 A Graph Model for GRS

5.1 Instant semantics 5.1.1 Stable information in RPS and TRS 5.1.2 ω-redex

5.2 ω-reductions and its properties 5.3 Meaning of a GRS term 5.4 Impact of sharing on program behavior 5.5 Congruence

6 Correctness of Optimizations 7 Future directions