CS 319 - The Lambda Calculus
Assignment 3, Winter 2000
Due Monday, 7 February

1. Demonstrate an interesting encoding of integers in the lambda calculus that is not suitable for computation.
2. Using weak bracket-abstraction, show that the $\overline{\eta}$ rule below does not imply extensionality.

   $$([x].\alpha x)=_{\overline{\eta}}\alpha x \alpha \overline{\eta}$$

   
   

3. Using weak bracket-abstraction, bound the length of $[x].\alpha$ and of $\overline{\alpha}$ in terms of the length of $\alpha$. Give examples showing that your bounds are tight. What difference does strong bracket-abstraction make?
4. Find out what happens to $\overline{\alpha}$ under weak reduction when $\alpha$ produces nested residuals under beta reduction.
5. Continue to work on general classes of solvable equations. You may do this as a joint project, and hand in a single joint presentation, if you like.