A pure attribute-grammar interpreter for the lambda calculus

Interpreters for the lambda calculus can be written in many sensible ways. One which particularly appeals to me is the term rewriting approach given by Dolstra and Visser 1. That version captures very nicely the reduction rules which are usually given in lambda calculus definitions and different rewriting strategies correspond to different evaluation orders. Anthony Sloane has implemented this approach to lambda calculus interpretation in Kiama2. Kiama is a language processing library for Scala which supports both term rewriting and attribute grammars and part of the kiama project is to explore the common ground between these two computational style. Thus, I present here an attribute grammar encoding of a lambda calculus interpreter in Kiama, primarily for comparison with the term rewriting version, but also because it is an interesting algorithm in its own right.

The code described in this article is available publically.

I have a request for you, dear reader. If you know of any previous work describing lambda calculus interpreters with attribute grammars, or showing that attribute grammars are turing-complete, please let me know. I don’t have a long history with attribute grammars and my search has turned up nothing.

Lambda Calculus

The lambda calculus is a language for computation which is exceedingly simple but still capable of computing anything which can be computed (i.e. is Turing-Complete). The calculus is usually described as follows, however I have elided some complicating details.

The possible expressions () of the language are:

An expression is either a variable, an abstraction over a variable where the value of the abstracted variable () will later be substituted in the body of the abstraction (), or an application which supplies values to abstractions for substituion.

The evaluation (reduction) rules, where represents one step of evaluating an expression, are:

-reduction tells us how to reduce an abstraction-application pair, and is the equivalent of function application. -reduction allows pointless abstractions (i.e ones that abstract over variables they they never mention) to be removed.

The two complicting details are

  • How is replaced with in the -reduction rule?
  • What is a free variable?

To keep this article short, I will not go into these issues and simply say that:

  • replacement (normally called substitution) must treat lambdas like you would any variable declaration in a lexically scoped programming language, new instances hide existing ones, and that
  • a free variable is a variable present in an expression for which we can’t find an enclosing abstraction (for example in ).

Interpreters for the Lambda Calculus

There are many (subtely) different ways to execute the two reduction rules of the lambda calculus, any correct one is called a lambda calculus interpreter. One of my faviourite is the term-rewriting example from Dolstra and Visser mentioned earlier. The reason I like this one is that is a very direct encoding of the reduction rules.

There are two separate problems when writing a lambda calculus interpreter:

  • How do I write the reduction rules?
  • In what order to I apply the reduction rules?

The first problem is obvious, we must translate the reduction rule into computer code. The second problem occurs because there are multiple correct ways to order the application of the reduction rules. This agnosticism to evaluation order is one of the important characteristics of the lambda calculus, but any interpreter must implement a particular reduction order to evaluate a term. Sometimes the order is built-into the reduction rules, by carefully putting recursive calls in the right place. However particularly nice lambda calculus interpreters break them apart, allowing you to change one without affecting the other. The term-rewriting version does exactly this. The reduction rules are encoded in one place and one can then define multiple traversal strategies, which all use the same reduction rules, to actually perform the evaluation.

Why an attribute grammar lambda calculus interpreter?

With this background, one might be tempted to ask, why build another interpreter? Firstly, I am interested in comparing term-rewriting and attribute grammars, and there is no better way to compare two computational styles than to compare their implementations of the computational style (the lambda calculus). Furthermore, attribute grammars decorate trees, while typical lambda calculus interpreters build or transform trees, describing the later with the former is an interesting and enlightening task. Also, the result I have come up with is interesting because we can see various features of computation revealed in it, such as stack frames and variable shadowing. Finally, it is possible to encode (at least) two different reduction orders in this attribute grammar solution and the difference between the two again highlights features of computation.

This pure attribute grammer intepreter for the lambda calculus, which I will call “PALC”, is written in Kiama/Scala. I have chosen this system because it is an excellent attribute grammar implementation, it supports both attribute grammars and term rewriting, and it has an existing implementation of the Dolstra and Visser interpreter3. Indeed, we have used the Kiama implementation of the Dolstra and Visser approach as our starting point, so the comparison with term rewriting is immediate.

PALC

A lambda calculus expression can be seen as a tree in a very natural way, it is this tree which we decorate with attributes in PALC. For example, if we use to indicate applications, we can generate a tree for the following lambda calculus term:

simple example

PALC, the pure attribute grammer lambda calclus interpreter, will decorate a tree such as this with three different attributes at each sub-expression (node) of the tree:

  • value: which is the computed value of the node rooted at this part of the tree.
  • app_stack: which is the stack of applications which have occurred higher in the tree.
  • env: which is an environment mapping variables to the nodes they have been bound to by an abstraction.

value is the only attribute we ultimately care about, but value relies on the other two attributes. We will describe the attributes in dependency order, which puts app_stack first since it does not depend on either of the other two.

app_stack

The app_stack attribute holds a stack of expressions which were encountered on the right hand side of an application expression above this expression. For example, the following tree has been decorated with its app_stack attributes. Notice that the stack holds references to the expressions in question, not copies of them. This is not strictly necessary, one could store a copy, but holding references makes the different evaluation orders easier to define.

decorated with app_stack

The app_stack for any particular expression depends on the parent of that expression. If there is no parent (i.e. this expression is the root of the tree) then there can’t have been any prior application expressions and the stack is empty. If the parent of this expression is an application expression then we know of one application that needs to be on the stack. The stack holds the actual parameter (the right hand side) of the application, so we add that to the stack. If the parent of this expression is a lambda expression, then one of the applications must have (just) been dispatched by that lambda, so we pop the top off the stack. For all other parent expression types, the stack is passed on unchanged.

We achieve this attribute decoration with the following Kiama attribute grammar specification

  val app_stack: Exp => AppStack =
    attr {
      case e => {
        (e.parent) match {
           case p@null                    => new AppStack()
           case p@App(e1,e2) if e2 ne e   => (p->app_stack).push(e2)
           case p@Lam(v,t,body)           => (p->app_stack).pop
           case p:Exp                     => p->app_stack
        }
      }
    }

The side condition of the App case ensures that the stack is only added to for the left hand side of the application node, since the right hand side does not contain the abstraction which will dispatch that application.

env

The env for any particular node depends on the parent of that node, and the app_stack at that node. The env attribute holds the environment, a map of variables to expressions, for this node and all its children. The environment is filled when an abstraction (which abstracts a variable) meets an application (which provides an expression to map that variable to). When using re-writing interpreters, we can look for an application/abstraction pair. However, an attribute grammer interpreter needs to give a value at every node. This is why we used the stack - it “holds” the application for us until we reach an abstraction which will give a variable to that parameter (the right hand side of that application). When we meet an abstraction we want to map the variable it abstracts to whatever is on the top of the stack - and we want to pop the stack. This is why you see the Lam rule for app_stack popping the stack. Again, the environment maps a variable to a reference to an expression. The example expression with the environment( [ ] ) filled in is

decorated with app_stack

Notice that there are two nodes where the environment is marked as ?(unknown). This has occured because the stack at this point is empty, but the lambda indicates we need to pop the stack to put something in the environment. This has happened because this abstraction has a different static location to its dynamic location. This abstraction is a formal parameter for the first abstraction, and will eventually be used within the body of another abstraction. At this point there will be something in the stack. We don’t actually need to do anything special to deal with this case because the attribute grammar won’t ever ask for the environment of that node in that position, so it never tries to calculate it.

We achieve the env attribute decoration with the following definition

  val env: Exp => Env =
    attr {
      case e => {
        (e.parent) match {
          case p@null          => new Env()
          case p@Lam(v,t,body) => (p->env) + (v -> (p->app_stack).top)
          case p:Exp           => p->env
        }
      }
    }

If the current node is the root, set up an empty environment; if the parent node is an abstraction, fill the environment with a map from the abstracted variable to whatever is on top of the stack; otherwise, use exactly the parent’s environment.

value

Once we have app_stack and env attributes, we can calculate the value for any node. In most cases, the value of a node is the value of one of its children. For abstractions, it is the value of the body, for applications it is the value of the left-hand side (the right-hand side is added to the stack). The only interesting case is the value of a variable. This depends on the environment. In simple cases, we just pull the variable from the environment and use whatever it is mapped to as the value. However, this “whatever it is mapped to” may be a partially evaluated expression (like the in our example). Thus what we actually need to do for variables is to find out what it is mapped to, clone that and make it a child of this variable. With this done, the value of this child supplies the value of the variable. If the thing we pulled from the environment was already evaluated fully, the value is immediate. If it is only partially evaluated, the evaluation continues in the context this variable sits in. This is how we eventually fill in the ? in the environment of our example, this node is never asked for its environment until it has been placed below the which maps to it. From here there is a value in the stack which can be used to populate the environment.

This cloning and attaching results in the following tree at the point the attribute value is being calculated for the lowest node in the tree.

first_expansion

However, the value of this depends on some values lower in this new tree, including the new lowest , which now maps to the number 5 in the new tree. Another cloning and attachment occurs giving the following tree.

second_expansion

This time the value of the newly attached tree is immediate and the value then propogates up the tree to the root

with values propogating up the tree

Although it seems like there is a lot going on here, the code to achieve this attribution is very simple

  val value : Exp => Exp = 
    attr {
      case e@Num(i)            => Num(i)
      case e@Var(idn)          => { (e->env).get(idn) match {
                                      case Some(resolves_to) => {
                                        val new_tree:Exp = Attributable.deepclone(resolves_to)
                                        initTree(new_tree)
                                        new_tree.parent = e
                                        new_tree->value
                                      }
                                      case None => e
                                    }
                                  }
      case e@Lam(v, t, body) if ((e->app_stack).isEmpty) 
                               => e // allows lambdas to evaluate to themselves when not in an evaluation context
      case e@Lam(v, t, body)   => body->value
      case e@App(e1, e2)       => e1->value
      case e@Opn(l, o, r)      => Num(o.eval(deNum(l->value), deNum(r->value)))
    }

This code includes an ability which is not striclty necessary based on what we have seen so far. The None case of the match on Var and the true branch on Lam allows nodes which are not in a valid evaluation context (for example a lambda not applied to anything) to be given a value representating a partially (or un-) evaluated expression. The attribute grammer won’t actually ever need these branches in terms with no unnapplied lambdas and no free variables. Instead, this allows the REPL in the example to report some answer for the value of an expression like \x.x. However, it does also allow us to experiment with evaluation order, which we discuss in the next section.

Evaluation Order

The attribute grammar above performs normal-order evaluation. When formal paramters are seen on the right and side of an application, they are put in the stack unevaluated. It is not until the value of the variable they are bound to is asked for that the value of that expression is also asked for.

However, we have complete control over when a formal parameter is evaluated, particularly since the value attribute is capable of doing partial evaluation. If we were to put the value of an expression into the stack, modifying app_stack to

  val app_stack: Exp => Stack[Exp] =
    attr {
    ...
           case p@App(e1,e2) if e2 ne e   => (p->app_stack).push(e2.value)
    ...
      }
    }

we would get strict-order evaluation. We still need to ask for the value of an expression when we pull it from the environment since the value calculation at stack-insertion time might only be able to partially evaluate the term.

Conclusion

I have shown that the untyped lambda calculus can be evaluated with a pure attribute grammer. The grammar uses no rewriting, no sneaky computation at nodes, no parameters passed to attributes, just an attribute grammar traversing a tree in dependency order. The resulting attribute grammar has a stack which corresponds to stack-frames and an environment corresponding to the dynamic execution environment. The attribute grammar is short, simple and can be extended very simply to support multiple evaluation strategies. Since this attribute grammar is written in Kiama/Scala, a direct comparison to term-rewriting interpreters is now possible.

I mentioned at the start of this article that I am interested in finding other attribute grammar lambda calculus interpreters or proofs of turing-completeness. This is becuase the system I describe here is a demonstration4 that attribute grammars are turing-complete, by way of an embedding of the lambda calculus. However, the attribute grammar presented here is a higher order attribute grammar5 because a tree is stored (by reference) in an attribute and the tree can be expanded as a result of attribute computation. I am interested to know if turing-completeness can be shown for other (simpler) classes of attribute grammars.

Footnotes