NB a. We write State p-> State for the set of partial functions from State to State.
   b. We write c= to denote an arbitrary partial order. (Nice asci art ...)

1. Consider the function f : (State p-> State) -> (State p-> State) as
   defined by Winskel on slide 6, but now with State = Var -> Z:

   f(w)(s) := s                                  if s(x) <= 0
   f(w)(s) := w(s[x|->s(x)-1, y|->s(x)*s(y)])    if s(x) > 0

   a. Do exercise 1.2.2. of Winskel at the end of Chapter 1, that is prove that
      	 w = f(w) ==> w_infty c= w
      for w_infty : State p-> State as defined a la Winskel's
      notes. (First redefine w_infty for our notion of State. I did it
      during the lecture.)

   b. Prove f(w_infty) = w_infty 

   c. Prove that for all s in State, exists n [f^n(bot)(s) = f^{n+1}(bot)(s)]
    
2. Do exercise 2.3.1 of Winskel at the end of Chapter 2, that is prove
   that the set of partial functions from X to Y forms a domain, with
   the definitions of ordering and lub given on slide 10.

3. Prove that the "vertical numbers" as defined by Winskel in Fig 1 on page 13, form a domain.

4. Which of the following is a domain? (In each case, you may choose a
   proper definition of "lub"; prove your answer.)

   a. (P(X), \subseteq), where P(X) is the powerset of X, \subseteq is
      the usual subset ordering.

   b. ([0,1], <=), where <= is the usual ordering on the real numbers

   c. ([0,1]\cap Q, <=), \cap is the intersection and Q is the
      rational numbers

   d. (Sigma^*, c=), where Sigma^* is the set of words over the
      alphabet Sigma := {a,b} and c= is the prefix ordering