Homework # 2
due September 20

Reading

Please read Chapter 5 in your ``textbook.''

Church Numerals

1. Do problem 5.2.4 from the book and then try it out using the fulluntyped implementation. What do you get for powr three two ? Explain.
2. scc scc two is six. Is this an instance of a general rule? Explain!

Evaluation

For each of the following situations, give a pure lambda-calculus term that has the given properties:

1. diverges under normal evaluation and under call-by-value evaluation, but not under call-by-name
2. diverges under normal evaluation but not under call-by-value
3. diverges under call-by-value but not under normal evaluation

Finally (for this part), give an informal proof that any term that terminates under normal evaluation or call-by-value evaluation must necessarily terminate under call-by-name evaluation.

Substitution

The book (5.3.5, p. 71) gives a definition of substitution that works up to alpha-conversion. Give a complete definition that does not rely on implicit alpha-conversion and yet is correct. It must not change the free variables of a term. You may assume that $\cal V$ is infinite.

About this document