Homework # 3
due September 27

Reading

Please read Chapters 6 and 7 in your textbook. It's not necessary to understand everything here. We won't dwell on the ``nameless representation'' of terms. But you need to know it exists so you can modify evaluation code in this and later homeworks.

Problems

Please do the following problems from the book:

6.1.1 (p76), 6.2.2 (p79), 6.2.3 (p79--full proof), 6.3.1 (p81).

Only turn in your answer to 6.2.3; the others have answers in the back of the book--use the solutions to check your answers. They will not be graded.

Discussion

The rule [E-APPABS] on page 81 is written

$$(\lambda.t_{1\,2}) v_2 \:\longrightarrow\: {\uparrow}^{-1}([0\mapsto{\uparrow}^1(v_2)]t_{1\,2})$$

This requires two shifting operations. Consider the following suggested definition of the rule:

$$(\lambda.t_{1\,2}) v_2 \:\longrightarrow\: [-1\mapsto v_2]{\uparrow}^{-1}(t_{1\,2})$$

If this rule works, explain why you think it isn't used in the book. If it doesn't work, give an example where it gives a different result than the definition in the book.

Programming

Change the implementation in fulluntyped to do call-by-name evaluation. Turn in a printout of the modified eval1 function. You should not need to do anything fancy.

About this document