NB We write State p-> State for the set of partial functions from State to State. 1. Do exercise 1.2.1. of Winskel at the end of Chapter 1. 2. Define the semantics for "repeat P until b" as a fixed point of a function g : (State p-> State) -> (State p-> State) (NB this program executes statement P and then checks the boolean b; if b holds, execution stops, if b doesn't hold, it iterates.) If you think "repeat" is easy, define a semantics for "for x = a to b do P" First try with a, b numbers, then think about the general situation, where a and b are arbitrary expressions. 3. 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. b. Prove f(w_infty) = w_infty for w_infty : State p-> State as defined a la Winskel's notes. (First redefine w_infty for our notion of State.) c. Prove that for all s in State, exists n [f^n(bot)(s) = f^{n+1}(bot)(s)]