Homework # 2
due September 16

Reading

Please read Chapter 3 in your textbook.

Problems

Please do problem 3.5.13 (Funny rules). Explain your answers, but no proof (natural language or SASyLF) is required.

Also answer the following question:

Which of the theorems 3.5.4, 3.5.7, 3.5.8, 3.5.11, 3.5.12 remain true after adding the rules for arithmetic expressions (Figure 3-2)?

Explain your answers; no proofs needed. (Ex. 3.5.14 and its solution should help, as should definition 3.5.15.)

Proofs

Do problem 3.5.17 and write the proof in SASyLF (only for the ``if'' sublanguage!). More precisely, prove that if $t \stackrel{*}{\rightarrow} t'$ and $t'$ is a value then $t \Downarrow t'$, and conversely if $t \Downarrow t'$, then $t \stackrel{*}{\rightarrow} t'$. (I am not requiring you to prove that $t'$ is a value.) You may use the solution in the back of the book (p. 498 in my edition) to help you write the proof.

When I solved this problem, I noticed I needed the following lemmas:

1. If $t \rightarrow t'$ and $t' \Downarrow v$, then $t \Downarrow v$.
2. If $t \stackrel{*}{\rightarrow} t'$ and $t' \Downarrow v$, then $t \Downarrow v$.
3. If $t_1 \stackrel{*}{\rightarrow} t_1'$ then $\texttt{if $t_1$\ then $t_2$\ else $t_3$} \stackrel{*}{\rightarrow} \texttt{if $t'_1$\ then $t_2$\ else $t_3$}$.

Adding succ, pred, iszero doubles the size of the proof--be thankful you don't need to handle them!

The file $CLASSHOME/src/homework2/homework2.slf.SKEL starts the work for you.

Submission

As with all homeworks, please turn in your homework problems on paper at the beginning of lecture. Please put the SASyLF proof in the appropriate homework directory in your AFS volume.

About this document