Homework # 3
due September 26

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!

(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/homework3/homework3.slf.SKEL starts the work for you.

Graduate Students

Find three papers from journals or academic conferences in programming languages (TOPLAS, POPL, OOPSLA, ECOOP) from the last 5 years which define an operational semantics (evaluation) for a programming language. For each one, determine whether the evaluation relation is

small-step

as with the book (with errors getting the program ``stuck'');

small-step with errors

as in Exercise 3.5.16

big-step

as in Exercise 3.5.17

Cite each paper and explain your categorization.

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