**Author:** Robin Cockett

**Date: **30th Oct 2006

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.

- Create a datatype for lambda calculus terms.
- Write a pretty printer for the lambda calculus terms.
- Develop a program to determine the free variables of a lambda calculus term.
- Write a program to determine the alpha-equivalence of two lambda calculus terms.
- Write a program to do a substitution of one lambda calculus term for another (avoiding variable capture).
- 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!)
- Write a program to display the steps of a by-value reduction and a leftmost outermost (by-name) reduction.

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

- if the term is
*(\x.N) M*then this is the next redex - if the term is
*N M*where*N*is not an abstraction then try to find the next redex in*N*(**leftmost**redex), only if this fails try to find a redex in*M*. - if the term is
*\x.N*then find a redex in*N*.

- if the term is
*(\x.N) M*then this is the next redex - if the term is
*N M*where*N*is not an abstraction then try to find the next redex in*N*, if this fails then simply fail to find a redex. - if the term is
*\x.N*then find a redex in*N*.

A

- the term is
*(\x.N) M*then search*M*for a redex (**rightmost**redex). If there is no redex in*M*, search*N*for a redex (i.e. ensure N is a value). If neither*M*nor*N*has a redex then this is the reduction. - the term is
*N M*where*N*is not an abstraction then try to find a reduction in*M*, only when this fails try to find a reduction in*N*(**rightmost**redex) - the term is
*\x.N*then find a reduction in*N*.

A further variant which you might like to play with is a

- the term is
*N M*then try to find a reduction in*M*, if this fails and*N*is an abstraction then this is the reduction, otherwise, and only then try to find a reduction in*N*(**rightmost**redex). - the term is
*\x.N*then find a reduction in*N*.

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:

*(\x.xx)(\x.xx)*, this is the term \omega. Note reduction does not terminate under any strategy -- even a head reduction.*(\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.- test whether addition defined by
*add n m = n succ m*is correct! - Evaluate
*snd (x,y)*using the pair representation. - Can you wite a multiply function for the Church numerals? (Look it up!) Test it on some numerals.
- Can you write an
*append*function for lists? - What about a
*reverse*function for lists?