CPSC 417: Foundations of Functional Programming

Author: Robin Cockett
Date: 30th Oct 2006

Due:  Tuesday, 3rd Nov.

Assignment #3:  A lambda calculus reducer in Haskell.

This assignment requires you to develop a number of pieces of code which will culminate in a suite of programs for handing lambda calculus terms.   You should develop these programs as I develop the theory in class.

  1.  Create a datatype for lambda calculus terms.
  2. Write a pretty printer for the lambda calculus terms.
  3.  Develop a program to determine the free variables of a lambda calculus term.
  4.  Write a program to determine the alpha-equivalence of two lambda calculus terms.
  5.  Write a program to do a substitution of one lambda calculus term for another (avoiding variable capture).
  6.  Write a program to do a one step beta-reduction.  This involves searching for a redex and reducing it - and reducing no other redexes!  If the lambda term is in normal form you should report this.  (Note: the way one searches for a redex determines the sort of reduction you do in the next question!)
  7.  Write a program to display the steps of a by-value reduction and a leftmost outermost (by-name) reduction.

Notes on  reduction order:

Here are brief descriptions of by-value reduction and by-name reduction (or leftmost outermost reduction).   Recall that by-name reduction will find the normal form if there is a normal form. By-value reduction, although it may fail to normalize is often the more efficient of the two.

A leftmost outermost (or by-name) reduction finds its next redex as follows:
There is a variant of this which I will call a head reduction which only partly reduces the term to what is called a head normal form.  A head reduction finds its next redex as follows:
A term is in head normal form, therefore, if and only if it is of the form \x_1...x_n.y N_1 ... N_m .

A by-value reduction finds its next redex as follows:
The important aspect of a by-value reduction is that whenever a reduction is applied all its subterms must be in normal form (i.e. cannot themselves be reduced).  Whether this is done by searching leftmost/rightmost is not critical ...

A further variant which you might like to play with is a rightmost reduction it can be defined as follows:
This strategy always tries to evaluate the argument of a function before it applies the function.

Can you invent your own reduction strategy???

Here are some (sources of) examples of lambda terms on which you may like to try out your reducer:
  1. (\x.xx)(\x.xx),  this is the term \omega.  Note reduction does not terminate under any strategy -- even a head reduction.
  2. (\xy.y) ((\x.xx)(\x.xx)) (\x.xx), this term has a normal form which is found by a head reduction and a leftmost outermost reduction but not by a by-value reduction.
  3. test whether addition defined by add n m = n succ m is correct!
  4. Evaluate snd (x,y) using the pair representation.
  5. Can you wite a multiply function for the Church numerals? (Look it up!)  Test it on some numerals.
  6. Can you write an append function for lists?
  7. What about a reverse function for lists?