CMSC 221/321
Homework set 1
Due: Thursday, Oct 7, 2010

Homework 1.1  Reading recommendations
-------------------------------------
1. Read up through Chapter 7 of the Harper notes, but don't get too worried
about the technicalities of Chapter 1 or abstract binding trees in
Chapter 5 (particularly section 5.4). We will be discussing variables
and variable bindings at length soon.  We also won't be concerning
ourselves with the technicalities of parsing. If you are interested,
study the parsing code in the calc.tgz code example.

2. Read Chapters 1 and 2 in Huttel, Transitions and Trees.


Homework 1.2
------------
Prove that small-step (transition) evaluation for SAE always
terminates.
(Hint: Think about the size of expressions.)


Homework 1.3
------------
Prove that the transistion relation is deterministic: for any 
e ∈ expr, there exists at most one e' such that e ↦ e'.
(Hint: Do induction on the derivation of the transition e ↦ e',
with case analysis on the last rule used in the derivation.  See
Harper's discussion of rule induction.)


Homework 1.4
------------
Prove Theorem 1.2 from Lecture 2 (equivalence of big-step and
small-step dynamic semantics).

You can find some hints in Harper, Chapter 7, for a slightly more
complicated version of the language with let-bindings of variables.
(Hint: There will be two different inductive proofs for the two
directions of implication (left to right and right to left).)

Homework 1.5
------------
Write an SML program implementing SAE evaluation based on the
small-step semantics (i.e. the function defined by ->!). Be sure
to test it on several representative expressions.  (Hint: the
code example arith-SOS.sml does this for a slightly more complicated
version of the language with let-expressions.)