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. 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 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 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 ??. Next we informally present the GRS for combinatory logic, and relate our GRS notation to Barendregt’s [?].

Consider the S rule:

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

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 ≡

Figure 2. Graph rule for the S combinator

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

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

\{ \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 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 ??.