Computer Science Department
Programming Methods Laboratory

Foundations of Programming
Ecole Polytechnique Federale de Lausanne
Exercises 4

Implement an interpreter for the lambda calculus in Funnel. An interpreter for a language is a function that, when applied to a term, performs the actions required to evaluate the expression:

    interpreter: Term -> Value

For the lambda calculus, an interpreter is described by the beta-reduction rule and an evaluation strategy (call-by-name, call-by-value, call-by-need). We start with implementing a call-by-name interpreter. Terms should be implemented using the Visitor design pattern, names are simply strings. Here is a framework for the definition of Terms:

val Term = {
  def Name(s) = { ... }
  def Lambda(x, t) = { ... }
  def Apply(t, u) = { ... }
Write a function toString that transforms a term into readable form:
def toString(t) = t.match {
Now implement a visitor for doing substitutions on lambda terms. For simplicity you can assume that lambda-abstractions have unique argument names.
def subst(s, y, t) = s.match {
Finally, you are able to implement beta-reduction with a call-by-name evaluation strategy. The following function eval is supposed to reduce a term as much as possible:
def eval(t) = t.match {
How do you have to modify eval so that a call-by-value evaluation strategy is used? Implement a call-by-value interpreter:
def eval_cbv(t) = t.match {
Initially we restricted ourselves only to lambda terms where every lambda-abstraction used an unique argument name. What do you have to change if we remove this restriction? For implementing alpha-conversion you can use the following function that creates unique names:
var nameCounter := 0
def newName = {
  nameCounter := nameCounter + 1
  "A" + nameCounter