CMSC 221/321
Homework set 2
Due: Tuesday, Oct 19, 2010

Homework 2.0: Reading
1. Harper, Chapters 9 & 11 (ignoring the static semantics parts of 9,
which we will get to later).
2. There are a couple very important early papers by Peter Landin
linked to on the class home page: "The mechanical evaluation of
expressions", and "The next 700 programming langauges". These are
well-worth taking a look at. "The mechanical evaluation..." introduced
the first abstract machine for defining the evaluation of a language,
namely the SECD. You can try to relate the SECD machine to Harper,
Chapter 11.


Homework 2.1: Formally state and then prove the equivalence of
SAE[CR] and SAE[CK].


Homework 2.2 : For SAEL[CRv], Prove that for any (nonvalue) expression
e ∈ SAEL, there is a unique context C such that e = C[r], where r is a
redex expression.


Homework 2.3 : Use both SAEL[CRv] and SAEL[CRn] to compute the value
of the following expression:

    let x = 4 in let y = 2 + 3 in x * (let z = 2 + x in z * z)


Homework 2.4: Write an SML program that implements SAEL[BSn] (that is,
a big-step evaluator for SAEL with subst-by-name semantics).


Homework 2.5: [This is a long-term project, due in about 4 weeks.]
Try to prove that SAEL with subst-by-name semantics is terminating
(the evaluation of every expression terminates).  You can start out
by trying to develop an intuition by working out a number of examples,
or by trying to construct a counter-example, an expression that does
not terminate.