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.

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” [?]. The program that results after lambda-lifting is in a “supercombinatory” form, and is treated as a first-order program [?].

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 [?]. 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 [?, ?]. This latter technique leads to provably optimal interpreters for the λ-calculus [?]. 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 [?] or Term Rewriting Systems [?, ?, ?, ?]. 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 [?] or [?] where only acyclic graphs are considered. Without cyclic graphs some important implementation ideas are ruled out. More recently, Klop et al. [?] 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 [?]. We think that our approach also leads to a simpler proof of confluence than in [?].

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 [?]. We formally describe GRSs, in Section ??. We introduce an ordering on terms based on sharing of subterms, and formulate the notion of a redex using this ordering. In Section ??, we introduce GRSs without interfering rules and prove their confluence. Section ?? gives a term model for non-interfering GRSs. In Section ??, we apply the results of Section ?? to prove the correctness of some compiler optimizations, while in Section ?? 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.,

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

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