PLDA Homework 2: Lambda calculus evaluator

Implement a normal order evaluator for pure untyped lambda calculus.
A parser is not required, processing the internal representation of a lambda-expression suffices.

Discussion You will need to find the leftmost outermost redex, i.e. a term of the form (lambda x. e1) e2 .

One option is to code this in two steps: first, check whether a (sub)expression has a redex; if so, then reduce it. Do not forget the case where in e1 e2, evaluating e1 reduces it to a lambda abstraction; then, its application to e2 can be reduced as well.

A better option is to implement checking and reducing at the same time.
One variant is to use an exception with an argument, say   exception Change of expr   where expr is your type for lambda expressions. If evaluation finds a redex, it throws the exception Change with the result of the substitution as argument; if nothing can be reduced, it simply returns the same expression.
In the general case of function application, try to evaluate first the function and then the argument, catching (separately) any exceptions; if an exception is caught, it means that a reduction step has occurred, and you can re-evaluate the now-reduced application.

A second, simpler variant (which also avoids any unnecessary re-evaluation attempt) is to just simulate finding the leftmost outermost redex. For this, unfold function applications, if the function itself is an application, keeping a list of arguments, i.e. App(App(e0, e1), e2) becomes e0 applied to [e1;e2], etc. Thus, most work will be done by a helper function that takes a function and a list of arguments, and either unfolds or evaluates. Unfolding stops if the function is a variable (in which case the arguments must be evaluated in turn), or a lambda-abstraction, in which case we have found a redex, reduce it, and then continue unfolding/evaluating.

Both variants give you the opportunity to print each reduction step, so you can trace your interpreter. You could use the following function for printing:

let rec printlam e =
  let rec printpar inner = function
    | V v -> print_string v
    | L (x, e) -> if inner then print_char '(';
      print_string ("L " ^ x ^ "."); printlam e;
      if inner then print_char ')';
    | App (e1, e2) -> printpar true e1; print_char ' '; printpar true e2
  in printpar false e