CMSC 221/321
Homework set 4
Due: 5pm, Friday, Oct 28, 2011

Reading: Lecture 6.

4.1. [20] In Homework 3.1 you were asked to show that all evaluations
of closed expressions in SAEL[SSv] terminate.  The same idea used for
SEA[SS] worked: the size (appropriately defined) of expressions were
reduced by any transition.  What about SEAL[SSn] (bind-by-name let)?

  (a) Show that the straightforward generalization of the size idea
      fails for SEAL[SSn] by giving an example where a transition
      yields a larger expression.

  (b) Try to define some more subtle measure of size of expression that
      might work as a basis for showing termination. [Hint: think
      about numbers and relative positions of Let nodes in the
      abstract syntax tree. This is rather difficult.]


4.2. [10] Verify that fact = Yv Fact defines the factorial in CBV
semantics by hand calculating (fact 2) using the Fun[SSv] rules. Follow
the example of the calculation of (fact 2) using the CBN Y combinator
in Lecture 6.


4.3. [25] Define a CR reduction system for CBV Fun (Call-By-Value). Use
this CR system to evaluate:

   App(Fun(x,Bapp(Plus(Num 2, Var x))), Num 3)


4.4. [25] Define a CEK abstract machine for CBV Fun.


4.5. [20] Write an SML program implementing the CEK machine from
problem 4.4. Test Fun programs to evaluate will be provided later.