COMP 511.  HWK #2 Due at start of next class.  Late homeworks will not be accepted.

1) Consider the big-step semantics defined on page 75.  

1.a) Write the full derivation of the evaluation of the term

     e == ((\lambda f .\lambda x. f x ((\lambda z. f x z) x))
           (\lambda a. \lambda b. a))
          (\lambda r. r)

That is, find some e' and build the full derivation

	e \hookrightarrow e'

It's best to do write this by hand.  Don't waste time typesetting any of
this assignment.

1.b) We can define the set of values as follows:

	v \in V ::= i | \lambda x.e

Prove that if e \hookrightarrow e' then e' \in V.  Give full details
of each step in your proof.

2) Consider the type system in Figure 5.2 on page 80.

2.a) For the term "e" you evaluated above, find a typing assignment.  That is,
find one (specific) \Gamma and one (specific) type t such that

	\Gamma |- e : t

2.b) Consider only the subset without <>, ~, and run.  (Note that this 
means you can ignore levels -- they are always zero when there are no 
multi-stage constructs).  Prove the following substitution lemma:

	- if   \Gamma       |- e_1          : t_1

          and  \Gamma x:t_1 |- e_2          : t_2

          then \Gamma       |- e_2 [x:=e_1] : t_2

Note that this proof only involves the type system.
Again, give full details in your proof.

3) Discuss the type systems for MetaML presented in chapter 4 and 5.
For each type system, give two new examples term (that is, not discussed in
the class or the chapter).  One term should be typeable, and the other
not typable.  Explain why such a term would be useful, and explain why it
is either typable or untyable (that is, give typing derivations, or show
that no such typing derivations can exist).

4) (Optional)  You may revise your review for Chapter 5 and submit it with
this homework.