Homework # 3
due September 23

Reading

Please read Chapter 5 in your textbook.

Church Numerals

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.

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

You may use $\omega$ defined below. Explain on paper.

Proofs

Prove the following theorems in SASyLF:

1. Prove that multi-step full beta-reduction of $\omega$ where
   
   $$\omega = (\lambda x \cdot x x)(\lambda x \cdot x x)$$
   
   
   never reaches a ``value,'' (a lambda abstraction). To do this, you need to specify multi-step full beta-reduction. If you use the same technique (binary recursive) for multi-step evaluation as in Homework #2, you will require another lemma. It is easier if you define multi-step evaluation to be right recursive.

2. Prove that call-by-value evaluation is deterministic.

About this document