Homework # 4
due September 30

Reading

Please read Chapter 6 in your textbook. It's not necessary to understand everything here. We won't dwell on the ``nameless representation'' of terms in later weeks.

Problems

Please do the following problems from the book:

6.1.1 (p76), 6.2.2 (p79) 6.3.1 (p81).

There is no need to turn the answers in, as the answers are in the back of the book. These are all easy exercises. Do them!

SASyLF Proofs

Prove that our definition of substitution is ``total,'' that is, that substitution is always defined if the arguments are valid. Also prove Exercise 6.2.6 when $s$ is a 0-term, and $t$ is a $j+1$-term.

Use the skeleton file to start both proofs. The skeleton file is very long because it includes a lot of helpful lemmas. Make sure you understand the lemmas, especially the ones that the skeleton file warns that you will need.

Discussion

1. 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 re-definition of the rule that does only one shift:
   
   $$(\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.

2. In our formulation of substitution and evaluation of nameless terms, we use the following version of the rule with no shifts:
   
   $$(\lambda.t_{1\,2}) v_2 \:\longrightarrow\: [0\mapsto v_2](t_{1\,2})$$
   
   
   When does this rule work? When does it not work? Explain!

About this document