CPSC 521: Foundations of Functional Programming
Author: Robin Cockett
Date: November 2011
Due: Friday, 18th 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, a leftmost outermost (by-name) reduction, and a head
reduction.
Notes on reduction order:
Here are brief descriptions of by-value reduction, by-name reduction
(or leftmost outermost reduction), and hed 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 (this defect is corrected by lazy
reduction). A head reduction is a reduction which always reduces
the head redex (if there is one) and reduces the term to head normal
form (if there is one).
A leftmost outermost reduction finds its next
redex as follows:
- if the term is (\x.N) M then this is the next redex
- if the term is MN
where
M is not an
abstraction then try to find the next redex in M (leftmost
redex), only if this fails, that is M
is in normal form, try to find a redex in N.
- if the term is \x.N then find the next redex in N.
There is a variant of this called a head reduction
which only partly reduces the term to 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 M N where M is not an
abstraction then try to find the next redex in M, if this fails
then simply fail to find a redex.
- if the term is \x.N then find a redex in N.
Recall that a term is in head normal form if and only if it is of the
form \x_1...x_n.y N_1 ... N_m .
A by-value reduction (rightmost innermost reduction) finds
its next redex as follows:
- the term is (\x.M) N then search N for a
redex (the rightmost redex).
If there is no redex in N,
that
is N is in normal form,
then search M for the next redex (the innermost redex). If M is
in normal form as well then this top-level reduction gives the next
reduction.
- the term is M N where M is not an
abstraction then find the next redex in N: if N is in normal form find the next
redex in M (the rightmost
redex).
- the term is \x.N then find the next redex 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 actually critical: the innermost reduction is
crucial ...
A further variant, which also is a by-value strategy is a rightmost reduction:
- the term is (\x.M) N then search N for a
redex. If this fails then this top-level reduction gives the next
reduction.
- the term is M N where M is not an
abstraction then find the next redex in N.
If
this fails find the next redex in M.
- the term is \x.M then find the next redex in M.
This strategy always tries to evaluate the argument of a function
before it applies the function.
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?