At the lecture, we gave a denotational semantics for the language L given by the grammar b:bit ::= "0" | "1" n:bin ::= b | n b The semantics is given by the model N, the natural numbers, and the interpretation [[ "0" ]] := 0 [[ "1" ]] := 1 [[ n b ]] := 2 * [[n]] + [[b]] In the lecture, we have recursively defined the operation 0(n), which prefixes a binary numeral n with a leading "0" as follows. O("0") := "0" "0" O("1") := "0" "1" O(n b) := O(n) b We have given an operational semantics => via the rules "0" => "0" "0" "1" => "0" "1" n => m ------------ n b => m b Exercises: ========= 1. Define the operation S(n), which computes the binary numeral which is the successor of n. 2.a Give an operational semantics for S(n), in the form of a relation n => m such that S(n) = m iff n => m b. Prove that S(n) = m iff n => m 3. Prove [[S(n)]] = [[n]] + 1 for all n. 4. a. Compute the denotational semantics of S1 := x := x+1; y:= x + x b. Compute the denotational semantics of S2 := if x>0 then x:= 1 else x:= -1 NB Your answer should be a "state transformer", i.e. an element of State p-> State, the set of partial functions from State to State. For us a State is a function r : Var -> Z (the integers)