Notation: I use
*  =>_tau to denote PCF evaluation.
*  <==> to denote "if and only if"
*  =_ctx to denote contextual equality
*  <=_ctx to denote contextual preorder
*  <_tau to denote the approximation relation (slide 39)


(1) Show that, if d <_nat M, e<_nat N and b<_bool P, then
    if(b,d,e)   <_nat   if P then M else N
(This is the "if" inductive case in the proof of the Fundamental
Property, Slide 40)

(2) Prove the following properties (by induction on tau)
(a) if d2 <= d1 and d1 <_tau M1, then d2 <_tau M1
(b) if d1 <_tau M1 and forall V(M1 =>_tau V implies M2 =>_tau V), then
    d1 <_tau M2
These properties constitute Lemma 7.2.1(iii)

(3) (Exercise 7.4.1.) For any PCF type tau and any closed terms M1 , M2
of type tau, show that
[23] forall V : tau, (M1 =>_tau V  <==>  M2 =>_tau V ) 
     implies M1 =_ctx M2 : tau.
[Hint: combine the Proposition on Slide 43 with Lemma 7.2.1(iii).]

(4) (Exercise 7.4.2.) Use [23] to show that beta-conversion is valid
up to contextual equivalence in PCF, in the sense that for all 
fn x : tau . M1 : tau -> tau'  and  M2 : tau,

    (fn x : τ . M1 ) M2 =_ctx  M1[M2/x] : tau .

(5) (Exercise 7.4.3.) Is the converse of [23] valid at all types?
[Hint: recall the extensionality property of <=_ctx at function types
(Slide 44) and consider the terms 
       fix(fn f : (nat->nat) . f ) 
and 
    fn x : nat . fix(fn x : nat . x ) 
of type nat -> nat.]