Homework due Wednesday 15 September 13.15

The numbers refer to the numbering of exercises in Pierce's book: We suggest that you use Haskell or your own favourite functional programming language for the implementation exercises.

Structural induction

1. THEOREM 3.3.4 is about the principle of structural induction on arithmetic expressions. On p 31 there is the general principle and on p 32 the three first cases are written out. Write out the remaining cases!

2. Spell out the principle of structural induction on untyped lambda terms! 

3. THEOREM 3.5.4 is proved by induction on a derivation of t --> t'. What this means is that there is one case for each of the three evaluation rules for Booleans (see Figure 3-1 on p 34). Spell out this induction principle in a similar style as in 1 and 2 above! This style of induction is sometimes called "rule induction". (This is a difficult but important exercise which is useful for understanding how Agda works.)

Arithmetic expressions

4. Exercise 3.5.18. Suppose we want to change the evaluation strategy of our language so that the then and the else branches of an if expression are evaluated (in that order) before the guard is evaluated. Show how the evaluation rules need to change to achieve this effect.

Lambda expressions

5. Give an example of a term which has both a free and a bound occurence of the same variable!

6.  Implement the type of lambda terms and write a function occursFree :: Var -> Term -> Bool
which checks whether a variable occurs free in a term or not! 

7. Adapt the evaluation rules for the lambda calculus in Figure 5.3 to describe (i) full beta-reduction and (ii) normal order evaluation.

8. Translate some terms into their nameless versions: 

\t.\f.t,
\s.\z.s (s (s z)),
\f,(\x.f (\y. (x x) y)) (\x. f (\y. (x x) y)),
(\x. (\x. x)) (\x. x).

Backslash is used for the lambda-sign.