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

(1) (Exercise 8.4.1) Suppose that a monotonic function 
p : (B_bot x B_bot) -> B_bot satisfies
  * p(true,bot) = true,
  * p(bot,true) = true,
  * p(false,false) = false.
Show that p coincides with the parallel-or function on Slide 45 in the
sense that p(d1,d2) = por(d1)(d2), for all d1, d2 in B_bot.

(2) (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).]

(3) (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 : tau . M1 ) M2 =_ctx  M1[M2/x] : tau .

(4) (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.]