Semantics of Programming Languages Comprehensive January 7, 1998

Instructions. Do all questions. You have 4 hours.

Question 1: All of the variables in the following command are integer variables. Give a formal proof (or natural deduction style proof-tree) that the following specification is partially correct:

{N ≥ 0 and N is even} X := N; Y := N; while Y > 0 do (X := X - 1; Y := Y - 2) {X = N div 2}

Question 2: There are many parts to this question. Read all of the parts before you try to start answering. In most cases the questions have concise answers that can quickly be written down. (Part(i) is the exception; that may be a little longer.) When you are asked to give an example, be concise.

Definition: A domain is an ω-complete partial order. (If you have forgotten the definition of an ω-complete partial order, you can infer it from part(a).)

Part a: Give an example of a partially ordered set in which every subset has an upper bound, but for which there is at least one chain which does not have a least upper bound. (Hence, your example would be an example of a partially ordered set in which every subset has an upper bound, but which is not a domain because it is not ω-complete.)

Part b: Consider the simple imperative language, as in Tennent. What is a state?

Part c: Given a nonempty set S, we may consider the discrete partially ordered set S̈ = (S, ⊑) whose partial order is defined by

s_{1} ⊑ s_{2} iff s_{1} = s_{2} .

Show that S̈ is a domain.

Part d: Show that if D is a domain, then so is the raised set D_{⊥}.

Part e: Let D be the discrete domain on three elements a, b, and c. Describe the ordering on D_{⊥}. (Just draw a diagram.)

Part f: Let D be a domain and S just an ordinary nonempty set. Show that the set S ⟶ D, ordered by

f ⊑ g iff for all s ∈ S : f(s) ⊑_{D} g(s)

is a domain.

Definition: Let D_{1} and D_{2} be domains with partial orders ⊑_{1} and ⊑_{2}, respectively. Let f : D_{1} ⟶ D_{2}. f is monotone iff x ⊑_{1} y implies f(x) ⊑_{2} f(y) for all x, y in D_{1}. Also, f is

ω-compact iff for every chain {x_{i} | i ∈ N} in D_{1}, the least upper bound, ⨆_{i=0}^{∞} f(x_{i}) is defined

in D_{2} and f( ⨆_{i=0}^{∞}x_{i}) ⊑_{2} ⨆_{i=0}^{∞} f(x_{i}). f is ω-continuous iff f is monotone and ω-compact. (This

definition agrees with Tennent’s definition of continuity on ω-complete partial orders.

Part g: Give an example of an ω-compact function f : D ⟶ D, where D is a domain, which is not monotone.

Part h: Let D be a domain with a bottom element ⊥ and let f : D ⟶ D be ω-continuous.

Show that ⨆_{i=0}^{∞} f^{i}(⊥) is the least fixed point of f. i.e. if a = ⨆_{i=0}^{∞} f^{i}(⊥) then f(a) = a and for

all d such that f(d) = d, a ⊑ d.

Part i: Let S be the set of states of the simple imperative language. The set of all partial functions from S to S, denoted by S ⇀ S, is identifiable with the set of functions

S ⟶ S̈_{⊥}

Let β be a function from S to {true, false}. Let κ be a function in S̈_{⊥} ⟶ S̈_{⊥} Now, define

Γ_{β,κ} : (S ⟶ S̈_{⊥}) ⟶ (S ⟶ S̈_{⊥})

by

Γ_{β,κ}(c) = λs. \{ \begin{matrix}c(κ(s)) & if β(s) = true \\ s & if β(s) = false \end{matrix}

Show that Γ_{β,κ} is ω-continuous.

Part j: The preceding development applies elementary techniques about domains to obtain the semantics of the while-command. Explain how. (Note that by part(h), Γ_{β,κ} has a least fixed point. Let β be the meaning of a Boolean expression B, and let κ be the meaning of a command C. Explain how Γ_{β,κ} is related to the semantics of while B do C.)

Question 3: Compare and contrast states vs. environments. (Think of states with regard to the semantics of the simple imperative language and think of environments with regard to the semantics of the simple recursive applicative language.)