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 Kiama^{2}. 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 turingcomplete, 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 TuringComplete). 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 abstractionapplication 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 termrewriting 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 builtinto 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 termrewriting 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 termrewriting 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 interpreter^{3}. 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:
PALC, the pure attribute grammer lambda calclus interpreter, will decorate a tree such as this with three different attributes at each subexpression (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.
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 rewriting 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
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 lefthand side (the righthand 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.
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.
This time the value of the newly attached tree is immediate and the value then propogates up the tree to the root
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 normalorder 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 strictorder evaluation. We still need to ask for the value
of an expression when we pull it from the environment since the value
calculation at stackinsertion 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 stackframes 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 termrewriting 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 turingcompleteness. This is becuase the system I describe here is a demonstration^{4} that attribute grammars are turingcomplete, by way of an embedding of the lambda calculus. However, the attribute grammar presented here is a higher order attribute grammar^{5} 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 turingcompleteness can be shown for other (simpler) classes of attribute grammars.
Footnotes

Dolstra, E., Visser, E.: Building interpreters with rewriting strategies. In: Proceedings of the 2nd Workshop on Language Descriptions, Tools and Applications. Electronic Notes in Theoretical Computer Science, vol. 65, pp. 57–76 (2002)↩

Anthony M. Sloane, Lennart C. L. Kats, and Eelco Visser. 2010. A Pure ObjectOriented Embedding of Attribute Grammars. Electron. Notes Theor. Comput. Sci. 253, 7 (September 2010), 205219.↩

Kaima REPL for Dolstra and Visser Interpreter extended with name analysis and type checking↩

Not strictly a proof, but it can clearly become one↩

H. H. Vogt, S. D. Swierstra, and M. F. Kuiper. 1989. Higher order attribute grammars. In Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation (PLDI ‘89), R. L. Wexelblat (Ed.). ACM, New York, NY, USA, 131145.↩