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.
- 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.
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:
- 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.
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:
- 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 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 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.
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:
- 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.
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:
- (\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?