CMSC 221/321
Homework set 1
Due: Thursday, Oct 6, 2011

Reading: Lectures 1, 2, and Induction Tutorial.


Homework 1.0 [15]
-------------
Do Exercises 1 and 2 in the Induction Tutorial.


Homework 1.1 [45]
------------
Prove that small-step (transition) evaluation for SAE always
terminates.

Hint: Think about the size of expressions. Each step of reduction
strictly decreases the size of the expression, given the right
definition of size.  So define a size function

   size: expr → Nat

and let's assume that size(Num(n)) = 0 (constants are assigned size 0
rather than 1), and correspondingly compound expressions should have
size > 0. You need to prove the following lemmas:

Lemma 1: For any transition e ↦ e', size(e) > size(e').
Lemma 2: ∀e. size(e) > 0 ⇒ ∃ e'. e ↦ e'. 
Lemma 3: ∀ n. P(n), where
  P(n) == ∀ e. size(e) = n => ∃ m. e ↦* Num(m)

The first lemma can be proved by induction on the derivation of
e ↦ e', the second by induction on the structure of e, and the third
by course-of-values induction on n.


Homework 1.2 [30]
------------
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
the discussion of rule induction in the Induction Tutorial.)


Homework 1.3 [10]
------------
Write an SML program implementing the size function on SAE exprs that
you defined for Homework 1.1.  Test it on a small but representative
sample of expressions.


Total: 100 points